Port LowParse combinators to Pulse

Makefile

@@ -105,19 +105,29 @@ lowparse-bitfields-test: lowparse
 	+$(MAKE) -C tests/bitfields
 
 ifeq (,$(NO_PULSE))
-lowparse-pulse-test:
-else
 lowparse-pulse-test: lowparse
-	+$(MAKE) -C tests/pulse
+	+$(MAKE) -C share/everparse/tests/lowparse
+#	+$(MAKE) -C tests/pulse # TODO: move it into `share/everparse/tests/lowparse` and re-enable it
+else
+lowparse-pulse-test:
 endif
 
 .PHONY: lowparse-pulse-test
 
 lowparse-test: lowparse-unit-test lowparse-bitfields-test lowparse-pulse-test
 
-quackyducky-test: quackyducky
+quackyducky-lowstar-test: quackyducky
 	+$(MAKE) -C tests
 
+.PHONY: quackyducky-lowstar-test
+
+quackyducky-pulse-test: quackyducky
+	+$(MAKE) -C share/everparse/tests/qd
+
+.PHONY: quackyducky-pulse-test
+
+quackyducky-test: quackyducky-lowstar-test quackyducky-pulse-test
+
 test: all lowparse-test quackyducky-test asn1-test cbor-test cddl-test
 
 # Disable 3d-unit-test on MacOS because there is a loop in Makefiles

share/everparse/tests/lowparse/.gitignore

@@ -0,0 +1,14 @@
+Example3/
+ExampleConstInt32le/
+Example2/
+Example5/
+ExampleEnum/
+Example7/
+Example8/
+Example9/
+Example10/
+Example11/
+Example12/
+ExampleDepLen/
+_output/
+*.checked

share/everparse/tests/lowparse/LowParseExample10.Aux.fst

@@ -0,0 +1,73 @@
+module LowParseExample10.Aux
+
+include LowParse.Spec.Combinators
+include LowParse.Spec.Int
+include LowParse.Spec.IfThenElse
+
+module U8 = FStar.UInt8
+module U16 = FStar.UInt16
+module U32 = FStar.UInt32
+
+(* Use ((U8.t & U8.t) & U8.t) instead of flbytes 3 *)
+
+inline_for_extraction
+let msg_type = (U8.t & U8.t) & U8.t
+
+inline_for_extraction
+let msg_type_HelloRetryRequest : msg_type = ((0xABuy, 0xCDuy), 0xEFuy)
+
+inline_for_extraction
+let msg_type_eq (x y: msg_type) : Tot bool =
+  let ((a1, b1), c1) = x in
+  let ((a2, b2), c2) = y in
+  a1 = a2 && b1 = b2 && c1 = c2
+
+type msg_type_other = (m: msg_type { msg_type_eq m msg_type_HelloRetryRequest == false })
+
+noeq
+type t_other = {
+  msg_type: msg_type_other;
+  contents: U16.t;
+}
+
+noeq
+type t =
+  | HelloRetryRequest of U32.t
+  | Other of t_other
+
+inline_for_extraction
+let t_tag_cond (x: msg_type) : Tot bool =
+  msg_type_eq x msg_type_HelloRetryRequest
+
+inline_for_extraction
+let t_payload (b: bool) : Tot Type =
+  if b then U32.t else U16.t
+
+inline_for_extraction
+let parse_t_payload (b: bool) : Tot (k: parser_kind & parser k (t_payload b)) =
+  if b then (| _ , parse_u32 |) else (| _, parse_u16 |)
+
+inline_for_extraction
+let t_synth (x: msg_type) (y: t_payload (t_tag_cond x)) : Tot t =
+  if t_tag_cond x
+  then HelloRetryRequest y
+  else Other ({ msg_type = x; contents = y })
+
+let parse_msg_type : parser _ msg_type =
+  parse_u8 `nondep_then` parse_u8 `nondep_then` parse_u8
+
+inline_for_extraction
+noextract
+let parse_t_param : parse_ifthenelse_param = {
+  parse_ifthenelse_tag_kind = _;
+  parse_ifthenelse_tag_t = _;
+  parse_ifthenelse_tag_parser = parse_msg_type;
+  parse_ifthenelse_tag_cond = t_tag_cond;
+  parse_ifthenelse_payload_t = t_payload;
+  parse_ifthenelse_payload_parser = parse_t_payload;
+  parse_ifthenelse_t = _;
+  parse_ifthenelse_synth = t_synth;
+  parse_ifthenelse_synth_injective = (fun t1 x1 t2 x2 -> ());
+}
+
+let parse_t : parser _ t = parse_ifthenelse parse_t_param

share/everparse/tests/lowparse/LowParseExample10.fst

@@ -0,0 +1,231 @@
+module LowParseExample10
+#lang-pulse
+include LowParseExample10.Aux
+open FStar.Tactics.V2
+open Pulse.Lib.Pervasives
+open Pulse.Lib.Slice
+open LowParse.Spec.Base
+
+module SZ = FStar.SizeT
+module R = Pulse.Lib.Reference
+module S = Pulse.Lib.Slice
+module LPS = LowParse.Pulse.Base
+module LPI = LowParse.Pulse.Int
+module LPC = LowParse.Pulse.Combinators
+module PPB = LowParse.PulseParse.Base
+module PPC = LowParse.PulseParse.Combinators
+module PPITE = LowParse.PulseParse.IfThenElse
+module Trade = Pulse.Lib.Trade.Util
+module U8 = FStar.UInt8
+module U16 = FStar.UInt16
+module U32 = FStar.UInt32
+module I32 = FStar.Int32
+module Cast = FStar.Int.Cast
+module A = Pulse.Lib.Array
+
+(* leaf_reader for parse_u8 *)
+
+inline_for_extraction noextract
+let leaf_read_u8 : PPB.leaf_reader parse_u8 =
+  PPB.leaf_reader_of_serialized (LPI.read_u8' ())
+
+(* leaf_reader for msg_type = parse_u8 `nondep_then` parse_u8 `nondep_then` parse_u8
+   Read the three bytes sequentially using peek_trade_gen *)
+
+inline_for_extraction noextract
+let leaf_read_msg_type : PPB.leaf_reader parse_msg_type =
+  PPC.leaf_read_nondep_then
+    (PPC.leaf_read_nondep_then leaf_read_u8 LPI.jump_u8 leaf_read_u8 ())
+    (LPC.jump_nondep_then LPI.jump_u8 LPI.jump_u8)
+    leaf_read_u8
+    ()
+
+(* Pulse validator *)
+
+inline_for_extraction
+let validate_t : LPS.validator parse_t =
+  PPITE.validate_ifthenelse parse_t_param
+    (PPC.validate_nondep_then (PPC.validate_nondep_then LPI.validate_u8 LPI.validate_u8) LPI.validate_u8)
+    leaf_read_msg_type
+    (fun b -> if b then LPI.validate_u32 else LPI.validate_u16)
+    ()
+
+(* Pulse jumper *)
+
+inline_for_extraction
+let jump_msg_type : LPS.jumper parse_msg_type =
+  LPC.jump_nondep_then (LPC.jump_nondep_then LPI.jump_u8 LPI.jump_u8) LPI.jump_u8
+
+inline_for_extraction
+let jump_t : LPS.jumper parse_t =
+  PPITE.jump_ifthenelse parse_t_param
+    jump_msg_type
+    leaf_read_msg_type
+    (fun b -> if b then LPI.jump_u32 else LPI.jump_u16)
+    ()
+
+(* leaf_readers for payload types *)
+
+inline_for_extraction noextract
+let leaf_read_u16 : PPB.leaf_reader parse_u16 =
+  PPB.leaf_reader_of_serialized (LPI.read_u16' ())
+
+inline_for_extraction noextract
+let leaf_read_u32 : PPB.leaf_reader parse_u32 =
+  PPB.leaf_reader_of_serialized (LPI.read_u32' ())
+
+(* Accessor: read the tag and payload from a validated ifthenelse.
+   After validation, use peek_trade_gen to get a sub-slice, read
+   the tag to determine which branch, then jump + read payload. *)
+
+#push-options "--z3rlimit 32"
+
+fn access_payload
+  (input: S.slice byte)
+  (#pm: perm)
+  (#v: Ghost.erased bytes)
+  (offset: SZ.t)
+  (off: SZ.t)
+  (_: squash (LPS.validator_success parse_t offset v off))
+  requires pts_to input #pm v
+  returns res: t
+  ensures pts_to input #pm v
+{
+  let sinput = Ghost.hide (Seq.slice v (SZ.v offset) (Seq.length v));
+  parse_ifthenelse_eq parse_t_param sinput;
+  nondep_then_eq (nondep_then parse_u8 parse_u8) parse_u8 sinput;
+  nondep_then_eq parse_u8 parse_u8 sinput;
+  parser_kind_prop_equiv parse_u8_kind parse_u8;
+  let tag_off = SZ.add offset 3sz;
+  let tag_val = PPB.read_parsed_from_validator_success leaf_read_msg_type input offset tag_off;
+  let b = t_tag_cond tag_val;
+  Seq.lemma_eq_elim
+    (Seq.slice sinput 3 (Seq.length sinput))
+    (Seq.slice v (SZ.v tag_off) (Seq.length v));
+  if b {
+    let payload = PPB.read_parsed_from_validator_success leaf_read_u32 input tag_off off;
+    HelloRetryRequest payload
+  } else {
+    let payload = PPB.read_parsed_from_validator_success leaf_read_u16 input tag_off off;
+    Other ({ msg_type = tag_val; contents = payload })
+  }
+}
+
+#pop-options
+
+(* synth_recip for parse_t_param (no serializer needed) *)
+
+let synth_recip_t : PPITE.ifthenelse_synth_recip_t parse_t_param =
+  fun (x: t) ->
+    match x with
+    | HelloRetryRequest y -> (| msg_type_HelloRetryRequest, y |)
+    | Other m -> (| m.msg_type, m.contents |)
+
+let synth_inverse_t (x: t) : Lemma
+  (let (| tg, y |) = synth_recip_t x in t_synth tg y == x)
+= ()
+
+(* clens definitions for the accessor type *)
+
+include LowParse.CLens
+
+let clens_HelloRetryRequest : clens t U32.t = {
+  clens_cond = (fun x -> HelloRetryRequest? x);
+  clens_get = (fun (x: t) -> (match x with HelloRetryRequest y -> y) <: Ghost U32.t (requires (HelloRetryRequest? x)) (ensures (fun _ -> True)));
+}
+
+let clens_other : clens t U16.t = {
+  clens_cond = (fun x -> Other? x);
+  clens_get = (fun (x: t) -> (match x with Other m -> m.contents) <: Ghost U16.t (requires (Other? x)) (ensures (fun _ -> True)));
+}
+
+(* Accessors using accessor_ifthenelse_payload combinator + accessor_ext *)
+
+inline_for_extraction
+let access_HelloRetryRequest : PPB.accessor parse_t parse_u32 clens_HelloRetryRequest =
+  PPC.accessor_ext
+    (PPITE.accessor_ifthenelse_payload parse_t_param synth_recip_t synth_inverse_t jump_msg_type true ())
+    clens_HelloRetryRequest ()
+
+inline_for_extraction
+let access_other : PPB.accessor parse_t parse_u16 clens_other =
+  PPC.accessor_ext
+    (PPITE.accessor_ifthenelse_payload parse_t_param synth_recip_t synth_inverse_t jump_msg_type false ())
+    clens_other ()
+
+(* Test function: validate, determine branch, and use the appropriate accessor *)
+
+#push-options "--z3rlimit 64"
+
+fn dummy
+  (input: S.slice byte)
+  (which: U32.t)
+  (#pm: perm)
+  (#v: Ghost.erased bytes)
+  requires S.pts_to input #pm v
+  returns res: U32.t
+  ensures S.pts_to input #pm v
+{
+  let mut poffset = 0sz;
+  let is_valid = validate_t input poffset;
+  if is_valid {
+    let off = !poffset;
+    let sinput = Ghost.hide (Seq.slice v (SZ.v 0sz) (Seq.length v));
+    parse_ifthenelse_eq parse_t_param sinput;
+    nondep_then_eq (nondep_then parse_u8 parse_u8) parse_u8 sinput;
+    nondep_then_eq parse_u8 parse_u8 sinput;
+    parser_kind_prop_equiv parse_u8_kind parse_u8;
+    let tag_val = PPB.read_parsed_from_validator_success leaf_read_msg_type input 0sz 3sz;
+    let b = t_tag_cond tag_val;
+    let input' = PPB.peek_trade_gen parse_t input 0sz off;
+    with v1 . assert (PPB.pts_to_parsed parse_t input' #(pm /. 2.0R) v1);
+    if b {
+      let sub = access_HelloRetryRequest input';
+      with v2 pm2 . assert (PPB.pts_to_parsed parse_u32 sub #pm2 v2);
+      let x = leaf_read_u32 sub;
+      Trade.elim (PPB.pts_to_parsed parse_u32 sub #pm2 v2) (PPB.pts_to_parsed parse_t input' #(pm /. 2.0R) v1);
+      Trade.elim (PPB.pts_to_parsed parse_t input' #(pm /. 2.0R) v1) (S.pts_to input #pm v);
+      x
+    } else {
+      let sub = access_other input';
+      with v2 pm2 . assert (PPB.pts_to_parsed parse_u16 sub #pm2 v2);
+      let x = leaf_read_u16 sub;
+      Trade.elim (PPB.pts_to_parsed parse_u16 sub #pm2 v2) (PPB.pts_to_parsed parse_t input' #(pm /. 2.0R) v1);
+      Trade.elim (PPB.pts_to_parsed parse_t input' #(pm /. 2.0R) v1) (S.pts_to input #pm v);
+      Cast.uint16_to_uint32 x
+    }
+  } else {
+    0ul
+  }
+}
+
+#pop-options
+
+
+fn test ()
+  requires emp
+  ensures emp
+{
+  let mut arr = [| 0uy ; 8sz |];
+  let input = S.from_array arr 8sz;
+  input.(0sz) <- 0xABuy;
+  input.(1sz) <- 0xCDuy;
+  input.(2sz) <- 0xEFuy;
+  input.(3sz) <- 0x55uy;
+  input.(4sz) <- 0xAAuy;
+  input.(5sz) <- 0x34uy;
+  input.(6sz) <- 0x45uy;
+  input.(7sz) <- 0x00uy;
+  let res = dummy input 42ul;
+  S.to_array input;
+  ()
+}
+
+fn main ()
+  requires emp
+  returns r: I32.t
+  ensures emp
+{
+  test ();
+  0l
+}