diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2021-01-29 19:20:07 +0000 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2021-01-29 19:20:07 +0000 |
| commit | b708486d60c4c0aa695dca4ee46861c87cebb9e1 (patch) | |
| tree | 89532b748657ded3bf86da3ae15166c42093ace8 /src/hls/RTLPar.v | |
| parent | cd6bf14e8f5ce68624ba20a33b8278c78cb632fb (diff) | |
| download | vericert-b708486d60c4c0aa695dca4ee46861c87cebb9e1.tar.gz vericert-b708486d60c4c0aa695dca4ee46861c87cebb9e1.zip | |
Fix definitions of proofs some more
Diffstat (limited to 'src/hls/RTLPar.v')
| -rw-r--r-- | src/hls/RTLPar.v | 12 |
1 files changed, 11 insertions, 1 deletions
diff --git a/src/hls/RTLPar.v b/src/hls/RTLPar.v index 3ad54f5..be9ff22 100644 --- a/src/hls/RTLPar.v +++ b/src/hls/RTLPar.v @@ -46,11 +46,21 @@ Section RELSEM. Context (ge: genv). + Inductive step_instr_list: val -> instr_state -> list instr -> instr_state -> Prop := + | exec_RBcons: + forall state i state' state'' instrs sp, + step_instr ge sp state i state' -> + step_instr_list sp state' instrs state'' -> + step_instr_list sp state (i :: instrs) state'' + | exec_RBnil: + forall state sp, + step_instr_list sp state nil state. + Inductive step_instr_block (sp : val) : instr_state -> bb -> instr_state -> Prop := | exec_instr_block_cons: forall state i state' state'' instrs, - step_instr_list ge sp state i state' -> + step_instr_list sp state i state' -> step_instr_block sp state' instrs state'' -> step_instr_block sp state (i :: instrs) state'' | exec_instr_block_nil: |