New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

feat: prove specification of Max program that manipulates memory via new VCG #136

Merged

shigoel merged 24 commits into main from mem-max-take-3-vcg-assertions

Sep 8, 2024

Collaborator

bollu commented Sep 3, 2024

Supercedes #128, and have broken down the patches into a patch sequence that we can peel commits from.

shigoel and others added 12 commits

August 26, 2024 00:11


          Add another proof method to obtain partial correctness, and use it to…

… prove Abs


          Redo AddLoop proof using partial_correctness_from_assertions

ad37fb1


          Merge branch 'main' into vcg_assertions

6a685ae


          Testing a strategy for termination proofs that can borrow from the sa…

7bac006

…me program's partial correctness proof


          chore: first commit, porting code over

d47b199


          feat: add projections from state to common registers

b9a2efb


          feat: AddWithCarry lemmas

873f2e8


          feat: ArmState.mem_w_eq_mem

83c06e4


          feat: Aligned_BitVecSub_64_4

2648d30


          chore: eqn lemmas for (cassert s0 si i)

0da4d40


          chore: add proofs that x > y iff (N = V) ∧ Z = 0

b20e6de


          chore: add MaxTandem example

4242cda

bollu mentioned this pull request

feat: prove specification of Max program that manipulates memory via new VCG #128

Closed

bollu added 2 commits

September 4, 2024 09:34


          Merge remote-tracking branch 'origin/main' into mem-max-take-3-vcg-as…

0c1da2e

…sertions


          chore: cleanup

aabff62

bollu marked this pull request as ready for review

September 4, 2024 15:03

bollu requested a review from shigoel as a code owner

September 4, 2024 15:03

pennyannn reviewed

View reviewed changes

Proofs/Experiments/Max/MaxTandem.lean Outdated Show resolved Hide resolved

pennyannn reviewed

View reviewed changes

Arm/Insts/Common.lean Show resolved Hide resolved

pennyannn reviewed

View reviewed changes

Arm/State.lean Show resolved Hide resolved

pennyannn reviewed

View reviewed changes

Proofs/Experiments/Max/MaxTandem.lean Show resolved Hide resolved

pennyannn reviewed

View reviewed changes

Proofs/Experiments/Max/MaxTandem.lean Show resolved Hide resolved

pennyannn reviewed

View reviewed changes

Proofs/Experiments/Max/MaxTandem.lean Show resolved Hide resolved

pennyannn reviewed

View reviewed changes

Proofs/Experiments/Max/MaxTandem.lean Show resolved Hide resolved

bollu mentioned this pull request

Move ArmState notation into a separate file #140

Closed

pennyannn reviewed

View reviewed changes

Proofs/Experiments/Max/MaxTandem.lean Show resolved Hide resolved

alexkeizer reviewed

View reviewed changes

Arm/State.lean Outdated Show resolved Hide resolved

Arm/State.lean Outdated Show resolved Hide resolved

Arm/State.lean Show resolved Hide resolved

bollu and others added 3 commits

September 4, 2024 15:43


          Update Arm/State.lean

45203d3

Co-authored-by: Alex Keizer <[email protected]>


          Update Arm/State.lean

8d88628

Co-authored-by: Alex Keizer <[email protected]>


          chore: cleanups suggested

5dafafc

bollu and others added 2 commits

September 4, 2024 15:46


          chore: check that we have all licenses

82ef7d6


          Merge branch 'main' into mem-max-take-3-vcg-assertions

f2e0000

shigoel reviewed

View reviewed changes

Arm/Insts/Common.lean Show resolved Hide resolved

shigoel reviewed

View reviewed changes

Arm/Insts/Common.lean Show resolved Hide resolved

shigoel reviewed

View reviewed changes

Proofs/Experiments/Max/MaxTandem.lean Outdated Show resolved Hide resolved


          Merge branch 'main' into mem-max-take-3-vcg-assertions

6898cae

Collaborator

shigoel commented Sep 5, 2024

Looks good in general, and I'd be interested to see whether you can reuse the symbolic simulation done during the partial correctness proof to also prove termination. See Correctness.by_the_method and the AddLoopTandem proof.

Collaborator Author

bollu commented Sep 5, 2024 •

edited

Loading

and I'd be interested to see whether you can reuse the symbolic simulation done during the partial correctness

I too would be interested, but I would prefer to do this after I prove memcpy partially correct :) That feels slightly higher up on the priority queue for me, since it's a target program that we promised to verify!

Happy to discuss and change plans.

shigoel and others added 3 commits

September 6, 2024 12:18


          Merge branch 'main' into mem-max-take-3-vcg-assertions

c28c73a


          chore: move to BitVec

7b789b8


          chore: add TODO to upstream.

291b802

Collaborator Author

bollu commented Sep 6, 2024

@shigoel done, I've fixed up the comments that I felt were actionable :)


          Merge branch 'main' into mem-max-take-3-vcg-assertions

619073b

shigoel approved these changes

View reviewed changes

shigoel merged commit 74aba78 into main

4 checks passed

shigoel deleted the mem-max-take-3-vcg-assertions branch

September 8, 2024 20:04

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet