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/RTLPargenproof.v | |
parent | 30baa719fb15c45b13cb869056e51ec7446c0207 (diff) | |
download | vericert-dd8d4ae9c320668ac5fd70f72ea76b768edf8165.tar.gz vericert-dd8d4ae9c320668ac5fd70f72ea76b768edf8165.zip |
Remove literal files again
Diffstat (limited to 'src/hls/RTLPargenproof.v')
-rw-r--r-- | src/hls/RTLPargenproof.v | 15 |
1 files changed, 11 insertions, 4 deletions
diff --git a/src/hls/RTLPargenproof.v b/src/hls/RTLPargenproof.v index 6d61572..4e88b13 100644 --- a/src/hls/RTLPargenproof.v +++ b/src/hls/RTLPargenproof.v @@ -16,7 +16,6 @@ * along with this program. If not, see <https://www.gnu.org/licenses/>. *) -(* [[file:../../docs/scheduler.org::rtlpargenproof-imports][rtlpargenproof-imports]] *) Require Import compcert.backend.Registers. Require Import compcert.common.AST. Require Import compcert.common.Errors. @@ -37,9 +36,18 @@ Require Import vericert.hls.Abstr. #[local] Open Scope positive. #[local] Open Scope forest. #[local] Open Scope pred_op. -(* rtlpargenproof-imports ends here *) -(* [[file:../../docs/scheduler.org::rtlpargenproof-main][rtlpargenproof-main]] *) +(*| +============== +RTLPargenproof +============== + +RTLBlock to abstract translation +================================ + +Correctness of translation from RTLBlock to the abstract interpretation language. +|*) + (*Definition is_regs i := match i with mk_instr_state rs _ => rs end. Definition is_mem i := match i with mk_instr_state _ m => m end. @@ -1134,4 +1142,3 @@ Proof. induction 2; try rewrite H; eauto with barg. Qed. Qed. End CORRECTNESS. -(* rtlpargenproof-main ends here *) |