diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2022-06-06 15:44:43 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2022-06-06 15:44:43 +0100 |
| commit | 703b43cb326feb971966edaa0b19c1548920f7ac (patch) | |
| tree | d8b3d8f96503aa479fb177f3334aa9e2b43574f3 /src/hls/Gible.v | |
| parent | baa7185e411df24c307691bd77fb91e908a257c6 (diff) | |
| download | vericert-703b43cb326feb971966edaa0b19c1548920f7ac.tar.gz vericert-703b43cb326feb971966edaa0b19c1548920f7ac.zip | |
Rearrange definitions and create IfConversion template
Diffstat (limited to 'src/hls/Gible.v')
| -rw-r--r-- | src/hls/Gible.v | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/src/hls/Gible.v b/src/hls/Gible.v index 4cecd2c..399935b 100644 --- a/src/hls/Gible.v +++ b/src/hls/Gible.v @@ -549,6 +549,18 @@ support if-conversion. step_cf_instr (State s f sp pc rs pr m) (RBgoto pc') E0 (State s f sp pc' rs pr m). + Lemma step_cf_instr_det : + forall st cf t st1 st2, + step_cf_instr st cf t st1 -> + step_cf_instr st cf t st2 -> + st1 = st2. + Proof using. + inversion 1; subst; simplify; clear H; + match goal with H: context[step_cf_instr] |- _ => inv H end; crush; + assert (vargs0 = vargs) by eauto using eval_builtin_args_determ; subst; + assert (vres = vres0 /\ m' = m'0) by eauto using external_call_deterministic; crush. + Qed. + (*| Top-level step -------------- |