diff options
author | James Pollard <james@pollard.dev> | 2020-06-03 19:38:40 +0100 |
---|---|---|
committer | James Pollard <james@pollard.dev> | 2020-06-03 19:38:40 +0100 |
commit | 0729bb6e93307567cc21702005ea1d8c8dddaf8f (patch) | |
tree | 552a10d138056ff26403dc3b72af6c32e27b55c6 /src/translation/HTLgenproof.v | |
parent | e3c66ff88570c5370b37f51404f71f485d2e5dfe (diff) | |
parent | 971b35fd4af24cfffc462df13f8c5b9be982858e (diff) | |
download | vericert-kvx-0729bb6e93307567cc21702005ea1d8c8dddaf8f.tar.gz vericert-kvx-0729bb6e93307567cc21702005ea1d8c8dddaf8f.zip |
Merge branch 'develop' into arrays-proof
Diffstat (limited to 'src/translation/HTLgenproof.v')
-rw-r--r-- | src/translation/HTLgenproof.v | 19 |
1 files changed, 7 insertions, 12 deletions
diff --git a/src/translation/HTLgenproof.v b/src/translation/HTLgenproof.v index a8177cf..e719070 100644 --- a/src/translation/HTLgenproof.v +++ b/src/translation/HTLgenproof.v @@ -107,11 +107,6 @@ Lemma assumption_32bit : valueToPos (posToValue 32 v) = v. Admitted. -Lemma assumption_32bit_bool : - forall b, - valueToBool (boolToValue 32 b) = b. -Admitted. - Lemma st_greater_than_res : forall m res : positive, m <> res. @@ -127,6 +122,11 @@ Lemma finish_not_res : f <> r. Admitted. +Lemma greater_than_max_func : + forall f st, + Plt (RTL.max_reg_function f) st. +Proof. Admitted. + Ltac inv_state := match goal with MSTATE : match_states _ _ |- _ => @@ -239,11 +239,6 @@ Section CORRECTNESS. exists assoc', HTL.step tge (HTL.State m st assoc) Events.E0 (HTL.State m st assoc'). - Lemma greater_than_max_func : - forall f st, - Plt (RTL.max_reg_function f) st. - Proof. Admitted. - Theorem transl_step_correct: forall (S1 : RTL.state) t S2, RTL.step ge S1 t S2 -> @@ -358,11 +353,11 @@ Section CORRECTNESS. eapply Verilog.erun_Vternary_true. eapply eval_cond_correct; eauto. constructor. - apply assumption_32bit_bool. + apply boolToValue_ValueToBool. eapply Verilog.erun_Vternary_false. eapply eval_cond_correct; eauto. constructor. - apply assumption_32bit_bool. + apply boolToValue_ValueToBool. trivial. constructor. trivial. |