Skip to content
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

Proof the po-max constraint for re-exec #25

Merged
merged 47 commits into from
Jan 15, 2025
Merged

Proof the po-max constraint for re-exec #25

merged 47 commits into from
Jan 15, 2025

Conversation

InnocentusLime
Copy link
Collaborator

@InnocentusLime InnocentusLime commented Jan 15, 2025 •
edited
Loading

Synopsis

  1. This PR proves the po-max constraint for re-execution
  2. In addition it closes admits in the lemmas in depends on (and some other admits)
  3. This PR also updates the way we handle set of determined and committed events

@InnocentusLime
Work on the sb trick lemma
6ede53a
@InnocentusLime
Prove immediate sb lemma
4d9e5b7
@InnocentusLime
Add helper lemmas for extra_sb
c1cb0ce
@InnocentusLime
Take out sb fact
0e8f0c1
@InnocentusLime
Close all admits in sb lemma
b98948f
@InnocentusLime
Alter the imm sb lemma to be about nin_sb
b93a5cc
@InnocentusLime
Apply the new lemma
6d71746
@InnocentusLime
Prove useful equality
a0483ce
@InnocentusLime
Take out a useful lemma
3b3ba99
@InnocentusLime
Cleanup
b488923
@InnocentusLime
Move sb lemmas out
98c66e8
@InnocentusLime
Shrink some proofs
f4c713b
@InnocentusLime
Another small speedup
426a978
@InnocentusLime
Close admits and shrink proofs
ca40a0c
@InnocentusLime
Progress re-exec sbimm lemma
23de37d
@InnocentusLime
dtrmt is now fixset
611d435
@InnocentusLime
Close on of sb admits
319ee21
@InnocentusLime
Add shortcut lemmas for mapped sets
44f76af
@InnocentusLime
Alter dtrmt definition
d387a41
@InnocentusLime
Simplify reexec
2b1c3cf
@InnocentusLime
Add useful lemma
b1f17ff
@InnocentusLime
Some proof drafts
33e2257
@InnocentusLime
Mapper lemmas
7557134
@InnocentusLime
More mapper lemmas
decbedb
@InnocentusLime
Global hint
a2a751e
@InnocentusLime
Port to new mapper
c853bdb
@InnocentusLime
Migrate to new mapper
85a7b85
@InnocentusLime
Repair lemma for threads
62d5e4b
@InnocentusLime
Restore most of acts lemma
376ba51
@InnocentusLime
Refine the proof
6c1cee1
@InnocentusLime InnocentusLime merged commit acc7570 into main Jan 15, 2025
16 checks passed
@InnocentusLime InnocentusLime deleted the dev-sb-lemma branch January 15, 2025 12:38
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
1 participant
@InnocentusLime