QUESTION: Does everparse produce actual parsers?

[samuelchassot]

Hi everyone, hi @tahina-pro,

I read the papers and am interested in the parser/serialiser pair generation of everparse. In the README.md it is also mentioned that this project is about producing verified parsers from 3d message format descriptions.
However, in the documentation, and in the code I managed to generate using the everparse.sh script, I can only find validation code.
Am I missing something?

Thanks a lot for your reply :)

[samuelchassot]

Okay I found that it is in fact quackyducky which does that (it is in the paper but almost absent from the documentation). I am however not able to produce C code with quackyducky yet.

[nikswamy]

The general philosophy of EverParse is to minimize the number of copies done by the parser.

So, usually, one runs a validator and then uses EverParse's accessors to read relevant parts of the input directly from the input buffer.

Additionally, in 3d you can augment the validation code with parsing actions that build some parsed representation of the input format. https://project-everest.github.io/everparse/3d-lang.html#actions

[samuelchassot]

Great! Thanks for the reply!

Okay, I see, it makes sense. And, if I understood correctly, the same apply to write data to a buffer: one has to use different functions to write different parts of the data, right?

I will check the actions of 3d, that seems interesting thanks!

Also, are you pushing 3d instead of quackyducky because one can do the same things (and more?) with 3d?

Thanks again :)

[nikswamy]

Not necessarily pushing 3d over qd. They have different roles. If you are trying to parse binary formatted data from an existing C application, then 3d is a good fit. If you're trying to use verified parsers within a larger F* project, then qd is likely a better fit.

[samuelchassot]

Thanks a lot for your reply :) That makes more sense now 👍

I am trying to write an example and I still have something I don't know: I made a toy an example with this spec:

struct {
    uint16 content<2..10>;
} content_one;

struct {
    uint16 content<12..15>;
} content_two;

enum {one(0), two(2), (255)} content_type;
struct {
    uint64 id;
    uint32 size;
    uint8 arr[size];
    content_type typ;
    select(typ) {
        case one: content_one;
        case two: content_two;
    } content;
    
} message;

I am now trying to write a simple program that serialises one of those and parses it back, just to demonstrate the capability of the tool :)

How should I write the uint64_t for example? Reading the paper, I have a sense of how to write list (with the finaliser) and the enum provides write/read functions. But what about the simple types? Should I write them in the buffer "by hand" but then how to make sure they are a valid representation of my value?

Thanks a lot for your help :)