Results for fold 1 Results for lemma freg_val: : forall ms sp rs r r', agree ms sp rs -> freg_of r = OK r' -> Val.lessdef (ms r) (rs#r') FAILURE! Tactics applied: 10000 Original Proof: [intros. rewrite <- (freg_of_eq _ _ H0). eapply preg_val; eauto.] Proof search time: 0 min, 50 sec Number of successful tactic applications: 1113 Number of failed tactic applications: 8888 Results for fold 2 Results for lemma ireg_val: : forall ms sp rs r r', agree ms sp rs -> ireg_of r = OK r' -> Val.lessdef (ms r) rs#r' FAILURE! Tactics applied: 10000 Original Proof: [intros. rewrite <- (ireg_of_eq _ _ H0). eapply preg_val; eauto.] Proof search time: 0 min, 59 sec Number of successful tactic applications: 1333 Number of failed tactic applications: 8668 Results for fold 3 Results for lemma label_pos_code_tail: : forall lbl c pos c', find_label lbl c = Some c' -> exists pos', label_pos lbl pos c = Some pos' /\ code_tail (pos' - pos) c c' /\ pos < pos' <= pos + list_length_z c FAILURE! Tactics applied: 10000 Original Proof: [induction c. simpl; intros. discriminate. simpl; intros until c'. case (is_label lbl a). intro EQ; injection EQ; intro; subst c'. exists (pos + 1). split. auto. split. replace (pos + 1 - pos) with (0 + 1) by omega. constructor. constructor. rewrite list_length_z_cons. generalize (list_length_z_pos c). omega. intros. generalize (IHc (pos + 1) c' H). intros [pos' [A [B C]]]. exists pos'. split. auto. split. replace (pos' - pos) with ((pos' - (pos + 1)) + 1) by omega. constructor. auto. rewrite list_length_z_cons. omega.] Proof search time: 0 min, 40 sec Number of successful tactic applications: 1548 Number of failed tactic applications: 8453 Results for fold 4 Results for lemma undef_regs_other: : forall r rl rs, (forall r', In r' rl -> r <> r') -> undef_regs rl rs r = rs r FAILURE! Tactics applied: 10000 Original Proof: [induction rl; simpl; intros. auto. rewrite IHrl by auto. rewrite Pregmap.gso; auto.] Proof search time: 0 min, 35 sec Number of successful tactic applications: 1787 Number of failed tactic applications: 8214 Results for fold 5 Results for lemma preg_val: : forall ms sp rs r, agree ms sp rs -> Val.lessdef (ms r) rs#(preg_of r) SUCCESS! Proof Found in EFSM: induction 1; simpl ; traceEq. Tactics applied: 1064 Original Proof: [intros. destruct H. auto.] Shorter Proof Found? no This is a novel proof proof search time: 0 min, 10 sec Number of successful tactic applications: 146 Number of failed tactic applications: 918 Results for fold 6 Results for lemma preg_vals: : forall ms sp rs, agree ms sp rs -> forall l, Val.lessdef_list (map ms l) (map rs (map preg_of l)) FAILURE! Tactics applied: 10000 Original Proof: [induction l; simpl. constructor. constructor. eapply preg_val; eauto. auto.] Proof search time: 0 min, 24 sec Number of successful tactic applications: 774 Number of failed tactic applications: 9227 Results for fold 7 Results for lemma lessdef_parent_sp: : forall s v, match_stack s -> Val.lessdef (parent_sp s) v -> v = parent_sp s FAILURE! Tactics applied: 10000 Original Proof: [intros. inv H0. auto. exploit parent_sp_def; eauto. tauto.] Proof search time: 0 min, 34 sec Number of successful tactic applications: 1694 Number of failed tactic applications: 8307 Results for fold 8 Results for lemma annot_arguments_match: : forall ms sp rs m m', agree ms sp rs -> Mem.extends m m' -> forall pl vl, Mach.annot_arguments ms m sp pl vl -> exists vl', Asm.annot_arguments rs m' (map transl_annot_param pl) vl' /\ Val.lessdef_list vl vl' FAILURE! Tactics applied: 10000 Original Proof: [induction 3; intros. exists (@nil val); split. constructor. constructor. exploit annot_arg_match; eauto. intros [v1' [A B]]. destruct IHlist_forall2 as [vl' [C D]]. exists (v1' :: vl'); split; constructor; auto.] Proof search time: 0 min, 32 sec Number of successful tactic applications: 1322 Number of failed tactic applications: 8679 Results for fold 9 Results for lemma code_tail_next_int: : forall fn ofs i c, list_length_z fn <= Int.max_unsigned -> code_tail (Int.unsigned ofs) fn (i :: c) -> code_tail (Int.unsigned (Int.add ofs Int.one)) fn c FAILURE! Tactics applied: 10000 Original Proof: [intros. rewrite Int.add_unsigned. change (Int.unsigned Int.one) with 1. rewrite Int.unsigned_repr. apply code_tail_next with i; auto. generalize (code_tail_bounds_2 _ _ _ _ H0). omega.] Proof search time: 0 min, 30 sec Number of successful tactic applications: 1349 Number of failed tactic applications: 8652 Results for fold 10 Results for lemma return_address_exists: : forall f sg ros c, is_tail (Mcall sg ros :: c) f.(Mach.fn_code) -> exists ra, return_address_offset f c ra FAILURE! Tactics applied: 10000 Original Proof: [intros. destruct (transf_function f) as [tf|] eqn:TF. + exploit transf_function_inv; eauto. intros (tc1 & ep1 & TR1 & TL1). exploit transl_code_tail; eauto. intros (tc2 & ep2 & TR2 & TL2). Opaque transl_instr. monadInv TR2. assert (TL3: is_tail x (fn_code tf)). { apply is_tail_trans with tc1; auto. apply is_tail_trans with tc2; auto. eapply transl_instr_tail; eauto. } exploit is_tail_code_tail. eexact TL3. intros [ofs CT]. exists (Int.repr ofs). red; intros. rewrite Int.unsigned_repr. congruence. exploit code_tail_bounds_1; eauto. apply transf_function_len in TF. omega. + exists Int.zero; red; intros. congruence.] Proof search time: 0 min, 49 sec Number of successful tactic applications: 1222 Number of failed tactic applications: 8779 Results for fold 11 Results for lemma agree_set_mreg: : forall ms sp rs r v rs', agree ms sp rs -> Val.lessdef v (rs'#(preg_of r)) -> (forall r', data_preg r' = true -> r' <> preg_of r -> rs'#r' = rs#r') -> agree (Regmap.set r v ms) sp rs' FAILURE! Tactics applied: 10000 Original Proof: [intros. destruct H. split; auto. rewrite H1; auto. apply sym_not_equal. apply preg_of_not_SP. intros. unfold Regmap.set. destruct (RegEq.eq r0 r). congruence. rewrite H1. auto. apply preg_of_data. red; intros; elim n. eapply preg_of_injective; eauto.] Proof search time: 0 min, 50 sec Number of successful tactic applications: 1767 Number of failed tactic applications: 8234 Results for fold 12 Results for lemma is_tail_code_tail: : forall c1 c2, is_tail c1 c2 -> exists ofs, code_tail ofs c2 c1 FAILURE! Tactics applied: 10000 Original Proof: [induction 1. exists 0; constructor. destruct IHis_tail as [ofs CT]. exists (ofs + 1); constructor; auto.] Proof search time: 0 min, 25 sec Number of successful tactic applications: 1257 Number of failed tactic applications: 8744 Results for fold 13 Results for lemma set_pregs_other_2: : forall r rl vl rs, preg_notin r rl -> set_regs (map preg_of rl) vl rs r = rs r FAILURE! Tactics applied: 10000 Original Proof: [induction rl; simpl; intros. auto. destruct vl; auto. assert (r <> preg_of a) by (destruct rl; tauto). assert (preg_notin r rl) by (destruct rl; simpl; tauto). rewrite IHrl by auto. apply Pregmap.gso; auto.] Proof search time: 0 min, 32 sec Number of successful tactic applications: 1662 Number of failed tactic applications: 8339 Results for fold 14 Results for lemma exec_straight_steps_2: : forall c rs m c' rs' m', exec_straight c rs m c' rs' m' -> list_length_z (fn_code fn) <= Int.max_unsigned -> forall b ofs, rs#PC = Vptr b ofs -> Genv.find_funct_ptr ge b = Some (Internal fn) -> code_tail (Int.unsigned ofs) (fn_code fn) c -> exists ofs', rs'#PC = Vptr b ofs' /\ code_tail (Int.unsigned ofs') (fn_code fn) c' FAILURE! Tactics applied: 10000 Original Proof: [induction 1; intros. exists (Int.add ofs Int.one). split. rewrite H0. rewrite H2. auto. apply code_tail_next_int with i1; auto. apply IHexec_straight with (Int.add ofs Int.one). auto. rewrite H0. rewrite H3. reflexivity. auto. apply code_tail_next_int with i; auto.] Proof search time: 0 min, 55 sec Number of successful tactic applications: 1988 Number of failed tactic applications: 8013 Results for fold 15 Results for lemma lessdef_parent_ra: : forall s v, match_stack s -> Val.lessdef (parent_ra s) v -> v = parent_ra s FAILURE! Tactics applied: 10000 Original Proof: [intros. inv H0. auto. exploit parent_ra_def; eauto. tauto.] Proof search time: 1 min, 34 sec Number of successful tactic applications: 1746 Number of failed tactic applications: 8255 Results for fold 16 Results for lemma preg_of_injective: : forall r1 r2, preg_of r1 = preg_of r2 -> r1 = r2 FAILURE! Tactics applied: 10000 Original Proof: [destruct r1; destruct r2; simpl; intros; reflexivity || discriminate.] Proof search time: 0 min, 25 sec Number of successful tactic applications: 691 Number of failed tactic applications: 9310 Results for fold 17 Results for lemma undef_regs_other_2: : forall r rl rs, preg_notin r rl -> undef_regs (map preg_of rl) rs r = rs r FAILURE! Tactics applied: 10000 Original Proof: [intros. apply undef_regs_other. intros. exploit list_in_map_inv; eauto. intros [mr [A B]]. subst. rewrite preg_notin_charact in H. auto.] Proof search time: 0 min, 38 sec Number of successful tactic applications: 1666 Number of failed tactic applications: 8335 Results for fold 18 Results for lemma parent_sp_def: : forall s, match_stack s -> parent_sp s <> Vundef SUCCESS! Proof Found in EFSM: induction 1; simpl ; unfold Vzero; congruence. Tactics applied: 1574 Original Proof: [induction 1; simpl. unfold Vzero; congruence. auto.] Shorter Proof Found? yes This is a novel proof proof search time: 0 min, 17 sec Number of successful tactic applications: 305 Number of failed tactic applications: 1269 Results for fold 19 Results for lemma exec_straight_steps_1: : forall c rs m c' rs' m', exec_straight c rs m c' rs' m' -> list_length_z (fn_code fn) <= Int.max_unsigned -> forall b ofs, rs#PC = Vptr b ofs -> Genv.find_funct_ptr ge b = Some (Internal fn) -> code_tail (Int.unsigned ofs) (fn_code fn) c -> plus step ge (State rs m) E0 (State rs' m') FAILURE! Tactics applied: 10000 Original Proof: [induction 1; intros. apply plus_one. econstructor; eauto. eapply find_instr_tail. eauto. eapply plus_left'. econstructor; eauto. eapply find_instr_tail. eauto. apply IHexec_straight with b (Int.add ofs Int.one). auto. rewrite H0. rewrite H3. reflexivity. auto. apply code_tail_next_int with i; auto. traceEq.] Proof search time: 0 min, 49 sec Number of successful tactic applications: 1539 Number of failed tactic applications: 8462 Results for fold 20 Results for lemma ireg_of_eq: : forall r r', ireg_of r = OK r' -> preg_of r = IR r' FAILURE! Tactics applied: 10000 Original Proof: [unfold ireg_of; intros. destruct (preg_of r); inv H; auto.] Proof search time: 0 min, 32 sec Number of successful tactic applications: 876 Number of failed tactic applications: 9125 Results for fold 21 Results for lemma find_instr_in: : forall c pos i, find_instr pos c = Some i -> In i c FAILURE! Tactics applied: 10000 Original Proof: [induction c; simpl. intros; discriminate. intros until i. case (zeq pos 0); intros. left; congruence. right; eauto.] Proof search time: 0 min, 29 sec Number of successful tactic applications: 1159 Number of failed tactic applications: 8842 Results for fold 22 Results for lemma tail_nolabel_cons: : forall i c k, nolabel i -> tail_nolabel k c -> tail_nolabel k (i :: c) FAILURE! Tactics applied: 10000 Original Proof: [intros. destruct H0. split. constructor; auto. intros. simpl. rewrite <- H1. destruct i; reflexivity || contradiction.] Proof search time: 0 min, 28 sec Number of successful tactic applications: 1560 Number of failed tactic applications: 8441 Results for fold 23 Results for lemma nextinstr_pc: : forall rs, (nextinstr rs)#PC = Val.add rs#PC Vone SUCCESS! Proof Found in EFSM: tauto. Tactics applied: 26 Original Proof: [intros. apply Pregmap.gss.] Shorter Proof Found? yes Single step proof reused proof search time: 0 min, 9 sec Number of successful tactic applications: 1 Number of failed tactic applications: 25 Results for fold 24 Results for lemma data_diff: : forall r r', data_preg r = true -> data_preg r' = false -> r <> r' SUCCESS! Proof Found in EFSM: induction 3; congruence. Tactics applied: 288 Original Proof: [congruence.] Shorter Proof Found? no This is a novel proof proof search time: 0 min, 6 sec Number of successful tactic applications: 47 Number of failed tactic applications: 241 Results for fold 25 Results for lemma agree_set_undef_mreg: : forall ms sp rs r v rl rs', agree ms sp rs -> Val.lessdef v (rs'#(preg_of r)) -> (forall r', data_preg r' = true -> r' <> preg_of r -> preg_notin r' rl -> rs'#r' = rs#r') -> agree (Regmap.set r v (Mach.undef_regs rl ms)) sp rs' FAILURE! Tactics applied: 10000 Original Proof: [intros. apply agree_set_mreg with (rs'#(preg_of r) <- (rs#(preg_of r))); auto. apply agree_undef_regs with rs; auto. intros. unfold Pregmap.set. destruct (PregEq.eq r' (preg_of r)). congruence. auto. intros. rewrite Pregmap.gso; auto.] Proof search time: 1 min, 8 sec Number of successful tactic applications: 1954 Number of failed tactic applications: 8047 Results for fold 26 Results for lemma parent_ra_def: : forall s, match_stack s -> parent_ra s <> Vundef FAILURE! Tactics applied: 10000 Original Proof: [induction 1; simpl. unfold Vzero; congruence. inv H0. congruence.] Proof search time: 0 min, 33 sec Number of successful tactic applications: 2047 Number of failed tactic applications: 7954 Results for fold 27 Results for lemma transl_code'_transl_code: : forall f il ep, transl_code' f il ep = transl_code f il ep FAILURE! Tactics applied: 10000 Original Proof: [intros. unfold transl_code'. rewrite transl_code_rec_transl_code. destruct (transl_code f il ep); auto.] Proof search time: 0 min, 30 sec Number of successful tactic applications: 2776 Number of failed tactic applications: 7225 Results for fold 28 Results for lemma preg_of_data: : forall r, data_preg (preg_of r) = true SUCCESS! Proof Found in EFSM: unfold preg_of; destruct r; auto. Tactics applied: 674 Original Proof: [intros. destruct r; reflexivity.] Shorter Proof Found? no This is a novel proof proof search time: 0 min, 10 sec Number of successful tactic applications: 87 Number of failed tactic applications: 587 Results for fold 29 Results for lemma return_address_offset_correct: : forall ge b ofs fb f c tf tc ofs', transl_code_at_pc ge (Vptr b ofs) fb f c false tf tc -> return_address_offset f c ofs' -> ofs' = ofs FAILURE! Tactics applied: 10000 Original Proof: [intros. inv H. red in H0. exploit code_tail_unique. eexact H12. eapply H0; eauto. intro. rewrite <- (Int.repr_unsigned ofs). rewrite <- (Int.repr_unsigned ofs'). congruence.] Proof search time: 0 min, 39 sec Number of successful tactic applications: 1632 Number of failed tactic applications: 8369 Results for fold 30 Results for lemma find_instr_tail: : forall c1 i c2 pos, code_tail pos c1 (i :: c2) -> find_instr pos c1 = Some i FAILURE! Tactics applied: 10000 Original Proof: [induction c1; simpl; intros. inv H. destruct (zeq pos 0). subst pos. inv H. auto. generalize (code_tail_pos _ _ _ H4). intro. omegaContradiction. inv H. congruence. replace (pos0 + 1 - 1) with pos0 by omega. eauto.] Proof search time: 3 min, 15 sec Number of successful tactic applications: 1601 Number of failed tactic applications: 8400 Results for fold 31 Results for lemma preg_of_not_SP: : forall r, preg_of r <> SP SUCCESS! Proof Found in EFSM: intros ; destruct r; discriminate. Tactics applied: 2334 Original Proof: [intros. unfold preg_of; destruct r; simpl; congruence.] Shorter Proof Found? yes This is a novel proof This proof contained a loop around a state proof search time: 0 min, 10 sec Number of successful tactic applications: 225 Number of failed tactic applications: 2109 Results for fold 32 Results for lemma agree_set_other: : forall ms sp rs r v, agree ms sp rs -> data_preg r = false -> agree ms sp (rs#r <- v) FAILURE! Tactics applied: 10000 Original Proof: [intros. apply agree_exten with rs. auto. intros. apply Pregmap.gso. congruence.] Proof search time: 0 min, 45 sec Number of successful tactic applications: 1659 Number of failed tactic applications: 8342 Results for fold 33 Results for lemma nextinstr_inv: : forall r rs, r <> PC -> (nextinstr rs)#r = rs#r SUCCESS! Proof Found in EFSM: destruct r; auto. tauto. Tactics applied: 1647 Original Proof: [intros. unfold nextinstr. apply Pregmap.gso. red; intro; subst. auto.] Shorter Proof Found? yes This is a novel proof proof search time: 0 min, 9 sec Number of successful tactic applications: 215 Number of failed tactic applications: 1432 Results for fold 34 Results for lemma transl_code_rec_transl_code: : forall f il ep k, transl_code_rec f il ep k = (do c <- transl_code f il ep; k c) FAILURE! Tactics applied: 10000 Original Proof: [induction il; simpl; intros. auto. rewrite IHil. destruct (transl_code f il (it1_is_parent ep a)); simpl; auto.] Proof search time: 2 min, 53 sec Number of successful tactic applications: 1615 Number of failed tactic applications: 8386 Results for fold 35 Results for lemma preg_of_not_PC: : forall r, preg_of r <> PC SUCCESS! Proof Found in EFSM: auto with asmgen. Tactics applied: 119 Original Proof: [intros. apply data_diff; auto with asmgen.] Shorter Proof Found? yes Single step proof reused proof search time: 0 min, 6 sec Number of successful tactic applications: 11 Number of failed tactic applications: 108 Results for fold 36 Results for lemma transl_code_tail: : forall f c1 c2, is_tail c1 c2 -> forall tc2 ep2, transl_code f c2 ep2 = OK tc2 -> exists tc1, exists ep1, transl_code f c1 ep1 = OK tc1 /\ is_tail tc1 tc2 FAILURE! Tactics applied: 10000 Original Proof: [induction 1; simpl; intros. exists tc2; exists ep2; split; auto with coqlib. monadInv H0. exploit IHis_tail; eauto. intros [tc1 [ep1 [A B]]]. exists tc1; exists ep1; split. auto. apply is_tail_trans with x. auto. eapply transl_instr_tail; eauto.] Proof search time: 0 min, 40 sec Number of successful tactic applications: 1344 Number of failed tactic applications: 8657 Results for fold 37 Results for lemma exec_straight_trans: : forall c1 rs1 m1 c2 rs2 m2 c3 rs3 m3, exec_straight c1 rs1 m1 c2 rs2 m2 -> exec_straight c2 rs2 m2 c3 rs3 m3 -> exec_straight c1 rs1 m1 c3 rs3 m3 FAILURE! Tactics applied: 10000 Original Proof: [induction 1; intros. apply exec_straight_step with rs2 m2; auto. apply exec_straight_step with rs2 m2; auto.] Proof search time: 3 min, 9 sec Number of successful tactic applications: 1829 Number of failed tactic applications: 8172 Results for fold 38 Results for lemma agree_undef_regs: : forall ms sp rl rs rs', agree ms sp rs -> (forall r', data_preg r' = true -> preg_notin r' rl -> rs'#r' = rs#r') -> agree (Mach.undef_regs rl ms) sp rs' FAILURE! Tactics applied: 10000 Original Proof: [intros. destruct H. split; auto. rewrite <- agree_sp0. apply H0; auto. rewrite preg_notin_charact. intros. apply not_eq_sym. apply preg_of_not_SP. intros. destruct (In_dec mreg_eq r rl). rewrite Mach.undef_regs_same; auto. rewrite Mach.undef_regs_other; auto. rewrite H0; auto. apply preg_of_data. rewrite preg_notin_charact. intros; red; intros. elim n. exploit preg_of_injective; eauto. congruence.] Proof search time: 0 min, 32 sec Number of successful tactic applications: 1277 Number of failed tactic applications: 8724 Results for fold 39 Results for lemma extcall_arguments_match: : forall ms m m' sp rs sg args, agree ms sp rs -> Mem.extends m m' -> Mach.extcall_arguments ms m sp sg args -> exists args', Asm.extcall_arguments rs m' sg args' /\ Val.lessdef_list args args' FAILURE! Tactics applied: 10000 Original Proof: [unfold Mach.extcall_arguments, Asm.extcall_arguments; intros. eapply extcall_args_match; eauto.] Proof search time: 0 min, 43 sec Number of successful tactic applications: 1223 Number of failed tactic applications: 8778 Results for fold 40 Results for lemma agree_undef_nondata_regs: : forall ms sp rl rs, agree ms sp rs -> (forall r, In r rl -> data_preg r = false) -> agree ms sp (undef_regs rl rs) FAILURE! Tactics applied: 10000 Original Proof: [induction rl; simpl; intros. auto. apply IHrl. apply agree_exten with rs; auto. intros. apply Pregmap.gso. red; intros; subst. assert (data_preg a = false) by auto. congruence. intros. apply H0; auto.] Proof search time: 0 min, 36 sec Number of successful tactic applications: 1671 Number of failed tactic applications: 8330 Results for fold 41 Results for lemma exec_straight_two: : forall i1 i2 c rs1 m1 rs2 m2 rs3 m3, exec_instr ge fn i1 rs1 m1 = Next rs2 m2 -> exec_instr ge fn i2 rs2 m2 = Next rs3 m3 -> rs2#PC = Val.add rs1#PC Vone -> rs3#PC = Val.add rs2#PC Vone -> exec_straight (i1 :: i2 :: c) rs1 m1 c rs3 m3 FAILURE! Tactics applied: 10000 Original Proof: [intros. apply exec_straight_step with rs2 m2; auto. apply exec_straight_one; auto.] Proof search time: 0 min, 32 sec Number of successful tactic applications: 1576 Number of failed tactic applications: 8425 Results for fold 42 Results for lemma sp_val: : forall ms sp rs, agree ms sp rs -> sp = rs#SP SUCCESS! Proof Found in EFSM: induction 1. auto. Tactics applied: 167 Original Proof: [intros. destruct H; auto.] Shorter Proof Found? yes This is a novel proof proof search time: 0 min, 6 sec Number of successful tactic applications: 8 Number of failed tactic applications: 159 Results for fold 43 Results for lemma nextinstr_inv1: : forall r rs, data_preg r = true -> (nextinstr rs)#r = rs#r SUCCESS! Proof Found in EFSM: intros ; apply Pregmap.gso. auto with asmgen. Tactics applied: 2630 Original Proof: [intros. apply nextinstr_inv. red; intro; subst; discriminate.] Shorter Proof Found? yes This is a novel proof proof search time: 0 min, 9 sec Number of successful tactic applications: 331 Number of failed tactic applications: 2299 Results for fold 44 Results for lemma code_tail_pos: : forall pos c1 c2, code_tail pos c1 c2 -> pos >= 0 FAILURE! Tactics applied: 10000 Original Proof: [induction 1. omega. omega.] Proof search time: 2 min, 10 sec Number of successful tactic applications: 1775 Number of failed tactic applications: 8226 Results for fold 45 Results for lemma tail_nolabel_trans: : forall c1 c2 c3, tail_nolabel c2 c3 -> tail_nolabel c1 c2 -> tail_nolabel c1 c3 FAILURE! Tactics applied: 10000 Original Proof: [intros. destruct H; destruct H0; split. eapply is_tail_trans; eauto. intros. rewrite H1; auto.] Proof search time: 0 min, 25 sec Number of successful tactic applications: 1798 Number of failed tactic applications: 8203 Results for fold 46 Results for lemma exec_straight_three: : forall i1 i2 i3 c rs1 m1 rs2 m2 rs3 m3 rs4 m4, exec_instr ge fn i1 rs1 m1 = Next rs2 m2 -> exec_instr ge fn i2 rs2 m2 = Next rs3 m3 -> exec_instr ge fn i3 rs3 m3 = Next rs4 m4 -> rs2#PC = Val.add rs1#PC Vone -> rs3#PC = Val.add rs2#PC Vone -> rs4#PC = Val.add rs3#PC Vone -> exec_straight (i1 :: i2 :: i3 :: c) rs1 m1 c rs4 m4 FAILURE! Tactics applied: 10000 Original Proof: [intros. apply exec_straight_step with rs2 m2; auto. eapply exec_straight_two; eauto.] Proof search time: 0 min, 45 sec Number of successful tactic applications: 1867 Number of failed tactic applications: 8134 Results for fold 47 Results for lemma agree_exten: : forall ms sp rs rs', agree ms sp rs -> (forall r, data_preg r = true -> rs'#r = rs#r) -> agree ms sp rs' FAILURE! Tactics applied: 10000 Original Proof: [intros. destruct H. split; auto. rewrite H0; auto. auto. intros. rewrite H0; auto. apply preg_of_data.] Proof search time: 0 min, 45 sec Number of successful tactic applications: 1524 Number of failed tactic applications: 8477 Results for fold 48 Results for lemma extcall_args_match: : forall ms sp rs m m', agree ms sp rs -> Mem.extends m m' -> forall ll vl, list_forall2 (Mach.extcall_arg ms m sp) ll vl -> exists vl', list_forall2 (Asm.extcall_arg rs m') ll vl' /\ Val.lessdef_list vl vl' FAILURE! Tactics applied: 10000 Original Proof: [induction 3; intros. exists (@nil val); split. constructor. constructor. exploit extcall_arg_match; eauto. intros [v1' [A B]]. destruct IHlist_forall2 as [vl' [C D]]. exists (v1' :: vl'); split; constructor; auto.] Proof search time: 0 min, 37 sec Number of successful tactic applications: 1457 Number of failed tactic applications: 8544 Results for fold 49 Results for lemma tail_nolabel_refl: : forall c, tail_nolabel c c SUCCESS! Proof Found in EFSM: intros. split ; constructor ; Tactics applied: 350 Original Proof: [intros; split. apply is_tail_refl. auto.] Shorter Proof Found? yes This is a novel proof This proof contained a loop around a state proof search time: 0 min, 10 sec Number of successful tactic applications: 59 Number of failed tactic applications: 291 Results for fold 50 Results for lemma nextinstr_set_preg: : forall rs m v, (nextinstr (rs#(preg_of m) <- v))#PC = Val.add rs#PC Vone FAILURE! Tactics applied: 10000 Original Proof: [intros. unfold nextinstr. rewrite Pregmap.gss. rewrite Pregmap.gso. auto. apply sym_not_eq. apply preg_of_not_PC.] Proof search time: 0 min, 48 sec Number of successful tactic applications: 2438 Number of failed tactic applications: 7563 Results for fold 51 Results for lemma annot_arg_match: : forall ms sp rs m m' p v, agree ms sp rs -> Mem.extends m m' -> Mach.annot_arg ms m sp p v -> exists v', Asm.annot_arg rs m' (transl_annot_param p) v' /\ Val.lessdef v v' FAILURE! Tactics applied: 10000 Original Proof: [intros. inv H1; simpl. exists (rs (preg_of r)); split. constructor. eapply preg_val; eauto. exploit Mem.load_extends; eauto. intros [v' [A B]]. exists v'; split; auto. inv H. econstructor; eauto.] Proof search time: 0 min, 37 sec Number of successful tactic applications: 1685 Number of failed tactic applications: 8316 Results for fold 52 Results for lemma agree_nextinstr: : forall ms sp rs, agree ms sp rs -> agree ms sp (nextinstr rs) FAILURE! Tactics applied: 10000 Original Proof: [intros. unfold nextinstr. apply agree_set_other. auto. auto.] Proof search time: 0 min, 27 sec Number of successful tactic applications: 1370 Number of failed tactic applications: 8631 Results for fold 53 Results for lemma agree_change_sp: : forall ms sp rs sp', agree ms sp rs -> sp' <> Vundef -> agree ms sp' (rs#SP <- sp') FAILURE! Tactics applied: 10000 Original Proof: [intros. inv H. split; auto. intros. rewrite Pregmap.gso; auto with asmgen.] Proof search time: 0 min, 31 sec Number of successful tactic applications: 1494 Number of failed tactic applications: 8507 Results for fold 54 Results for lemma extcall_arg_match: : forall ms sp rs m m' l v, agree ms sp rs -> Mem.extends m m' -> Mach.extcall_arg ms m sp l v -> exists v', Asm.extcall_arg rs m' l v' /\ Val.lessdef v v' FAILURE! Tactics applied: 10000 Original Proof: [intros. inv H1. exists (rs#(preg_of r)); split. constructor. eapply preg_val; eauto. unfold load_stack in H2. exploit Mem.loadv_extends; eauto. intros [v' [A B]]. rewrite (sp_val _ _ _ H) in A. exists v'; split; auto. econstructor. eauto. assumption.] Proof search time: 0 min, 34 sec Number of successful tactic applications: 1347 Number of failed tactic applications: 8654 Results for fold 55 Results for lemma agree_set_mregs: : forall sp rl vl vl' ms rs, agree ms sp rs -> Val.lessdef_list vl vl' -> agree (Mach.set_regs rl vl ms) sp (set_regs (map preg_of rl) vl' rs) FAILURE! Tactics applied: 10000 Original Proof: [induction rl; simpl; intros. auto. inv H0. auto. apply IHrl; auto. eapply agree_set_mreg. eexact H. rewrite Pregmap.gss. auto. intros. apply Pregmap.gso; auto.] Proof search time: 0 min, 57 sec Number of successful tactic applications: 1776 Number of failed tactic applications: 8225 Results for fold 56 Results for lemma freg_of_eq: : forall r r', freg_of r = OK r' -> preg_of r = FR r' FAILURE! Tactics applied: 10000 Original Proof: [unfold freg_of; intros. destruct (preg_of r); inv H; auto.] Proof search time: 0 min, 32 sec Number of successful tactic applications: 866 Number of failed tactic applications: 9135 Results for fold 57 Results for lemma code_tail_next: : forall fn ofs i c, code_tail ofs fn (i :: c) -> code_tail (ofs + 1) fn c FAILURE! Tactics applied: 10000 Original Proof: [assert (forall ofs fn c, code_tail ofs fn c -> forall i c', c = i :: c' -> code_tail (ofs + 1) fn c'). induction 1; intros. subst c. constructor. constructor. constructor. eauto. eauto.] Proof search time: 0 min, 35 sec Number of successful tactic applications: 987 Number of failed tactic applications: 9014 OVERALL RESULTS SUMMARY EFSMProver proved 11 out of 57 lemmas. Success rate of 19.298245614035086% There were 0 errors. 46 proof attempts exhausted the automaton On average, a proof was found after applying 988 tactics The longest proof consisted of 4 tactics There were 8 shorter proofs found Of the 46 failures, 46 of them used all 10000 tactics There were 2 reused proofs found There were 9 novel proofs found Of the 46 failures, the average number of tactics used was 10000 On average, a proof was found after 0 min, 9 sec On average, a failed proof attempt took 0 min, 51 sec On average, any (success or failure) proof attempt took 0 min, 43 sec The longest time to find a proof was 0 min, 17 sec The shortest time to find a proof was 0 min, 6 sec There were 0 proofs containing repeated tactics There were 2 proofs that repeated states