feat: benchmark setup (#183)

### Description:

Add a basic benchmark setup:
- `benchmark` command, which has a theorem-like syntax, but doesn't get
added to the environment, and runs the proof 5 times, reporting both the
individual and average runtime,
- similarly, a `logHeartbeats` tactic combinator, which measures the
heartbeats used by an arbitrary tactic.
- Add a benchmark folder, with files for SHA512 runs with: 150, 225, and
400 steps (which are the numbers I've been reporting so far)
- Adds a `make benchmark` Make-target, to build the aforementioned
files. Crucially, this target is *not* part of `make all`, for all our
sanity's sake (running 400 steps of SHA512 for 5 times takes a while)

### Testing:

What tests have been run? Did `make all` succeed for your changes? Was
conformance testing successful on an Aarch64 machine? yes

### License:

By submitting this pull request, I confirm that my contribution is
made under the terms of the Apache 2.0 license.

---------

Co-authored-by: Siddharth <[email protected]>
Co-authored-by: Shilpi Goel <[email protected]>

.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

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,50 @@
+/-
+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 [0: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
+  let geomean := (totalRunTime.toFloat.pow (1.0 / 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

README.md

@@ -1,5 +1,5 @@
 # LNSym: Native Code Symbolic Simulator in Lean
-[![Makefile CI](https://github.com/leanprover/LNSym/actions/workflows/makefile.yml/badge.svg)](https://github.com/leanprover/LNSym/actions/workflows/makefile.yml) 
+[![Makefile CI](https://github.com/leanprover/LNSym/actions/workflows/makefile.yml/badge.svg)](https://github.com/leanprover/LNSym/actions/workflows/makefile.yml)
 
 LNSym is a symbolic simulator for Armv8 machine-code programs.
 
@@ -41,6 +41,8 @@ native-code programs of interest.
 
 `awslc_elf`: perform ELF loading tests for AWS-LC.
 
+`benchmarks`: run benchmarks for the symbolic simulator.
+
 ### Makefile variables that can be passed in at the command line
 
 `VERBOSE`: Verbose mode; prints disassembly of the instructions being

Tactics/Sym.lean

@@ -439,15 +439,13 @@ elab "sym_n" whileTac?:(sym_while)? n:num s:(sym_at)? : tactic => do
 
         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
 

Tactics/SymContext.lean

@@ -242,12 +242,12 @@ def inferStatePrefixAndNumber : SymM Unit := do
       state_prefix := (state.get? 0).getD 's' |>.toString,
       currentStateNumber })
   else
-    SymM.logWarning "\
-      Expected state to be a single letter followed by a number, but found:
-        {state}
+    SymM.logWarning m!"\
+Expected state to be a single letter followed by a number, but found:
+  {state}
 
-      Falling back to the default numbering schema,
-      with `s1` as the first new intermediate state"
+Falling back to the default numbering scheme, \
+with `s1` as the first new intermediate state"
     modifyThe SymContext ({ · with
       state_prefix := "s",
       currentStateNumber := 1 })

lakefile.lean

@@ -32,6 +32,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