proposition: Lemma step_checker_correct : let rho := Form.interp_state_var (Atom.interp_form_hatom t_i t_func t_atom) (Atom.interp_form_hatom_bv t_i t_func t_atom) t_form in Form.check_form t_form -> Atom.check_atom t_atom -> Atom.wt t_i t_func t_atom -> forall s, S.valid rho s -> forall st : step, S.valid rho (step_checker s st).
proof: Proof. set (empty_bv := (fun (a:Atom.atom) s => BITVECTOR_LIST.zeros s)). intros rho H1 H2 H10 s Hs. destruct (Form.check_form_correct (Atom.interp_form_hatom t_i t_func t_atom) (Atom.interp_form_hatom_bv t_i t_func t_atom) _ H1) as [[Ht1 Ht2] Ht3]. destruct (Atom.check_atom_correct _ H2) as [Ha1 Ha2]. intros [pos res|pos cid c|pos cid lf|pos|pos|pos l|pos l|pos l i|pos cid |pos cid|pos cid i|pos l fl|pos l fl|pos l1 l2 fl|pos cl c|pos l|pos orig res l |pos orig res|pos res|pos res|pos orig1 orig2 res|pos orig res|pos orig res |pos orig1 orig2 res|pos orig1 orig2 res |pos orig1 orig2 res|pos orig1 orig2 res|pos orig1 orig2 res|pos orig1 orig2 res |pos cl |pos orig res |pos orig res |pos orig res | pos orig1 orig2 res | pos orig1 orig2 res |pos res|pos res |pos res |pos prem_id prem concl p|pos lemma plemma concl p]; simpl; try apply S.valid_set_clause; auto with smtcoq_core. - apply S.valid_set_resolve; auto with smtcoq_core. - apply S.valid_set_weaken; auto with smtcoq_core. - apply valid_check_flatten; auto with smtcoq_core; intros h1 h2 H. + rewrite (Syntactic.check_hatom_correct_bool _ _ _ Ha1 Ha2 _ _ H); auto with smtcoq_core. + rewrite (Syntactic.check_neg_hatom_correct_bool _ _ _ H10 Ha1 Ha2 _ _ H); auto with smtcoq_core. - apply valid_check_True; auto with smtcoq_core. - apply valid_check_False; auto with smtcoq_core. - apply valid_check_BuildDef; auto with smtcoq_core. - apply valid_check_BuildDef2; auto with smtcoq_core. - apply valid_check_BuildProj; auto with smtcoq_core. - apply valid_check_ImmBuildDef; auto with smtcoq_core. - apply valid_check_ImmBuildDef2; auto with smtcoq_core. - apply valid_check_ImmBuildProj; auto with smtcoq_core. - apply valid_check_trans; auto with smtcoq_core. - apply valid_check_congr; auto with smtcoq_core. - apply valid_check_congr_pred; auto with smtcoq_core. - apply valid_check_micromega; auto with smtcoq_core. - apply valid_check_diseq; auto with smtcoq_core. - apply valid_check_spl_arith; auto with smtcoq_core. - apply valid_check_distinct_elim; auto with smtcoq_core. - eapply valid_check_bbVar; eauto with smtcoq_core. - apply valid_check_bbConst; auto with smtcoq_core. - apply valid_check_bbOp; auto with smtcoq_core. - apply valid_check_bbNot; auto with smtcoq_core. - apply valid_check_bbNeg; auto with smtcoq_core. - apply valid_check_bbAdd; auto with smtcoq_core. - apply valid_check_bbConcat; auto with smtcoq_core. - apply valid_check_bbMult; auto with smtcoq_core. - apply valid_check_bbUlt; auto with smtcoq_core. - apply valid_check_bbSlt; auto with smtcoq_core. - apply valid_check_bbEq; auto with smtcoq_core. - apply valid_check_bbDiseq; auto with smtcoq_core. - apply valid_check_bbExtract; auto with smtcoq_core. - apply valid_check_bbZextend; auto with smtcoq_core. - apply valid_check_bbSextend; auto with smtcoq_core. - apply valid_check_bbShl; auto with smtcoq_core. - apply valid_check_bbShr; auto with smtcoq_core. - apply valid_check_roweq; auto with smtcoq_core. - apply valid_check_rowneq; auto with smtcoq_core. - apply valid_check_ext; auto with smtcoq_core. - apply valid_check_hole; auto with smtcoq_core. - apply valid_check_forall_inst with lemma; auto with smtcoq_core. Qed.
imports: Bool Int63 PArray Misc State SMT_terms Syntactic Arithmetic Operators Assumptions Cnf Euf Lia BVList Bva_checker Array_checker