feat: benchmark setup

Benchmarks.lean

@@ -0,0 +1,3 @@
+import Benchmarks.SHA512_150
+import Benchmarks.SHA512_225
+import Benchmarks.SHA512_400

Benchmarks/Command.lean

@@ -0,0 +1,47 @@
+/-
+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
+  for _ in List.range n do
+    let start ← IO.monoMsNow
+    elabCommand stx
+    let endTime ← IO.monoMsNow
+    let runTime := endTime - start
+    runTimes := runTimes.push runTime
+    totalRunTime := totalRunTime + runTime
+
+  let avg := totalRunTime.toFloat / n.toFloat / 1000
+  logInfo m!"\
+{id}:
+  average runtime over {n} runs:
+    {avg}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,16 @@
+/-
+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 := by
+  unfold SHA512Bench
+  intros
+  sym_n 150
+  done

Benchmarks/SHA512_225.lean

@@ -0,0 +1,16 @@
+/-
+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 := by
+  unfold SHA512Bench
+  intros
+  sym_n 225
+  done

Benchmarks/SHA512_400.lean

@@ -0,0 +1,16 @@
+/-
+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 := by
+  unfold SHA512Bench
+  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

Tactics/Sym.lean

@@ -319,7 +319,6 @@ def sym1 (c : SymContext) (whileTac : TSyntax `tactic) : TacticM SymContext :=
       let goal ← goal.clear hStep.fvarId
       replaceMainGoal [goal]
 
-      traceHeartbeats
       return c
 
 /- used in `sym_n` tactic to specify an initial state -/
@@ -423,15 +422,13 @@ Did you remember to generate step theorems with:
 
         let goal ← subst goal hEqId
         trace[Tactic.sym] "performed subsitutition in:\n{goal}"
-        traceHeartbeats
 
         replaceMainGoal [goal]
 
     -- Rudimentary aggregation: we feed all the axiomatic effect hypotheses
     -- added while symbolically evaluating to `simp`
     let msg := m!"aggregating (non-)effects"
     withTraceNode `Tactic.sym (fun _ => pure msg) <| withMainContext do
-      traceHeartbeats "pre"
       let goal? ← LNSymSimp (← getMainGoal) c.aggregateSimpCtx c.aggregateSimprocs
       replaceMainGoal goal?.toList
 

lakefile.lean

@@ -27,6 +27,9 @@ lean_lib «Tactics» where
 lean_lib «Doc» where
   -- add library configuration options here
 
+lean_lib «Benchmarks» where
+  -- add library configuration options here
+
 @[default_target]
 lean_exe «lnsym» where
   root := `Main