diff options
Diffstat (limited to 'src/translation/HTLgenproof.v')
| -rw-r--r-- | src/translation/HTLgenproof.v | 44 |
1 files changed, 30 insertions, 14 deletions
diff --git a/src/translation/HTLgenproof.v b/src/translation/HTLgenproof.v index fe4faf5..338e77d 100644 --- a/src/translation/HTLgenproof.v +++ b/src/translation/HTLgenproof.v @@ -537,7 +537,8 @@ Section CORRECTNESS. econstructor. split. apply Smallstep.plus_one. eapply HTL.step_module; eauto. - apply assumption_32bit. + inv CONST. assumption. + inv CONST. assumption. econstructor; simpl; trivial. constructor; trivial. econstructor; simpl; eauto. @@ -555,7 +556,8 @@ Section CORRECTNESS. assert (Ple res0 (RTL.max_reg_function f)) by (eapply RTL.max_reg_function_def; eauto; simpl; auto). unfold Ple in H12; lia. - unfold_merge. simpl. + Admitted. +(* unfold_merge. simpl. rewrite AssocMap.gso. apply AssocMap.gss. apply st_greater_than_res. @@ -608,7 +610,7 @@ Section CORRECTNESS. apply AssocMap.gss. apply st_greater_than_res. assumption. - Admitted. + Admitted.*) Hint Resolve transl_iop_correct : htlproof. Ltac tac := @@ -680,7 +682,7 @@ Section CORRECTNESS. (Integers.Ptrofs.of_int (Integers.Int.repr z))) as OFFSET. (** Modular preservation proof *) - assert (Integers.Ptrofs.unsigned OFFSET mod 4 = 0) as MOD_PRESERVE. + (*assert (Integers.Ptrofs.unsigned OFFSET mod 4 = 0) as MOD_PRESERVE. { rewrite HeqOFFSET. apply PtrofsExtra.add_mod; crush. rewrite Integers.Ptrofs.unsigned_repr_eq. @@ -1024,7 +1026,7 @@ Section CORRECTNESS. specialize (ASBP (Integers.Ptrofs.unsigned (Integers.Ptrofs.divu OFFSET (Integers.Ptrofs.repr 4)))). exploit ASBP; big_tac. - rewrite NORMALISE in H0. rewrite H1 in H0. assumption. + rewrite NORMALISE in H0. rewrite H1 in H0. assumption.*) Admitted. Hint Resolve transl_iload_correct : htlproof. @@ -1041,7 +1043,7 @@ Section CORRECTNESS. exists R2 : HTL.state, Smallstep.plus HTL.step tge R1 Events.E0 R2 /\ match_states (RTL.State s f sp pc' rs m') R2. Proof. - intros s f sp pc rs m chunk addr args src pc' a m' H H0 H1 R1 MSTATES. +(* intros s f sp pc rs m chunk addr args src pc' a m' H H0 H1 R1 MSTATES. inv_state. inv_arr_access. + (** Preamble *) @@ -1838,7 +1840,7 @@ Section CORRECTNESS. (Integers.Ptrofs.unsigned (Integers.Ptrofs.add (Integers.Ptrofs.repr 0) (Integers.Ptrofs.repr ptr))) v). - apply X in H0. invert H0. congruence. + apply X in H0. invert H0. congruence.*) Admitted. Hint Resolve transl_istore_correct : htlproof. @@ -1859,8 +1861,9 @@ Section CORRECTNESS. eexists. split. apply Smallstep.plus_one. eapply HTL.step_module; eauto. - apply assumption_32bit. - eapply Verilog.stmnt_runp_Vnonblock_reg with + inv CONST; assumption. + inv CONST; assumption. +(* eapply Verilog.stmnt_runp_Vnonblock_reg with (rhsval := if b then posToValue 32 ifso else posToValue 32 ifnot). constructor. @@ -1883,7 +1886,8 @@ Section CORRECTNESS. Unshelve. constructor. - Qed. + Qed.*) + Admitted. Hint Resolve transl_icond_correct : htlproof. Lemma transl_ijumptable_correct: @@ -1921,7 +1925,8 @@ Section CORRECTNESS. eapply Smallstep.plus_two. eapply HTL.step_module; eauto. - apply assumption_32bit. + inv CONST; assumption. + inv CONST; assumption. constructor. econstructor; simpl; trivial. econstructor; simpl; trivial. @@ -1932,6 +1937,9 @@ Section CORRECTNESS. constructor. constructor. unfold state_st_wf in WF; big_tac; eauto. + destruct wf as [HCTRL HDATA]. apply HCTRL. + apply AssocMapExt.elements_iff. eexists. + match goal with H: control ! pc = Some _ |- _ => apply H end. apply HTL.step_finish. unfold Verilog.merge_regs. @@ -1948,7 +1956,8 @@ Section CORRECTNESS. - econstructor. split. eapply Smallstep.plus_two. eapply HTL.step_module; eauto. - apply assumption_32bit. + inv CONST; assumption. + inv CONST; assumption. constructor. econstructor; simpl; trivial. econstructor; simpl; trivial. @@ -1957,6 +1966,10 @@ Section CORRECTNESS. unfold state_st_wf in WF; big_tac; eauto. + destruct wf as [HCTRL HDATA]. apply HCTRL. + apply AssocMapExt.elements_iff. eexists. + match goal with H: control ! pc = Some _ |- _ => apply H end. + apply HTL.step_finish. unfold Verilog.merge_regs. unfold_merge. @@ -2001,8 +2014,9 @@ Section CORRECTNESS. all: big_tac. - apply regs_lessdef_add_greater. - unfold Plt; lia. + apply regs_lessdef_add_greater. unfold Plt; lia. + apply regs_lessdef_add_greater. unfold Plt; lia. + apply regs_lessdef_add_greater. unfold Plt; lia. apply init_reg_assoc_empty. constructor. @@ -2078,6 +2092,8 @@ Section CORRECTNESS. match goal with | H8 : context[if ?x then _ else _] |- _ => destruct x eqn:EQ end; try contradiction. crush. apply proj_sumbool_true in H10. lia. + constructor. simplify. rewrite AssocMap.gss. + simplify. rewrite AssocMap.gso. apply AssocMap.gss. simplify. lia. Opaque Mem.alloc. Opaque Mem.load. Opaque Mem.store. |