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.

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

Prove Raft Correct #16

Merged
merged 42 commits into from Aug 6, 2015
Merged

Prove Raft Correct #16

merged 42 commits into from Aug 6, 2015

Conversation

wilcoxjay
Copy link
Member

Wooooo!

dwoos and others added 30 commits July 28, 2015 15:33
@dwoos
Add message ghost vars in net
769f3f4 
One proof is admitted; should be easy to fix :)
@wilcoxjay
fix build
848ff4f
@wilcoxjay
add raft ghost log refinement
14c93df
@wilcoxjay
fix E2E build.
dc78c34 
The new refinement added some low-cost hints that were messing up the
statement of the theorem by resolving to the wrong refinement layer. It
is now annotated so that it is stated about the base system, not any of
the refinements.
@dwoos
contiguous_findAtIndex
4c5d88f
@wilcoxjay
prove contiguous_findAtIndex
4de1a63
@dwoos
Add all_the_way lifting and lowering
4f7d527
@dwoos
prove ghost_log_correct
98f632c
@dwoos
Strengthen GhostLogCorrect
430a050
@dwoos
Add primed decomp to msg refinement
0accb14
@dwoos
state and prove ghost logs log properties
992d028
@dwoos
Use pre-state instead of post state for ghost log
6665c9f
@dwoos
Admit some invariants
401707f
@dwoos
Ghost log log matching proved
49cb6cc
@wilcoxjay
lifted sms
1a95854
@wilcoxjay
state CRC nw invariant
fc4fbbc
@dwoos
Correct definition of InLogInAllEntries
64bc70b
@dwoos
Prove ILIAE
11ee763
@dwoos
prove GLAE
04f7ede
@wilcoxjay
wip commit_invariant_append_entries
e6843f4
@dwoos
lift SMSNW'
e32551f
@wilcoxjay
kill first case of AE CRC host
e9c7f2b
@dwoos
t' -> currentTerm in pre-state
18238a9
@dwoos
correct statement of commit preservation thing
9e8ee1f
@wilcoxjay
finish CRC AE host case!
6f3c6dc
@wilcoxjay
establish nw invariant!
00fddd6
@wilcoxjay
preserve nw invariant in CRC hCR case!
d12d98c
@dwoos
Prove hAE preserves committed!
e85143f
@wilcoxjay
finish rest of CRC cases!
05fcf5f
@wilcoxjay
fix duplicate lifted_entries_sorted_nw!!
9c7d8e0
@dwoos
Copy link
Member

dwoos commented Aug 6, 2015

🌵 👶

dwoos added a commit that referenced this pull request Aug 6, 2015
@dwoos
Merge pull request #16 from uwplse/msg-ghost-vars
5541d7b 
Prove Raft Correct
@dwoos dwoos merged commit 5541d7b into master Aug 6, 2015
@domoritz
Copy link

domoritz commented Aug 7, 2015

✨

@wilcoxjay wilcoxjay deleted the msg-ghost-vars branch February 10, 2016 18:57
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.

None yet
3 participants
@wilcoxjay @dwoos @domoritz