From 2d4a513b8d0245db8dcac05d9300e44f06d6eca5 Mon Sep 17 00:00:00 2001
From: Anne Pacalet <anne.pacalet@inria.fr>
Date: Fri, 5 Sep 2008 15:24:47 +0000
Subject: [PATCH] M3

---
 doc/wp/Wp.v | 473 +++++++++++++++++++++++++++++++++++++++++++++-------
 1 file changed, 409 insertions(+), 64 deletions(-)

diff --git a/doc/wp/Wp.v b/doc/wp/Wp.v
index 0e1c9dcfd97..1eb1d88c256 100644
--- a/doc/wp/Wp.v
+++ b/doc/wp/Wp.v
@@ -1,6 +1,9 @@
 Require Import String.
 Require Import List.
 
+(*----------------------------------------------------------------------------*)
+(** * Low level memory *)
+
 Parameter MemAddr : Set.
 Parameter Size : Set.
 Parameter BVal : Set.
@@ -12,14 +15,18 @@ Definition MemZone := (MemAddr * Size)%type.
 
 Parameter DisjMemZones : MemZone -> MemZone -> Prop.
 Parameter InclMemZones : MemZone -> MemZone -> Prop.
+
 Axiom InclMemZones_refl : forall z, InclMemZones z z.
 Axiom InclNotDisj : forall z1 z2, InclMemZones z1 z2 -> ~ DisjMemZones z1 z2.
-Axiom InclDisj : forall z1 z1' z2, InclMemZones z1' z1 ->  DisjMemZones z1 z2 -> DisjMemZones z1' z2.
+Axiom InclDisj : forall z1 z1' z2, InclMemZones z1' z1 ->  DisjMemZones z1 z2 
+  -> DisjMemZones z1' z2.
 
 Definition Mem := MemZone -> BVal.
 
+(** when we read a value, it as the requested size *)
 Axiom SizeofR : forall (m:Mem) a sz, SizeofBVal (m (a, sz)) = sz.
 
+(** Write in the memory *)
 Parameter W : Mem -> MemAddr -> BVal -> Mem.
 
 Axiom RWdisj : forall mem a1 v z2,  
@@ -28,9 +35,9 @@ Axiom RWdisj : forall mem a1 v z2,
 Axiom RWsame : forall mem a v z,
   z = (a, SizeofBVal v) -> (W mem a v) z = v.
 
-(** * Models on variables *)
+(*----------------------------------------------------------------------------*)
+(** * Variables, Path and Data *)
 
-(** ** Variables, Path and Data *)
 Parameter Var : Set.
 Parameter eq_var : forall (v1 v2 : Var), {v1=v2}+{v1<>v2}.
 Parameter Field : Set.
@@ -55,19 +62,384 @@ Definition Path := list Proj.
 Definition NoPath : Path := nil.
 Hint Unfold NoPath.
 
+(** ** Elements to compute memory addresses *)
+
+
+(** Address of a variable *)
+Parameter VarAddr : Var -> MemAddr.
+
+(** Add the offset of the field *)
+Parameter AddFieldOffset : MemAddr -> Field -> MemAddr.
+
+Parameter SizeofVarPath : Var -> Path -> Size.
+
+Definition VarZone (v:Var) : MemZone :=
+  (VarAddr v, SizeofVarPath v nil).
+
+Axiom VarZoneDisj : forall v1 v2, DisjMemZones (VarZone v1) (VarZone v2).
+
 (** ** Values *)
 
 Parameter Val : Set.
 
+(** Projection in the value of an object *)
+Parameter ValField : Val ->  Field -> Val.
+
+(** ** To and from bit representation *)
+
+(** Transform a value into its BVal representation *)
+Parameter Bits : Val -> BVal.
+
 (** Notice that Interp needs the type T to transform a BVal
 into a Val of type T. TODO *)
 Parameter Interp : BVal -> Val.
-Parameter Bits : Val -> BVal.
 Axiom InterpBits : forall v, Interp (Bits v) = v.
 Axiom BitsInterp : forall b, Bits (Interp b) = b.
 
-(** Projection in the value of an object *)
-Parameter ValProj : Val ->  Field -> Val.
+(** Interpret a BVal as a MemAddr *)
+Parameter Val2Addr : Val -> MemAddr.
+Definition BVal2Addr b : MemAddr := Val2Addr (Interp b).
+
+(*----------------------------------------------------------------------------*)
+(** * C program *)
+
+(** ** Statements *)
+Parameter OpC : Set.
+
+(** Expressions *)
+Inductive ExpC : Set :=
+  | Ecnst : Val -> ExpC 
+  | Edata : Var -> Path -> ExpC
+  | Eop : ExpC -> OpC -> ExpC -> ExpC 
+.
+
+(** Statements : only assign at the moment *)
+Inductive Stmt : Set :=
+  | Iasgn : Var -> Path -> ExpC -> Stmt
+.
+
+(** ** Statements semantic *)
+
+(** Take the value stored at [p] and interpret it as an address.*)
+Definition IndirAddr (mem:Mem) (p:MemAddr) : MemAddr := 
+  BVal2Addr (mem (p, SizeofPtr)).
+
+(** Recursively compute an address by interpreting the path *)
+Fixpoint PathAddr (mem:Mem) (a:MemAddr) (ch:Path) {struct ch} : MemAddr := 
+  match ch with
+  | nil => a
+  | Pfield proj :: tl => PathAddr mem (AddFieldOffset a proj) tl
+  | Pindir :: tl => PathAddr mem (IndirAddr mem a) tl
+  end.
+
+Lemma PathAddr_split : forall mem a ch1 ch2,
+  PathAddr mem a (ch1++ch2) = PathAddr mem (PathAddr mem a ch1) ch2.
+Proof.
+intros mem a ch1 ch2.
+generalize a.
+induction ch1.
+
+simpl;  auto.
+
+clear a; intro a.
+destruct a0.
+
+simpl PathAddr at 1 3.
+rewrite IHch1; auto.
+
+simpl PathAddr at 1 3.
+rewrite IHch1; auto.
+Qed.
+
+Definition VarPathAddr (mem:Mem) (v:Var) (ch:Path) : MemAddr := 
+  PathAddr mem (VarAddr v) ch.
+
+Parameter EvalOpC : Val -> OpC -> Val -> Val.
+
+Definition EvalVar (mem:Mem) v := 
+  Interp (mem ((VarAddr v), (SizeofVarPath v NoPath))).
+
+Definition EvalIndir (mem:Mem) (a:MemAddr) : Val :=
+  Interp (mem (a, SizeofPtr)).
+
+Fixpoint EvalPath (mem:Mem) (val:Val) (ch:Path) {struct ch} : Val := 
+  match ch with
+| nil => val
+| (Pfield f)::tl =>  EvalPath mem (ValField val f) tl
+| Pindir::tl =>  EvalPath mem (EvalIndir mem (Val2Addr val)) tl
+end.
+
+(** Evaluation of a C expression *)
+Fixpoint EvalExpC mem exp {struct exp} : Val := match exp with
+  | Ecnst val  => val
+  | Edata v ch => EvalPath mem (EvalVar mem v) ch
+  | Eop e1 o e2 => EvalOpC (EvalExpC mem e1) o (EvalExpC mem e2)
+end.
+
+(** Finally, we define how the memory is modified by an assignment *)
+Definition exec m1 s m2 : Prop := match s with
+  | (Iasgn v ch e) =>  m2 = W m1 (VarPathAddr m1 v ch) (Bits (EvalExpC m1 e))
+end.
+
+(*----------------------------------------------------------------------------*)
+(** * Predicates *)
+
+(** ** Definitions *)
+
+(** binary relational operations on expressions to build predicates*)
+Parameter OpR : Set.
+
+(** binary operations on predicates *)
+Parameter OpP : Set.
+
+(** predicates (can take the type of the expressions) *)
+Inductive PredDef (E:Set) : Set :=
+  | Pe : E -> OpR -> E -> PredDef E
+  | Po : PredDef E -> OpP -> PredDef E -> PredDef E
+.
+Implicit Arguments Pe [E].
+Implicit Arguments Po [E].
+
+(** ** Evaluation *)
+Parameter EvalOpR : Val -> OpR -> Val -> Prop.
+Parameter EvalOpP : Prop -> OpP -> Prop -> Prop.
+Fixpoint EvalPred (E:Set) (EvalExp : E -> Val) 
+                  (p:PredDef E) {struct p} : Prop := match p with
+  | (Pe e1 o e2) => EvalOpR (EvalExp e1) o (EvalExp e2)
+  | (Po p1 o p2) => EvalOpP (EvalPred E EvalExp p1) 
+                          o (EvalPred E EvalExp p2)
+end.
+
+(** ** Substitution *)
+Fixpoint SubstInPred (E:Set) (SubstE : E -> E) (p : PredDef E) {struct p} := 
+  match p with
+  | (Pe e1 o e2) => (Pe (SubstE e1) o (SubstE e2))
+  | (Po p1 o p2) => (Po (SubstInPred E SubstE p1) o (SubstInPred E SubstE p2))
+end.
+
+
+(*----------------------------------------------------------------------------*)
+(** * Model 3 : low level *)
+
+(** ** Definitions *)
+Parameter OpE3 : Set.
+Parameter Mem3 : Set.
+Parameter Val3 : Set.
+
+Inductive Exp3 : Set :=
+  | E3cnst : Val3 -> Exp3
+  | E3star : Exp3
+  | E3addr : Var -> Exp3
+  | E3shift : Exp3 -> Field -> Exp3
+  | E3load : Exp3 -> Exp3 -> Size -> Exp3 (* load mem addr size *)
+  | E3store : Exp3 -> Exp3 -> Exp3 -> Exp3 (* store mem addr val *)
+  | E3op : Exp3 -> OpE3 -> Exp3 -> Exp3
+.
+
+Definition Pred3 := PredDef Exp3.
+
+(** ** Translations to Exp3 *)
+
+Parameter OpC_to_OpE3 : OpC -> OpE3.
+Parameter Val_to_Val3 : Val -> Val3.
+
+Fixpoint Path_to_Exp3 (addr:Exp3) (ch:Path) {struct ch} := match ch with
+| nil => addr
+| (Pfield f)::tl => Path_to_Exp3 (E3shift addr f) tl
+| Pindir::tl => Path_to_Exp3 (E3load E3star  addr SizeofPtr) tl
+end.
+
+Lemma Path_to_Exp3_split : forall a ch1 ch2,
+  Path_to_Exp3 a (ch1++ch2) = Path_to_Exp3 (Path_to_Exp3 a ch1) ch2.
+Proof.
+intros a ch1 ch2.
+generalize a.
+induction ch1.
+
+simpl;  auto.
+
+clear a; intro a.
+destruct a0.
+
+simpl Path_to_Exp3 at 1 3.
+rewrite IHch1; auto.
+
+simpl Path_to_Exp3 at 1 3.
+rewrite IHch1; auto.
+Qed.
+
+Definition VarPathAddrExp3 (v:Var) (ch:Path) : Exp3 :=
+  Path_to_Exp3 (E3addr v) ch.
+
+Fixpoint ExpC_to_Exp3 (e:ExpC) {struct e} : Exp3 := match e with
+  | Ecnst v => E3cnst (Val_to_Val3 v)
+  | Edata v ch => E3load E3star (VarPathAddrExp3 v ch) (SizeofVarPath v ch)
+  | Eop e1 o e2 => E3op (ExpC_to_Exp3 e1) (OpC_to_OpE3 o) (ExpC_to_Exp3 e2)
+end.
+
+Fixpoint SubstStarInExp3 (new_star:Exp3) (exp:Exp3) {struct exp} : Exp3 := 
+match exp with
+| E3cnst _ => exp
+| E3star => new_star
+| E3addr _ => exp
+| E3shift e f => E3shift (SubstStarInExp3 new_star e) f
+| E3load e1 e2 sz => E3load (SubstStarInExp3 new_star e1)
+                            (SubstStarInExp3 new_star e2) sz
+| E3store e1 e2 e3 => E3store (SubstStarInExp3 new_star e1)
+                              (SubstStarInExp3 new_star e2) 
+                              (SubstStarInExp3 new_star e3)
+| E3op e1 o e2 => E3op  (SubstStarInExp3 new_star e1)
+                      o (SubstStarInExp3 new_star e2)
+end.
+
+Definition SubstStarInPred3 st p :=
+  SubstInPred Exp3  (SubstStarInExp3 st) p.
+
+Definition NewStar v ch e :=
+  (E3store E3star (Path_to_Exp3 (E3addr v) ch) (ExpC_to_Exp3 e)).
+
+Definition WP3 (s:Stmt) (p:Pred3) : Pred3 := match s with 
+  | (Iasgn v ch e) =>   SubstStarInPred3 (NewStar v ch e) p
+end.
+
+(** ** Evaluation *)
+
+Parameter Val2Mem : Val -> Mem.
+
+Parameter EvalVal3 : Val3 -> Val.
+
+Parameter EvalMemAddr : MemAddr -> Val.
+Axiom Val2EvalAddr : forall addr, Val2Addr (EvalMemAddr addr) = addr.
+
+Definition EvalValAddr v : Val := EvalMemAddr (VarAddr v).
+
+Parameter EvalMem : Mem -> Val.
+Axiom Val2EvalMem : forall m, Val2Mem (EvalMem m) = m.
+
+Parameter EvalShift : Val -> Field -> Val.
+Axiom Val2EvalShift : forall va f,
+  Val2Addr (EvalShift va f) = AddFieldOffset (Val2Addr va) f.
+
+Definition EvalLoad mem addr sz : Val :=
+  Interp ((Val2Mem mem) ((Val2Addr addr), sz)).
+Lemma Var2EvalLoad : forall m va,
+  Val2Addr (EvalLoad (EvalMem m) va SizeofPtr) = IndirAddr m (Val2Addr va).
+Proof.
+intros m va.
+unfold IndirAddr.
+unfold BVal2Addr.
+apply (f_equal Val2Addr).
+unfold EvalLoad.
+apply (f_equal Interp).
+rewrite Val2EvalMem.
+auto.
+Qed.
+
+Definition EvalStore mem addr val : Val :=
+  EvalMem (W (Val2Mem mem) (Val2Addr addr) (Bits val)).
+
+Parameter EvalOp3 : Val -> OpE3 -> Val -> Val.
+
+Fixpoint EvalExp3 (m : Mem) (exp:Exp3) {struct exp} : Val := match exp with
+| E3cnst val3 => EvalVal3 val3
+| E3star => EvalMem m
+| E3addr v => EvalValAddr v
+| E3shift e f => EvalShift (EvalExp3 m e) f
+| E3load e1 e2 sz => EvalLoad (EvalExp3 m e1) (EvalExp3 m e2) sz
+| E3store e1 e2 e3 => EvalStore (EvalExp3 m e1) (EvalExp3 m e2) (EvalExp3 m e3)
+| E3op e1 o e2 => EvalOp3 (EvalExp3 m e1) o (EvalExp3 m e2)
+end.
+
+Axiom EvalExp3ok : forall m e,
+  EvalExp3 m (ExpC_to_Exp3 e) = EvalExpC m e.
+
+(** this one is a consequence of the previous one for exp = &(v.ch)
+but we cannot write this exp in ExpC. *)
+Lemma Val2Addr_ok : forall m v ch,
+Val2Addr (EvalExp3 m (VarPathAddrExp3 v ch)) =
+VarPathAddr m v ch.
+Proof.
+intros m v ch.
+pose (P := fun (ch:list Proj) => 
+           Val2Addr (EvalExp3 m (VarPathAddrExp3 v ch)) = VarPathAddr m v ch).
+fold (P ch).
+apply rev_ind; unfold P; clear P.
+
+simpl. unfold EvalValAddr.
+apply Val2EvalAddr; auto.
+
+clear ch.
+intros p ch HI.
+unfold VarPathAddr, VarPathAddrExp3 in *.
+rewrite PathAddr_split.
+rewrite Path_to_Exp3_split.
+rewrite <- HI.
+
+set (x := Path_to_Exp3 (E3addr v) ch).
+destruct p; simpl.
+apply Val2EvalShift.
+
+set (va := EvalExp3 m x).
+apply Var2EvalLoad.
+Qed.
+
+Definition EvalPred3 m p := EvalPred Exp3 (EvalExp3 m) p.
+
+(** ** Verification *)
+
+Lemma UpdateVsSubstInExp3 : forall m1 m2 v ch e exp st, 
+  m2 = W m1 (VarPathAddr m1 v ch) (Bits (EvalExpC m1 e)) ->
+  st = NewStar v ch e
+  -> EvalExp3 m1 (SubstStarInExp3 st exp) = EvalExp3 m2 exp
+.
+Proof.
+intros m1 m2 v ch e exp st Hm2 Hst.
+induction exp; simpl; auto.
+
+subst st; simpl; unfold EvalLoad, EvalStore; simpl.
+apply (f_equal EvalMem).
+rewrite Val2EvalMem.
+rewrite EvalExp3ok.
+subst m2.
+apply (f_equal3 W); auto.
+rewrite <- (Val2Addr_ok m1 v ch).
+apply (f_equal Val2Addr).
+apply (f_equal2 EvalExp3); auto.
+apply (f_equal2 EvalShift); auto.
+apply (f_equal3 EvalLoad); auto.
+apply (f_equal3 EvalStore); auto.
+apply (f_equal3 EvalOp3); auto.
+Qed.
+
+
+Theorem WP3ok : forall s p m1 m2, exec m1 s m2 -> 
+  EvalPred3 m1 (WP3 s p) = EvalPred3 m2 p.
+Proof.
+intros s p m1 m2 E.
+destruct s as [v ch e].
+simpl in E.
+unfold EvalPred3.
+simpl.
+induction p. 
+
+simpl.
+rewrite (UpdateVsSubstInExp3 m1  m2 v ch e e0); auto.
+rewrite (UpdateVsSubstInExp3 m1  m2 v ch e e1); auto.
+
+simpl.
+fold (SubstStarInPred3 (NewStar v ch e) p1). rewrite IHp1.
+fold (SubstStarInPred3 (NewStar v ch e) p2). rewrite IHp2.
+auto.
+Qed.
+
+STOP.
+
+(*----------------------------------------------------------------------------*)
+(*----------------------------------------------------------------------------*)
+(*----------------------------------------------------------------------------*)
+(*----------------------------------------------------------------------------*)
+
+(** * Models on variables *)
 
 (** Modification of a part of an object *)
 Parameter MuVal : Val -> Field -> Val -> Val.
@@ -90,33 +462,11 @@ Qed.
 
 (** ** Adresses/Read/Write *)
 
-Parameter VarAddr : Var -> MemAddr.
-Parameter FieldOffset : MemAddr -> Field -> MemAddr.
-Parameter IndirAddr : Val -> MemAddr.
-
-Definition ReadPtr (mem:Mem) addr : Val := Interp (mem (addr, SizeofPtr)).
-
-Fixpoint PathAddr (mem:Mem) (a:MemAddr) (ch:Path) {struct ch} : MemAddr := 
-  match ch with
-  | nil => a
-  | Pfield proj :: tl => PathAddr mem (FieldOffset a proj) tl
-  | Pindir :: tl => PathAddr mem (IndirAddr (ReadPtr mem a)) tl
-  end.
-
-Definition Addr (mem:Mem) (v:Var) (ch:Path) : MemAddr := 
-  PathAddr mem (VarAddr v) ch.
-
-Parameter SizeofVarPath : Var -> Path -> Size.
-
 Definition ValidAsgn v ch val := SizeofVarPath v ch = SizeofBVal (Bits val).
 
 Definition VarPathZone (mem:Mem) (v:Var) (ch:Path) : MemZone :=
   ((Addr mem v ch), SizeofVarPath v ch).
 
-Definition VarZone (v:Var) : MemZone :=
-  (VarAddr v, SizeofVarPath v nil).
-
-Axiom VarZoneDisj : forall v1 v2, DisjMemZones (VarZone v1) (VarZone v2).
 
 Axiom ProjAddrIncl : forall m v ch f ch', ch' = ch++(Pfield f)::nil ->
   InclMemZones (Addr m v ch' , SizeofVarPath v ch')  
@@ -216,10 +566,6 @@ Definition Pred := PredDef Exp.
 Implicit Arguments Pe [E].
 Implicit Arguments Po [E].
 
-(** ** Statements *)
-Inductive Stmt : Set :=
-  Iasgn : Var -> Path -> Exp -> Stmt
-.
 
 
 
@@ -236,10 +582,7 @@ Fixpoint SubstInExp v (ch:Path) e exp {struct exp} := match exp with
   | (Eop e1 op e2) => (Eop (SubstInExp v ch e e1) op  (SubstInExp v ch e e2))
 end.
 
-Fixpoint SubstInPred v ch exp p {struct p} := match p with
-  | (Pe e1 o e2) => (Pe (SubstInExp v ch exp e1) o (SubstInExp v ch exp e2))
-  | (Po p1 o p2) => (Po (SubstInPred v ch exp p1) o (SubstInPred v ch exp p2))
-end.
+
 
 (** ** Evaluations *)
 
@@ -250,8 +593,6 @@ Ex. [MuPtr p x] <--> *p = x
 Parameter MuPtr : Val -> Val -> Val.
 
 Parameter EvalOpE : Val -> OpE -> Val -> Val.
-Parameter EvalOpR : Val -> OpR -> Val -> Prop.
-Parameter EvalOpP : Prop -> OpP -> Prop -> Prop.
 
 Fixpoint EvalMu mem val_v ch val_e {struct ch} : Val := match ch with
   | nil => val_e
@@ -262,47 +603,33 @@ Fixpoint EvalMu mem val_v ch val_e {struct ch} : Val := match ch with
       MuPtr val_v (EvalMu mem (ReadPtr mem (IndirAddr val_v)) ch val_e)
 end.
 
-Lemma EvalMuTailProj : forall m v ch f val,
-EvalMu m (R m v nil) (ch ++ Pfield f :: nil) val =
+Lemma EvalMuTailProj : forall m v ch p f val, p = Pfield f ->
+EvalMu m (R m v nil) (ch ++ p :: nil) val =
 EvalMu m (R m v nil) ch (MuVal (R m v ch) f val).
 Proof.
 intros m v ch.
-pose (P := fun v ch => forall f val,
-EvalMu m (R m v nil) (ch ++ Pfield f :: nil) val =
+pose (P := fun v ch => forall p f val, p = Pfield f ->
+EvalMu m (R m v nil) (ch ++ p :: nil) val =
 EvalMu m (R m v nil) ch (MuVal (R m v ch) f val)).
 fold (P v ch).
 revert ch.
 apply (Path_ind _ P).
 
 unfold P; clear P.
-intro val.
-simpl ; auto.
+intros p f val Hp.
+subst p; simpl ; auto.
 
 unfold P; clear P.
-intros ch f Hi f' val.
-rewrite Hi.
+intros ch p Hi p' f' val Hp'.
 
+(* Maybe false when ch ends with Indir ? *)
+Admitted.
 
 
 
-Fixpoint EvalExp mem exp {struct exp} : Val := match exp with
-  | Ecnst val  => val
-  | Evar v => R mem v NoPath
-  | Eproj d ch => ValProj (EvalExp mem d) ch
-  | Eindir e => ReadPtr mem (IndirAddr (EvalExp mem e))
-  | Emu v ch e => EvalMu mem (EvalExp mem v) ch (EvalExp mem e)
-  | Eop e1 o e2 => EvalOpE (EvalExp mem e1) o (EvalExp mem e2)
-end.
 
-Fixpoint EvalPred (mem: Mem) (p:Pred) {struct p} : Prop := match p with
-  | (Pe e1 o e2) => EvalOpR (EvalExp mem e1) o (EvalExp mem e2)
-  | (Po p1 o p2) => EvalOpP (EvalPred mem p1) o (EvalPred mem p2)
-end.
 
 
-Definition exec m1 s m2 : Prop := match s with
-  | (Iasgn v ch e) =>  m2 = W_var_path m1 v ch  (EvalExp m1 e)
-end.
 
 
 Module M0.
@@ -352,6 +679,17 @@ destruct (in_inv Hin); clear Hin.
 subst a. intro H2; subst f; discriminate H2.
 apply IHp; auto.
 Qed.
+Lemma NoIndirInPathTail : forall ch p, NoIndirInPath (ch++p::nil) -> NoIndirInPath ch.
+intros ch p.
+induction ch.
+auto.
+intro H.
+destruct a.
+eapply NIPproj; eauto.
+inversion H. apply IHch; auto.
+absurd_hyp H; auto.
+intro A; inversion A. discriminate H3.
+Qed.
 
 Inductive NoIndirInExp : Exp -> Prop := 
 | NIEcnst : forall c, NoIndirInExp (Ecnst c)
@@ -485,10 +823,9 @@ intros ch f Hi val' Hva NIch.
 destruct f; auto.
 rewrite W_proj.
 rewrite <- Hi; auto.
-
+apply EvalMuTailProj; auto.
 
 (* --------------------- *)
-Focus 2.
 unfold ValidAsgn.
 fold (SizeofVal (MuVal (R m1 v ch) f val')).
 rewrite SizeofMuVal.
@@ -497,8 +834,16 @@ rewrite SizeofInterp.
 rewrite SizeofR.
 auto.
 
+
+eapply NoIndirInPathTail; eauto.
+
+(* --------------------- *)
+absurd_hyp NIch; auto.
+induction ch; simpl.
+intro H; inversion H. discriminate H3.
+
+
 (* --------------------- *)
-Focus 2.
 unfold R, Addr.
 simpl.
 set (z' := (VarAddr v', SizeofVarPath v' NoPath)).
-- 
GitLab