Questions about monadic parser combinators

[yuyuankang]

Hi,

I am currently working with LowParse to interpret some basic data structures in F*. Here is the data structure:

type simple_struct= {
  num1:uint16;
  num2:uint32
}

Additionally, I have developed the following parsers:

let p = parse_u16
let p' (v1: uint16) = and_then parse_u32 (fun v2 -> parse_ret ({ num1 = v1; num2 = v2 }))

To merge the parsers p and p', such as in and_then p p', it requires me to formally demonstrate that p' is injective.

let proof_p'_injective ()
  : Lemma (ensures (forall x1 x2 b1 b2 . and_then_cases_injective_precond p' x1 x2 b1 b2 ==> x1 == x2))
  = 
  let proof_p'_injective_aux (x1 x2: uint16) (b1 b2: bytes)
    : Lemma (requires and_then_cases_injective_precond p' x1 x2 b1 b2) (ensures x1 == x2) 
       [SMTPat (parse (p' x1) b1); SMTPat (parse (p' x2) b2)]
    =
    and_then_eq parse_u32 (fun v2 -> parse_ret ({ num1 = x1; num2 = v2 })) b1;
    and_then_eq parse_u32 (fun v2 -> parse_ret ({ num1 = x2; num2 = v2 })) b2;
    let Some (v1, _) = parse (p' x1) b1 in
    let Some (v2, _) = parse (p' x2) b2 in
    assert (v1.num1 == x1);
    assert (v2.num1 == x2);
    ()
  in   
  ()

let parse_simple_struct =
  proof_p'_injective ();
  and_then p p' 

Could there be a more efficient method to construct a parser for simple_struct? Are there any examples I could reference for using monadic parser combinators?

Thank you!

[nikswamy]

@tahina-pro should comment.

But, using and_then directly is often inconvenient. parse_dtuple2 is often easier to use: https://github.com/project-everest/everparse/blob/master/src/lowparse/LowParse.Spec.Combinators.fsti#L1186

Also, if you really need to use and_then directly, then these lemmas (and others nearby in the same file) help with decomposing the injectivity proof: https://github.com/project-everest/everparse/blob/master/src/lowparse/LowParse.Spec.Combinators.fsti#L327

[yuyuankang]

I tried parse_dtuple2, it is indeed much easier to use. Thank you for the suggestions!