feat: add sha512 memory aliasing simp_mem DSL based version.

leanprover · Oct 16, 2024 · 2122f81 · 2122f81
1 parent 168eec2
commit 2122f81
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 3 deletions.
diff --git a/Arm/Memory/SeparateAutomation.lean b/Arm/Memory/SeparateAutomation.lean
@@ -524,8 +524,8 @@ The kind of simplification that must be performed. If we are told
 that we must simplify a separation, a subset, or a read of a write,
 we perform this kind of simplification.
 -/
-syntax guidanceKindSeparate := &"sep" <|> &"⟂"
-syntax guidanceKindSubset := &"sub" <|> &"⊆"-- &"⊂"
+syntax guidanceKindSeparate := &"sep" <|> &"⟂" 
+syntax guidanceKindSubset := &"sub" <|> &"⊂" <|> &"⊆"-- &"⊂"
 syntax guidanceKindSubsetRead := &"r" -- &"⊂"
 syntax guidanceKind := guidanceKindSeparate <|> guidanceKindSubset (guidanceKindSubsetRead ("at" term)?)? 
 

diff --git a/Proofs/Experiments/SHA512MemoryAliasing.lean b/Proofs/Experiments/SHA512MemoryAliasing.lean
@@ -152,7 +152,7 @@ work for `16#64 + ktbl_addr`?
   have hSHA2_k512_length : SHA2.k_512.length = 80 := rfl
   conv =>
     lhs
-    simp_mem sub r at h_s1_ktbl with [] -- It should fail if it makes no progress. Also, make small examples that demonstrate such failures.
+    simp_mem ⊂ r at h_s1_ktbl with [] -- It should fail if it makes no progress. Also, make small examples that demonstrate such failures.
   rfl
 
 /--
-Original file line number
+Diff line change
@@ Expand Up / @@ -152,7 +152,7 @@ work for `16#64 + ktbl_addr`? @@
       have hSHA2_k512_length : SHA2.k_512.length = 80 := rfl
       conv =>
         lhs
-        simp_mem sub r at h_s1_ktbl with [] -- It should fail if it makes no progress. Also, make small examples that demonstrate such failures.
+        simp_mem ⊂ r at h_s1_ktbl with [] -- It should fail if it makes no progress. Also, make small examples that demonstrate such failures.
       rfl
     /--
@@ Expand Down @@