diff options
Diffstat (limited to 'src/hls/GibleSeqgenproof.v')
| -rw-r--r-- | src/hls/GibleSeqgenproof.v | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/src/hls/GibleSeqgenproof.v b/src/hls/GibleSeqgenproof.v index 7451510..1d1d4b7 100644 --- a/src/hls/GibleSeqgenproof.v +++ b/src/hls/GibleSeqgenproof.v @@ -253,6 +253,12 @@ whole execution (in one big step) of the basic block. Definition match_prog (p: RTL.program) (tp: GibleSeq.program) := Linking.match_program (fun cu f tf => transl_fundef f = Errors.OK tf) eq p tp. + Lemma transf_program_match: + forall p tp, transl_program p = OK tp -> match_prog p tp. + Proof. + intros. apply Linking.match_transform_partial_program; auto. + Qed. + Context (TRANSL : match_prog prog tprog). Lemma symbols_preserved: |