diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2022-05-31 02:04:52 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2022-05-31 02:04:52 +0100 |
| commit | 2d4be10eeadcbb6aa4cc3d48e596dfc500a0d773 (patch) | |
| tree | 913bde0d9390832b1cc61f49bbdf0f0ce740c623 | |
| parent | aaaf75ca0ac353f5c662f775b3f3104cc4944d87 (diff) | |
| download | vericert-2d4be10eeadcbb6aa4cc3d48e596dfc500a0d773.tar.gz vericert-2d4be10eeadcbb6aa4cc3d48e596dfc500a0d773.zip | |
Update the Gible semantics with correct termination
| -rw-r--r-- | src/hls/Gible.v | 19 |
1 files changed, 10 insertions, 9 deletions
diff --git a/src/hls/Gible.v b/src/hls/Gible.v index e7378ea..0ab8c1f 100644 --- a/src/hls/Gible.v +++ b/src/hls/Gible.v @@ -234,7 +234,7 @@ Step Instruction Variant step_instr: val -> istate -> instr -> istate -> Prop := | exec_RBnop: forall sp ist, - step_instr sp ist RBnop ist + step_instr sp (Iexec ist) RBnop (Iexec ist) | exec_RBop: forall op v res args rs m sp p ist pr, eval_operation ge sp op rs##args m = Some v -> @@ -283,14 +283,15 @@ nested to describe the execution of nested lists. Inductive step_list {A} (step_i: val -> istate -> A -> istate -> Prop): val -> istate -> list A -> istate -> Prop := -| exec_RBcons: - forall state i state' state'' instrs sp, - step_i sp state i state' -> - step_list step_i sp state' instrs state'' -> - step_list step_i sp state (i :: instrs) state'' -| exec_RBnil: - forall state sp, - step_list step_i sp state nil state. +| exec_RBcons : + forall state i state' state'' instrs sp cf, + step_i sp (Iexec state) i (Iexec state') -> + step_list step_i sp (Iexec state') instrs (Iterm state'' cf) -> + step_list step_i sp (Iexec state) (i :: instrs) (Iterm state'' cf) +| exec_RBterm : + forall state sp i state' cf instrs, + step_i sp (Iexec state) i (Iterm state' cf) -> + step_list step_i sp (Iexec state) (i :: instrs) (Iterm state' cf). (*| Top-Level Type Definitions |