diff options
| author | Michalis Pardalos <m.pardalos@gmail.com> | 2021-06-10 22:01:26 +0100 |
|---|---|---|
| committer | Michalis Pardalos <m.pardalos@gmail.com> | 2021-06-10 22:01:26 +0100 |
| commit | f7616136f1a2f3561500b1c28219ae725c4cda17 (patch) | |
| tree | fed32ce1b6ff600883d5735891de7d2119f38b7a /src/hls/ApplyExternctrl.v | |
| parent | 6957832da6522c7099b9554bfc68b67e0fb39444 (diff) | |
| download | vericert-f7616136f1a2f3561500b1c28219ae725c4cda17.tar.gz vericert-f7616136f1a2f3561500b1c28219ae725c4cda17.zip | |
Remove all Admitted from top-level Compiler.v
Diffstat (limited to 'src/hls/ApplyExternctrl.v')
| -rw-r--r-- | src/hls/ApplyExternctrl.v | 16 |
1 files changed, 16 insertions, 0 deletions
diff --git a/src/hls/ApplyExternctrl.v b/src/hls/ApplyExternctrl.v index 44c6b83..5ddbd4a 100644 --- a/src/hls/ApplyExternctrl.v +++ b/src/hls/ApplyExternctrl.v @@ -178,3 +178,19 @@ End APPLY_EXTERNCTRL. Definition transf_fundef (prog : HTL.program) := transf_partial_fundef (module_apply_externctrl prog). Definition transf_program (prog : HTL.program) := transform_partial_program (transf_fundef prog) prog. + +(* Semantics *) + +Definition match_prog : HTL.program -> HTL.program -> Prop := + Linking.match_program (fun ctx f tf => ApplyExternctrl.transf_fundef ctx f = OK tf) eq. + +Lemma transf_program_match : forall p tp, + ApplyExternctrl.transf_program p = OK tp -> match_prog p tp. +Admitted. + +Lemma transf_program_correct : forall p tp, + match_prog p tp -> Smallstep.forward_simulation (HTL.semantics p) (HTL.semantics tp). +Admitted. + +Instance TransfLink : Linking.TransfLink match_prog. +Admitted. |