Merge branch 'master' into _taramana_pulse

project-everest · Jan 8, 2025 · de121ca · de121ca
2 parents 2a41fcb + 5d821a7
commit de121ca
Show file tree

Hide file tree

Showing 5 changed files with 575 additions and 124 deletions.
diff --git a/src/lowparse/LowParse.Spec.Base.fst b/src/lowparse/LowParse.Spec.Base.fst
@@ -23,11 +23,6 @@ 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)
@@ -101,10 +96,6 @@ 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)

diff --git a/src/lowparse/LowParse.Spec.Base.fsti b/src/lowparse/LowParse.Spec.Base.fsti
@@ -368,24 +368,6 @@ 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)
@@ -848,23 +830,6 @@ 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)

diff --git a/src/lowparse/LowParse.Spec.Fuel.fst b/src/lowparse/LowParse.Spec.Fuel.fst
@@ -199,6 +199,13 @@ let parser_kind_prop_fuel_ext
   injective_fuel_ext fuel f1 f2
 
 let close_by_fuel'
+  (#t: Type)
+  (f: (nat -> Tot (bare_parser t)))
+  (closure: ((b: bytes) -> GTot (n: nat { Seq.length b < n })))
+: Tot (bare_parser t)
+= fun x -> f (closure x) x
+
+let tot_close_by_fuel'
   (#t: Type)
   (f: (nat -> Tot (tot_bare_parser t)))
   (closure: ((b: bytes) -> Tot (n: nat { Seq.length b < n })))
@@ -208,8 +215,8 @@ let close_by_fuel'
 let close_by_fuel_correct
   (#t: Type)
   (k: parser_kind)
-  (f: (nat -> Tot (tot_bare_parser t)))
-  (closure: ((b: bytes) -> Tot (n: nat { Seq.length b < n })))
+  (f: (nat -> Tot (bare_parser t)))
+  (closure: ((b: bytes) -> GTot (n: nat { Seq.length b < n })))
   (f_ext: (
     (fuel: nat) ->
     (b: bytes { Seq.length b < fuel }) ->
@@ -242,6 +249,42 @@ let close_by_fuel_correct
   parser_kind_prop_equiv k (close_by_fuel' f closure)
 
 let close_by_fuel
+  (#k: parser_kind)
+  (#t: Type)
+  (f: (nat -> Tot (parser k t)))
+  (closure: ((b: bytes) -> GTot (n: nat { Seq.length b < n })))
+  (f_ext: (
+    (fuel: nat) ->
+    (b: bytes { Seq.length b < fuel }) ->
+    Lemma
+    (f fuel b == f (closure b) b)
+  ))
+: Tot (parser k t)
+= close_by_fuel_correct k f closure f_ext (fun fuel -> parser_kind_prop_equiv k (f fuel));
+  close_by_fuel' f closure
+
+let tot_close_by_fuel_correct
+  (#t: Type)
+  (k: parser_kind)
+  (f: (nat -> Tot (tot_bare_parser t)))
+  (closure: ((b: bytes) -> Tot (n: nat { Seq.length b < n })))
+  (f_ext: (
+    (fuel: nat) ->
+    (b: bytes { Seq.length b < fuel }) ->
+    Lemma
+    (f fuel b == f (closure b) b)
+  ))
+  (f_prop: (
+    (fuel: nat) ->
+    Lemma
+    (parser_kind_prop_fuel fuel k (f fuel))
+  ))
+: Lemma
+  (parser_kind_prop k (tot_close_by_fuel' f closure))
+= close_by_fuel_correct k f closure f_ext f_prop;
+  parser_kind_prop_ext k (tot_close_by_fuel' f closure) (close_by_fuel' f closure)
+
+let tot_close_by_fuel
   (#k: parser_kind)
   (#t: Type)
   (f: (nat -> Tot (tot_parser k t)))
@@ -253,5 +296,5 @@ let close_by_fuel
     (f fuel b == f (closure b) b)
   ))
 : Tot (tot_parser k t)
-= close_by_fuel_correct k f closure f_ext (fun fuel -> parser_kind_prop_equiv k (f fuel));
-  close_by_fuel' f closure
+= tot_close_by_fuel_correct k f closure f_ext (fun fuel -> parser_kind_prop_equiv k (f fuel));
+  tot_close_by_fuel' f closure