Merge branch 'master' of github.com:project-everest/everparse into ta…

…ramana_ci

.docker/produce-binary.Dockerfile

@@ -1,6 +1,6 @@
 # This Dockerfile should be run from the root EverParse directory
 
-ARG ocaml_version=4.12
+ARG ocaml_version=4.14
 FROM ocaml/opam:ubuntu-20.04-ocaml-$ocaml_version
 
 ADD --chown=opam:opam ./ $HOME/everparse/

.docker/standalone.Dockerfile

@@ -1,6 +1,6 @@
 # This Dockerfile should be run from the root EverParse directory
 
-ARG ocaml_version=4.12
+ARG ocaml_version=4.14
 FROM ocaml/opam:ubuntu-23.10-ocaml-$ocaml_version
 
 ADD --chown=opam:opam ./ $HOME/everparse/

doc/build.rst

@@ -80,7 +80,7 @@ Linux
    * wget
    * which
 
-3. Run ``opam init --compiler=4.12.0`` and follow the instructions. This will install OCaml.
+3. Run ``opam init --compiler=4.14.0`` and follow the instructions. This will install OCaml.
 
    This step will modify your configuration scripts to add the path to
    OCaml and its libraries to the PATH environment variable every time
@@ -89,8 +89,8 @@ Linux
 
    .. note::
 
-      You need to specify an OCaml version number (between 4.08.0 and
-      4.12.x), so that OCaml will be installed in your user profile,
+      You need to specify an OCaml version number (between 4.12.0 and
+      4.14.x), so that OCaml will be installed in your user profile,
       because some EverParse dependencies do not work well with a
       system-wide OCaml. Thus, if opam says that there is an
       ambiguity, you should re-run ``opam init`` with the non-system

src/lowparse/LowParse.Low.Bytes.fst

@@ -395,6 +395,8 @@ let jump_bounded_vlbytes
 : Tot (jumper (parse_bounded_vlbytes min max))
 = jump_bounded_vlbytes' min max (log256' max)
 
+#push-options "--z3rlimit 32"
+
 let valid_exact_all_bytes_elim
   (h: HS.mem)
   (#rrel #rel: _)
@@ -415,8 +417,6 @@ let valid_exact_all_bytes_elim
   assert (no_lookahead_on (parse_flbytes length) (bytes_of_slice_from_to h input pos pos') (bytes_of_slice_from h input pos));
   assert (injective_postcond (parse_flbytes length) (bytes_of_slice_from_to h input pos pos') (bytes_of_slice_from h input pos))
 
-#push-options "--z3rlimit 32"
-
 let valid_bounded_vlbytes'_elim
   (h: HS.mem)
   (min: nat)

src/lowparse/LowParse.Spec.Base.fst

@@ -23,6 +23,11 @@ let parser_kind_prop_ext
 = no_lookahead_ext f1 f2;
   injective_ext f1 f2
 
+let tot_bare_parser_of_bare_parser
+  #t
+  p
+= Ghost.reveal (FStar.Ghost.Pull.pull p)
+
 let is_weaker_than_correct
   (k1: parser_kind)
   (k2: parser_kind)
@@ -96,6 +101,10 @@ let serializer_correct_implies_complete
   in
   Classical.forall_intro (Classical.move_requires prf)
 
+let tot_bare_serializer_of_bare_serializer
+  s
+= FStar.Ghost.Pull.pull s
+
 let serializer_parser_unique'
   (#k1: parser_kind)
   (#t: Type)

src/lowparse/LowParse.Spec.Base.fsti

@@ -32,6 +32,15 @@ let parse
 : GTot (option (t * consumed_length input))
 = p input
 
+let parse_consume
+  (#t: Type)
+  (p: bare_parser t)
+  (input: bytes)
+: GTot (option (consumed_length input))
+= match parse p input with
+  | None -> None
+  | Some (_, consumed) -> Some consumed
+
 (** Injectivity of parsing *)
 
 let injective_precond
@@ -359,6 +368,31 @@ let tot_parser
 : Tot Type
 = (f: tot_bare_parser t { parser_kind_prop k f } )
 
+val tot_bare_parser_of_bare_parser
+  (#t: Type)
+  (p: bare_parser t)
+: Ghost (tot_bare_parser t)
+    (requires True)
+    (ensures (fun p' -> forall x . parse p' x == parse p x))
+
+let tot_parser_of_parser
+  (#k: parser_kind)
+  (#t: Type)
+  (p: parser k t)
+: Ghost (tot_parser k t)
+    (requires True)
+    (ensures (fun p' -> forall x . parse p' x == parse p x))
+= let p' = tot_bare_parser_of_bare_parser p in
+  parser_kind_prop_ext k p p';
+  p'
+
+let parser_of_tot_parser
+  (#k: parser_kind)
+  (#t: Type)
+  (p: tot_parser k t)
+: Tot (parser k t)
+= p
+
 inline_for_extraction
 let get_parser_kind
   (#k: parser_kind)
@@ -658,6 +692,23 @@ let serializer_correct
 : GTot Type0
 = forall (x: t) .{:pattern (parse p (f x))} parse p (f x) == Some (x, Seq.length (f x))
 
+let serializer_correct_ext_gen
+  (#k1: parser_kind)
+  (#t1: Type)
+  (p1: parser k1 t1)
+  (f1: bare_serializer t1)
+  (#k2: parser_kind)
+  (#t2: Type)
+  (p2: parser k2 t2)
+  (f2: bare_serializer t1)
+: Lemma
+  (requires (t1 == t2 /\
+    (forall (input: bytes) . parse p1 input == parse p2 input) /\
+    (forall (x: t1) . f1 x == f2 x)
+  ))
+  (ensures (serializer_correct p1 f1 <==> serializer_correct p2 f2))
+= ()
+
 let serializer_correct_ext
   (#k1: parser_kind)
   (#t1: Type)
@@ -701,6 +752,34 @@ let serializer
 : Tot Type
 = (f: bare_serializer t { serializer_correct p f } )
 
+inline_for_extraction
+let tot_bare_serializer
+  (t: Type)
+: Tot Type
+= t -> Tot bytes
+
+[@unifier_hint_injective]
+let tot_serializer
+  (#k: parser_kind)
+  (#t: Type)
+  (p: tot_parser k t)
+: Tot Type
+= (f: tot_bare_serializer t { serializer_correct #k p f } )
+
+let mk_tot_serializer
+  (#k: parser_kind)
+  (#t: Type)
+  (p: tot_parser k t)
+  (f: tot_bare_serializer t)
+  (prf: (
+    (x: t) ->
+    Lemma
+    (parse p (f x) == Some (x, Seq.length (f x)))
+  ))
+: Tot (tot_serializer p)
+= Classical.forall_intro prf;
+  f
+
 let mk_serializer
   (#k: parser_kind)
   (#t: Type)
@@ -753,6 +832,13 @@ let serialize_ext'
   (ensures (fun _ -> True))
 = serialize_ext p1 s1 p2
 
+let bare_serialize
+  (#t: Type)
+  (s: bare_serializer t)
+  (x: t)
+: GTot bytes
+= s x
+
 let serialize
   (#k: parser_kind)
   (#t: Type)
@@ -762,6 +848,45 @@ let serialize
 : GTot bytes
 = s x
 
+val tot_bare_serializer_of_bare_serializer
+  (#t: Type)
+  (s: bare_serializer t)
+: Ghost (tot_bare_serializer t)
+    (requires True)
+    (ensures (fun s' -> forall x . bare_serialize s' x == bare_serialize s x))
+
+let tot_serializer_of_serializer
+  (#k: parser_kind)
+  (#t: Type)
+  (#p: parser k t)
+  (s: serializer p)
+: Ghost (tot_serializer (tot_parser_of_parser p))
+    (requires True)
+    (ensures (fun s' -> forall x . bare_serialize s' x == serialize #k s x))
+= tot_bare_serializer_of_bare_serializer s
+
+let serializer_of_tot_serializer
+  (#k: parser_kind)
+  (#t: Type)
+  (#p: tot_parser k t)
+  (s: tot_serializer p)
+: Tot (serializer (parser_of_tot_parser p))
+= s
+
+let tot_serialize_ext
+  (#k1: parser_kind)
+  (#t1: Type)
+  (p1: tot_parser k1 t1)
+  (s1: tot_serializer p1)
+  (#k2: parser_kind)
+  (#t2: Type)
+  (p2: tot_parser k2 t2)
+: Pure (tot_serializer p2)
+  (requires (t1 == t2 /\ (forall (input: bytes) . parse p1 input == parse p2 input)))
+  (ensures (fun _ -> True))
+= serializer_correct_ext #k1 p1 s1 #k2 p2;
+  (s1 <: tot_bare_serializer t2)
+
 let parse_serialize
   (#k: parser_kind)
   (#t: Type)
@@ -800,6 +925,21 @@ let serializer_unique
   let _ = parse p (s2 x) in
   serializer_correct_implies_complete p s2
 
+let serializer_unique_strong
+  (#t: Type)
+  (#k1: parser_kind)
+  (#p1: parser k1 t)
+  (s1: serializer p1)
+  (#k2: parser_kind)
+  (#p2: parser k2 t)
+  (s2: serializer p2)
+  (x: t)
+: Lemma
+  (requires (forall x . parse p1 x == parse p2 x))
+  (ensures (s1 x == s2 x))
+= let s1' = serialize_ext p2 s2 p1 in
+  serializer_unique p1 s1 s1' x
+
 let serializer_injective
   (#k: parser_kind)
   (#t: Type)
@@ -871,6 +1011,21 @@ val serialize_length
   ))
   [SMTPat (Seq.length (serialize s x))]
 
+let tot_serialize_length
+  (#k: parser_kind)
+  (#t: Type)
+  (#p: tot_parser k t)
+  (s: tot_serializer p)
+  (x: t)
+: Lemma
+  (let x = Seq.length (bare_serialize s x) in
+   k.parser_kind_low <= x /\ (
+   match k.parser_kind_high with
+   | None -> True
+   | Some y -> x <= y
+  ))
+= serialize_length #k #t #p s x
+
 val serialize_not_fail
   (#k: parser_kind)
   (#t: Type)
@@ -898,6 +1053,21 @@ let serialize_strong_prefix
   parse_strong_prefix p (serialize s x2) (serialize s x2 `Seq.append` q2);
   Seq.lemma_append_inj (serialize s x1) q1 (serialize s x2) q2
 
+let tot_serialize_strong_prefix
+  (#k: parser_kind)
+  (#t: Type)
+  (#p: tot_parser k t)
+  (s: tot_serializer p)
+  (x1 x2: t)
+  (q1 q2: bytes)
+: Lemma
+  (requires (
+    k.parser_kind_subkind == Some ParserStrong /\
+    bare_serialize s x1 `Seq.append` q1 == bare_serialize s x2 `Seq.append` q2
+  ))
+  (ensures (x1 == x2 /\ q1 == q2))
+= serialize_strong_prefix #k #t #p s x1 x2 q1 q2
+
 let parse_truncate
   (#k: parser_kind)
   (#t: Type)

src/lowparse/LowParse.Spec.BitFields.fst

@@ -92,6 +92,9 @@ let rec synth_bitfield_ext (#tot: pos) (#t: Type) (cl: uint_t tot t) (lo: nat) (
 let parse_bitfield (#t: Type) (#k: parser_kind) (p: parser k t) (#tot: pos) (cl: uint_t tot t) (l: list nat { valid_bitfield_widths 0 tot l }) : Tot (parser k (bitfields cl 0 tot l)) =
   p `parse_synth` synth_bitfield cl 0 tot l
 
+let tot_parse_bitfield (#t: Type) (#k: parser_kind) (p: tot_parser k t) (#tot: pos) (cl: uint_t tot t) (l: list nat { valid_bitfield_widths 0 tot l }) : Tot (tot_parser k (bitfields cl 0 tot l)) =
+  p `tot_parse_synth` synth_bitfield cl 0 tot l
+
 let rec synth_bitfield_recip' (#tot: pos) (#t: Type) (cl: uint_t tot t) (lo: nat) (hi: nat { lo <= hi /\ hi <= tot }) (l: list nat { valid_bitfield_widths lo hi l }) (x: bitfields cl lo hi l) : Tot t (decreases l) =
   match l with
   | [] -> cl.uint_to_t 0
@@ -151,6 +154,17 @@ let serialize_bitfield
     (synth_bitfield_recip cl 0 tot l)
     ()
 
+let tot_serialize_bitfield
+  (#t: Type) (#k: parser_kind) (#p: tot_parser k t) (s: tot_serializer #k p)
+  (#tot: pos) (cl: uint_t tot t) (l: list nat { valid_bitfield_widths 0 tot l })
+: Tot (tot_serializer #k (tot_parse_bitfield p cl l))
+= tot_serialize_synth
+    p
+    (synth_bitfield cl 0 tot l)
+    s
+    (synth_bitfield_recip cl 0 tot l)
+    ()
+
 let parse_bitfield64 (l: list nat { valid_bitfield_widths 0 64 l }) : Tot (parser parse_u64_kind (bitfields uint64 0 64 l)) =
   parse_bitfield parse_u64 uint64 l