diff options
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 -------------- |