### Description:

This PR simplifies the definition of `partInstall`. Its signature used
to be:
```
abbrev partInstall (hi lo : Nat) (val : BitVec (hi - lo + 1)) (x : BitVec n): BitVec n
```
and now it becomes:
```
abbrev partInstall (start len : Nat) (val : BitVec len) (x : BitVec n): BitVec n
```
This follows the same pattern in `extractLsb` vs `extractLsb'`. By doing
this, we are able to simplify several functions that depends on
`partInstall`.

### 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.

…nding `AxEffects` field (#207)

### Description:

Benchmarks suggest this could be marginally slower than before (the
SHA512_400 benchmark slowed down from 19.0 to 19.2 second, i.e., within
noise levels).

Still, it's a good change to make, because it will make effect
aggregation easier.

### 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: Shilpi Goel <[email protected]>

…` and `truncate_of_concat_is_lsb` (#221)

### Description:

This PR extends `truncate_of_concat_is_lsb_64` to arbitrary-width
bitvectors.

### Testing:

What tests have been run? Did `make all` succeed for your changes? Yes
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.

)

### Description:

Stacked on #207.

When an write to memory or a write to a register that is not SP is made,
we update the proof of stack alignment. When a write to SP is made, we
create a new mvar with the proof obligation that the new value is
aligned, and store that mvar in a new `sideConditions` field.

### 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: Shilpi Goel <[email protected]>

…ling support (#204)

### Description:

This PR gives more fine-grained control over benchmarrking:
- It adds an option to control how many runs we do
- We change the makefile to invoke Lean directly, instead of using Lake.
This is needed to ensure we don't get cached data
- We've moved the driving of the benchmarks/profiling to a shell script
(which is called from the makefile), and ensured benchmarking /
profiling data gets logged to files automatically.

### 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: Shilpi Goel <[email protected]>

### Description:

Stacked on:
- [x] #209 
- [x] #204 

### 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: Shilpi Goel <[email protected]>

…ep in `sym_n` (#213)

### Description:

Stacked on:
- [x] #204 
- [x] #207 
- [x] #209 
- [x] #211 

This PR implements "snorkeling" of the heartbeat budget.

This unfortunately does not buy us much, as aggregation for 500 steps
already seems to hit both the recursion limit and heartbeat budget, by
itself.

### 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: Shilpi Goel <[email protected]>

### Description:

Stacked on: #214 

Renames `section Monad` to `section MonadicGetters` or `section
MonadicGettersAndSetters`, depending on whether the particular section
has a setter in it.

### Testing:

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

Things were only renamed, nothing should've broken.

### License:

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

### Description:

Some work towards proving the functional correctness of GCM Gmult. 

Summary of changes:
1. Removed `h : esize > 0` from the `ShiftInfo` structure.
2. Added a `dsimproc` for `AdvSIMDExpandImm`. Cleaned up other
`dsimproc`s.
3. Defined `GCMGmultV8_alt`, an alternative GCM GMult definition that
does not traffic in lists.
4. Massaged the functional correctness goal a bit.

### 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.

…g inf. (#223)

### Description:

This PR replaces `bv_omega` with `bv_omega_bench`, which is used to
write benchmarking results into a user-specified filepath. This enables
us to extract out benchmarks to be upstreamed, as begun in
leanprover/lean4#5622.

We make the file path, whether the benchmark run is enabled or not, and
the minimum time necessary to be added to the benchmark all
user-configurable parameters.


### Testing:

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

### 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: Shilpi Goel <[email protected]>

…followed by (evalTactic omega) (#195)

### Description:

We're attempting to make `simp_mem` faster by controlling the evaluation
of both `simp` and `omega`. Toward this, as a first step, we invoke
`simp` ourselves.

### Testing:

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

Conformance succeeds. 

### License:

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

### Description:

Extracted from #179, stacked on #220.

We extract out memory-effects related code from AxEffects into a new
MemoryEffects structure. This PR is purely a non-functional change, but
will serve as the starting point of integrating simp_mem with sym_n.

The current simplification is effectively a no-op, since the proof state
is not massaged to the way `simp_mem` wants it to be. Subsequent PRs
will focus on massaging the goal state to be as `simp_mem` likes, and
then trying to symbolically simplify the memory expression we see.

### 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 @bollu<[email protected]>

---------

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

fixes #115

### Description:

This was a really interesting bugfix, and was my bug. The `simp_mem`
tactic tries to handle hypotheses of the form `mem.read addr1 n1 =
mem.read addr2 n2` by registering both sides as useful information that
it should exploit.

However, the part that flips the equality forgot to flip the equality :)

Debugging this was enormously painful, because for whatever reason, the
kernel spends an enormously long time checking the proof, and then gives
up with "deterministic timeout". Regardless, here's the patch that fixes
it:

```diff
@@ -314,7 +305,7 @@ we can have some kind of funny situation where both LHS and RHS are ReadBytes.
 For example, `mem1.read base1 n = mem2.read base2 n`.
 In such a scenario, we should record both reads.
 -/
-def ReadBytesEqProof.ofExpr? (eval : Expr) (etype : Expr) :  Array ReadBytesEqProof := Id.run do
+def ReadBytesEqProof.ofExpr? (eval : Expr) (etype : Expr) :  MetaM (Array ReadBytesEqProof) := do
   let mut out := #[]
   if let .some ⟨_ty, lhs, rhs⟩ := etype.eq? then do
     let lhs := lhs
@@ -323,7 +314,7 @@ def ReadBytesEqProof.ofExpr? (eval : Expr) (etype : Expr) :  Array ReadBytesEqPr
       out := out.push { val := rhs, read := read, h := eval }
 
     if let .some read := ReadBytesExpr.ofExpr? rhs then
-      out:= out.push { val := lhs, read := read, h := eval }
+      out:= out.push { val := lhs, read := read, h := ← mkEqSymm eval }
   return out
 
 inductive Hypothesis
@@ -358,8 +349,8 @@ def State.init (cfg : SimpMemConfig) : State :=
```necessary?

### Testing:

cosim succeeds. 


### 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: Shilpi Goel <[email protected]>

### Issues:

Closes #127 

### Testing

Cosim succeeds. I simplified the tests in CSE/ to reduce noise.

### 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: Shilpi Goel <[email protected]>

### Issues:

Closes #137

### Description:

We prove `mem_separate_of_mem_separate'`, showing that the old defn
aligns with the new defn for non-zero-width-inervals.

### Testing:

We do not change any executable defs, and cosim succeeds.

### 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: Shilpi Goel <[email protected]>

### Description:

Bumps the toolchain to the latest nightly. Mostly in the (unlikely) hope
that some of our `instantiateMVars` performance woes might disappear.

### 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.

…gram = ?program` (#236)

### Issues:

Resolves a [TODO in
SHA512Prelude](https://github.com/leanprover/LNSym/blob/2e4d59cbd6f76eb8d63ed41ccbda38b49dd9c7ae/Proofs/SHA512/SHA512Prelude.lean#L144)

### Description:

We add the capability for `sym_aggregate` to rewrite along hypotheses
about the program of an ArmState.

### 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.

…h the option of the same name. (#235)

### Description:

We rename `Tactic.sym.debug` to `Tactic.sym.info` to be consistent with
the `simp_mem.info` traceclass. Also, we rename `withVerboseTraceNode`
to `withInfoTraceNode` to explicitly refer to the new name, and ensure
it uses the right trace class (rather than the non-existent
`Tactic.sym.verbose`)

### 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: Shilpi Goel <[email protected]>

### Description:

Rudimentary implementation of statically determining the GPR/SFPs that
may be modified by the program.

### 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]>

### 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: Shilpi Goel <[email protected]>

#224)

### Description:

Changes the memory effect proof to be of type `<currentState>.mem =
<trace of memory writes>.mem`, instead of the quantified statement that
the result of reading from memory at any bytes and any address of either
state agrees.

* To keep aggregation working with the new statement, we had to add
`memory_rules` to the simpsets that are used by sym_n.
* This meant we had to enhance `memory_rules` to do, e.g.,
read-over-write reasoning, and
* We had to change the `s[base, n]` notation to desugar into
`s.mem.read_bytes ..`

### 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]>