diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2020-05-29 14:42:09 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2020-05-29 14:42:09 +0100 |
| commit | 3beb6e00213c5e7409d4574b663e5c6bf7490d66 (patch) | |
| tree | f6c41838303d256384c62340f7709cc4514a7ff7 /src/translation | |
| parent | 3ee0bfa7367fde5f9ec0dfd77f921f22f9e64563 (diff) | |
| download | vericert-3beb6e00213c5e7409d4574b663e5c6bf7490d66.tar.gz vericert-3beb6e00213c5e7409d4574b663e5c6bf7490d66.zip | |
Change AssocMap to Maps.PTree
Diffstat (limited to 'src/translation')
| -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 : |