diff options
Diffstat (limited to 'src/translation/HTLgenproof.v')
| -rw-r--r-- | src/translation/HTLgenproof.v | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/src/translation/HTLgenproof.v b/src/translation/HTLgenproof.v index 499b6b5..b7b9d27 100644 --- a/src/translation/HTLgenproof.v +++ b/src/translation/HTLgenproof.v @@ -100,7 +100,8 @@ Lemma valToValue_lessdef : Proof. split; intros. destruct v; try discriminate; constructor. - unfold valToValue in H. inversion H. unfold intToValue + unfold valToValue in H. inversion H. + Admitted. (* Need to eventually move posToValue 32 to posToValueAuto, as that has this proof. *) Lemma assumption_32bit : @@ -159,11 +160,12 @@ Section CORRECTNESS. Let tge : HTL.genv := HTL.genv_empty. Lemma eval_correct : - forall sp op rs args m v e assoc f, + forall sp op rs args m v v' e assoc f, Op.eval_operation ge sp op (List.map (fun r : BinNums.positive => Registers.Regmap.get r rs) args) m = Some v -> tr_op op args e -> - Verilog.expr_runp f assoc e (valToValue v). + valToValue v = Some v' -> + Verilog.expr_runp f assoc e v'. Admitted. Lemma eval_cond_correct : |