diff options
author | Michalis Pardalos <m.pardalos@gmail.com> | 2021-05-16 15:17:24 +0100 |
---|---|---|
committer | Michalis Pardalos <m.pardalos@gmail.com> | 2021-05-16 15:18:48 +0100 |
commit | 29ef1d2d374dcca6ea719c63339f18900be2532f (patch) | |
tree | 5a9225eddeeefae523f8eead3f26513f42bb28af /src/hls/HTLgenproof.v | |
parent | 2429e158ecdb4ab8150fa26af776e806d7fd019c (diff) | |
download | vericert-29ef1d2d374dcca6ea719c63339f18900be2532f.tar.gz vericert-29ef1d2d374dcca6ea719c63339f18900be2532f.zip |
Most of Ireturn proof
Diffstat (limited to 'src/hls/HTLgenproof.v')
-rw-r--r-- | src/hls/HTLgenproof.v | 59 |
1 files changed, 54 insertions, 5 deletions
diff --git a/src/hls/HTLgenproof.v b/src/hls/HTLgenproof.v index d297c80..077a8dc 100644 --- a/src/hls/HTLgenproof.v +++ b/src/hls/HTLgenproof.v @@ -1143,12 +1143,11 @@ Section CORRECTNESS. - inv CONST. assumption. - inv CONST. assumption. - repeat econstructor. - - repeat econstructor. simpl. apply H5. + - repeat econstructor. intuition eauto. - big_tac. - assert (HPle: Ple res0 (RTL.max_reg_function f)) - by (eapply RTL.max_reg_function_def; eauto; simpl; auto). - - unfold Ple in HPle. lia. + assert (Ple res0 (RTL.max_reg_function f)) + by eauto using RTL.max_reg_function_def. + xomega. - big_tac. + apply regs_lessdef_add_match. assumption. apply regs_lessdef_add_greater. unfold Plt; lia. assumption. @@ -1172,6 +1171,56 @@ Section CORRECTNESS. Qed. Hint Resolve transl_iop_correct : htlproof. + Lemma return_val_exec_spec : forall f or asr asa, + Verilog.expr_runp f asr asa (return_val or) + (match or with + | Some r => asr#r + | None => ZToValue 0 + end). + Proof. destruct or; repeat econstructor. Qed. + + Lemma transl_ireturn_correct: + forall (s : list RTL.stackframe) (f : RTL.function) (stk : Values.block) + (pc : positive) (rs : RTL.regset) (m : mem) (or : option Registers.reg) + (m' : mem), + (RTL.fn_code f) ! pc = Some (RTL.Ireturn or) -> + Mem.free m stk 0 (RTL.fn_stacksize f) = Some m' -> + forall R1 : HTL.state, + match_states (RTL.State s f (Values.Vptr stk Integers.Ptrofs.zero) pc rs m) R1 -> + exists R2 : HTL.state, + Smallstep.plus HTL.step tge R1 Events.E0 R2 /\ + match_states (RTL.Returnstate s (Registers.regmap_optget or Values.Vundef rs) m') R2. + Proof. + intros * H H0 * MSTATE. + inv_state. + inv CONST. simplify. + eexists. split. + - eapply Smallstep.plus_two. + + eapply HTL.step_module; eauto; try solve [ repeat econstructor ]. + * repeat econstructor. apply return_val_exec_spec. + * big_tac. + * admit. + + simplify. + eapply HTL.step_finish. + * big_tac. + * big_tac. + + eauto with htlproof. + - constructor; eauto with htlproof. + destruct or. + + rewrite fso. (* Return value is not fin *) + * big_tac. + inv MASSOC. + apply H10. + eapply RTL.max_reg_function_use; eauto; crush. + * assert (Ple r (RTL.max_reg_function f)) + by (eapply RTL.max_reg_function_use; eauto; crush). + xomega. + + eauto with htlproof. + Unshelve. + exact tt. eauto. + Admitted. + Hint Resolve transl_ireturn_correct : htlproof. + Ltac tac := repeat match goal with | [ _ : error _ _ = OK _ _ _ |- _ ] => discriminate |