From 74819dfa35ee60feb81811247d59775bd66630d0 Mon Sep 17 00:00:00 2001 From: James Pollard Date: Thu, 2 Jul 2020 17:00:14 +0100 Subject: Complete ZToValue_valueToNat. --- src/translation/HTLgenproof.v | 38 ++++++++++++++++---------------------- 1 file changed, 16 insertions(+), 22 deletions(-) (limited to 'src/translation/HTLgenproof.v') 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. -- cgit