diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2022-07-04 13:56:29 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2022-07-04 13:56:29 +0100 |
| commit | 839ae9a65535e25e52207d46e274385e0709a90f (patch) | |
| tree | 90bd42ccefd449d72a8256f5f531d34feb71d618 /src/hls/Gible.v | |
| parent | ac9ae4bb523fece46a8213bc8258335e7dadc298 (diff) | |
| download | vericert-839ae9a65535e25e52207d46e274385e0709a90f.tar.gz vericert-839ae9a65535e25e52207d46e274385e0709a90f.zip | |
Working on scheduling proof
Diffstat (limited to 'src/hls/Gible.v')
| -rw-r--r-- | src/hls/Gible.v | 13 |
1 files changed, 13 insertions, 0 deletions
diff --git a/src/hls/Gible.v b/src/hls/Gible.v index 8971535..cacca85 100644 --- a/src/hls/Gible.v +++ b/src/hls/Gible.v @@ -344,6 +344,19 @@ Inductive step_list2 {A} (step_i: val -> istate -> A -> istate -> Prop): | exec_RBnil2 : forall sp i, step_list2 step_i sp i nil i. +Inductive step_list_inter {A} (step_i: val -> istate -> A -> istate -> Prop): + val -> istate -> list A -> istate -> Prop := +| exec_term_RBcons : + forall i0 i1 i2 i instrs sp, + step_i sp (Iexec i0) i i1 -> + step_list_inter step_i sp i1 instrs i2 -> + step_list_inter step_i sp (Iexec i0) (i :: instrs) i2 +| exec_term_RBnil : + forall sp i, step_list_inter step_i sp i nil i +| exec_term_RBcons_term : + forall i cf l sp, + step_list_inter step_i sp (Iterm i cf) l (Iterm i cf). + (*| Top-Level Type Definitions ========================== |