probe and validate as a derived form in the interpreter

src/3d/prelude/EverParse3d.Actions.Base.fst

@@ -12,12 +12,12 @@ module CP = EverParse3d.CopyBuffer
 module AppCtxt = EverParse3d.AppCtxt
 module LPE = EverParse3d.ErrorCode
 open FStar.Tactics.Typeclasses
-
+open FStar.FunctionalExtensionality
 module B = LowStar.Buffer
 module U8 = FStar.UInt8
 module P = EverParse3d.Prelude
-
-let hinv = HS.mem -> Tot Type0
+module F = FStar.FunctionalExtensionality
+let hinv = HS.mem ^-> prop
 let liveness_inv = i:hinv {
   forall l h0 h1. {:pattern (i h1); (modifies l h0 h1)}  i h0 /\ modifies l h0 h1 /\ address_liveness_insensitive_locs `loc_includes` l ==> i h1
 }
@@ -26,8 +26,8 @@ let slice_inv = mem_inv
 let inv_implies (inv0 inv1:slice_inv) =
   forall h.
     inv0 h ==> inv1 h
-let true_inv : slice_inv = fun _ -> True
-let conj_inv (i0 i1:slice_inv) : slice_inv = fun h -> i0 h /\ i1 h
+let true_inv : slice_inv = F.on HS.mem #prop (fun _ -> True)
+let conj_inv (i0 i1:slice_inv) : slice_inv = F.on HS.mem #prop (fun h -> i0 h /\ i1 h)
 let eloc = (l: FStar.Ghost.erased B.loc { B.address_liveness_insensitive_locs `B.loc_includes` l })
 let eloc_union (l1 l2:eloc) : Tot eloc = B.loc_union l1 l2
 let eloc_none : eloc = B.loc_none
@@ -36,14 +36,20 @@ let eloc_disjoint (l1 l2:eloc) = B.loc_disjoint l1 l2 /\ True
 let inv_implies_refl inv = ()
 let inv_implies_true inv0 = ()
 let inv_implies_conj inv0 inv1 inv2 h01 h02 = ()
+let conj_inv_true_left_unit i =
+  FStar.PredicateExtensionality.predicateExtensionality _ (conj_inv true_inv i) i
+let conj_inv_true_right_unit i =
+  FStar.PredicateExtensionality.predicateExtensionality _ (conj_inv i true_inv) i
 
 let eloc_includes_none l = ()
 let eloc_includes_union l0 l1 l2 h01 h02 = ()
 let eloc_includes_refl l = ()
+let eloc_union_none_left_unit l = ()
+let eloc_union_none_right_unit l = ()
 
 let bpointer a = B.pointer a
 let ptr_loc #a (x:B.pointer a) : Tot eloc = B.loc_buffer x
-let ptr_inv #a (x:B.pointer a) : slice_inv = fun h -> B.live h x
+let ptr_inv #a (x:B.pointer a) : slice_inv = F.on HS.mem #prop (fun h -> B.live h x /\ True)
 let app_ctxt = AppCtxt.app_ctxt
 let app_loc (x:AppCtxt.app_ctxt) (l:eloc) : eloc = 
   AppCtxt.properties x;
@@ -1662,20 +1668,29 @@ let action_field_ptr
        let open LowParse.Slice in
        LPL.offset input (LPL.uint64_to_uint32 startPosition)
 *)
+module T = FStar.Tactics
+let ptr_inv_elim (x:B.pointer 'a)
+  : Lemma
+    (ensures forall h. ptr_inv x h ==> B.live h x)
+  = introduce forall h. ptr_inv x h ==> B.live h x
+         with assert (ptr_inv x h ==> B.live h x)
+                  by (T.norm [delta])
 
 noextract
 inline_for_extraction
 let action_deref
       (#a:_) (x:B.pointer a)
    : action (ptr_inv x) loc_none false a
-   = fun _ _ _ _ _ _ -> !*x
+   = fun _ _ _ _ _ _ -> 
+        ptr_inv_elim x;
+        !*x
 
 noextract
 inline_for_extraction
 let action_assignment
       (#a:_) (x:B.pointer a) (v:a)
    : action (ptr_inv x) (ptr_loc x) false unit
-   = fun _ _ _ _ _ _ -> x *= v
+   = fun _ _ _ _ _ _ -> ptr_inv_elim x; x *= v
 
 (* FIXME: This is now unsound.
 noextract
@@ -1706,7 +1721,7 @@ let mk_external_action  #_ f = fun _ _ _ _ _ _ -> f ()
 let copy_buffer_inv (x:CP.t)
 : slice_inv
 = CP.properties x;
-  CP.inv x
+  F.on HS.mem #prop (CP.inv x)
 let copy_buffer_loc (x:CP.t)
 : eloc
 = CP.loc_of x

src/3d/prelude/EverParse3d.Actions.Base.fsti

@@ -41,12 +41,20 @@ val inv_implies_true (inv0:slice_inv) : Tot (squash (inv0 `inv_implies` true_inv
 
 val inv_implies_conj (inv0 inv1 inv2: slice_inv) (h01: squash (inv0 `inv_implies` inv1)) (h02: squash (inv0 `inv_implies` inv2)) : Tot (squash (inv0 `inv_implies` (inv1 `conj_inv` inv2)))
 
+val conj_inv_true_left_unit (inv:slice_inv) : Tot (squash (true_inv `conj_inv` inv == inv))
+
+val conj_inv_true_right_unit (inv:slice_inv) : Tot (squash (inv `conj_inv` true_inv == inv))
+
 val eloc_includes_none (l1:eloc) : Tot (squash (l1 `eloc_includes` eloc_none))
 
 val eloc_includes_union (l0: eloc) (l1 l2: eloc) (h01: squash (l0 `eloc_includes` l1)) (h02: squash (l0 `eloc_includes` l2)) : Tot (squash (l0 `eloc_includes` (l1 `eloc_union` l2)))
 
 val eloc_includes_refl (l: eloc) : Tot (squash (l `eloc_includes` l))
 
+val eloc_union_none_left_unit (l:eloc) : Tot (squash (eloc_none `eloc_union` l == l))
+
+val eloc_union_none_right_unit (l:eloc) : Tot (squash (l `eloc_union` eloc_none == l))
+
 inline_for_extraction
 noextract
 val bpointer (a: Type0) : Tot Type0

src/3d/prelude/EverParse3d.Interpreter.fst

@@ -833,6 +833,31 @@ type typ
       terminator:dtyp_as_type element_type ->
       typ P.parse_string_kind A.true_inv A.eloc_none false
 
+[@@specialize]
+let t_probe_then_validate
+      (fieldname:string)
+      (len:U64.t)
+      (probe:CP.probe_fn)
+      (dest:CP.t)
+      (#nz #wk:_) (#pk:P.parser_kind nz wk)
+      (#has_reader #i:_)
+      (#l:A.eloc { A.copy_buffer_loc dest `A.eloc_disjoint` l })
+      (td:dtyp pk has_reader i l)
+ : typ (parser_kind_of_itype UInt64)
+       (A.conj_inv i (A.copy_buffer_inv dest))
+       (A.eloc_union l (A.copy_buffer_loc dest))
+       false
+ = let t = 
+    T_with_dep_action fieldname
+     (DT_IType UInt64)
+     (fun src ->
+        Atomic_action (Action_probe_then_validate td src len dest probe))
+   in
+   coerce_eq (
+    A.eloc_union_none_left_unit (A.eloc_union l (A.copy_buffer_loc dest));
+    A.conj_inv_true_left_unit (A.conj_inv i (A.copy_buffer_inv dest))
+   ) t
+
 
 (* Type denotation of `typ` *)
 let rec as_type
@@ -892,6 +917,7 @@ let rec as_type
     | T_string _ elt_t terminator ->
       P.cstring (dtyp_as_type elt_t) terminator
 
+
 (* Parser denotation of `typ` *)
 let rec as_parser
           #nz #wk (#pk:P.parser_kind nz wk)
@@ -1205,7 +1231,8 @@ let specialization_steps =
                 `%fst;
                 `%snd;
                 `%Mktuple2?._1;
-                `%Mktuple2?._2]@projector_names)]
+                `%Mktuple2?._2;
+                `coerce_eq]@projector_names)]
 
 let specialize_tac steps (_:unit)
   : T.Tac unit