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

consistently use bullets for goals in proofs #98

Merged
merged 1 commit into from
Oct 20, 2023
Merged

consistently use bullets for goals in proofs #98

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
14 changes: 5 additions & 9 deletions raft-proofs/AppendEntriesLeaderProof.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -18,9 +18,7 @@ Section AppendEntriesLeader.
Context {orig_base_params : BaseParams}.
Context {one_node_params : OneNodeParams orig_base_params}.
Context {raft_params : RaftParams orig_base_params}.

Context {rri : raft_refinement_interface}.

Context {aecfli : append_entries_came_from_leaders_interface}.
Context {ollpti : one_leaderLog_per_term_interface}.
Context {lltsi : leaderLogs_term_sanity_interface}.
Expand Down Expand Up @@ -84,7 +82,6 @@ Section AppendEntriesLeader.
- repeat find_higher_order_rewrite.
update_destruct_simplify.
+ eapply appendEntries_leader_predicate_TTLM_preserved; eauto using handleClientRequest_TTLM.
eauto.
+ eauto.
- find_apply_lem_hyp handleClientRequest_packets.
subst. simpl in *. intuition.
Expand Down Expand Up @@ -113,7 +110,6 @@ Section AppendEntriesLeader.
- repeat find_higher_order_rewrite.
update_destruct_simplify.
+ eapply appendEntries_leader_predicate_TTLM_preserved; eauto using handleTimeout_TTLM.
eauto.
+ eauto.
- do_in_map.
find_eapply_lem_hyp handleTimeout_packets; eauto.
Expand Down Expand Up @@ -141,7 +137,7 @@ Section AppendEntriesLeader.
- repeat find_higher_order_rewrite.
update_destruct_simplify.
+ eapply appendEntries_leader_predicate_TTLM_preserved.
2-9:eauto using handleAppendEntries_TTLM.
2-7:eauto using handleAppendEntries_TTLM.
eauto.
+ eauto.
- find_apply_lem_hyp handleAppendEntries_not_append_entries.
Expand Down Expand Up @@ -169,7 +165,7 @@ Section AppendEntriesLeader.
- repeat find_higher_order_rewrite.
update_destruct_simplify.
+ eapply appendEntries_leader_predicate_TTLM_preserved.
2-9: eauto using handleAppendEntriesReply_TTLM.
2-7: eauto using handleAppendEntriesReply_TTLM.
eauto.
+ eauto.
- find_apply_lem_hyp handleAppendEntriesReply_packets.
Expand Down Expand Up @@ -197,7 +193,7 @@ Section AppendEntriesLeader.
- repeat find_higher_order_rewrite.
update_destruct_simplify.
+ eapply appendEntries_leader_predicate_TTLM_preserved.
2-9:eauto using handleRequestVote_TTLM.
2-7:eauto using handleRequestVote_TTLM.
eauto.
+ eauto.
- find_apply_lem_hyp handleRequestVote_no_append_entries.
Expand Down Expand Up @@ -345,7 +341,7 @@ Section AppendEntriesLeader.
- repeat find_higher_order_rewrite.
update_destruct_simplify.
+ eapply appendEntries_leader_predicate_TTLM_preserved.
2-9: eauto using doLeader_TTLM.
2-7: eauto using doLeader_TTLM.
match goal with
| [ H : nwState ?net ?h = (?gd, ?d) |- _ ] =>
replace d with (snd (nwState net h)) in * by (rewrite H; auto)
Expand Down Expand Up @@ -386,7 +382,7 @@ Section AppendEntriesLeader.
- repeat find_higher_order_rewrite.
update_destruct_simplify.
+ eapply appendEntries_leader_predicate_TTLM_preserved.
2-9: eauto using doGenericServer_TTLM.
2-7: eauto using doGenericServer_TTLM.
match goal with
| [ H : nwState ?net ?h = (?gd, ?d) |- _ ] =>
replace d with (snd (nwState net h)) in * by (rewrite H; auto)
Expand Down
8 changes: 4 additions & 4 deletions raft-proofs/PrefixWithinTermProof.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -229,7 +229,7 @@ Section PrefixWithinTerm.
10: { eauto. }
5: { eauto. }
4: { eauto. }
all:eauto; try lia. repeat find_rewrite; auto.
all:eauto; try lia.
+ exfalso.
find_eapply_lem_hyp Prefix_maxIndex; eauto.
lia.
Expand All @@ -256,7 +256,7 @@ Section PrefixWithinTerm.
10: { eauto. }
5: { eauto. }
4: { eauto. }
all:eauto; try lia. repeat find_rewrite; auto.
all:eauto; try lia.
+ exfalso.
find_eapply_lem_hyp Prefix_maxIndex; eauto.
lia.
Expand Down Expand Up @@ -285,7 +285,7 @@ Section PrefixWithinTerm.
10: { eauto. }
5: { eauto. }
4: { eauto. }
all:eauto; try lia. repeat find_rewrite; auto.
all:eauto; try lia.
+ exfalso.
find_eapply_lem_hyp Prefix_maxIndex; eauto.
lia.
Expand All @@ -309,7 +309,7 @@ Section PrefixWithinTerm.
10: { eauto. }
5: { eauto. }
4: { eauto. }
all:eauto; try lia. repeat find_rewrite; auto.
all:eauto; try lia.
+ exfalso.
find_eapply_lem_hyp Prefix_maxIndex; eauto.
lia.
Expand Down
Loading