diff options
| author | James Pollard <james@pollard.dev> | 2020-07-02 17:00:14 +0100 |
|---|---|---|
| committer | James Pollard <james@pollard.dev> | 2020-07-02 17:00:14 +0100 |
| commit | 74819dfa35ee60feb81811247d59775bd66630d0 (patch) | |
| tree | 47df2d6dcd356f04808b8cdb0b70f4f4b7b8d3b1 /src/translation/HTLgenproof.v | |
| parent | cf19dd40f466691d28f4dfd86211724b700aa217 (diff) | |
| download | vericert-kvx-74819dfa35ee60feb81811247d59775bd66630d0.tar.gz vericert-kvx-74819dfa35ee60feb81811247d59775bd66630d0.zip | |
Complete ZToValue_valueToNat.
Diffstat (limited to 'src/translation/HTLgenproof.v')
| -rw-r--r-- | src/translation/HTLgenproof.v | 38 |
1 files changed, 16 insertions, 22 deletions
diff --git a/src/translation/HTLgenproof.v b/src/translation/HTLgenproof.v index e4bbb8f..38fe27a 100644 --- a/src/translation/HTLgenproof.v +++ b/src/translation/HTLgenproof.v @@ -849,16 +849,13 @@ Section CORRECTNESS. all: big_tac. - 1: { - assert (HPle : Ple dst (RTL.max_reg_function f)). - eapply RTL.max_reg_function_def. eassumption. auto. - apply ZExtra.Pge_not_eq. apply ZExtra.Ple_Plt_Succ. assumption. - } - 2: { - assert (HPle : Ple dst (RTL.max_reg_function f)). - eapply RTL.max_reg_function_def. eassumption. auto. - apply ZExtra.Pge_not_eq. apply ZExtra.Ple_Plt_Succ. assumption. - } + 1: { assert (HPle : Ple dst (RTL.max_reg_function f)). + eapply RTL.max_reg_function_def. eassumption. auto. + apply ZExtra.Pge_not_eq. apply ZExtra.Ple_Plt_Succ. assumption. } + + 2: { assert (HPle : Ple dst (RTL.max_reg_function f)). + eapply RTL.max_reg_function_def. eassumption. auto. + apply ZExtra.Pge_not_eq. apply ZExtra.Ple_Plt_Succ. assumption. } (** Match assocmaps *) apply regs_lessdef_add_match; big_tac. @@ -952,22 +949,19 @@ Section CORRECTNESS. all: big_tac. - 1: { - assert (HPle : Ple dst (RTL.max_reg_function f)). - eapply RTL.max_reg_function_def. eassumption. auto. - apply ZExtra.Pge_not_eq. apply ZExtra.Ple_Plt_Succ. assumption. - } - 2: { - assert (HPle : Ple dst (RTL.max_reg_function f)). - eapply RTL.max_reg_function_def. eassumption. auto. - apply ZExtra.Pge_not_eq. apply ZExtra.Ple_Plt_Succ. assumption. - } + 1: { assert (HPle : Ple dst (RTL.max_reg_function f)). + eapply RTL.max_reg_function_def. eassumption. auto. + apply ZExtra.Pge_not_eq. apply ZExtra.Ple_Plt_Succ. assumption. } + + 2: { assert (HPle : Ple dst (RTL.max_reg_function f)). + eapply RTL.max_reg_function_def. eassumption. auto. + apply ZExtra.Pge_not_eq. apply ZExtra.Ple_Plt_Succ. assumption. } (** Match assocmaps *) apply regs_lessdef_add_match; big_tac. (** Equality proof *) - match goal with + match goal with (* Prevents issues with evars *) | [ |- context [valueToNat ?x] ] => assert (Z.to_nat (Integers.Ptrofs.unsigned @@ -2110,7 +2104,7 @@ Section CORRECTNESS. repeat (unfold_match B). inversion B. subst. exploit main_tprog_internal; eauto; intros. rewrite symbols_preserved. replace (AST.prog_main tprog) with (AST.prog_main prog). - Apply Heqo. symmetry; eapply Linking.match_program_main; eauto. + apply Heqo. symmetry; eapply Linking.match_program_main; eauto. inversion H5. econstructor; split. econstructor. apply (Genv.init_mem_transf_partial TRANSL'); eauto. |