BLOCKED: refactor: reimplement initNextStep without evalTactic #219
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
|
I'm going a bit mad with this instantiateMVars nonsense. Compare a profile from #214 with a profile from the current PR --- both are running the SHA512_225 benchmark. You'll notice the former takes 8 seconds in total, of which 1.2 is spent on However, all of that is lost on the metavariable instantiation. This profile was made with a toolchain version that doesn't have a node for |
3 tasks
### 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]>
alexkeizer
changed the title
|
This is currently blocked, waiting on a diagnosis of leanprover/lean4#5610 |
### 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]>
alexkeizer
force-pushed
the
replace-init_next_step
branch
from
92c26e4
to
2f2093d
Compare
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Description:
Work in progress: this currently causes a slowdown, more investigation is needed.
Testing:
What tests have been run? Did
make allsucceed for your changes? Wasconformance 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.