From 5e74413490019b0909f248ec2e0c331f11be6f5d Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Thu, 7 Oct 2021 19:48:51 +0100 Subject: RTLPargen now uses Abstr as symbolic execution target --- src/hls/RTLPargen.v | 706 +--------------------------------------------------- 1 file changed, 1 insertion(+), 705 deletions(-) diff --git a/src/hls/RTLPargen.v b/src/hls/RTLPargen.v index 2f24a42..fee24f3 100644 --- a/src/hls/RTLPargen.v +++ b/src/hls/RTLPargen.v @@ -31,321 +31,7 @@ Require Import vericert.hls.RTLBlock. Require Import vericert.hls.RTLPar. Require Import vericert.hls.RTLBlockInstr. -#[local] -Open Scope positive. - -(*| -Schedule Oracle -=============== - -This oracle determines if a schedule was valid by performing symbolic execution on the input and -output and showing that these behave the same. This acts on each basic block separately, as the -rest of the functions should be equivalent. -|*) - -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}. -Proof. - decide equality; apply Pos.eq_dec. -Defined. - -Lemma comparison_eq: forall (x y : comparison), {x = y} + {x <> y}. -Proof. - decide equality. -Defined. - -Lemma condition_eq: forall (x y : Op.condition), {x = y} + {x <> y}. -Proof. - generalize comparison_eq; intro. - generalize Int.eq_dec; intro. - generalize Int64.eq_dec; intro. - decide equality. -Defined. - -Lemma addressing_eq : forall (x y : Op.addressing), {x = y} + {x <> y}. -Proof. - generalize Int.eq_dec; intro. - generalize AST.ident_eq; intro. - generalize Z.eq_dec; intro. - generalize Ptrofs.eq_dec; intro. - decide equality. -Defined. - -Lemma typ_eq : forall (x y : AST.typ), {x = y} + {x <> y}. -Proof. - decide equality. -Defined. - -Lemma operation_eq: forall (x y : Op.operation), {x = y} + {x <> y}. -Proof. - generalize Int.eq_dec; intro. - generalize Int64.eq_dec; intro. - generalize Float.eq_dec; intro. - generalize Float32.eq_dec; intro. - generalize AST.ident_eq; intro. - generalize condition_eq; intro. - generalize addressing_eq; intro. - generalize typ_eq; intro. - decide equality. -Defined. - -Lemma memory_chunk_eq : forall (x y : AST.memory_chunk), {x = y} + {x <> y}. -Proof. - decide equality. -Defined. - -Lemma list_typ_eq: forall (x y : list AST.typ), {x = y} + {x <> y}. -Proof. - generalize typ_eq; intro. - decide equality. -Defined. - -Lemma option_typ_eq : forall (x y : option AST.typ), {x = y} + {x <> y}. -Proof. - generalize typ_eq; intro. - decide equality. -Defined. - -Lemma signature_eq: forall (x y : AST.signature), {x = y} + {x <> y}. -Proof. - repeat decide equality. -Defined. - -Lemma list_operation_eq : forall (x y : list Op.operation), {x = y} + {x <> y}. -Proof. - generalize operation_eq; intro. - decide equality. -Defined. - -Lemma list_reg_eq : forall (x y : list reg), {x = y} + {x <> y}. -Proof. - generalize Pos.eq_dec; intros. - decide equality. -Defined. - -Lemma sig_eq : forall (x y : AST.signature), {x = y} + {x <> y}. -Proof. - repeat decide equality. -Defined. - -Lemma instr_eq: forall (x y : instr), {x = y} + {x <> y}. -Proof. - generalize Pos.eq_dec; intro. - generalize typ_eq; intro. - generalize Int.eq_dec; intro. - generalize memory_chunk_eq; intro. - generalize addressing_eq; intro. - generalize operation_eq; intro. - generalize condition_eq; intro. - generalize signature_eq; intro. - generalize list_operation_eq; intro. - generalize list_reg_eq; intro. - generalize AST.ident_eq; intro. - repeat decide equality. -Defined. - -Lemma cf_instr_eq: forall (x y : cf_instr), {x = y} + {x <> y}. -Proof. - generalize Pos.eq_dec; intro. - generalize typ_eq; intro. - generalize Int.eq_dec; intro. - generalize Int64.eq_dec; intro. - generalize Float.eq_dec; intro. - generalize Float32.eq_dec; intro. - generalize Ptrofs.eq_dec; intro. - generalize memory_chunk_eq; intro. - generalize addressing_eq; intro. - generalize operation_eq; intro. - generalize condition_eq; intro. - generalize signature_eq; intro. - generalize list_operation_eq; intro. - generalize list_reg_eq; intro. - generalize AST.ident_eq; intro. - repeat decide equality. -Defined. - -(*| -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. - Proof. destruct x; destruct y; crush. Qed. - - 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. - -- 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. - -Then, to make recursion over expressions easier, expression_list is also defined in the datatype, as -that enables mutual recursive definitions over the datatypes. -|*) - -Definition unsat p := forall a, sat_predicate p a = false. -Definition sat p := exists a, sat_predicate p a = true. - -Inductive expression : Type := -| Ebase : resource -> expression -| Eop : Op.operation -> expression_list -> expression -> 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 -> expression -with expression_list : Type := -| Enil : expression_list -| Econs : expression -> expression_list -> expression_list -. - -(*Inductive pred_expr : Type := -| PEsingleton : option pred_op -> expression -> pred_expr -| PEcons : option pred_op -> expression -> pred_expr -> pred_expr.*) - -Module NonEmpty. - -Inductive non_empty (A: Type) := -| singleton : A -> non_empty A -| cons : A -> non_empty A -> non_empty A -. - -Arguments singleton [A]. -Arguments cons [A]. - -Declare Scope non_empty_scope. -Delimit Scope non_empty_scope with non_empty. - -Module NonEmptyNotation. -Infix "::|" := cons (at level 60, right associativity) : non_empty_scope. -End NonEmptyNotation. -Import 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. - -End NonEmpty. - -Module NE := NonEmpty. -Import NE.NonEmptyNotation. - -#[local] Open Scope non_empty_scope. - -Definition predicated A := NE.non_empty (option pred_op * A). - -Definition pred_expr := predicated expression. - -Definition pred_list_wf l : Prop := - forall a b, In (Some a) l -> In (Some b) l -> a <> b -> unsat (Pand a b). - -Definition pred_list_wf_ep (l: pred_expr) : Prop := - pred_list_wf (NE.to_list (NE.map fst l)). - -Lemma unsat_correct1 : - forall a b c, - unsat (Pand a b) -> - sat_predicate a c = true -> - sat_predicate b c = false. -Proof. - unfold unsat in *. intros. - simplify. specialize (H c). - apply andb_false_iff in H. inv H. rewrite H0 in H1. discriminate. - auto. -Qed. - -Lemma unsat_correct2 : - forall a b c, - unsat (Pand a b) -> - sat_predicate b c = true -> - sat_predicate a c = false. -Proof. - unfold unsat in *. intros. - simplify. specialize (H c). - apply andb_false_iff in H. inv H. auto. rewrite H0 in H1. discriminate. -Qed. - -Lemma unsat_not a: unsat (Pand a (Pnot a)). -Proof. unfold unsat; simplify; auto with bool. Qed. - -Lemma unsat_commut a b: unsat (Pand a b) -> unsat (Pand b a). -Proof. unfold unsat; simplify; eauto with bool. Qed. - -Lemma sat_dec a n b: sat_pred n a = Some b -> {sat a} + {unsat a}. -Proof. - unfold sat, unsat. destruct b. - intros. left. destruct s. - exists (Sat.interp_alist x). auto. - intros. tauto. -Qed. - -Lemma sat_equiv : - forall a b, - unsat (Por (Pand a (Pnot b)) (Pand (Pnot a) b)) -> - forall c, sat_predicate a c = sat_predicate b c. -Proof. - unfold unsat. intros. specialize (H c); simplify. - destruct (sat_predicate b c) eqn:X; - destruct (sat_predicate a c) eqn:X2; - crush. -Qed. +#[local] Open Scope positive. (*Parameter op_le : Op.operation -> Op.operation -> bool. Parameter chunk_le : AST.memory_chunk -> AST.memory_chunk -> bool. @@ -435,396 +121,6 @@ with eplist_le (e1 e2: expr_pred_list) : bool := end .*) -(*| -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 (None, (Ebase v)) - | Some v' => v' - end. - -Notation "a # b" := (get_forest b a) (at level 1). -Notation "a # b <- c" := (Rtree.set b c a) (at level 1, b at next level). - -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} (genv : Genv.t A unit). - -Inductive sem_value : - val -> instr_state -> expression -> val -> Prop := -| Sbase_reg: - forall sp rs r m pr, - sem_value sp (mk_instr_state rs pr m) (Ebase (Reg r)) (rs !! r) -| Sop: - forall rs m op args v lv sp m' mem_exp pr, - sem_mem sp (mk_instr_state rs pr m) mem_exp m' -> - sem_val_list sp (mk_instr_state rs pr m) args lv -> - Op.eval_operation genv sp op lv m' = Some v -> - sem_value sp (mk_instr_state rs pr m) (Eop op args mem_exp) v -| Sload : - forall st mem_exp addr chunk args a v m' lv sp, - sem_mem sp st mem_exp m' -> - sem_val_list sp st args lv -> - Op.eval_addressing genv sp addr lv = Some a -> - Memory.Mem.loadv chunk m' a = Some v -> - sem_value sp st (Eload chunk addr args mem_exp) v -with sem_pred : - val -> instr_state -> expression -> bool -> Prop := -| Spred: - forall st mem_exp args c lv m' v sp, - sem_mem sp st mem_exp m' -> - sem_val_list sp st args lv -> - Op.eval_condition c lv m' = Some v -> - sem_pred sp st (Esetpred c args mem_exp) v -| Sbase_pred: - forall rs pr m p sp, - sem_pred sp (mk_instr_state rs pr m) (Ebase (Pred p)) (pr !! p) -with sem_mem : - val -> instr_state -> expression -> Memory.mem -> Prop := -| Sstore : - forall st mem_exp val_exp m'' addr v a m' chunk args lv sp, - sem_mem sp st mem_exp m' -> - sem_value sp st val_exp v -> - sem_val_list sp st args lv -> - Op.eval_addressing genv sp addr lv = Some a -> - Memory.Mem.storev chunk m' a v = Some m'' -> - sem_mem sp st (Estore val_exp chunk addr args mem_exp) m'' -| Sbase_mem : - forall rs m sp pr, - sem_mem sp (mk_instr_state rs pr m) (Ebase Mem) m -with sem_val_list : - val -> instr_state -> expression_list -> list val -> Prop := -| Snil : - forall st sp, - sem_val_list sp st Enil nil -| Scons : - forall st e v l lv sp, - sem_value sp st e v -> - sem_val_list sp st l lv -> - sem_val_list sp st (Econs e l) (v :: lv) -. - -Inductive sem_pred_expr {A: Type} (sem: val -> instr_state -> expression -> A -> Prop): - val -> instr_state -> pred_expr -> A -> Prop := -| sem_pred_expr_base : - forall sp st e v, - sem sp st e v -> - sem_pred_expr sem sp st (NE.singleton (None, e)) v -| sem_pred_expr_p : - forall sp st e p v, - eval_predf (instr_st_predset st) p = true -> - sem sp st e v -> - sem_pred_expr sem sp st (NE.singleton (Some p, e)) v -| sem_pred_expr_cons_true : - forall sp st e pr p' v, - eval_predf (instr_st_predset st) pr = true -> - sem sp st e v -> - sem_pred_expr sem sp st ((Some pr, e)::|p') v -| sem_pred_expr_cons_false : - forall sp st e pr p' v, - eval_predf (instr_st_predset st) pr = false -> - sem_pred_expr sem sp st p' v -> - sem_pred_expr sem sp st ((Some pr, e)::|p') v -| sem_pred_expr_cons_None : - forall sp st e p' v, - sem sp st e v -> - sem_pred_expr sem sp st ((None, e)::|p') v -. - -Definition collapse_pe (p: pred_expr) : option expression := - match p with - | NE.singleton (None, p) => Some p - | _ => None - end. - -Inductive sem_predset : - val -> instr_state -> forest -> predset -> Prop := -| Spredset: - forall st f sp rs', - (forall pe x, - collapse_pe (f # (Pred x)) = Some pe -> - sem_pred sp st pe (rs' !! x)) -> - sem_predset sp st f rs'. - -Inductive sem_regset : - val -> instr_state -> forest -> regset -> Prop := -| Sregset: - forall st f sp rs', - (forall x, sem_pred_expr sem_value sp st (f # (Reg x)) (rs' !! x)) -> - sem_regset sp st f rs'. - -Inductive sem : - val -> instr_state -> forest -> instr_state -> Prop := -| Sem: - forall st rs' m' f sp pr', - sem_regset sp st f rs' -> - sem_predset sp st f pr' -> - sem_pred_expr sem_mem sp st (f # Mem) m' -> - sem sp st 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 exp1, Eop op2 el2 exp2 => - 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 m1, Esetpred c2 el2 m2 => - 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. -Proof. - intro e1; - apply expression_ind2 with - (P := fun (e1 : expression) => - forall e2, beq_expression e1 e2 = true -> e1 = e2) - (P0 := fun (e1 : expression_list) => - forall e2, beq_expression_list e1 e2 = true -> e1 = e2); - try solve [repeat match goal with - | [ H : context[match ?x with _ => _ end] |- _ ] => destruct x eqn:? - | [ H : context[if ?x then _ else _] |- _ ] => destruct x eqn:? - end; subst; f_equal; crush; eauto using Peqb_true_eq]. - destruct e2; try discriminate. eauto. -Abort. - -Definition hash_tree := PTree.t expression. - -Definition find_tree (el: expression) (h: hash_tree) : option positive := - match filter (fun x => beq_expression el (snd x)) (PTree.elements h) with - | (p, _) :: nil => Some p - | _ => None - end. - -Definition combine_option {A} (a b: option A) : option A := - match a, b with - | Some a', _ => Some a' - | _, Some b' => Some b' - | _, _ => None - end. - -Definition max_key {A} (t: PTree.t A) := - fold_right Pos.max 1%positive (map fst (PTree.elements t)). - -Definition hash_expr (max: predicate) (e: expression) (h: hash_tree): predicate * hash_tree := - match find_tree e h with - | Some p => (p, h) - | None => - let nkey := Pos.max max (max_key h) + 1 in - (nkey, PTree.set nkey e h) - end. - -Fixpoint encode_expression (max: predicate) (pe: pred_expr) (h: hash_tree): pred_op * hash_tree := - match pe with - | NE.singleton (None, e) => - let (p, h') := hash_expr max e h in - (Pvar p, h') - | NE.singleton (Some p, e) => - let (p', h') := hash_expr max e h in - (Por (Pnot p) (Pvar p'), h') - | (Some p, e)::|pe' => - let (p', h') := hash_expr max e h in - let (p'', h'') := encode_expression max pe' h' in - (Pand (Por (Pnot p) (Pvar p')) p'', h'') - | (None, e)::|pe' => - let (p', h') := hash_expr max e h in - let (p'', h'') := encode_expression max pe' h' in - (Pand (Pvar p') p'', h'') - end. - -Fixpoint max_predicate (p: pred_op) : positive := - match p with - | Pvar p => p - | Pand a b => Pos.max (max_predicate a) (max_predicate b) - | Por a b => Pos.max (max_predicate a) (max_predicate b) - | Pnot a => max_predicate a - end. - -Fixpoint max_pred_expr (pe: pred_expr) : positive := - match pe with - | NE.singleton (None, _) => 1 - | NE.singleton (Some p, _) => max_predicate p - | (Some p, _) ::| pe' => Pos.max (max_predicate p) (max_pred_expr pe') - | (None, _) ::| pe' => (max_pred_expr pe') - end. - -Definition beq_pred_expr (bound: nat) (pe1 pe2: pred_expr) : bool := - match pe1, pe2 with - (*| PEsingleton None e1, PEsingleton None e2 => beq_expression e1 e2 - | PEsingleton (Some p1) e1, PEsingleton (Some p2) e2 => - if beq_expression e1 e2 - then match sat_pred_simple bound (Por (Pand p1 (Pnot p2)) (Pand p2 (Pnot p1))) with - | Some None => true - | _ => false - end - else false - | PEsingleton (Some p) e1, PEsingleton None e2 - | PEsingleton None e1, PEsingleton (Some p) e2 => - if beq_expression e1 e2 - then match sat_pred_simple bound (Pnot p) with - | Some None => true - | _ => false - end - else false*) - | 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 - match sat_pred_simple bound (Por (Pand p1 (Pnot p2)) (Pand p2 (Pnot p1))) with - | Some None => true - | _ => false - end - end. - -Definition empty : forest := Rtree.empty _. - -Definition check := Rtree.beq (beq_pred_expr 10000). - -Compute (check (empty # (Reg 2) <- - (((Some (Pand (Pvar 4) (Pnot (Pvar 4)))), (Ebase (Reg 9))) ::| - (NE.singleton ((Some (Pvar 2)), (Ebase (Reg 3)))))) - (empty # (Reg 2) <- (NE.singleton ((Some (Por (Pvar 2) (Pand (Pvar 3) (Pnot (Pvar 3))))), - (Ebase (Reg 3)))))). - -Lemma check_correct: forall (fa fb : forest), - check fa fb = true -> (forall x, fa # x = fb # x). -Proof. - (*unfold check, get_forest; intros; - pose proof beq_expression_correct; - match goal with - [ Hbeq : context[Rtree.beq], y : Rtree.elt |- _ ] => - apply (Rtree.beq_sound beq_expression fa fb) with (x := y) in Hbeq - end; - repeat destruct_match; crush. -Qed.*) - Abort. - -Lemma get_empty: - forall r, empty#r = NE.singleton (None, Ebase r). -Proof. - intros; unfold get_forest; - destruct_match; auto; [ ]; - match goal with - [ H : context[Rtree.get _ empty] |- _ ] => rewrite Rtree.gempty in H - end; discriminate. -Qed. - -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). -Proof. - induction m1; intros. - - simpl. rewrite PTree.bempty_correct. split; intros. - rewrite PTree.gleaf. rewrite H. auto. - generalize (H x). rewrite PTree.gleaf. destruct (PTree.get x m2); tauto. - - destruct m2. - + unfold beq2. rewrite PTree.bempty_correct. split; intros. - rewrite H. rewrite PTree.gleaf. auto. - generalize (H x). rewrite PTree.gleaf. - destruct (PTree.get x (PTree.Node m1_1 o m1_2)); tauto. - + simpl. split; intros. - * destruct (andb_prop _ _ H). destruct (andb_prop _ _ H0). - rewrite IHm1_1 in H3. rewrite IHm1_2 in H1. - destruct x; simpl. apply H1. apply H3. - destruct o; destruct o0; auto || congruence. - * apply andb_true_intro. split. apply andb_true_intro. split. - generalize (H xH); simpl. destruct o; destruct o0; tauto. - apply IHm1_1. intros; apply (H (xO x)). - apply IHm1_2. intros; apply (H (xI x)). -Qed. - -Lemma map1: - forall w dst dst', - dst <> dst' -> - (empty # dst <- w) # dst' = NE.singleton (None, Ebase dst'). -Proof. intros; unfold get_forest; rewrite Rtree.gso; auto; apply get_empty. Qed. - -Lemma genmap1: - forall (f : forest) w dst dst', - dst <> dst' -> - (f # dst <- w) # dst' = f # dst'. -Proof. intros; unfold get_forest; rewrite Rtree.gso; auto. Qed. - -Lemma map2: - forall (v : pred_expr) x rs, - (rs # x <- v) # x = v. -Proof. intros; unfold get_forest; rewrite Rtree.gss; trivial. Qed. - -Lemma tri1: - forall x y, - Reg x <> Reg y -> x <> y. -Proof. crush. Qed. - 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) -- cgit