diff options
author | Yann Herklotz <git@yannherklotz.com> | 2022-06-03 18:08:05 +0100 |
---|---|---|
committer | Yann Herklotz <git@yannherklotz.com> | 2022-06-03 18:08:05 +0100 |
commit | db4da00aea8b51bc9d90d83f981b9163eec3c540 (patch) | |
tree | 83d7f3bb6d8d70d7e7471917f1434cd2571a9c63 /src/hls/Gible.v | |
parent | a64b65a9f5b52372b413c31873fa14c3b1785b00 (diff) | |
download | vericert-db4da00aea8b51bc9d90d83f981b9163eec3c540.tar.gz vericert-db4da00aea8b51bc9d90d83f981b9163eec3c540.zip |
Work on CondElim proof
Diffstat (limited to 'src/hls/Gible.v')
-rw-r--r-- | src/hls/Gible.v | 20 |
1 files changed, 20 insertions, 0 deletions
diff --git a/src/hls/Gible.v b/src/hls/Gible.v index 0ab8c1f..ea6bece 100644 --- a/src/hls/Gible.v +++ b/src/hls/Gible.v @@ -140,6 +140,16 @@ Definition max_reg_instr (m: positive) (i: instr) := | RBexit _ c => max_reg_cfi m c end. +Definition max_pred_instr (m: positive) (i: instr) := + match i with + | RBop (Some p) op args res => Pos.max m (max_predicate p) + | RBload (Some p) chunk addr args dst => Pos.max m (max_predicate p) + | RBstore (Some p) chunk addr args src => Pos.max m (max_predicate p) + | RBsetpred (Some p') c args p => Pos.max m (Pos.max p (max_predicate p')) + | RBexit (Some p) c => Pos.max m (max_predicate p) + | _ => m + end. + Definition regset := Regmap.t val. Definition predset := PMap.t bool. @@ -293,6 +303,16 @@ Inductive step_list {A} (step_i: val -> istate -> A -> istate -> Prop): step_i sp (Iexec state) i (Iterm state' cf) -> step_list step_i sp (Iexec state) (i :: instrs) (Iterm state' cf). +Inductive step_list2 {A} (step_i: val -> istate -> A -> istate -> Prop): + val -> istate -> list A -> istate -> Prop := +| exec_RBcons2 : + forall i0 i1 i2 i instrs sp, + step_i sp i0 i i1 -> + step_list2 step_i sp i1 instrs i2 -> + step_list2 step_i sp i0 (i :: instrs) i2 +| exec_RBnil2 : + forall sp i, step_list2 step_i sp i nil i. + (*| Top-Level Type Definitions ========================== |