Results for fold 1 Results for lemma data_diff: : forall r r', data_preg r = true -> data_preg r' = false -> r <> r' SUCCESS! Proof Found in EFSM: congruence. Tactics applied: 133 Original Proof: [congruence.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 8 sec Number of successful tactic applications: 15 Number of failed tactic applications: 118 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, 42 sec Number of successful tactic applications: 1347 Number of failed tactic applications: 8654 Results for lemma tail_nolabel_refl: : forall c, tail_nolabel c c SUCCESS! Proof Found in EFSM: split ; auto with coqlib. Tactics applied: 440 Original Proof: [intros; split. apply is_tail_refl. auto.] Shorter Proof Found? yes This is a novel proof proof search time: 0 min, 8 sec Number of successful tactic applications: 71 Number of failed tactic applications: 369 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, 30 sec Number of successful tactic applications: 961 Number of failed tactic applications: 9040 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, 35 sec Number of successful tactic applications: 1476 Number of failed tactic applications: 8525 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, 33 sec Number of successful tactic applications: 1412 Number of failed tactic applications: 8589 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, 21 sec Number of successful tactic applications: 513 Number of failed tactic applications: 9488 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, 27 sec Number of successful tactic applications: 1361 Number of failed tactic applications: 8640 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, 35 sec Number of successful tactic applications: 1497 Number of failed tactic applications: 8504 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, 38 sec Number of successful tactic applications: 1369 Number of failed tactic applications: 8632 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, 29 sec Number of successful tactic applications: 1492 Number of failed tactic applications: 8509 Results for lemma preg_of_not_PC: : forall r, preg_of r <> PC SUCCESS! Proof Found in EFSM: destruct r; discriminate. Tactics applied: 470 Original Proof: [intros. apply data_diff; auto with asmgen.] Shorter Proof Found? yes This is a novel proof proof search time: 0 min, 8 sec Number of successful tactic applications: 60 Number of failed tactic applications: 410 Results for fold 2 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, 47 sec Number of successful tactic applications: 1687 Number of failed tactic applications: 8314 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. auto. Tactics applied: 120 Original Proof: [intros. destruct H. auto.] Shorter Proof Found? yes This is a novel proof proof search time: 0 min, 8 sec Number of successful tactic applications: 13 Number of failed tactic applications: 107 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 SUCCESS! Proof Found in EFSM: induction 1; simpl ; econstructor ; eauto. Tactics applied: 2657 Original Proof: [induction 1; intros. apply exec_straight_step with rs2 m2; auto. apply exec_straight_step with rs2 m2; auto.] Shorter Proof Found? yes This is a novel proof proof search time: 0 min, 17 sec Number of successful tactic applications: 548 Number of failed tactic applications: 2109 Results for lemma nextinstr_inv1: : forall r rs, data_preg r = true -> (nextinstr rs)#r = rs#r SUCCESS! Proof Found in EFSM: destruct r; reflexivity || discriminate. Tactics applied: 204 Original Proof: [intros. apply nextinstr_inv. red; intro; subst; discriminate.] Shorter Proof Found? yes This is a novel proof This proof contained a loop around a state proof search time: 0 min, 8 sec Number of successful tactic applications: 43 Number of failed tactic applications: 161 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, 39 sec Number of successful tactic applications: 2347 Number of failed tactic applications: 7654 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, 38 sec Number of successful tactic applications: 1713 Number of failed tactic applications: 8288 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, 45 sec Number of successful tactic applications: 2079 Number of failed tactic applications: 7922 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: 0 min, 37 sec Number of successful tactic applications: 1992 Number of failed tactic applications: 8009 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: 1631 Number of failed tactic applications: 8370 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: 2361 Original Proof: [induction 1; simpl. unfold Vzero; congruence. auto.] Shorter Proof Found? yes This is a novel proof proof search time: 0 min, 13 sec Number of successful tactic applications: 481 Number of failed tactic applications: 1880 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, 37 sec Number of successful tactic applications: 1992 Number of failed tactic applications: 8009 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: 0 min, 37 sec Number of successful tactic applications: 1556 Number of failed tactic applications: 8445 Results for fold 3 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, 46 sec Number of successful tactic applications: 1768 Number of failed tactic applications: 8233 Results for lemma code_tail_pos: : forall pos c1 c2, code_tail pos c1 c2 -> pos >= 0 SUCCESS! Proof Found in EFSM: induction 1; omega. Tactics applied: 171 Original Proof: [induction 1. omega. omega.] Shorter Proof Found? yes This is a novel proof proof search time: 0 min, 4 sec Number of successful tactic applications: 21 Number of failed tactic applications: 150 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, 34 sec Number of successful tactic applications: 1498 Number of failed tactic applications: 8503 Results for lemma nextinstr_pc: : forall rs, (nextinstr rs)#PC = Val.add rs#PC Vone SUCCESS! Proof Found in EFSM: split ; Tactics applied: 41 Original Proof: [intros. apply Pregmap.gss.] Shorter Proof Found? yes Single step proof reused proof search time: 0 min, 4 sec Number of successful tactic applications: 2 Number of failed tactic applications: 39 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, 26 sec Number of successful tactic applications: 1230 Number of failed tactic applications: 8771 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, 46 sec Number of successful tactic applications: 1472 Number of failed tactic applications: 8529 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: 0 min, 30 sec Number of successful tactic applications: 1211 Number of failed tactic applications: 8790 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, 38 sec Number of successful tactic applications: 1288 Number of failed tactic applications: 8713 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, 53 sec Number of successful tactic applications: 1769 Number of failed tactic applications: 8232 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: 1769 Number of failed tactic applications: 8232 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, 35 sec Number of successful tactic applications: 2099 Number of failed tactic applications: 7902 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, 29 sec Number of successful tactic applications: 1239 Number of failed tactic applications: 8762 Results for fold 4 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, 25 sec Number of successful tactic applications: 913 Number of failed tactic applications: 9088 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, 47 sec Number of successful tactic applications: 1631 Number of failed tactic applications: 8370 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: 142 Original Proof: [intros. destruct H; auto.] Shorter Proof Found? yes This is a novel proof proof search time: 0 min, 5 sec Number of successful tactic applications: 12 Number of failed tactic applications: 130 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, 34 sec Number of successful tactic applications: 1375 Number of failed tactic applications: 8626 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, 23 sec Number of successful tactic applications: 908 Number of failed tactic applications: 9093 Results for lemma nextinstr_inv: : forall r rs, r <> PC -> (nextinstr rs)#r = rs#r SUCCESS! Proof Found in EFSM: destruct r; tauto. Tactics applied: 237 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, 5 sec Number of successful tactic applications: 41 Number of failed tactic applications: 196 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, 23 sec Number of successful tactic applications: 877 Number of failed tactic applications: 9124 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, 41 sec Number of successful tactic applications: 1645 Number of failed tactic applications: 8356 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, 24 sec Number of successful tactic applications: 1217 Number of failed tactic applications: 8784 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, 32 sec Number of successful tactic applications: 1916 Number of failed tactic applications: 8085 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, 59 sec Number of successful tactic applications: 1411 Number of failed tactic applications: 8590 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, 32 sec Number of successful tactic applications: 1821 Number of failed tactic applications: 8180 Results for fold 5 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, 22 sec Number of successful tactic applications: 1080 Number of failed tactic applications: 8921 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, 26 sec Number of successful tactic applications: 1208 Number of failed tactic applications: 8793 Results for lemma preg_of_not_SP: : forall r, preg_of r <> SP FAILURE! Tactics applied: 10000 Original Proof: [intros. unfold preg_of; destruct r; simpl; congruence.] Proof search time: 0 min, 16 sec Number of successful tactic applications: 856 Number of failed tactic applications: 9145 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, 22 sec Number of successful tactic applications: 1114 Number of failed tactic applications: 8887 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: 1239 Number of failed tactic applications: 8762 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, 32 sec Number of successful tactic applications: 1600 Number of failed tactic applications: 8401 Results for lemma preg_of_data: : forall r, data_preg (preg_of r) = true FAILURE! Tactics applied: 10000 Original Proof: [intros. destruct r; reflexivity.] Proof search time: 0 min, 16 sec Number of successful tactic applications: 565 Number of failed tactic applications: 9436 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: 0 min, 31 sec Number of successful tactic applications: 1426 Number of failed tactic applications: 8575 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, 25 sec Number of successful tactic applications: 1319 Number of failed tactic applications: 8682 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 634 tactics The longest proof consisted of 4 tactics There were 10 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, 8 sec On average, a failed proof attempt took 0 min, 34 sec On average, any (success or failure) proof attempt took 0 min, 29 sec The longest time to find a proof was 0 min, 17 sec The shortest time to find a proof was 0 min, 4 sec There were 0 proofs containing repeated tactics There were 1 proofs that repeated states