vericert.hls.Abstr
#[local] Open Scope positive.
#[local] Open Scope pred_op.
Schedule Oracle
Definition reg := positive.
Inductive resource : Set :=
| Reg : reg -> resource
| Pred : reg -> resource
| Mem : resource.
The following defines quite a few equality comparisons automatically, however, these can be
optimised heavily if written manually, as their proofs are not needed.
Lemma resource_eq : forall (r1 r2 : resource), {r1 = r2} + {r1 <> r2}.
Lemma comparison_eq: forall (x y : comparison), {x = y} + {x <> y}.
Lemma condition_eq: forall (x y : Op.condition), {x = y} + {x <> y}.
Lemma addressing_eq : forall (x y : Op.addressing), {x = y} + {x <> y}.
Lemma typ_eq : forall (x y : AST.typ), {x = y} + {x <> y}.
Lemma operation_eq: forall (x y : Op.operation), {x = y} + {x <> y}.
Lemma memory_chunk_eq : forall (x y : AST.memory_chunk), {x = y} + {x <> y}.
Lemma list_typ_eq: forall (x y : list AST.typ), {x = y} + {x <> y}.
Lemma option_typ_eq : forall (x y : option AST.typ), {x = y} + {x <> y}.
Lemma signature_eq: forall (x y : AST.signature), {x = y} + {x <> y}.
Lemma list_operation_eq : forall (x y : list Op.operation), {x = y} + {x <> y}.
Lemma list_reg_eq : forall (x y : list reg), {x = y} + {x <> y}.
Lemma sig_eq : forall (x y : AST.signature), {x = y} + {x <> y}.
Lemma instr_eq: forall (x y : instr), {x = y} + {x <> y}.
Lemma cf_instr_eq: forall (x y : cf_instr), {x = y} + {x <> y}.
We then create equality lemmas for a resource and a module to index resources uniquely. The
indexing is done by setting Mem to 1, whereas all other infinitely many registers will all be
shifted right by 1. This means that they will never overlap.
Module R_indexed.
Definition t := resource.
Definition index (rs: resource) : positive :=
match rs with
| Reg r => xO (xO r)
| Pred r => xI (xI r)
| Mem => 1%positive
end.
Lemma index_inj: forall (x y: t), index x = index y -> x = y.
Definition eq := resource_eq.
End R_indexed.
We can then create expressions that mimic the expressions defined in RTLBlock and RTLPar, which use
expressions instead of registers as their inputs and outputs. This means that we can accumulate all
the results of the operations as general expressions that will be present in those registers.
Then, to make recursion over expressions easier, expression_list is also defined in the datatype, as
that enables mutual recursive definitions over the datatypes.
- Ebase: the starting value of the register.
- Eop: Some arithmetic operation on a number of registers.
- Eload: A load from a memory location into a register.
- Estore: A store from a register to a memory location.
Inductive expression : Type :=
| Ebase : resource -> expression
| Eop : Op.operation -> expression_list -> expression
| Eload : AST.memory_chunk -> Op.addressing -> expression_list -> expression -> expression
| Estore : expression -> AST.memory_chunk -> Op.addressing -> expression_list -> expression -> expression
| Esetpred : Op.condition -> expression_list -> expression
with expression_list : Type :=
| Enil : expression_list
| Econs : expression -> expression_list -> expression_list
.
Module NonEmpty.
Inductive non_empty (A: Type) :=
| singleton : A -> non_empty A
| cons : A -> non_empty A -> non_empty A
.
Module NonEmptyNotation.
Infix "::|" := cons (at level 60, right associativity) : non_empty_scope.
End NonEmptyNotation.
#[local] Open Scope non_empty_scope.
Fixpoint map {A B} (f: A -> B) (l: non_empty A): non_empty B :=
match l with
| singleton a => singleton (f a)
| a ::| b => f a ::| map f b
end.
Fixpoint to_list {A} (l: non_empty A): list A :=
match l with
| singleton a => a::nil
| a ::| b => a :: to_list b
end.
Fixpoint app {A} (l1 l2: non_empty A) :=
match l1 with
| singleton a => a ::| l2
| a ::| b => a ::| app b l2
end.
Fixpoint non_empty_prod {A B} (l: non_empty A) (l': non_empty B) :=
match l with
| singleton a => map (fun x => (a, x)) l'
| a ::| b => app (map (fun x => (a, x)) l') (non_empty_prod b l')
end.
Fixpoint of_list {A} (l: list A): option (non_empty A) :=
match l with
| a::b =>
match of_list b with
| Some b' => Some (a ::| b')
| _ => None
end
| nil => None
end.
Fixpoint replace {A} (f: A -> A -> bool) (a b: A) (l: non_empty A) :=
match l with
| a' ::| l' => if f a a' then b ::| replace f a b l' else a' ::| replace f a b l'
| singleton a' => if f a a' then singleton b else singleton a'
end.
Inductive In {A: Type} (x: A) : non_empty A -> Prop :=
| In_cons : forall a b, x = a \/ In x b -> In x (a ::| b)
| In_single : In x (singleton x).
Lemma in_dec:
forall A (a: A) (l: non_empty A),
(forall a b: A, {a = b} + {a <> b}) ->
{In a l} + {~ In a l}.
End NonEmpty.
Module NE := NonEmpty.
#[local] Open Scope non_empty_scope.
Definition predicated A := NE.non_empty (pred_op * A).
Definition pred_expr := predicated expression.
Using IMap we can create a map from resources to any other type, as resources can be uniquely
identified as positive numbers.
Module Rtree := ITree(R_indexed).
Definition forest : Type := Rtree.t pred_expr.
Definition get_forest v (f: forest) :=
match Rtree.get v f with
| None => NE.singleton (T, (Ebase v))
| Some v' => v'
end.
Notation "a # b" := (get_forest b a) (at level 1) : forest.
Notation "a # b <- c" := (Rtree.set b c a) (at level 1, b at next level) : forest.
#[local] Open Scope forest.
Definition maybe {A: Type} (vo: A) (pr: predset) p (v: A) :=
match p with
| Some p' => if eval_predf pr p' then v else vo
| None => v
end.
Definition get_pr i := match i with mk_instr_state a b c => b end.
Definition get_m i := match i with mk_instr_state a b c => c end.
Definition eval_predf_opt pr p :=
match p with Some p' => eval_predf pr p' | None => true end.
Finally we want to define the semantics of execution for the expressions with symbolic values,
so the result of executing the expressions will be an expressions.
Section SEMANTICS.
Context {A : Type}.
Record ctx : Type := mk_ctx {
ctx_is: instr_state;
ctx_sp: val;
ctx_ge: Genv.t A unit;
}.
Definition ctx_rs ctx := is_rs (ctx_is ctx).
Definition ctx_ps ctx := is_ps (ctx_is ctx).
Definition ctx_mem ctx := is_mem (ctx_is ctx).
Inductive sem_value : ctx -> expression -> val -> Prop :=
| Sbase_reg:
forall r ctx,
sem_value ctx (Ebase (Reg r)) ((ctx_rs ctx) !! r)
| Sop:
forall ctx op args v lv,
sem_val_list ctx args lv ->
Op.eval_operation (ctx_ge ctx) (ctx_sp ctx) op lv (ctx_mem ctx) = Some v ->
sem_value ctx (Eop op args) v
| Sload :
forall ctx mexp addr chunk args a v m' lv,
sem_mem ctx mexp m' ->
sem_val_list ctx args lv ->
Op.eval_addressing (ctx_ge ctx) (ctx_sp ctx) addr lv = Some a ->
Memory.Mem.loadv chunk m' a = Some v ->
sem_value ctx (Eload chunk addr args mexp) v
with sem_pred : ctx -> expression -> bool -> Prop :=
| Spred:
forall ctx args c lv v,
sem_val_list ctx args lv ->
Op.eval_condition c lv (ctx_mem ctx) = Some v ->
sem_pred ctx (Esetpred c args) v
| Sbase_pred:
forall ctx p,
sem_pred ctx (Ebase (Pred p)) ((ctx_ps ctx) !! p)
with sem_mem : ctx -> expression -> Memory.mem -> Prop :=
| Sstore :
forall ctx mexp vexp chunk addr args lv v a m' m'',
sem_mem ctx mexp m' ->
sem_value ctx vexp v ->
sem_val_list ctx args lv ->
Op.eval_addressing (ctx_ge ctx) (ctx_sp ctx) addr lv = Some a ->
Memory.Mem.storev chunk m' a v = Some m'' ->
sem_mem ctx (Estore vexp chunk addr args mexp) m''
| Sbase_mem :
forall ctx,
sem_mem ctx (Ebase Mem) (ctx_mem ctx)
with sem_val_list : ctx -> expression_list -> list val -> Prop :=
| Snil :
forall ctx,
sem_val_list ctx Enil nil
| Scons :
forall ctx e v l lv,
sem_value ctx e v ->
sem_val_list ctx l lv ->
sem_val_list ctx (Econs e l) (v :: lv)
.
Inductive sem_pred_expr {B: Type} (sem: ctx -> expression -> B -> Prop):
ctx -> pred_expr -> B -> Prop :=
| sem_pred_expr_cons_true :
forall ctx e pr p' v,
eval_predf (ctx_ps ctx) pr = true ->
sem ctx e v ->
sem_pred_expr sem ctx ((pr, e) ::| p') v
| sem_pred_expr_cons_false :
forall ctx e pr p' v,
eval_predf (ctx_ps ctx) pr = false ->
sem_pred_expr sem ctx p' v ->
sem_pred_expr sem ctx ((pr, e) ::| p') v
| sem_pred_expr_single :
forall ctx e pr v,
eval_predf (ctx_ps ctx) pr = true ->
sem ctx e v ->
sem_pred_expr sem ctx (NE.singleton (pr, e)) v
.
Definition collapse_pe (p: pred_expr) : option expression :=
match p with
| NE.singleton (T, p) => Some p
| _ => None
end.
Inductive sem_predset : ctx -> forest -> predset -> Prop :=
| Spredset:
forall ctx f rs',
(forall x, sem_pred_expr sem_pred ctx (f # (Pred x)) (rs' !! x)) ->
sem_predset ctx f rs'.
Inductive sem_regset : ctx -> forest -> regset -> Prop :=
| Sregset:
forall ctx f rs',
(forall x, sem_pred_expr sem_value ctx (f # (Reg x)) (rs' !! x)) ->
sem_regset ctx f rs'.
Inductive sem : ctx -> forest -> instr_state -> Prop :=
| Sem:
forall ctx rs' m' f pr',
sem_regset ctx f rs' ->
sem_predset ctx f pr' ->
sem_pred_expr sem_mem ctx (f # Mem) m' ->
sem ctx f (mk_instr_state rs' pr' m').
End SEMANTICS.
Fixpoint beq_expression (e1 e2: expression) {struct e1}: bool :=
match e1, e2 with
| Ebase r1, Ebase r2 => if resource_eq r1 r2 then true else false
| Eop op1 el1, Eop op2 el2 =>
if operation_eq op1 op2 then
beq_expression_list el1 el2 else false
| Eload chk1 addr1 el1 e1, Eload chk2 addr2 el2 e2 =>
if memory_chunk_eq chk1 chk2
then if addressing_eq addr1 addr2
then if beq_expression_list el1 el2
then beq_expression e1 e2 else false else false else false
| Estore e1 chk1 addr1 el1 m1, Estore e2 chk2 addr2 el2 m2 =>
if memory_chunk_eq chk1 chk2
then if addressing_eq addr1 addr2
then if beq_expression_list el1 el2
then if beq_expression m1 m2
then beq_expression e1 e2 else false else false else false else false
| Esetpred c1 el1, Esetpred c2 el2 =>
if condition_eq c1 c2
then beq_expression_list el1 el2 else false
| _, _ => false
end
with beq_expression_list (el1 el2: expression_list) {struct el1} : bool :=
match el1, el2 with
| Enil, Enil => true
| Econs e1 t1, Econs e2 t2 => beq_expression e1 e2 && beq_expression_list t1 t2
| _, _ => false
end
.
Scheme expression_ind2 := Induction for expression Sort Prop
with expression_list_ind2 := Induction for expression_list Sort Prop.
Lemma beq_expression_correct:
forall e1 e2, beq_expression e1 e2 = true -> e1 = e2.
Lemma beq_expression_refl: forall e, beq_expression e e = true.
Lemma beq_expression_list_refl: forall e, beq_expression_list e e = true.
Lemma beq_expression_correct2:
forall e1 e2, beq_expression e1 e2 = false -> e1 <> e2.
Lemma expression_dec: forall e1 e2: expression, {e1 = e2} + {e1 <> e2}.
Definition pred_expr_item_eq (pe1 pe2: pred_op * expression) : bool :=
@equiv_dec _ SATSetoid _ (fst pe1) (fst pe2) && beq_expression (snd pe1) (snd pe2).
Lemma pred_expr_dec: forall (pe1 pe2: pred_op * expression),
{pred_expr_item_eq pe1 pe2 = true} + {pred_expr_item_eq pe1 pe2 = false}.
Lemma pred_expr_dec2: forall (pe1 pe2: pred_op * expression),
{pred_expr_item_eq pe1 pe2 = true} + {~ pred_expr_item_eq pe1 pe2 = true}.
Module HashExpr <: Hashable.
Definition t := expression.
Definition eq_dec := expression_dec.
End HashExpr.
Module HT := HashTree(HashExpr).
Definition combine_option {A} (a b: option A) : option A :=
match a, b with
| Some a', _ => Some a'
| _, Some b' => Some b'
| _, _ => None
end.
Fixpoint norm_expression (max: predicate) (pe: pred_expr) (h: hash_tree)
: (PTree.t pred_op) * hash_tree :=
match pe with
| NE.singleton (p, e) =>
let (p', h') := hash_value max e h in
(PTree.set p' p (PTree.empty _), h')
| (p, e) ::| pr =>
let (p', h') := hash_value max e h in
let (p'', h'') := norm_expression max pr h' in
match p'' ! p' with
| Some pr_op =>
(PTree.set p' (pr_op ∨ p) p'', h'')
| None =>
(PTree.set p' p p'', h'')
end
end.
Definition mk_pred_stmnt' e p_e := ¬ p_e ∨ Plit (true, e).
Definition mk_pred_stmnt t := PTree.fold (fun x a b => mk_pred_stmnt' a b ∧ x) t T.
Definition mk_pred_stmnt_l (t: list (predicate * pred_op)) := fold_left (fun x a => uncurry mk_pred_stmnt' a ∧ x) t T.
Definition encode_expression max pe h :=
let (tree, h) := norm_expression max pe h in
(mk_pred_stmnt tree, h).
Fixpoint max_pred_expr (pe: pred_expr) : positive :=
match pe with
| NE.singleton (p, e) => max_predicate p
| (p, e) ::| pe' => Pos.max (max_predicate p) (max_pred_expr pe')
end.
Definition empty : forest := Rtree.empty _.
Definition ge_preserved {A B C D: Type} (ge: Genv.t A B) (tge: Genv.t C D) : Prop :=
(forall sp op vl m, Op.eval_operation ge sp op vl m =
Op.eval_operation tge sp op vl m)
/\ (forall sp addr vl, Op.eval_addressing ge sp addr vl =
Op.eval_addressing tge sp addr vl).
Lemma ge_preserved_same:
forall A B ge, @ge_preserved A B A B ge ge.
#[local] Hint Resolve ge_preserved_same : core.
Inductive match_states : instr_state -> instr_state -> Prop :=
| match_states_intro:
forall ps ps' rs rs' m m',
(forall x, rs !! x = rs' !! x) ->
(forall x, ps !! x = ps' !! x) ->
m = m' ->
match_states (mk_instr_state rs ps m) (mk_instr_state rs' ps' m').
Lemma match_states_refl x : match_states x x.
Lemma match_states_commut x y : match_states x y -> match_states y x.
Lemma match_states_trans x y z :
match_states x y -> match_states y z -> match_states x z.
#[global]
Instance match_states_Equivalence : Equivalence match_states :=
{ Equivalence_Reflexive := match_states_refl ;
Equivalence_Symmetric := match_states_commut ;
Equivalence_Transitive := match_states_trans ; }.
Inductive similar {A B} : @ctx A -> @ctx B -> Prop :=
| similar_intro :
forall ist ist' sp ge tge,
ge_preserved ge tge ->
match_states ist ist' ->
similar (mk_ctx ist sp ge) (mk_ctx ist' sp tge).
Definition beq_pred_expr_once (pe1 pe2: pred_expr) : bool :=
match pe1, pe2 with
| pe1, pe2 =>
let max := Pos.max (max_pred_expr pe1) (max_pred_expr pe2) in
let (p1, h) := encode_expression max pe1 (PTree.empty _) in
let (p2, h') := encode_expression max pe2 h in
equiv_check p1 p2
end.
Definition forall_ptree {A:Type} (f:positive->A->bool) (m:Maps.PTree.t A) : bool :=
Maps.PTree.fold (fun (res: bool) (i: positive) (x: A) => res && f i x) m true.
Remark ptree_forall:
forall (A: Type) (f: positive -> A -> bool) (m: Maps.PTree.t A),
Maps.PTree.fold (fun (res: bool) (i: positive) (x: A) => res && f i x) m true = true ->
forall i x, Maps.PTree.get i m = Some x -> f i x = true.
Lemma forall_ptree_true:
forall (A: Type) (f: positive -> A -> bool) (m: Maps.PTree.t A),
forall_ptree f m = true ->
forall i x, Maps.PTree.get i m = Some x -> f i x = true.
Definition tree_equiv_check_el (np2: PTree.t pred_op) (n: positive) (p: pred_op): bool :=
match np2 ! n with
| Some p' => equiv_check p p'
| None => equiv_check p ⟂
end.
Definition tree_equiv_check_None_el (np2: PTree.t pred_op) (n: positive) (p: pred_op): bool :=
match np2 ! n with
| Some p' => true
| None => equiv_check p ⟂
end.
Variant sem_pred_tree {A B: Type} (sem: ctx -> expression -> B -> Prop):
@ctx A -> PTree.t expression -> PTree.t pred_op -> B -> Prop :=
| sem_pred_tree_intro :
forall ctx expr e pr v et pt,
eval_predf (ctx_ps ctx) pr = true ->
sem ctx expr v ->
pt ! e = Some pr ->
et ! e = Some expr ->
sem_pred_tree sem ctx et pt v.
Variant predicated_mutexcl {A: Type} : predicated A -> Prop :=
| predicated_mutexcl_intros : forall pe,
(forall x y, NE.In x pe -> NE.In y pe -> x <> y -> fst x ⇒ ¬ fst y) ->
predicated_mutexcl pe.
Lemma hash_value_in :
forall max e et h h0,
hash_value max e et = (h, h0) ->
h0 ! h = Some e.
Lemma norm_expr_constant :
forall x m h t h' e p,
norm_expression m x h = (t, h') ->
h ! e = Some p ->
h' ! e = Some p.
Lemma predicated_cons :
forall A (a:pred_op * A) x,
predicated_mutexcl (a ::| x) ->
predicated_mutexcl x.
Lemma norm_expr_mutexcl :
forall m pe h t h' e e' p p',
norm_expression m pe h = (t, h') ->
predicated_mutexcl pe ->
t ! e = Some p ->
t ! e' = Some p' ->
e <> e' ->
p ⇒ ¬ p'.
Lemma norm_expression_sem_pred :
forall A B sem ctx pe v,
sem_pred_expr sem ctx pe v ->
forall pt et et' max,
predicated_mutexcl pe ->
max_pred_expr pe <= max ->
norm_expression max pe et = (pt, et') ->
@sem_pred_tree A B sem ctx et' pt v.
Lemma norm_expression_sem_pred2 :
forall A B sem ctx v pt et et',
@sem_pred_tree A B sem ctx et' pt v ->
forall pe,
predicated_mutexcl pe ->
norm_expression (max_pred_expr pe) pe et = (pt, et') ->
sem_pred_expr sem ctx pe v.
Definition beq_pred_expr (pe1 pe2: pred_expr) : bool :=
let max := Pos.max (max_pred_expr pe1) (max_pred_expr pe2) in
let (np1, h) := norm_expression max pe1 (PTree.empty _) in
let (np2, h') := norm_expression max pe2 h in
forall_ptree (tree_equiv_check_el np2) np1
&& forall_ptree (tree_equiv_check_None_el np1) np2.
Definition check := Rtree.beq beq_pred_expr.
Lemma inj_asgn_eg : forall a b, (a =? b)%nat = (a =? a)%nat -> a = b.
Lemma inj_asgn :
forall a b, (forall (f: nat -> bool), f a = f b) -> a = b.
Lemma inj_asgn_false:
forall n1 n2 , ~ (forall c: nat -> bool, c n1 = negb (c n2)).
Lemma negb_inj:
forall a b,
negb a = negb b -> a = b.
Lemma sat_predicate_Plit_inj :
forall p1 p2,
Plit p1 == Plit p2 -> p1 = p2.
Definition ind_preds t :=
forall e1 e2 p1 p2 c,
e1 <> e2 ->
t ! e1 = Some p1 ->
t ! e2 = Some p2 ->
sat_predicate p1 c = true ->
sat_predicate p2 c = false.
Definition ind_preds_l t :=
forall (e1: predicate) e2 p1 p2 c,
e1 <> e2 ->
In (e1, p1) t ->
In (e2, p2) t ->
sat_predicate p1 c = true ->
sat_predicate p2 c = false.
Section CORRECT.
Definition fd := @fundef RTLBlock.bb.
Definition tfd := @fundef RTLPar.bb.
Context (ictx: @ctx fd) (octx: @ctx tfd) (HSIM: similar ictx octx).
Lemma sem_value_mem_det:
forall e v v' m m',
(sem_value ictx e v -> sem_value octx e v' -> v = v')
/\ (sem_mem ictx e m -> sem_mem octx e m' -> m = m').
Lemma sem_value_mem_corr:
forall e v m,
(sem_value ictx e v -> sem_value octx e v)
/\ (sem_mem ictx e m -> sem_mem octx e m).
Lemma sem_value_det:
forall e v v',
sem_value ictx e v -> sem_value octx e v' -> v = v'.
Lemma sem_value_corr:
forall e v,
sem_value ictx e v -> sem_value octx e v.
Lemma sem_mem_det:
forall e v v',
sem_mem ictx e v -> sem_mem octx e v' -> v = v'.
Lemma sem_mem_corr:
forall e v,
sem_mem ictx e v -> sem_mem octx e v.
Lemma sem_val_list_det:
forall e l l',
sem_val_list ictx e l -> sem_val_list octx e l' -> l = l'.
Lemma sem_val_list_corr:
forall e l,
sem_val_list ictx e l -> sem_val_list octx e l.
Lemma sem_pred_det:
forall e v v',
sem_pred ictx e v -> sem_pred octx e v' -> v = v'.
Lemma sem_pred_corr:
forall e v,
sem_pred ictx e v -> sem_pred octx e v.
#[local] Opaque PTree.set.
Lemma exists_norm_expr :
forall x pe expr m t h h',
NE.In (pe, expr) x ->
norm_expression m x h = (t, h') ->
exists e pe', t ! e = Some pe' /\ pe ⇒ pe' /\ h' ! e = Some expr.
Lemma norm_expr_implies :
forall x m h t h' e expr p,
norm_expression m x h = (t, h') ->
h' ! e = Some expr ->
t ! e = Some p ->
exists p', NE.In (p', expr) x /\ p' ⇒ p.
Lemma norm_expr_In :
forall A B sem ctx x pe expr v,
@sem_pred_expr A B sem ctx x v ->
NE.In (pe, expr) x ->
eval_predf (ctx_ps ctx) pe = true ->
sem ctx expr v.
Lemma norm_expr_forall_impl :
forall m x h t h' e1 e2 p1 p2,
predicated_mutexcl x ->
norm_expression m x h = (t, h') ->
t ! e1 = Some p1 -> t ! e2 = Some p2 -> e1 <> e2 ->
p1 ⇒ ¬ p2.
Lemma norm_expr_replace :
forall A B sem ctx x pe expr v,
@sem_pred_expr A B sem ctx x v ->
eval_predf (ctx_ps ctx) pe = false ->
@sem_pred_expr A B sem ctx (NE.replace pred_expr_item_eq (pe, expr) (⟂, expr) x) v.
Section SEM_PRED.
Context (B: Type).
Context (isem: @ctx fd -> expression -> B -> Prop).
Context (osem: @ctx tfd -> expression -> B -> Prop).
Context (SEMSIM: forall e v v', isem ictx e v -> osem octx e v' -> v = v').
Lemma check_correct_sem_value:
forall x x' v v' t t' h h',
beq_pred_expr x x' = true ->
predicated_mutexcl x -> predicated_mutexcl x' ->
norm_expression (Pos.max (max_pred_expr x) (max_pred_expr x')) x (PTree.empty _) = (t, h) ->
norm_expression (Pos.max (max_pred_expr x) (max_pred_expr x')) x' h = (t', h') ->
sem_pred_tree isem ictx h t v ->
sem_pred_tree osem octx h' t' v' ->
v = v'.
Lemma check_correct_sem_value2:
forall x x' v v',
beq_pred_expr x x' = true ->
predicated_mutexcl x ->
predicated_mutexcl x' ->
sem_pred_expr isem ictx x v ->
sem_pred_expr osem octx x' v' ->
v = v'.
Lemma check_correct_sem_value3:
forall x x' v v',
beq_pred_expr x x' = true ->
sem_pred_expr isem ictx x v ->
sem_pred_expr osem octx x' v' ->
v = v'.
End SEM_PRED.
Section SEM_PRED_CORR.
Context (B: Type).
Context (isem: @ctx fd -> expression -> B -> Prop).
Context (osem: @ctx tfd -> expression -> B -> Prop).
Context (SEMCORR: forall e v, isem ictx e v -> osem octx e v).
Lemma sem_pred_tree_corr:
forall x x' v t t' h h',
beq_pred_expr x x' = true ->
predicated_mutexcl x -> predicated_mutexcl x' ->
norm_expression (Pos.max (max_pred_expr x) (max_pred_expr x')) x (PTree.empty _) = (t, h) ->
norm_expression (Pos.max (max_pred_expr x) (max_pred_expr x')) x' h = (t', h') ->
sem_pred_tree isem ictx h t v ->
sem_pred_tree osem octx h' t' v.
End SEM_PRED_CORR.
Lemma check_correct: forall (fa fb : forest) i i',
check fa fb = true ->
sem ictx fa i ->
sem octx fb i' ->
match_states i i'.
Lemma check_correct2:
forall (fa fb : forest) i,
check fa fb = true ->
sem ictx fa i ->
exists i', sem octx fb i' /\ match_states i i'.
End CORRECT.
Lemma get_empty:
forall r, empty#r = NE.singleton (T, Ebase r).
Fixpoint beq2 {A B : Type} (beqA : A -> B -> bool) (m1 : PTree.t A) (m2 : PTree.t B) {struct m1} : bool :=
match m1, m2 with
| PTree.Leaf, _ => PTree.bempty m2
| _, PTree.Leaf => PTree.bempty m1
| PTree.Node l1 o1 r1, PTree.Node l2 o2 r2 =>
match o1, o2 with
| None, None => true
| Some y1, Some y2 => beqA y1 y2
| _, _ => false
end
&& beq2 beqA l1 l2 && beq2 beqA r1 r2
end.
Lemma beq2_correct:
forall A B beqA m1 m2,
@beq2 A B beqA m1 m2 = true <->
(forall (x: PTree.elt),
match PTree.get x m1, PTree.get x m2 with
| None, None => True
| Some y1, Some y2 => beqA y1 y2 = true
| _, _ => False
end).
Lemma map1:
forall w dst dst',
dst <> dst' ->
(empty # dst <- w) # dst' = NE.singleton (T, Ebase dst').
Lemma genmap1:
forall (f : forest) w dst dst',
dst <> dst' ->
(f # dst <- w) # dst' = f # dst'.
Lemma map2:
forall (v : pred_expr) x rs,
(rs # x <- v) # x = v.
Lemma tri1:
forall x y,
Reg x <> Reg y -> x <> y.