diff options
author | Yann Herklotz <git@yannherklotz.com> | 2020-08-12 19:14:49 +0200 |
---|---|---|
committer | Yann Herklotz <git@yannherklotz.com> | 2020-08-12 19:15:03 +0200 |
commit | 78898d5e6316b2a43398e12549ff9754883ed9d8 (patch) | |
tree | aeb30c15133069a8ac632bd29238c0e32ac2583c /src | |
parent | f9d3eaa70b8818d6e3d3ac57e789f58a99ae64e6 (diff) | |
download | vericert-78898d5e6316b2a43398e12549ff9754883ed9d8.tar.gz vericert-78898d5e6316b2a43398e12549ff9754883ed9d8.zip |
Remove unnecessary commented proof
Diffstat (limited to 'src')
-rw-r--r-- | src/translation/HTLgenproof.v | 23 |
1 files changed, 0 insertions, 23 deletions
diff --git a/src/translation/HTLgenproof.v b/src/translation/HTLgenproof.v index ee88d3a..6664617 100644 --- a/src/translation/HTLgenproof.v +++ b/src/translation/HTLgenproof.v @@ -879,29 +879,6 @@ Section CORRECTNESS. constructor. Qed. - -(* Lemma eval_cond_correct : - forall s, - match_states (RTL.State stk f sp pc rs m) (HTL.State res ml st asr asa) -> - (RTL.fn_code f) ! st = Some (RTL.Iop (Op.Ocmp cond) args pc' res0) -> - (Values.Val.of_optbool - (Op.eval_condition cond (map (fun r : positive => Registers.Regmap.get r rs) args) m)) = v -> - translate_condition cond args s = OK e s' i -> - exists v' : value, Verilog.expr_runp f' asr asa e v' /\ val_value_lessdef v v'. - - Lemma value_select_optbool : - Values.Val.normalize (Values.Val.of_optbool b) - - Lemma eval_cond_correct : - forall e asa asr f' m args rs cond, - exists v' : value, - Verilog.expr_runp f' asr asa e v' /\ - val_value_lessdef - (Values.Val.of_optbool - (Op.eval_condition cond - (map (fun r : positive => Registers.Regmap.get r rs) args) m)) v'. - Admitted. -*) (** The proof of semantic preservation for the translation of instructions is a simulation argument based on diagrams of the following form: << |