Merge pull request #1219 from GaloisInc/saw-core-heapster-final-merge

Prelude and saw-core-coq changes from Heapster
GaloisInc · May 11, 2021 · 614c9df · 614c9df
2 parents 2d92f2a + aeeb588
commit 614c9df
Show file tree

Hide file tree

Showing 12 changed files with 1,792 additions and 400 deletions.
diff --git a/.gitignore b/.gitignore
@@ -28,3 +28,4 @@ intTests/test*/*.out
 intTests/test_crucible_jvm/Stat.class
 intTests/test_profiling/prof
 intTests/test_smtlib/*.smt2
+saw-core-coq/coq/.Makefile.coq.d
diff --git a/saw-core-coq/coq/generated/CryptolToCoq/SAWCorePrelude.v b/saw-core-coq/coq/generated/CryptolToCoq/SAWCorePrelude.v
diff --git a/saw-core-coq/coq/handwritten/CryptolToCoq/CompM.v b/saw-core-coq/coq/handwritten/CryptolToCoq/CompM.v
@@ -923,3 +923,10 @@ Lemma refinesM_assumingM_l {A} (P:Prop) (m1 m2 : CompM A) :
 Proof.
   apply refinesM_forallM_l.
 Qed.
+
+(* NOTE: the other direction does not hold *)
+Lemma assumingM_bindM {A B} (P:Prop) (m: CompM A) (Q: A -> CompM B) :
+  refinesM ((assumingM P m) >>= Q) (assumingM P (m >>= Q)).
+Proof.
+  apply forallM_bindM.
+Qed.
diff --git a/saw-core-coq/coq/handwritten/CryptolToCoq/CompMExtra.v b/saw-core-coq/coq/handwritten/CryptolToCoq/CompMExtra.v