enrich kinds for parse_nlist (work in progress)

project-everest · Oct 21, 2024 · 377333a · 377333a
1 parent f34c9a1
commit 377333a
Show file tree

Hide file tree

Showing 6 changed files with 101 additions and 55 deletions.
diff --git a/src/3d/prelude/EverParse3d.Actions.Base.fst b/src/3d/prelude/EverParse3d.Actions.Base.fst
@@ -1244,29 +1244,31 @@ noextract
 inline_for_extraction
 let validate_nlist
   (n:U32.t)
+  (n_is_const:option nat { memoizes_n_as_const n_is_const n})
   #wk
   (#k:parser_kind true wk)
   #t
   (#p:parser k t)
   #inv #disj #l #ha #ar
   (v: validate_with_action_t p inv disj l ha ar)
-: Tot (validate_with_action_t (parse_nlist n p) inv disj l ha false)
+: Tot (validate_with_action_t (parse_nlist n n_is_const p) inv disj l ha false)
 = validate_weaken
     #false #WeakKindStrongPrefix #(LowParse.Spec.FLData.parse_fldata_kind (U32.v n) LowParse.Spec.List.parse_list_kind) #(list t)
     (validate_fldata_consumes_all n (validate_list v))
-    kind_nlist
+    (kind_nlist k n_is_const)
 
 inline_for_extraction noextract
 let validate_nlist_total_constant_size_mod_ok
       (n:U32.t)
+      (n_is_const:option nat { memoizes_n_as_const n_is_const n})
       #wk 
       (#k:parser_kind true wk)
       (#t: Type)
       (p:parser k t)
       inv
       disj
       l
-  : Pure (validate_with_action_t (parse_nlist n p) inv disj l false true)
+  : Pure (validate_with_action_t (parse_nlist n n_is_const p) inv disj l false true)
   (requires (
     let open LP in
     k.parser_kind_subkind == Some ParserStrong /\
@@ -1278,22 +1280,23 @@ let validate_nlist_total_constant_size_mod_ok
   (ensures (fun _ -> True))
 = [@inline_let]
   let _ =
-    parse_nlist_total_fixed_size_kind_correct n p
+    parse_nlist_total_fixed_size_kind_correct n n_is_const p
   in
   validate_total_constant_size_no_read'
-    (LP.strengthen (LP.total_constant_size_parser_kind (U32.v n)) (parse_nlist n p))
+    (LP.strengthen (LP.total_constant_size_parser_kind (U32.v n)) (parse_nlist n n_is_const p))
     (Cast.uint32_to_uint64 n)
     () inv disj l
 
 inline_for_extraction noextract
 let validate_nlist_constant_size_mod_ko
       (n:U32.t)
+      (n_is_const:option nat{ memoizes_n_as_const n_is_const n})
       (#wk: _)
       (#k:parser_kind true wk)
       #t
       (p:parser k t)
       inv disj l
-  : Pure (validate_with_action_t (parse_nlist n p) inv disj l false true)
+  : Pure (validate_with_action_t (parse_nlist n n_is_const p) inv disj l false true)
   (requires (
     let open LP in
     k.parser_kind_subkind == Some ParserStrong /\
@@ -1307,12 +1310,12 @@ let validate_nlist_constant_size_mod_ko
      let h = FStar.HyperStack.ST.get () in
      [@inline_let]
      let f () : Lemma
-       (requires (Some? (LP.parse (parse_nlist n p) (I.get_remaining input h))))
+       (requires (Some? (LP.parse (parse_nlist n n_is_const p) (I.get_remaining input h))))
        (ensures False)
      = let sq = I.get_remaining input h in
        let sq' = Seq.slice sq 0 (U32.v n) in
        LowParse.Spec.List.list_length_constant_size_parser_correct p sq' ;
-       let Some (l, _) = LP.parse (parse_nlist n p) sq in
+       let Some (l, _) = LP.parse (parse_nlist n n_is_const p) sq in
        assert (U32.v n == FStar.List.Tot.length l `Prims.op_Multiply` k.LP.parser_kind_low) ;
        FStar.Math.Lemmas.cancel_mul_mod (FStar.List.Tot.length l) k.LP.parser_kind_low ;
        assert (U32.v n % k.LP.parser_kind_low == 0)
@@ -1325,12 +1328,13 @@ let validate_nlist_constant_size_mod_ko
 inline_for_extraction noextract
 let validate_nlist_total_constant_size'
       (n:U32.t)
+      (n_is_const:option nat { memoizes_n_as_const n_is_const n })
       #wk
       (#k:parser_kind true wk)
       #t
       (p:parser k t)
       inv disj l
-  : Pure (validate_with_action_t (parse_nlist n p) inv disj l false true)
+  : Pure (validate_with_action_t (parse_nlist n n_is_const p) inv disj l false true)
   (requires (
     let open LP in
     k.parser_kind_subkind == Some ParserStrong /\
@@ -1341,19 +1345,19 @@ let validate_nlist_total_constant_size'
   (ensures (fun _ -> True))
 = fun ctxt error_handler_fn input start_position -> // n is not an integer constant, so we need to eta-expand and swap fun and if
   if n `U32.rem` U32.uint_to_t k.LP.parser_kind_low = 0ul
-  then validate_nlist_total_constant_size_mod_ok n p inv disj l ctxt error_handler_fn input start_position
-  else validate_nlist_constant_size_mod_ko n p inv disj l ctxt error_handler_fn input start_position
+  then validate_nlist_total_constant_size_mod_ok n n_is_const p inv disj l ctxt error_handler_fn input start_position
+  else validate_nlist_constant_size_mod_ko n n_is_const p inv disj l ctxt error_handler_fn input start_position
 
 inline_for_extraction noextract
 let validate_nlist_total_constant_size
-      (n_is_const: bool)
       (n:U32.t)
+      (n_is_const: option nat { memoizes_n_as_const n_is_const n })
       #wk
       (#k:parser_kind true wk)
       (#t: Type)
       (p:parser k t)
       inv disj l
-: Pure (validate_with_action_t (parse_nlist n p) inv disj l false true)
+: Pure (validate_with_action_t (parse_nlist n n_is_const p) inv disj l false true)
   (requires (
     let open LP in
     k.parser_kind_subkind = Some ParserStrong /\
@@ -1366,31 +1370,31 @@ let validate_nlist_total_constant_size
   if
     if k.LP.parser_kind_low = 1
     then true
-    else if n_is_const
+    else if Some? n_is_const
     then U32.v n % k.LP.parser_kind_low = 0
     else false
   then
-    validate_nlist_total_constant_size_mod_ok n p inv disj l
+    validate_nlist_total_constant_size_mod_ok n n_is_const p inv disj l
   else if
-    if n_is_const
+    if Some? n_is_const
     then U32.v n % k.LP.parser_kind_low <> 0
     else false
   then
-    validate_nlist_constant_size_mod_ko n p inv disj l
+    validate_nlist_constant_size_mod_ko n n_is_const p inv disj l
   else
-    validate_nlist_total_constant_size' n p inv disj l
+    validate_nlist_total_constant_size' n n_is_const p inv disj l
 
 noextract
 inline_for_extraction
 let validate_nlist_constant_size_without_actions
-    (n_is_const: bool)
-    (payload_is_constant_size: bool)
     (n:U32.t)
+    (n_is_const:option nat { memoizes_n_as_const n_is_const n })
+    (payload_is_constant_size: bool)
     #wk
     (#k:parser_kind true wk)
     #t (#p:parser k t) #inv #disj #l #ar
     (v: validate_with_action_t p inv disj l false ar)
-: Tot (validate_with_action_t (parse_nlist n p) inv disj l false false)
+: Tot (validate_with_action_t (parse_nlist n n_is_const p) inv disj l false false)
 = 
   if payload_is_constant_size
   then (
@@ -1401,12 +1405,12 @@ let validate_nlist_constant_size_without_actions
       k.parser_kind_metadata = Some ParserKindMetadataTotal &&
       k.parser_kind_low < 4294967296
     then
-      validate_drop (validate_nlist_total_constant_size n_is_const n p inv disj l)
+      validate_drop (validate_nlist_total_constant_size n n_is_const p inv disj l)
     else
-      validate_nlist n v
+      validate_nlist n n_is_const v
   )
   else
-    validate_nlist n v
+    validate_nlist n n_is_const v
 
 #push-options "--z3rlimit_factor 16 --z3cliopt smt.arith.nl=false"
 #restart-solver

diff --git a/src/3d/prelude/EverParse3d.Actions.Base.fsti b/src/3d/prelude/EverParse3d.Actions.Base.fsti
@@ -561,6 +561,7 @@ val validate_ite
 noextract inline_for_extraction
 val validate_nlist
        (n:U32.t)
+       (n_is_const:option nat { memoizes_n_as_const n_is_const n})
        (#wk: _)
        (#k:parser_kind true wk)
        (#[@@@erasable] t:Type)
@@ -570,13 +571,13 @@ val validate_nlist
        (#[@@@erasable] l:eloc)
        (#ha #allow_reading:bool)
        (v: validate_with_action_t p inv disj l ha allow_reading)
-: validate_with_action_t (parse_nlist n p) inv disj l ha false
+: validate_with_action_t (parse_nlist n n_is_const p) inv disj l ha false
 
 noextract inline_for_extraction
 val validate_nlist_constant_size_without_actions
-       (n_is_const: bool)
-       (payload_is_constant_size:bool)
        (n:U32.t)
+       (n_is_const: option nat { memoizes_n_as_const n_is_const n })
+       (payload_is_constant_size:bool)
        (#wk: _)
        (#k:parser_kind true wk)
        (#[@@@erasable] t:Type)
@@ -586,7 +587,7 @@ val validate_nlist_constant_size_without_actions
        (#[@@@erasable] l:eloc)
        (#allow_reading:bool)
        (v: validate_with_action_t p inv disj l false allow_reading)
-: Tot (validate_with_action_t (parse_nlist n p) inv disj l false false)
+: Tot (validate_with_action_t (parse_nlist n n_is_const p) inv disj l false false)
 
 noextract inline_for_extraction
 val validate_t_at_most

diff --git a/src/3d/prelude/EverParse3d.Kinds.fst b/src/3d/prelude/EverParse3d.Kinds.fst
@@ -75,27 +75,52 @@ let impos_kind
 /// Lists/arrays
 inline_for_extraction
 noextract
-let kind_nlist
+let kind_nlist_default
+: parser_kind false WeakKindStrongPrefix
+= let open LP in
+  let open FStar.Mul in
+  {
+    parser_kind_low = 0;
+    parser_kind_high = None;
+    parser_kind_subkind = Some ParserStrong;
+    parser_kind_metadata = None
+  }
+
+inline_for_extraction
+noextract
+let kind_nlist #b #w kelt nopt
   : parser_kind false WeakKindStrongPrefix
   = let open LP in
-    {
-      parser_kind_low = 0;
-      parser_kind_high = None;
-      parser_kind_subkind = Some ParserStrong;
-      parser_kind_metadata = None
-    }
+    let open FStar.Mul in
+    match nopt with
+    | None -> kind_nlist_default
+    | Some byte_size -> 
+      if Some kelt.parser_kind_low = kelt.parser_kind_high
+      && byte_size <> 0
+      && kelt.parser_kind_low % byte_size = 0
+      && kelt.parser_kind_subkind = Some ParserStrong
+      && kelt.parser_kind_metadata = Some ParserKindMetadataTotal
+      then (
+        {
+          parser_kind_low = byte_size;
+          parser_kind_high = Some byte_size;
+          parser_kind_subkind = Some ParserStrong;
+          parser_kind_metadata = None; //Some ParserKindMetadataTotal
+        }
+      )
+      else kind_nlist_default
 
 let kind_all_bytes
   : parser_kind false WeakKindConsumesAll
   = LowParse.Spec.Bytes.parse_all_bytes_kind
 
 let kind_t_at_most
   : parser_kind false WeakKindStrongPrefix
-  = kind_nlist
+  = kind_nlist_default
 
 let kind_t_exact
   : parser_kind false WeakKindStrongPrefix
-  = kind_nlist
+  = kind_nlist_default
 
 let parse_string_kind
   : parser_kind true WeakKindStrongPrefix

diff --git a/src/3d/prelude/EverParse3d.Kinds.fsti b/src/3d/prelude/EverParse3d.Kinds.fsti
@@ -68,7 +68,7 @@ val impos_kind
 /// Lists/arrays
 inline_for_extraction
 noextract
-val kind_nlist
+val kind_nlist #b #w (k:parser_kind b w) (n:option nat)
   : parser_kind false WeakKindStrongPrefix
 
 val kind_all_bytes

diff --git a/src/3d/prelude/EverParse3d.Prelude.fst b/src/3d/prelude/EverParse3d.Prelude.fst
@@ -101,13 +101,14 @@ let parse_ite e p1 p2
 let nlist (n:U32.t) (t:Type) = list t
 
 inline_for_extraction noextract
-let parse_nlist n #wk #k #t p
+let parse_nlist n n_is_const #wk #k #t p
   = let open LowParse.Spec.FLData in
     let open LowParse.Spec.List in
     parse_weaken
             #false #WeakKindStrongPrefix #(parse_fldata_kind (U32.v n) parse_list_kind) #(list t)
             (LowParse.Spec.FLData.parse_fldata (LowParse.Spec.List.parse_list p) (U32.v n))
-            #false kind_nlist
+            #false
+            (kind_nlist k n_is_const)
 
 let all_bytes = Seq.seq LP.byte
 let parse_all_bytes' 
@@ -180,7 +181,8 @@ let validator_no_read #nz #wk (#k:parser_kind nz wk) (#t:Type) (p:parser k t)
   = LPL.validator_no_read #k #t p
 
 let parse_nlist_total_fixed_size_aux
-  (n:U32.t) (#wk: _) (#k:parser_kind true wk) #t (p:parser k t)
+  (n:U32.t) (n_is_const:option nat { memoizes_n_as_const n_is_const n })
+  (#wk: _) (#k:parser_kind true wk) #t (p:parser k t)
   (x: LP.bytes)
 : Lemma
   (requires (
@@ -192,7 +194,7 @@ let parse_nlist_total_fixed_size_aux
     Seq.length x >= U32.v n
   ))
   (ensures (
-    Some? (LP.parse (parse_nlist n p) x)
+    Some? (LP.parse (parse_nlist n n_is_const p) x)
   ))
 = let x' = Seq.slice x 0 (U32.v n) in
   let cnt = (U32.v n / k.LP.parser_kind_low) in
@@ -202,7 +204,8 @@ let parse_nlist_total_fixed_size_aux
   LP.parser_kind_prop_equiv LowParse.Spec.List.parse_list_kind (LowParse.Spec.List.parse_list p)
 
 let parse_nlist_total_fixed_size_kind_correct
-  (n:U32.t) (#wk: _) (#k:parser_kind true wk) #t (p:parser k t)
+  (n:U32.t) (n_is_const:option nat { memoizes_n_as_const n_is_const n })
+  (#wk: _) (#k:parser_kind true wk) #t (p:parser k t)
 : Lemma
   (requires (
     let open LP in
@@ -212,15 +215,18 @@ let parse_nlist_total_fixed_size_kind_correct
     k.parser_kind_metadata == Some ParserKindMetadataTotal
   ))
   (ensures (
-    LP.parser_kind_prop (LP.total_constant_size_parser_kind (U32.v n)) (parse_nlist n p)
+    LP.parser_kind_prop (LP.total_constant_size_parser_kind (U32.v n)) (parse_nlist n n_is_const p)
   ))
-= LP.parser_kind_prop_equiv (LowParse.Spec.FLData.parse_fldata_kind (U32.v n) LowParse.Spec.List.parse_list_kind) (parse_nlist n p);
-  LP.parser_kind_prop_equiv (LP.total_constant_size_parser_kind (U32.v n)) (parse_nlist n p);
-  Classical.forall_intro (Classical.move_requires (parse_nlist_total_fixed_size_aux n p))
+= LP.parser_kind_prop_equiv (LowParse.Spec.FLData.parse_fldata_kind (U32.v n) LowParse.Spec.List.parse_list_kind) (parse_nlist n n_is_const p);
+  LP.parser_kind_prop_equiv (LP.total_constant_size_parser_kind (U32.v n)) (parse_nlist n n_is_const p);
+  Classical.forall_intro (Classical.move_requires (parse_nlist_total_fixed_size_aux n n_is_const p))
 
 inline_for_extraction noextract
-let validate_nlist_total_constant_size_mod_ok (n:U32.t) #wk (#k:parser_kind true wk) (#t: Type) (p:parser k t)
-  : Pure (validator_no_read (parse_nlist n p))
+let validate_nlist_total_constant_size_mod_ok
+    (n:U32.t)
+    (n_is_const:option nat { memoizes_n_as_const n_is_const n })
+    #wk (#k:parser_kind true wk) (#t: Type) (p:parser k t)
+  : Pure (validator_no_read (parse_nlist n n_is_const p))
   (requires (
     let open LP in
     k.parser_kind_subkind == Some ParserStrong /\
@@ -235,11 +241,11 @@ let validate_nlist_total_constant_size_mod_ok (n:U32.t) #wk (#k:parser_kind true
          let h = FStar.HyperStack.ST.get () in
          [@inline_let]
          let _ =
-           parse_nlist_total_fixed_size_kind_correct n p;
-           LPL.valid_facts (parse_nlist n p) h sl (LPL.uint64_to_uint32 pos);
-           LPL.valid_facts (LP.strengthen (LP.total_constant_size_parser_kind (U32.v n)) (parse_nlist n p)) h sl (LPL.uint64_to_uint32 pos)
+           parse_nlist_total_fixed_size_kind_correct n n_is_const p;
+           LPL.valid_facts (parse_nlist n n_is_const p) h sl (LPL.uint64_to_uint32 pos);
+           LPL.valid_facts (LP.strengthen (LP.total_constant_size_parser_kind (U32.v n)) (parse_nlist n n_is_const p)) h sl (LPL.uint64_to_uint32 pos)
          in
-         LPL.validate_total_constant_size_no_read (LP.strengthen (LP.total_constant_size_parser_kind (U32.v n)) (parse_nlist n p)) (FStar.Int.Cast.uint32_to_uint64 n) () sl len pos
+         LPL.validate_total_constant_size_no_read (LP.strengthen (LP.total_constant_size_parser_kind (U32.v n)) (parse_nlist n n_is_const p)) (FStar.Int.Cast.uint32_to_uint64 n) () sl len pos
       )
 
 module LUT = LowParse.Spec.ListUpTo

diff --git a/src/3d/prelude/EverParse3d.Prelude.fsti b/src/3d/prelude/EverParse3d.Prelude.fsti
@@ -110,11 +110,21 @@ val parse_ite (#nz:_) (#wk: _) (#k:parser_kind nz wk)
 ////////////////////////////////////////////////////////////////////////////////
 // Variable-sized list whose size in bytes is exactly n
 ////////////////////////////////////////////////////////////////////////////////
+unfold
+let memoizes_n_as_const (n_is_const:option nat) (n:U32.t) =
+  Some? n_is_const ==> Some?.v n_is_const = U32.v n
+
 val nlist (n:U32.t) (t:Type u#r) : Type u#r
 
 inline_for_extraction noextract
-val parse_nlist (n:U32.t) (#wk: _) (#k:parser_kind true wk) (#t:_) (p:parser k t)
-  : Tot (parser kind_nlist (nlist n t))
+val parse_nlist
+        (n:U32.t)
+        (n_const:option nat { Some? n_const ==> Some?.v n_const == U32.v n })
+        (#wk: _)
+        (#k:parser_kind true wk)
+        (#t:_)
+        (p:parser k t)
+  : Tot (parser (kind_nlist k n_const) (nlist n t))
 
 /////
 // Parse all of the remaining bytes of the input buffer