Use itree SpecM monad instead of CompM in Heapster

.github/workflows/ci.yml

@@ -277,11 +277,15 @@ jobs:
 
       - uses: ocaml/setup-ocaml@v2
         with:
-          ocaml-compiler: 4.12.x
+          ocaml-compiler: 4.14.x
 
       - run: opam repo add coq-released https://coq.inria.fr/opam/released
 
-      - run: opam install -y coq=8.13.2 coq-bits=1.1.0
+      - run: opam install -y coq=8.15.2 coq-bits=1.1.0
+
+        # If you change the entree-specs commit below, make sure you update the
+        # documentation in saw-core-coq/README.md accordingly.
+      - run: opam pin -y entree-specs https://github.com/GaloisInc/entree-specs.git#b011f29680fdde87489bc06ae98bfff0f97795b3
 
       # FIXME: the following steps generate Coq libraries for the SAW core to
       # Coq translator and builds them; if we do other Coq tests, these steps

heapster-saw/examples/_CoqProject

@@ -2,37 +2,40 @@
 -Q ../../saw-core-coq/coq/handwritten/CryptolToCoq   CryptolToCoq
 -Q . Examples
 
+# FIXME: Uncomment _proofs files when they're updated with the latest automation
 linked_list_gen.v
 linked_list_proofs.v
 xor_swap_gen.v
-xor_swap_proofs.v
+#xor_swap_proofs.v
 xor_swap_rust_gen.v
-xor_swap_rust_proofs.v
+#xor_swap_rust_proofs.v
 c_data_gen.v
-c_data_proofs.v
+#c_data_proofs.v
 string_set_gen.v
-string_set_proofs.v
+#string_set_proofs.v
 loops_gen.v
-loops_proofs.v
+#loops_proofs.v
 iter_linked_list_gen.v
-iter_linked_list_proofs.v
+#iter_linked_list_proofs.v
 iso_recursive_gen.v
-iso_recursive_proofs.v
+#iso_recursive_proofs.v
 memcpy_gen.v
-memcpy_proofs.v
+#memcpy_proofs.v
 rust_data_gen.v
-rust_data_proofs.v
+#rust_data_proofs.v
 rust_lifetimes_gen.v
-rust_lifetimes_proofs.v
+#rust_lifetimes_proofs.v
 arrays_gen.v
-arrays_proofs.v
+#arrays_proofs.v
 clearbufs_gen.v
-clearbufs_proofs.v
+#clearbufs_proofs.v
 exp_explosion_gen.v
-exp_explosion_proofs.v
+#exp_explosion_proofs.v
 mbox_gen.v
 mbox_proofs.v
 global_var_gen.v
-global_var_proofs.v
+#global_var_proofs.v
 sha512_gen.v
 #sha512_proofs.v
+io_gen.v
+#io_proofs.v

heapster-saw/examples/c_data.saw

@@ -26,7 +26,8 @@ heapster_assume_fun env "malloc"
   "(sz:bv 64). arg0:eq(llvmword(8*sz)) -o \
              \ arg0:true, ret:array(W,0,<sz,*8,fieldsh(true))"
   "\\ (sz:Vec 64 Bool) -> \
-    \ returnM (BVVec 64 sz #()) \
+    \ retS VoidEv emptyFunStack \
+            \ (BVVec 64 sz #()) \
             \ (genBVVec 64 sz #() (\\ (i:Vec 64 Bool) (_:is_bvult 64 i sz) -> ()))";
 
 

heapster-saw/examples/global_var.sawcore

@@ -2,9 +2,12 @@ module GlobalVar where
 
 import Prelude;
 
-acquireLockM : Vec 64 Bool -> CompM (Vec 64 Bool * Vec 64 Bool);
-acquireLockM u = returnM (Vec 64 Bool * Vec 64 Bool)
-			 (u,u);
+acquireLockM : Vec 64 Bool ->
+               SpecM VoidEv emptyFunStack (Vec 64 Bool * Vec 64 Bool);
+acquireLockM u =
+  retS VoidEv emptyFunStack (Vec 64 Bool * Vec 64 Bool) (u,u);
 
-releaseLockM : Vec 64 Bool -> Vec 64 Bool -> CompM (Vec 64 Bool);
-releaseLockM u new_u = returnM (Vec 64 Bool) new_u;
+releaseLockM : Vec 64 Bool -> Vec 64 Bool ->
+               SpecM VoidEv emptyFunStack (Vec 64 Bool);
+releaseLockM u new_u =
+  retS VoidEv emptyFunStack (Vec 64 Bool) new_u;

heapster-saw/examples/io.c

@@ -0,0 +1,7 @@
+#include<unistd.h>
+
+#define HELLO "Hello, World!"
+
+void hello_world () {
+  write (1, HELLO, sizeof(HELLO));
+}

heapster-saw/examples/io.saw

@@ -0,0 +1,30 @@
+enable_experimental;
+env <- heapster_init_env_from_file "io.sawcore" "io.bc";
+
+// Set the event type
+heapster_set_event_type env "ioEv";
+
+// Integer types
+heapster_define_perm env "int64" " " "llvmptr 64" "exists x:bv 64.eq(llvmword(x))";
+heapster_define_perm env "int32" " " "llvmptr 32" "exists x:bv 32.eq(llvmword(x))";
+heapster_define_perm env "int8" " " "llvmptr 8" "exists x:bv 8.eq(llvmword(x))";
+
+heapster_define_perm env "int8array" "rw:rwmodality,len:bv 64" "llvmptr 64"
+  "array(rw,0,<len,*1,fieldsh(8,int8<>))";
+
+// Assume the read and write functions call their corresponding events
+heapster_assume_fun env "\01_write"
+  "(len:bv 64). \
+   \ arg0:int32<>, arg1:int8array<R,len>, arg2:eq(llvmword(len)) -o ret:int64<>"
+  "\\ (len:Vec 64 Bool) (fd:Vec 32 Bool) (buf:buffer len) -> \
+    \ triggerS ioEv emptyFunStack (writeEv fd len buf)";
+
+
+///
+/// And now to start type-checking!
+///
+
+heapster_typecheck_fun env "hello_world" "(). empty -o empty";
+
+// Finally, export everything to Coq
+heapster_export_coq env "io_gen.v";

heapster-saw/examples/io.sawcore

@@ -0,0 +1,31 @@
+
+module io where
+
+import Prelude;
+
+bitvector : Nat -> sort 0;
+bitvector n = Vec n Bool;
+
+-- The type of buffers of a given length
+buffer : bitvector 64 -> sort 0;
+buffer len = BVVec 64 len (bitvector 8);
+
+data ioEvArgs : sort 0 where {
+  writeEv : bitvector 32 -> (len:bitvector 64) -> buffer len ->
+            ioEvArgs;
+  readEv : bitvector 32 -> bitvector 64 -> ioEvArgs;
+}
+
+ioEvRet : ioEvArgs -> sort 0;
+ioEvRet args =
+  ioEvArgs#rec
+    (\ (_:ioEvArgs) -> sort 0)
+    (\ (_:bitvector 32) (len:bitvector 64) (_:buffer len) -> bitvector 64)
+    (\ (_:bitvector 32) (len:bitvector 64) ->
+       Sigma (bitvector 64)
+             (\ (len_ret:bitvector 64) ->
+                is_bvule 64 len_ret len * buffer len_ret))
+  args;
+
+ioEv : EvType;
+ioEv = Build_EvType ioEvArgs ioEvRet;

heapster-saw/examples/io_proofs.v

@@ -0,0 +1,19 @@
+From Coq          Require Import Lists.List.
+From Coq          Require Import String.
+From Coq          Require Import Vectors.Vector.
+From CryptolToCoq Require Import SAWCoreScaffolding.
+From CryptolToCoq Require Import SAWCoreVectorsAsCoqVectors.
+From CryptolToCoq Require Import SAWCoreBitvectors.
+
+From CryptolToCoq Require Import SAWCorePrelude.
+From CryptolToCoq Require Import SpecMExtra.
+From EnTree       Require Import Automation.
+Import SAWCorePrelude.
+Import SpecMNotations.
+Local Open Scope entree_scope.
+
+Require Import Examples.io_gen.
+Import io.
+
+Print hello_world__bodies.
+Print __x1_write.

heapster-saw/examples/linked_list.sawcore

@@ -6,7 +6,7 @@ import Prelude;
 List_def : (a:sort 0) -> sort 0;
 List_def a = List a;
 
-mallocSpec : (sz:Vec 64 Bool) -> CompM (BVVec 64 sz #());
+mallocSpec : (sz:Vec 64 Bool) -> SpecM VoidEv emptyFunStack (BVVec 64 sz #());
 mallocSpec sz =
-  returnM (BVVec 64 sz #())
-          (genBVVec 64 sz #() (\ (i:Vec 64 Bool) (_:is_bvult 64 i sz) -> ()));
+  retS VoidEv emptyFunStack (BVVec 64 sz #())
+       (genBVVec 64 sz #() (\ (i:Vec 64 Bool) (_:is_bvult 64 i sz) -> ()));

heapster-saw/examples/linked_list_proofs.v

@@ -6,17 +6,158 @@ From CryptolToCoq Require Import SAWCoreVectorsAsCoqVectors.
 From CryptolToCoq Require Import SAWCoreBitvectors.
 
 From CryptolToCoq Require Import SAWCorePrelude.
-From CryptolToCoq Require Import CompMExtra.
+From CryptolToCoq Require Import SpecMExtra.
+From EnTree       Require Import Automation.
+Import SAWCorePrelude.
+Import SpecMNotations.
+Local Open Scope entree_scope.
 
 Require Import Examples.linked_list_gen.
 Import linked_list.
 
-Import SAWCorePrelude.
+
+(* QOL: nicer names for bitvector and list arguments *)
+#[local] Hint Extern 901 (IntroArg Any (bitvector _) _) =>
+  let e := fresh "x" in IntroArg_intro e : refines prepostcond. 
+#[local] Hint Extern 901 (IntroArg Any (list _) _) =>
+  let e := fresh "l" in IntroArg_intro e : refines prepostcond. 
+#[local] Hint Extern 901 (IntroArg Any (List_def _) _) =>
+  let e := fresh "l" in IntroArg_intro e : refines prepostcond. 
+
+#[local] Hint Extern 901 (IntroArg RetAny (bitvector _) _) =>
+  let e := fresh "r_x" in IntroArg_intro e : refines prepostcond. 
+#[local] Hint Extern 901 (IntroArg RetAny list _) =>
+  let e := fresh "r_l" in IntroArg_intro e : refines prepostcond. 
+#[local] Hint Extern 901 (IntroArg RetAny List_def _) =>
+  let e := fresh "r_l" in IntroArg_intro e : refines prepostcond.
+
+
+(* bitvector (in)equality automation *)
+
+Lemma simpl_llvm_bool_eq (b : bool) :
+  negb (bvEq 1 (if b then intToBv 1 (-1) else intToBv 1 0) (intToBv 1 0)) = b.
+Proof. destruct b; eauto. Qed.
+
+Definition simpl_llvm_bool_eq_IntroArg n (b1 b2 : bool) (goal : Prop) :
+  IntroArg n (b1 = b2) (fun _ => goal) ->
+  IntroArg n (negb (bvEq 1 (if b1 then intToBv 1 (-1) else intToBv 1 0) (intToBv 1 0)) = b2) (fun _ => goal).
+Proof. rewrite simpl_llvm_bool_eq; eauto. Defined.
+
+#[local] Hint Extern 101 (IntroArg _ (negb (bvEq 1 (if _ then intToBv 1 (-1) else intToBv 1 0) (intToBv 1 0)) = _) _) =>
+  simple eapply simpl_llvm_bool_eq_IntroArg : refines.
+
+
+(* List destruction automation *)
+
+Arguments FunsTo_Nil {a}.
+Arguments FunsTo_Cons {a tp}.
+
+Lemma spec_refines_either_unfoldList_nil_l (E1 E2 : EvType) Γ1 Γ2 R1 R2
+  (RPre : SpecPreRel E1 E2 Γ1 Γ2) (RPost : SpecPostRel E1 E2 Γ1 Γ2)
+  (RR : Rel R1 R2) A f g (P : SpecM E2 Γ2 R2) :
+  spec_refines RPre RPost RR (f tt) P ->
+  spec_refines RPre RPost RR (eithers _ (FunsTo_Cons f (FunsTo_Cons g FunsTo_Nil))
+                                        (unfoldList A nil)) P.
+Proof. eauto. Qed.
+
+Lemma spec_refines_either_unfoldList_cons_l (E1 E2 : EvType) Γ1 Γ2 R1 R2
+  (RPre : SpecPreRel E1 E2 Γ1 Γ2) (RPost : SpecPostRel E1 E2 Γ1 Γ2)
+  (RR : Rel R1 R2) A a l f g (P : SpecM E2 Γ2 R2) :
+  spec_refines RPre RPost RR (g (a, l)) P ->
+  spec_refines RPre RPost RR (eithers _ (FunsTo_Cons f (FunsTo_Cons g FunsTo_Nil))
+                                        (unfoldList A (a :: l))) P.
+Proof. eauto. Qed.
+
+Ltac eithers_unfoldList A l :=
+  let l' := eval cbn [ fst snd projT1 ] in l in
+  lazymatch l' with
+  | nil =>
+    simple apply (spec_refines_either_unfoldList_nil_l _ _ _ _ _ _ _ _ _ A)
+  | ?a :: ?l0 =>
+    simple apply (spec_refines_either_unfoldList_cons_l _ _ _ _ _ _ _ _ _ A a l0)
+  | _ => let a  := fresh "x" in
+         let l0 := fresh "l0" in
+         let eq := fresh "e_destruct" in
+         destruct l' as [| a l0 ] eqn:eq;
+         [ eithers_unfoldList A (@nil A) | eithers_unfoldList A (a :: l0) ];
+         simpl foldList; cbn [ list_rect ] in *;
+         cbn [ fst snd projT1 ];
+         revert eq; apply (IntroArg_fold Destruct)
+  end.
+
+Global Hint Extern 100 (spec_refines _ _ _ (eithers _ _ (unfoldList ?A ?l)) _) =>
+  eithers_unfoldList A l : refines.
+Global Hint Extern 100 (spec_refines _ _ _ _ (eithers _ _ (unfoldList ?A ?l))) =>
+  eithers_unfoldList A l : refines.
+
+Global Hint Extern 901 (RelGoal _) =>
+  progress (simpl foldList in *; cbn [ list_rect ] in *) : refines.
+
+Global Hint Extern 100 (Shelve (list_rect _ _ _ ?m)) =>
+  progress cbn [ list_rect ] in * : refines.
+Global Hint Extern 100 (Shelve (list_rect _ _ _ ?m)) =>
+  progress cbn [ list_rect ] in * : refines.
+
+Lemma IntroArg_eq_list_nil_nil n A goal :
+  goal -> IntroArg n (@nil A = nil) (fun _ => goal).
+Proof. do 2 intro; eauto. Qed.
+
+Lemma IntroArg_eq_list_cons_cons n A (a1 a2 : A) l1 l2 goal :
+  IntroArg n (a1 = a2) (fun _ => IntroArg n (l1 = l1) (fun _ => goal)) ->
+  IntroArg n (a1 :: l1 = a2 :: l2) (fun _ => goal).
+Proof. intros H eq; dependent destruction eq; apply H; eauto. Qed.
+
+Lemma IntroArg_eq_list_nil_cons n A (a : A) l goal :
+  IntroArg n (nil = a :: l) (fun _ => goal).
+Proof. intro eq; dependent destruction eq. Qed.
+
+Lemma IntroArg_eq_list_cons_nil n A (a : A) l goal :
+  IntroArg n (a :: l = nil) (fun _ => goal).
+Proof. intro eq; dependent destruction eq. Qed.
+
+Global Hint Extern 101 (nil = nil) =>
+  simple apply IntroArg_eq_list_nil_nil : refines.
+Global Hint Extern 101 (_ :: _ = _ :: _) =>
+  simple apply IntroArg_eq_list_cons_cons : refines.
+Global Hint Extern 101 (nil = _ :: _) =>
+  simple apply IntroArg_eq_list_nil_cons : refines.
+Global Hint Extern 101 (_ :: _ = nil) =>
+  simple apply IntroArg_eq_list_nil_cons : refines.
+
+Lemma is_elem_spec_ref x l :
+  spec_refines eqPreRel eqPostRel eq
+    (is_elem x l)
+    (total_spec (fun _ => True)
+                (fun '(x, l) r => (~ List.In x l /\ r = intToBv 64 0)
+                                  \/ (List.In x l /\ r = intToBv 64 1))
+                (x, l)).
+Proof.
+  unfold is_elem, is_elem__bodies.
+  prove_refinement.
+  - wellfounded_decreasing_nat.
+    exact (length l0).
+  - prepost_case 0 0.
+    + exact (x0 = x1 /\ l0 = l1).
+    + exact (r = r0).
+    + prepost_exclude_remaining.
+  - time "is_elem_spec_ref" prove_refinement_continue.
+    all: try ((left ; split; [eauto | easy]) ||
+              (right; split; [eauto | easy])); simpl.
+    1-2: apply bvEq_eq in e_if; eauto.
+    1-2: apply bvEq_neq in e_if.
+    1-2: destruct H as [[]|[]]; [ left | right ].
+    1-4: split; eauto.
+    1-2: intros []; eauto.
+Qed.
 
 
-Lemma no_errors_is_elem : refinesFun is_elem (fun _ _ => noErrorsSpec).
+(* =========== TODO: Update the below with the new automation =========== *)
+(*
+
+Lemma no_errors_is_elem x l :
+  spec_refines eqPreRel eqPostRel eq (is_elem x l) no_errors_spec.
 Proof.
-  unfold is_elem, is_elem__tuple_fun, noErrorsSpec.
+  unfold is_elem, no_errors_spec.
   time "no_errors_is_elem" prove_refinement.
 Qed.
 
@@ -256,3 +397,5 @@ Proof.
   unfold sorted_insert_no_malloc, sorted_insert_no_malloc__tuple_fun, sorted_insert_fun.
   time "sorted_insert_no_malloc_fun_ref" prove_refinement.
 Qed.
+
+*)

heapster-saw/examples/mbox.saw

@@ -67,13 +67,15 @@ heapster_define_perm env "boolean" " " "llvmptr 1" "exists x:bv 1.eq(llvmword(x)
 //   "\\ (len:Vec 64 Bool) (x y:BVVec 64 len (Vec 8 Bool)) -> \
 //     \ returnM (BVVec 64 len (Vec 8 Bool) * (BVVec 64 len (Vec 8 Bool) * #())) (y, (y, ()))";
 
-heapster_assume_fun env "llvm.objectsize.i64.p0i8" "().empty -o empty" "returnM #() ()";
+heapster_assume_fun env "llvm.objectsize.i64.p0i8" "().empty -o empty"
+                    "retS VoidEv emptyFunStack #() ()";
 
 heapster_assume_fun env "__memcpy_chk"
   "(len:bv 64). arg0:byte_array<W,len>, arg1:byte_array<W,len>, arg2:eq(llvmword (len)) -o \
               \ arg0:byte_array<W,len>, arg1:byte_array<W,len>"
   "\\ (len:Vec 64 Bool) (_ src : BVVec 64 len (Vec 8 Bool)) -> \
-    \ returnM (BVVec 64 len (Vec 8 Bool) * BVVec 64 len (Vec 8 Bool)) (src, src)";
+    \ retS VoidEv emptyFunStack \
+         \ (BVVec 64 len (Vec 8 Bool) * BVVec 64 len (Vec 8 Bool)) (src, src)";
 
 
 //------------------------------------------------------------------------------