propagating disjointness_pre inference through the interpreter

project-everest · Nov 29, 2023 · 563c2b5 · 563c2b5
1 parent 263bdfa
commit 563c2b5
Show file tree

Hide file tree

Showing 4 changed files with 224 additions and 163 deletions.
diff --git a/src/3d/prelude/EverParse3d.Actions.All.fsti b/src/3d/prelude/EverParse3d.Actions.All.fsti
@@ -10,15 +10,15 @@ noextract
 inline_for_extraction
 val action_field_ptr
       (u:squash (EverParse3d.Actions.BackendFlag.backend_flag == BackendFlagBuffer))
-   : action true_inv eloc_none true ___PUINT8
+   : action true_inv disjointness_trivial eloc_none true ___PUINT8
 
 noextract
 inline_for_extraction
 val action_field_ptr_after
       (u:squash (EverParse3d.Actions.BackendFlag.backend_flag == BackendFlagExtern))
       (sz: FStar.UInt64.t)
       (write_to: bpointer ___PUINT8)
-   : action (ptr_inv write_to) (ptr_loc write_to) false bool // if action returns true, writes some value to write_to. if false, do nothing
+   : action (ptr_inv write_to) disjointness_trivial (ptr_loc write_to) false bool // if action returns true, writes some value to write_to. if false, do nothing
 
 noextract
 inline_for_extraction
@@ -27,10 +27,10 @@ val action_field_ptr_after_with_setter
       (sz: FStar.UInt64.t)
       (#output_loc: eloc)
       (write_to: (___PUINT8 -> Tot (external_action output_loc)))
-   : action true_inv output_loc false bool // if action returns true, writes some value to write_to. if false, do nothing
+   : action true_inv disjointness_trivial output_loc false bool // if action returns true, writes some value to write_to. if false, do nothing
 
 noextract
 inline_for_extraction
 val action_field_pos_32
       (u:squash (EverParse3d.Actions.BackendFlag.backend_flag == BackendFlagBuffer))
-   : action true_inv eloc_none false FStar.UInt32.t
+   : action true_inv disjointness_trivial eloc_none false FStar.UInt32.t
diff --git a/src/3d/prelude/EverParse3d.Actions.Base.fst b/src/3d/prelude/EverParse3d.Actions.Base.fst
@@ -1375,7 +1375,7 @@ let validate_weaken_inv_loc
       #nz #wk (#k:parser_kind nz wk) #t (#p:parser k t)
       #inv #disj (#l:eloc) #ar
       (inv':slice_inv{inv' `inv_implies` inv})
-      (#disj':_{ disj' `imp_disjointness` disj})
+      (disj':_{ disj' `imp_disjointness` disj})
       (l':eloc{l' `eloc_includes` l})
       (v:validate_with_action_t p inv disj l ar)
   : Tot (validate_with_action_t p inv' disj' l' ar)

diff --git a/src/3d/prelude/EverParse3d.Actions.Base.fsti b/src/3d/prelude/EverParse3d.Actions.Base.fsti
@@ -543,7 +543,7 @@ val validate_weaken_inv_loc
        (#[@@@erasable] l:eloc)
        (#allow_reading:bool)
        ([@@@erasable] inv':slice_inv{inv' `inv_implies` inv})
-       (#[@@@erasable] disj':disjointness_pre { disj' `imp_disjointness` disj })
+       ([@@@erasable] disj':disjointness_pre { disj' `imp_disjointness` disj })
        ([@@@erasable] l':eloc{l' `eloc_includes` l})
        (v:validate_with_action_t p inv disj l allow_reading)
   : Tot (validate_with_action_t p inv' disj' l' allow_reading)
@@ -801,7 +801,7 @@ val probe_then_validate
       (v:validate_with_action_t p inv disj l allow_reading)
       (src:U64.t)
       (len:U64.t)
-      (dest:CP.t { copy_buffer_loc dest `eloc_disjoint` l })
+      (dest:CP.t)
       (probe:CP.probe_fn)
   : action (conj_inv inv (copy_buffer_inv dest))
            (conj_disjointness (disjoint (copy_buffer_loc dest) l) disj)