blob: 3e930439ddeaf32a3893fce80090efdd8e7907e0 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
|
Require Import Coqlib Floats Values Memory.
Require Import Integers.
Require Import Op Registers.
Require Import BTL_SEtheory.
Require Import BTL_SEsimuref.
(** Target op simplifications using "fake" values *)
Definition target_op_simplify (op: operation) (lr: list reg) (hrs: ristate): option sval :=
None.
Definition target_cbranch_expanse (prev: ristate) (cond: condition) (args: list reg) : option (condition * list_sval) :=
None.
(* Main proof of simplification *)
Lemma target_op_simplify_correct ctx op lr hrs fsv st args: forall
(H: target_op_simplify op lr hrs = Some fsv)
(REF: ris_refines ctx hrs st)
(OK0: ris_ok ctx hrs)
(OK1: eval_list_sval ctx (list_sval_inj (map (si_sreg st) lr)) = Some args),
eval_sval ctx fsv = eval_operation (cge ctx) (csp ctx) op args (cm0 ctx).
Proof.
unfold target_op_simplify; simpl.
intros H ? ? ?.
congruence.
Qed.
Lemma target_cbranch_expanse_correct hrs c l ctx st c' l': forall
(TARGET: target_cbranch_expanse hrs c l = Some (c', l'))
(REF: ris_refines ctx hrs st)
(OK: ris_ok ctx hrs),
eval_scondition ctx c' l' =
eval_scondition ctx c (list_sval_inj (map (si_sreg st) l)).
Proof.
unfold target_cbranch_expanse; simpl.
intros H ? ?.
congruence.
Qed.
Global Opaque target_op_simplify.
Global Opaque target_cbranch_expanse.
|
