diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2022-03-26 15:48:47 +0000 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2022-03-26 15:48:47 +0000 |
| commit | dd8d4ae9c320668ac5fd70f72ea76b768edf8165 (patch) | |
| tree | a7c6fa3f15ab227516b00b8186789aeb420b642e /src/hls/HTLgenproof.v | |
| parent | 30baa719fb15c45b13cb869056e51ec7446c0207 (diff) | |
| download | vericert-dd8d4ae9c320668ac5fd70f72ea76b768edf8165.tar.gz vericert-dd8d4ae9c320668ac5fd70f72ea76b768edf8165.zip | |
Remove literal files again
Diffstat (limited to 'src/hls/HTLgenproof.v')
| -rw-r--r-- | src/hls/HTLgenproof.v | 39 |
1 files changed, 21 insertions, 18 deletions
diff --git a/src/hls/HTLgenproof.v b/src/hls/HTLgenproof.v index bf4b057..bf1ef1c 100644 --- a/src/hls/HTLgenproof.v +++ b/src/hls/HTLgenproof.v @@ -1004,22 +1004,25 @@ Section CORRECTNESS. constructor. Qed. - (** The proof of semantic preservation for the translation of instructions - is a simulation argument based on diagrams of the following form: -<< - match_states - code st rs ------------------------- State m st assoc - || | - || | - || | - \/ v - code st rs' ------------------------ State m st assoc' - match_states ->> - where [tr_code c data control fin rtrn st] is assumed to hold. - - The precondition and postcondition is that that should hold is [match_assocmaps rs assoc]. - *) +(*| +The proof of semantic preservation for the translation of instructions is a +simulation argument based on diagrams of the following form: + +:: +> match_states +> code st rs ------------------------- State m st assoc +> || | +> || | +> || | +> \/ v +> code st rs' ------------------------ State m st assoc' +> match_states + +where ``tr_code c data control fin rtrn st`` is assumed to hold. + +The precondition and postcondition is that that should hold is ``match_assocmaps +rs assoc``. +|*) Definition transl_instr_prop (instr : RTL.instruction) : Prop := forall m asr asa fin rtrn st stmt trans res, @@ -1091,7 +1094,7 @@ Section CORRECTNESS. apply Smallstep.plus_one. eapply HTL.step_module; eauto. inv CONST; assumption. - inv CONST; assumption. + inv CONST; assumption. (* processing of state *) econstructor. crush. @@ -2569,7 +2572,7 @@ Section CORRECTNESS. Smallstep.plus HTL.step tge R1 Events.E0 R2 /\ match_states (RTL.State s f sp pc' rs m) R2. Proof. intros s f sp pc rs m arg tbl n pc' H H0 H1 R1 MSTATE. - + #[local] Hint Resolve transl_ijumptable_correct : htlproof.*) Lemma transl_ireturn_correct: |