From 3beb6e00213c5e7409d4574b663e5c6bf7490d66 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Fri, 29 May 2020 14:42:09 +0100 Subject: Change AssocMap to Maps.PTree --- src/translation/HTLgenproof.v | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) (limited to 'src/translation') 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 : -- cgit