Skip to content

Commit a4fd99c

Browse files
hackedyhackedy
committed
wip
1 parent 112b7ee commit a4fd99c

File tree

2 files changed

+188
-0
lines changed

2 files changed

+188
-0
lines changed

‎systems/TreeAggregationDynamicLabeledCorrect.v

+74
Original file line numberDiff line numberDiff line change
@@ -109,6 +109,76 @@ Definition leaf_node (net : ordered_dynamic_network) (failed : list name) (n : n
109109
min_root_path_length failed n l ->
110110
l' <= l.
111111

112+
(* something like this *)
113+
Lemma node_level_one_has_root_level_zero :
114+
forall s n d r,
115+
root r ->
116+
event_step_star step_ordered_dynamic_failure step_ordered_dynamic_failure_init (hd s) ->
117+
lb_step_execution lb_step_ordered_dynamic_failure s ->
118+
In n (hd s).(evt_a).(snd).(odnwNodes) ->
119+
~ In n (hd s).(evt_a).(fst) ->
120+
~ In r (hd s).(evt_a).(fst) ->
121+
(hd s).(evt_a).(snd).(odnwState) n = Some d ->
122+
level d.(adjacent) d.(levels) = Some 1 ->
123+
always (now (fun e =>
124+
exists d',
125+
e.(evt_a).(snd).(odnwState) n = Some d' /\
126+
NMap.find r d.(levels) = Some 0)) s.
127+
Proof.
128+
Admitted.
129+
130+
Lemma node_level_one_preserved :
131+
forall s n d,
132+
event_step_star step_ordered_dynamic_failure step_ordered_dynamic_failure_init (hd s) ->
133+
lb_step_execution lb_step_ordered_dynamic_failure s ->
134+
In n (hd s).(evt_a).(snd).(odnwNodes) ->
135+
~ In n (hd s).(evt_a).(fst) ->
136+
(hd s).(evt_a).(snd).(odnwState) n = Some d ->
137+
level d.(adjacent) d.(levels) = Some 1 ->
138+
always (now (fun e =>
139+
exists d',
140+
e.(evt_a).(snd).(odnwState) n = Some d' /\
141+
level d.(adjacent) d.(levels) = Some 1)) s.
142+
Proof.
143+
intros.
144+
(* three options:
145+
when the root gets a new message it sends back "my level = 0"
146+
- incoming new from you to root !! means you don't have a level for root yet
147+
- incoming level (lvl = 0) from root !! means you don't have a level for root yet
148+
- you already saw a level message from root
149+
150+
there's a lemma showing if you have a New message from you to root, then he
151+
can't have sent anything *)
152+
Admitted.
153+
154+
Lemma root_neighbors_get_level_one :
155+
forall s n,
156+
event_step_star step_ordered_dynamic_failure step_ordered_dynamic_failure_init (hd s) ->
157+
lb_step_execution lb_step_ordered_dynamic_failure s ->
158+
In n (hd s).(evt_a).(snd).(odnwNodes) ->
159+
~ In n (hd s).(evt_a).(fst) ->
160+
min_root_path_length (hd s).(evt_a).(fst) n 1 ->
161+
continuously (now (fun e =>
162+
exists d,
163+
e.(evt_a).(snd).(odnwState) n = Some d /\
164+
level d.(adjacent) d.(levels) = Some 1)) s.
165+
Proof.
166+
Admitted.
167+
168+
Lemma nodes_get_correct_level :
169+
forall s n dist,
170+
event_step_star step_ordered_dynamic_failure step_ordered_dynamic_failure_init (hd s) ->
171+
lb_step_execution lb_step_ordered_dynamic_failure s ->
172+
In n (hd s).(evt_a).(snd).(odnwNodes) ->
173+
~ In n (hd s).(evt_a).(fst) ->
174+
min_root_path_length (hd s).(evt_a).(fst) n dist ->
175+
continuously (now (fun e =>
176+
exists d,
177+
e.(evt_a).(snd).(odnwState) n = Some d /\
178+
level d.(adjacent) d.(levels) = Some dist)) s.
179+
Proof.
180+
Admitted.
181+
112182
Lemma leaf_nodes_eventually_have_unit :
113183
forall s failed n d,
114184
event_step_star step_ordered_dynamic_failure step_ordered_dynamic_failure_init (hd s) ->
@@ -160,6 +230,10 @@ Lemma mass_always_conserved :
160230
lb_step_execution lb_step_ordered_dynamic_failure s ->
161231
always (now (mass_conserved_opt_event failed)) s.
162232
Proof.
233+
intros.
234+
subst.
235+
generalize s.
236+
find_copy_eapply_lem_hyp step_ordered_dynamic_failure_star_lb_step_execution; eauto.
163237
Admitted.
164238

165239
Definition no_fail_incoming_active_event

‎systems/TreeDynamicCorrect.v

+114
Original file line numberDiff line numberDiff line change
@@ -1021,6 +1021,83 @@ end; simpl in *.
10211021
exact: @ordered_dynamic_nodes_no_dup _ _ _ _ Tree_FailMsgParams _ _ _ H.
10221022
Qed.
10231023

1024+
Set Bullet Behavior "Strict Subproofs".
1025+
1026+
(* todo: put this in structtact *)
1027+
Lemma collate_ls_in_in :
1028+
forall (A B : Type) A_eq_dec s f to m x a b,
1029+
In x (f a b) ->
1030+
In x (@collate_ls A B A_eq_dec s f to m a b).
1031+
Proof.
1032+
intros.
1033+
prep_induction s.
1034+
induction s.
1035+
- auto.
1036+
- intros.
1037+
simpl.
1038+
apply IHs.
1039+
destruct (A_eq_dec a a0), (A_eq_dec to b); subst.
1040+
+ rewrite update2_eq; auto using in_or_app.
1041+
+ rewrite update2_diff2; auto using in_or_app.
1042+
+ rewrite update2_diff1; auto using in_or_app.
1043+
+ rewrite update2_diff1; auto using in_or_app.
1044+
Qed.
1045+
1046+
Lemma collate_ls_cases :
1047+
forall (A B : Type) A_eq_dec s f to m a b,
1048+
@collate_ls A B A_eq_dec s f to m a b = f a b \/
1049+
exists l,
1050+
(forall x, In x l -> x = m) /\
1051+
@collate_ls A B A_eq_dec s f to m a b = f a b ++ l.
1052+
Proof.
1053+
intros.
1054+
prep_induction s; induction s as [|h s].
1055+
- auto.
1056+
- intros.
1057+
simpl in *.
1058+
destruct (A_eq_dec to b), (A_eq_dec h a); subst.
1059+
+ admit.
1060+
+ rewrite collate_ls_neq_update2; auto.
1061+
+ admit.
1062+
+ admit.
1063+
Admitted.
1064+
1065+
Lemma collate_ls_in_neq_in_before :
1066+
forall (A B : Type) A_eq_dec s f to m x a b,
1067+
In x (@collate_ls A B A_eq_dec s f to m a b) ->
1068+
x <> m ->
1069+
In x (f a b).
1070+
Proof.
1071+
intros.
1072+
pose proof (collate_ls_cases A_eq_dec s f to m a b); break_or_hyp.
1073+
- now find_rewrite.
1074+
- break_exists; break_and.
1075+
find_rewrite.
1076+
find_apply_lem_hyp in_app_or; break_or_hyp => //.
1077+
find_apply_hyp_hyp.
1078+
congruence.
1079+
Qed.
1080+
1081+
Lemma collate_map2snd_in_neq_in_before :
1082+
forall (A B : Type) A_eq_dec from f m dsts a b x,
1083+
In x (@collate A B A_eq_dec from f (map2snd m dsts) a b) ->
1084+
x <> m ->
1085+
In x (f a b).
1086+
Proof.
1087+
intros.
1088+
prep_induction dsts.
1089+
induction dsts.
1090+
- auto.
1091+
- simpl.
1092+
Admitted.
1093+
1094+
(* todo put in StructTact *)
1095+
Ltac apply_lem_prop_hyp lem P :=
1096+
match goal with
1097+
| [ H : context [ P ] |- _ ] =>
1098+
apply lem in H
1099+
end.
1100+
10241101
Lemma Tree_in_level_adjacent_or_incoming_new :
10251102
forall net failed tr,
10261103
step_ordered_dynamic_failure_star step_ordered_dynamic_failure_init (failed, net) tr ->
@@ -1029,6 +1106,43 @@ Lemma Tree_in_level_adjacent_or_incoming_new :
10291106
forall d, net.(odnwState) n = Some d ->
10301107
NSet.In n' d.(adjacent) \/ In New (net.(odnwPackets) n' n).
10311108
Proof.
1109+
intros.
1110+
change failed with (fst (failed, net)) in H0.
1111+
change net with (snd (failed, net)) in H1, H2.
1112+
change net with (snd (failed, net)).
1113+
remember step_ordered_dynamic_failure_init as y in *.
1114+
move: Heqy.
1115+
induction H using refl_trans_1n_trace_n1_ind.
1116+
- intro H_init.
1117+
subst.
1118+
simpl in *.
1119+
by auto.
1120+
- intro H_init.
1121+
match goal with
1122+
| [ H : step_ordered_dynamic_failure _ _ _ |- _ ] => invcs H
1123+
end.
1124+
+ destruct (name_eq_dec h n).
1125+
* subst.
1126+
right.
1127+
admit.
1128+
* copy_eapply_prop_hyp NSet.In failed0; eauto.
1129+
find_copy_eapply_lem_hyp ordered_dynamic_state_not_initialized_not_failed; eauto.
1130+
break_or_hyp.
1131+
-- by auto.
1132+
-- right.
1133+
apply collate_ls_in_in.
1134+
apply collate_in_in.
1135+
assumption.
1136+
-- apply_lem_prop_hyp collate_ls_in_neq_in_before @collate_ls => //.
1137+
apply_lem_prop_hyp collate_map2snd_in_neq_in_before @collate => //.
1138+
-- now find_erewrite_lem update_diff.
1139+
+ find_apply_lem_hyp net_handlers_NetHandler.
1140+
net_handler_cases => //=;
1141+
admit. (* use net_handler_cases somewhere here *)
1142+
+ find_apply_lem_hyp input_handlers_IOHandler.
1143+
io_handler_cases => //=;
1144+
admit. (* use io_handler_cases somewhere here *)
1145+
+ admit.
10321146
Admitted.
10331147

10341148
Lemma Tree_in_before_all_level_fail :

0 commit comments

Comments
 (0)