proposition: Lemma prove_no_fault: forall program h s n run_steps, StepStar.step_star (init program) h s -> (forall n, ~List.In n nids -> program n <> fault) -> (forall sched_length, check_all_schedules nids (run_steps + sched_length) nil nil (init program) (check_no_fault nids) = true) -> AbsExec.prog (s n) <> fault /\ (forall l, List.In l h -> l <> fault_label n).
proof: Proof. Proof using max_nid_eq. intros program h s n run_steps Hss Hnot_nit_no_fault Hcheck_scheds. generalize (step_star_not_in_nids _ _ _ n Hss); intro Hnot_nids_eq. apply step_star_fun_complete in Hss. destruct Hss as [sched Hss]. eapply check_all_schedules_correct with (sched1:=nil) (check:=check_no_fault nids) (max_steps:= run_steps + List.length sched) in Hss. * unfold check_no_fault in Hss. apply Bool.andb_true_iff in Hss. destruct Hss as [Hno_fault_label Hnot_fault]. simpl in *. rewrite List.forallb_forall in *. specialize (Hnot_nit_no_fault n). specialize (Hnot_fault n). nid_cases n; (split; [ intro HH; try solve [ rewrite HH in Hnot_fault; simpl in Hnot_fault; rewrite ?Bool.andb_false_r in Hnot_fault; discriminate ] | intros l Hin2; specialize (Hno_fault_label l Hin2); destruct l; try discriminate ]). clear max_nid_eq. destruct (List.in_dec NId_eq_dec n nids) as [Hin | Hnin]. - specialize (Hnot_fault Hin). rewrite HH in Hnot_fault. simpl in Hnot_fault. rewrite ?Bool.andb_false_r in Hnot_fault. discriminate. - rewrite <-Hnot_nids_eq in HH; simpl in *; auto. intuition (subst; auto). * eapply valid_schedule_step_star_fun; eauto. * lia. * eapply Hcheck_scheds. Qed.
imports: Coq(FunctionalExtensionality List Arith Lia) Chapar(Predefs KVStore)