From 9acb804500b590edbff66cd802216f58dde169cd Mon Sep 17 00:00:00 2001 From: James Pollard Date: Fri, 12 Jun 2020 16:54:28 +0100 Subject: Some work on store proof. --- src/translation/HTLgenproof.v | 49 +++++++++++++++++++++++++++++++++---------- 1 file changed, 38 insertions(+), 11 deletions(-) diff --git a/src/translation/HTLgenproof.v b/src/translation/HTLgenproof.v index 34fa8ec..6dc4c21 100644 --- a/src/translation/HTLgenproof.v +++ b/src/translation/HTLgenproof.v @@ -415,16 +415,6 @@ Section CORRECTNESS. | [ _ : context[match ?x with | _ => _ end] |- _ ] => destruct x end. - Ltac t := - match goal with - | [ _ : Mem.loadv _ _ ?a = Some _ |- _ ] => - let PTR := fresh "PTR" in - assert (exists b ofs, a = Values.Vptr b ofs) as PTR; - [> destruct a; simpl in *; try discriminate; - repeat eexists |] - | [ H: Values.Vptr _ _ = Values.Vptr _ _ |- _] => invert H - end. - Opaque Nat.div. - destruct c, chunk, addr, args; simplify; rt; simplify. @@ -522,6 +512,11 @@ Section CORRECTNESS. invert H6. assumption. + assert (Integers.Ptrofs.repr x = i0) by admit. + rewrite H0 in H7. + rewrite H1 in H7. + discriminate. + assumption. assumption. @@ -533,7 +528,39 @@ Section CORRECTNESS. econstructor; simplify; try reflexivity; eassumption. - - admit. + - destruct c, chunk, addr, args; simplify; rt; simplify. + + admit. + + admit. + + admit. + + + eexists. split. + eapply Smallstep.plus_one. + eapply HTL.step_module; eauto. + econstructor. econstructor. econstructor. simplify. + eapply Verilog.stmnt_runp_Vblock_arr. simplify. + econstructor. econstructor. econstructor. simplify. + + reflexivity. + + unfold_merge. apply AssocMap.gss. + + simplify. rewrite assumption_32bit. econstructor. + + unfold_merge. + apply regs_lessdef_add_greater. + apply greater_than_max_func. + assumption. + + assumption. + + unfold state_st_wf. inversion 1. simplify. + unfold_merge. apply AssocMap.gss. + + admit. + + econstructor; simplify; try reflexivity. + admit. + - eexists. split. apply Smallstep.plus_one. eapply HTL.step_module; eauto. -- cgit