diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2020-06-02 14:11:01 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2020-06-02 14:11:01 +0100 |
| commit | 5416713c9d6a64839fabf2a923e4dd3bb25ac5fc (patch) | |
| tree | 4b00cdcc6aa3957b5ee3a8f1c3a7b8f4c7d1eff4 /src/translation | |
| parent | d15f20e641220f0b9f316f529b8770c450a89a49 (diff) | |
| download | vericert-5416713c9d6a64839fabf2a923e4dd3bb25ac5fc.tar.gz vericert-5416713c9d6a64839fabf2a923e4dd3bb25ac5fc.zip | |
Get whole proof to compile
Diffstat (limited to 'src/translation')
| -rw-r--r-- | src/translation/HTLgenproof.v | 31 |
1 files changed, 17 insertions, 14 deletions
diff --git a/src/translation/HTLgenproof.v b/src/translation/HTLgenproof.v index 1c3d21c..5cdddb2 100644 --- a/src/translation/HTLgenproof.v +++ b/src/translation/HTLgenproof.v @@ -191,6 +191,7 @@ Section CORRECTNESS. Senv.equiv (Genv.to_senv ge) (Genv.to_senv tge). Proof (Genv.senv_transf_partial TRANSL). + Hint Resolve senv_preserved : htlproof. Lemma eval_correct : forall sp op rs args m v v' e assoc f, @@ -204,7 +205,10 @@ Section CORRECTNESS. Lemma eval_cond_correct : forall cond (args : list Registers.reg) s1 c s' i rs args m b f assoc, translate_condition cond args s1 = OK c s' i -> - Op.eval_condition cond (List.map (fun r : BinNums.positive => Registers.Regmap.get r rs) args) m = Some b -> + Op.eval_condition + cond + (List.map (fun r : BinNums.positive => Registers.Regmap.get r rs) args) + m = Some b -> Verilog.expr_runp f assoc c (boolToValue 32 b). Admitted. @@ -366,8 +370,8 @@ Section CORRECTNESS. rewrite assumption_32bit. apply match_state. apply rs0. unfold_merge. - apply regs_lessdef_regs. assumption. - assumption. + apply regs_lessdef_add_greater. apply greater_than_max_func. + assumption. assumption. unfold state_st_wf. intros. inversion H1. subst. unfold_merge. @@ -375,7 +379,7 @@ Section CORRECTNESS. rewrite assumption_32bit. apply match_state. apply rs0. unfold_merge. - apply regs_lessdef_regs. assumption. + apply regs_lessdef_add_greater. apply greater_than_max_func. assumption. assumption. unfold state_st_wf. intros. inversion H1. @@ -441,13 +445,6 @@ Section CORRECTNESS. Admitted. Hint Resolve transl_step_correct : htlproof. - Lemma senv_preserved : - forall id : AST.ident, - Globalenvs.Senv.public_symbol (Smallstep.symbolenv (HTL.semantics tprog)) id = - Globalenvs.Senv.public_symbol (Smallstep.symbolenv (RTL.semantics prog)) id. - Proof. Admitted. - Hint Resolve senv_preserved : htlproof. - Lemma transl_initial_states : forall s1 : Smallstep.state (RTL.semantics prog), Smallstep.initial_state (RTL.semantics prog) s1 -> @@ -464,8 +461,14 @@ Section CORRECTNESS. Proof. Admitted. Hint Resolve transl_final_states : htlproof. - Theorem transf_program_correct: - Smallstep.forward_simulation (RTL.semantics prog) (HTL.semantics tprog). - Proof. eauto with htlproof. Qed. +Theorem transf_program_correct: + Smallstep.forward_simulation (RTL.semantics prog) (HTL.semantics tprog). +Proof. + eapply Smallstep.forward_simulation_plus. + apply senv_preserved. + eexact transl_initial_states. + eexact transl_final_states. + exact transl_step_correct. +Qed. End CORRECTNESS. |