Merge branch 'main' into address-normalization-simproc

.github/workflows/makefile.yml

@@ -42,3 +42,8 @@ jobs:
       if : ${{ runner.os == 'macOS' }}
       run: |
           make cosim NUM_TESTS=100
+
+    - name: Run LNSym Benchmarks (Ubuntu)
+      if : ${{ runner.os != 'macOS' }}
+      run: |
+          make benchmarks

Arm/Memory/SeparateAutomation.lean

@@ -89,9 +89,12 @@ The tactic shall be implemented as follows:
 
 section BvOmega
 
--- |TODO: Upstream BitVec.le_def unfolding to bv_omega.
-macro "bv_omega'" : tactic =>
-  `(tactic| (try simp only [bv_toNat, mem_legal'] at * <;> try rw [BitVec.le_def]) <;> bv_omega)
+/- We tag `mem_legal'` as `bv_toNat` here, since we want to actually lazily unfold this.
+Doing it here lets us remove it from `bv_toNat` simp-set as a change to `SeparateAutomation.lean`,
+without needing us to modify the core definitions file which incurs a recompile cost,
+making experimentation annoying.
+-/
+attribute [bv_toNat] mem_legal'
 
 end BvOmega
 
@@ -113,7 +116,7 @@ structure SimpMemConfig where
     ⊢ a + 5 < b
     ```
   -/
-  useOmegaToClose : Bool := true
+  useOmegaToClose : Bool := false
 
 /-- Context for the `SimpMemM` monad, containing the user configurable options. -/
 structure Context where
@@ -428,7 +431,7 @@ def omega : SimpMemM Unit := do
   -- https://leanprover.zulipchat.com/#narrow/stream/326056-ICERM22-after-party/topic/Regression.20tests/near/290131280
   -- @bollu: TODO: understand what precisely we are recovering from.
   withoutRecover do
-    evalTactic (← `(tactic| bv_omega'))
+    evalTactic (← `(tactic| bv_omega))
 
 section Hypotheses
 

Benchmarks.lean

@@ -0,0 +1,8 @@
+/-
+Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author(s): Alex Keizer
+-/
+import Benchmarks.SHA512_150
+import Benchmarks.SHA512_225
+import Benchmarks.SHA512_400

Benchmarks/Command.lean

@@ -0,0 +1,54 @@
+/-
+Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author(s): Alex Keizer
+-/
+import Lean
+
+open Lean Parser.Command Elab.Command
+
+elab "benchmark" id:ident declSig:optDeclSig val:declVal : command => do
+  let stx ← `(command| example $declSig:optDeclSig $val:declVal )
+
+  let n := 5
+  let mut runTimes := #[]
+  let mut totalRunTime := 0
+  -- geomean = exp(log((a₁ a₂ ... aₙ)^1/n)) = 
+  -- exp(1/n * (log a₁ + log a₂ + log aₙ)).
+  let mut totalRunTimeLog := 0
+  for _ in [0:n] do
+    let start ← IO.monoMsNow
+    elabCommand stx
+    let endTime ← IO.monoMsNow
+    let runTime := endTime - start
+    runTimes := runTimes.push runTime
+    totalRunTime := totalRunTime + runTime
+    totalRunTimeLog := totalRunTimeLog + Float.log runTime.toFloat
+
+  let avg := totalRunTime.toFloat / n.toFloat / 1000
+  let geomean := (Float.exp (totalRunTimeLog / n.toFloat)) / 1000.0
+  logInfo m!"\
+{id}:
+  average runtime over {n} runs:
+    {avg}s
+  geomean over {n} runs:
+    {geomean}s
+
+  indidividual runtimes:
+    {runTimes}
+"
+
+/-- The default `maxHeartbeats` setting.
+
+NOTE: even if the actual default value changes at some point in the future,
+this value should *NOT* be updated, to ensure the percentages we've reported
+in previous versions remain comparable. -/
+def defaultMaxHeartbeats : Nat := 200000
+
+open Elab.Tactic in
+elab "logHeartbeats" tac:tactic : tactic => do
+  let ((), heartbeats) ← withHeartbeats <|
+    evalTactic tac
+  let percent := heartbeats / (defaultMaxHeartbeats * 10)
+
+  logInfo m!"used {heartbeats / 1000} heartbeats ({percent}% of the default maximum)"

Benchmarks/SHA512.lean

@@ -0,0 +1,23 @@
+/-
+Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author(s): Alex Keizer
+-/
+import Proofs.SHA512.SHA512StepLemmas
+
+/-!
+### Symbolic Simulation for SHA512
+This file sets up the basic shape of a simulation of SHA512
+for a set number of instructions
+-/
+
+namespace Benchmarks
+
+def SHA512Bench (nSteps : Nat) : Prop :=
+  ∀ (s0 sf : ArmState)
+    (_h_s0_pc : read_pc s0 = 0x1264c4#64)
+    (_h_s0_err : read_err s0 = StateError.None)
+    (_h_s0_sp_aligned : CheckSPAlignment s0)
+    (_h_s0_program : s0.program = SHA512.program)
+    (_h_run : sf = run nSteps s0),
+    r StateField.ERR sf = StateError.None

Benchmarks/SHA512_150.lean

@@ -0,0 +1,15 @@
+/-
+Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author(s): Alex Keizer
+-/
+import Tactics.Sym
+import Benchmarks.Command
+import Benchmarks.SHA512
+
+open Benchmarks
+
+benchmark sha512_150_instructions : SHA512Bench 150 := fun s0 => by
+  intros
+  sym_n 150
+  done

Benchmarks/SHA512_225.lean

@@ -0,0 +1,15 @@
+/-
+Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author(s): Alex Keizer
+-/
+import Tactics.Sym
+import Benchmarks.Command
+import Benchmarks.SHA512
+
+open Benchmarks
+
+benchmark sha512_225_instructions : SHA512Bench 225 := fun s0 => by
+  intros
+  sym_n 225
+  done

Benchmarks/SHA512_400.lean

@@ -0,0 +1,15 @@
+/-
+Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author(s): Alex Keizer
+-/
+import Tactics.Sym
+import Benchmarks.SHA512
+import Benchmarks.Command
+
+open Benchmarks
+
+benchmark sha512_400_instructions : SHA512Bench 400 := fun s0 => by
+  intros
+  sym_n 400
+  done

Makefile

@@ -9,8 +9,10 @@ LAKE = lake
 NUM_TESTS?=3
 VERBOSE?=--verbose
 
-.PHONY: all 
+.PHONY: all
 all: specs correctness proofs tests cosim
+# Note that we don't include benchmarks in `all`,
+# to avoid slowing down CI too much
 
 .PHONY: specs
 	time -p $(LAKE) build Specs
@@ -35,8 +37,12 @@ awslc_elf:
 cosim:
 	time -p lake exe lnsym $(VERBOSE) --num-tests $(NUM_TESTS)
 
+.PHONY: benchmarks
+benchmarks:
+	$(LAKE) build Benchmarks
+
 .PHONY: clean clean_all
-clean: 
+clean:
 	$(LAKE) clean
 
 clean_all: clean

Proofs/Experiments/Memcpy/MemCpyVCG.lean

@@ -469,7 +469,7 @@ theorem Memcpy.extracted_2 (s0 si : ArmState)
   have h_upper_bound := hsep.hb.omega_def
   have h_upper_bound₂ := h_pre_1.hb.omega_def
   have h_upper_bound₃ := hsep.ha.omega_def
-  have h_width_lt : (0x10#64).toNat * (s0.x0 - (si.x0 - 0x1#64)).toNat < 2 ^ 64 := by simp_mem
+  have h_width_lt : (0x10#64).toNat * (s0.x0 - (si.x0 - 0x1#64)).toNat < 2 ^ 64 := by simp_mem (config := {useOmegaToClose := true})
   rw [Memory.read_bytes_write_bytes_eq_read_bytes_of_mem_separate']
   · rw [h_assert_6]
     skip_proof simp_mem

Proofs/Experiments/MemoryAliasing.lean

@@ -47,7 +47,7 @@ theorem subset_3 (l : mem_subset' a 16 b 16) : mem_subset' (a+6) 10 b 16 := by
 
 /-- Show that we can perform address arithmetic based on subset constraints. -/
 theorem subset_4 (l : mem_subset' a 16 b 16) : a = b := by
-  simp_mem
+  simp_mem (config := {useOmegaToClose := true})
 
 /-- Show that we can perform address arithmetic based on subset constraints.
 Only two configurations possible:
@@ -59,7 +59,7 @@ a0 a1 a2 ..
 b0 b1 b2 b3
 -/
 theorem subset_5 (l : mem_subset' a 3 b 4) : a ≤ b + 1 := by
-  simp_mem
+  simp_mem (config := {useOmegaToClose := true})
 
 end MemSubset
 
@@ -134,7 +134,8 @@ Check that we can close address relationship goals that require
 us to exploit memory separateness properties.
 -/
 theorem mem_separate_9  (h : mem_separate' a 100 b 100)
-  (hab : a < b) : a + 50 ≤ b := by simp_mem
+  (hab : a < b) : a + 50 ≤ b := by
+  simp_mem (config := {useOmegaToClose := true})
 
 end MemSeparate
 
@@ -199,7 +200,7 @@ theorem mem_automation_test_4
   simp only [memory_rules]
   simp_mem
   congr 1
-  bv_omega' -- TODO: address normalization.
+  bv_omega -- TODO: address normalization.
 
 /-- info: 'mem_automation_test_4' depends on axioms: [propext, Classical.choice, Quot.sound] -/
 #guard_msgs in #print axioms mem_automation_test_4
@@ -214,8 +215,9 @@ theorem overlapping_read_test_1 {out : BitVec (16 * 8)}
     read_mem_bytes 16 src_addr s = out := by
   simp only [memory_rules] at h ⊢
   simp_mem
+  simp only [Nat.reduceMul, Nat.sub_self, BitVec.extractLsBytes_eq_self, BitVec.cast_eq]
 
-/-- info: 'ReadOverlappingRead.overlapping_read_test_1' depends on axioms: [propext, Quot.sound] -/
+/-- info: 'ReadOverlappingRead.overlapping_read_test_1' depends on axioms: [propext, Classical.choice, Quot.sound] -/
 #guard_msgs in #print axioms overlapping_read_test_1
 
 /-- A read overlapping with another read. -/
@@ -227,7 +229,7 @@ theorem overlapping_read_test_2 {out : BitVec (16 * 8)}
   simp_mem
   · congr
     -- ⊢ (src_addr + 6).toNat - src_addr.toNat = 6
-    bv_omega'
+    bv_omega
 /--
 info: 'ReadOverlappingRead.overlapping_read_test_2' depends on axioms: [propext, Classical.choice, Quot.sound]
 -/
@@ -246,13 +248,13 @@ theorem overlapping_read_test_3
   simp_mem
   · congr
     -- ⊢ (src_addr + 6).toNat - src_addr.toNat = 6
-    bv_omega'
+    bv_omega
 /--
 info: 'ReadOverlappingRead.overlapping_read_test_3' depends on axioms: [propext, Classical.choice, Quot.sound]
 -/
 #guard_msgs in #print axioms overlapping_read_test_3
 
-/- TODO(@bollu): This test case hangs at `bv_omega'`. This is to be debugged.
+/- TODO(@bollu): This test case hangs at `bv_omega`. This is to be debugged.
 /-- A read in the goal state overlaps with a read in the
 right hand side of the hypotheis `h`.
 -/
@@ -266,7 +268,7 @@ theorem overlapping_read_test_4
   simp_mem
   · congr
     -- ⊢ (src_addr + 6).toNat - src_addr.toNat = 6
-    bv_omega' -- TODO: Lean gets stuck here?
+    bv_omega -- TODO: Lean gets stuck here?
 
 #guard_msgs in #print axioms overlapping_read_test_4
 -/
@@ -288,7 +290,7 @@ theorem test_2 {val : BitVec _}
     Memory.read_bytes 6 (src_addr + 10) (Memory.write_bytes 16 src_addr val mem) =
     val.extractLsBytes 10 6 := by
   simp_mem
-  have : ((src_addr + 10).toNat - src_addr.toNat) = 10 := by bv_omega'
+  have : ((src_addr + 10).toNat - src_addr.toNat) = 10 := by bv_omega
   rw [this]
 
 /--
@@ -427,14 +429,6 @@ error: unsolved goals
 info: [simp_mem.info] Searching for Hypotheses
 [simp_mem.info] Summary: Found 0 hypotheses
 [simp_mem.info] ⚙️ Matching on ⊢ False
-[simp_mem.info] Unknown memory expression ⊢ False. Trying reduction to omega (`config.useOmegaToClose = true`):
-  [simp_mem.info] Adding omega facts from hypotheses
-  [simp_mem.info] Executing `omega` to close False
-  [simp_mem.info] goal (Note: can be large)
-    [simp_mem.info] ⊢ False
-  [simp_mem.info] ❌️ `omega` failed with error:
-      omega could not prove the goal:
-      No usable constraints found. You may need to unfold definitions so `omega` can see linear arithmetic facts about `Nat` and `Int`, which may also involve multiplication, division, and modular remainder by constants.
 [simp_mem.info] Performing Rewrite At Main Goal
   [simp_mem.info] Simplifying goal.
 [simp_mem.info] ❌️ No progress made in this iteration. halting.
@@ -453,14 +447,6 @@ error: ❌️ simp_mem failed to make any progress.
 info: [simp_mem.info] Searching for Hypotheses
 [simp_mem.info] Summary: Found 0 hypotheses
 [simp_mem.info] ⚙️ Matching on ⊢ False
-[simp_mem.info] Unknown memory expression ⊢ False. Trying reduction to omega (`config.useOmegaToClose = true`):
-  [simp_mem.info] Adding omega facts from hypotheses
-  [simp_mem.info] Executing `omega` to close False
-  [simp_mem.info] goal (Note: can be large)
-    [simp_mem.info] ⊢ False
-  [simp_mem.info] ❌️ `omega` failed with error:
-      omega could not prove the goal:
-      No usable constraints found. You may need to unfold definitions so `omega` can see linear arithmetic facts about `Nat` and `Int`, which may also involve multiplication, division, and modular remainder by constants.
 [simp_mem.info] Performing Rewrite At Main Goal
   [simp_mem.info] Simplifying goal.
 [simp_mem.info] ❌️ No progress made in this iteration. halting.

Proofs/Experiments/SHA512MemoryAliasing.lean

@@ -97,7 +97,7 @@ theorem sha512_block_armv8_prelude_sym_ctx_access (s0 : ArmState)
   -- @shilpi: should this also be proven automatically? feels a little unreasonable to me.
   · congr
     -- ⊢ (ctx_addr s0 + 48#64).toNat - (ctx_addr s0).toNat = 48
-    bv_omega'
+    bv_omega
 
 /--
 info: 'SHA512MemoryAliasing.sha512_block_armv8_prelude_sym_ctx_access' depends on axioms: [propext,