# Library AndersenIter

``` Require Import Arith List TheoryList. Require Import ListUtil Tactics Maps. Require Import Pointer Machine AndersenModel AndersenSound. Lemma incl_add : forall s a,   AllocSet.incl s (AllocSet.add s a) = true. Lemma incl_add2 : forall s1 s2 a,   AllocSet.incl s1 s2 = true   -> AllocSet.incl (AllocSet.add s1 a) (AllocSet.add s2 a) = true. Hint Resolve incl_add2. Lemma incl_union2 : forall s1 s2 s3 s4,   AllocSet.incl s1 s3 = true   -> AllocSet.incl s2 s4 = true   -> AllocSet.incl (AllocSet.union s1 s2)   (AllocSet.union s3 s4) = true. Hint Resolve incl_union2. Lemma incl_fold1 : forall (f : allocation_site -> AllocSet.set) x ls s,   AllocSet.In x (fold_left     (fun known site =>       AllocSet.union known (f site))     ls s) = true   -> (AllocSet.In x s = true     \/ exists y, In y ls /\ AllocSet.In x (f y) = true). Lemma incl_fold2 : forall (f : allocation_site -> AllocSet.set) x ls s,   (AllocSet.In x s = true     \/ exists y, In y ls /\ AllocSet.In x (f y) = true)   -> AllocSet.In x (fold_left     (fun known site =>       AllocSet.union known (f site))     ls s) = true. Lemma incl_elems : forall t1 t2 y,   AllocSet.incl t1 t2 = true   -> In y (AllocSet.elems t1)   -> In y (AllocSet.elems t2). Lemma incl_fold_read : forall (f1 f2 : allocation_site -> AllocSet.set) s1 s2 t1 t2,   (forall a, AllocSet.incl (f1 a) (f2 a) = true)   -> AllocSet.incl s1 s2 = true   -> AllocSet.incl t1 t2 = true   -> AllocSet.incl   (fold_left     (fun known site =>       AllocSet.union known (f1 site))     (AllocSet.elems t1) s1)   (fold_left     (fun known site =>       AllocSet.union known (f2 site))     (AllocSet.elems t2) s2) = true. Hint Resolve incl_fold_read. Lemma incl_fold3' : forall a (f : allocation_site -> AllocSet.set) s ls h,   AllocMap.sel h a = AllocSet.union (f a) s   -> AllocMap.sel   (fold_left (fun known site =>     AllocMap.upd known site (AllocSet.union (f site) s))   ls h) a = AllocSet.union (f a) s. Lemma incl_fold3 : forall f s a ls h,   if In_eq_dec eq_nat_dec a ls     then AllocMap.sel (fold_left (fun known site =>       AllocMap.upd known site (AllocSet.union (f site) s))     ls h) a = AllocSet.union (f a) s     else AllocMap.sel (fold_left (fun known site =>       AllocMap.upd known site (AllocSet.union (f site) s))     ls h) a = AllocMap.sel h a. Lemma incl_fold_write : forall a s1 s2 t1 t2 h1 h2,   AllocSet.incl (AllocMap.sel h1 a) (AllocMap.sel h2 a) = true   -> AllocSet.incl s1 s2 = true   -> AllocSet.incl t1 t2 = true   -> AllocSet.incl   (AllocMap.sel (fold_left (fun known site =>     AllocMap.upd known site (AllocSet.union (AllocMap.sel h1 site) s1))   (AllocSet.elems t1) h1) a)   (AllocMap.sel (fold_left (fun known site =>     AllocMap.upd known site (AllocSet.union (AllocMap.sel h2 site) s2))   (AllocSet.elems t2) h2) a) = true. Hint Resolve incl_fold_write. Definition ins_sites i :=   match i with     | AbsAllocate _ site => AllocSet.add AllocSet.empty site     | _ => AllocSet.empty   end. Module VarSet : SET with Definition dom := var := AllocSet. Definition ins_vars i :=   match i with     | AbsAllocate v _ => VarSet.add VarSet.empty v     | AbsCopy v1 v2 => VarSet.add (VarSet.add VarSet.empty v1) v2     | AbsRead v1 v2 => VarSet.add (VarSet.add VarSet.empty v1) v2     | AbsWrite v1 v2 => VarSet.add (VarSet.add VarSet.empty v1) v2   end. Section prog.    Variable program : list abstract_instruction.   Definition pSites := fold_left AllocSet.union (map ins_sites program).   Definition pVars := fold_left VarSet.union (map ins_vars program). End prog. Section fixed_point.    Variable program : list abstract_instruction.   Definition progSites := pSites program AllocSet.empty.   Definition progVars := pVars program VarSet.empty.   Record approx' (abs1 abs2 : abstract_state) : Prop := {     approxVars : forall v, AllocSet.incl       (VarMap.sel (avars abs1) v) (VarMap.sel (avars abs2) v) = true;     approxHeap : forall a, AllocSet.incl       (AllocMap.sel (aheap abs1) a) (AllocMap.sel (aheap abs2) a) = true   }.   Lemma increasing' : forall abs ins,     approx' abs (abstract_exec ins abs).   Lemma monotonic' : forall abs abs' ins,     approx' abs abs'     -> approx' (abstract_exec ins abs) (abstract_exec ins abs').   Lemma approx_refl' : forall s, approx' s s.   Lemma approx_trans' : forall s1 s2 s3,     approx' s1 s2 -> approx' s2 s3 -> approx' s1 s3.   Lemma approx_init' : forall s, approx' abstract_initState s.   Record valid (abs : abstract_state) : Prop := {     validVarsDom : forall v, VarSet.In v progVars = false       -> AllocSet.incl (VarMap.sel (avars abs) v) AllocSet.empty = true;     validHeapDom : forall a, AllocSet.In a progSites = false       -> AllocSet.incl (AllocMap.sel (aheap abs) a) AllocSet.empty = true;     validVars : forall v, AllocSet.incl (VarMap.sel (avars abs) v) progSites = true;     validHeap : forall a, AllocSet.incl (AllocMap.sel (aheap abs) a) progSites = true   }.   Definition astate := sig valid.   Definition approx (abs1 abs2 : astate) := approx' (proj1_sig abs1) (proj1_sig abs2).   Record approxStrict (abs1 abs2 : astate) : Prop := {     strictApprox : approx abs2 abs1;     strictNe : (exists v, VarSet.In v progVars = true       /\ AllocSet.incl (VarMap.sel (avars (proj1_sig abs1)) v)       (VarMap.sel (avars (proj1_sig abs2)) v) = false)     \/ exists a, AllocSet.In a progSites = true       /\ AllocSet.incl (AllocMap.sel (aheap (proj1_sig abs1)) a)       (AllocMap.sel (aheap (proj1_sig abs2)) a) = false   }.   Definition ainstruction := sig (fun ins => In ins program).   Lemma fold_In_union : forall a ls s,     AllocSet.In a s = true     -> AllocSet.In a (fold_left AllocSet.union ls s) = true.    Hint Resolve VarSet.incl_In VarSet.incl_union_left.   Lemma fold_In_unionv : forall a ls s,     VarSet.In a s = true     -> VarSet.In a (fold_left VarSet.union ls s) = true.   Lemma allocate_site : forall v a prog s,     In (AbsAllocate v a) prog       -> AllocSet.In a (pSites prog s) = true.   Lemma incl_add3 : forall x s1 s2,     AllocSet.In x s2 = true     -> AllocSet.incl s1 s2 = true     -> AllocSet.incl (AllocSet.add s1 x) s2 = true.   Lemma incl_union : forall s1 s2 s3,     AllocSet.incl s1 s3 = true     -> AllocSet.incl s2 s3 = true     -> AllocSet.incl (AllocSet.union s1 s2) s3 = true.   Lemma incl_valid_read : forall (f : allocation_site -> AllocSet.set) s2 ls s1,     AllocSet.incl s1 s2 = true     -> (forall site, AllocSet.incl (f site) s2 = true)     -> AllocSet.incl     (fold_left       (fun known site => AllocSet.union known (f site))       ls s1) s2 = true.   Lemma incl_valid_write : forall a s1 s2 f ls h,     AllocSet.incl s1 s2 = true     -> (forall a, AllocSet.incl (f a) s2 = true)     -> (forall a, AllocSet.incl (AllocMap.sel h a) s2 = true)     -> AllocSet.incl     (AllocMap.sel       (fold_left         (fun known site => AllocMap.upd known site           (AllocSet.union (f site) s1))         ls h) a)     s2 = true.       Hint Resolve VarSet.In_add_eq VarSet.In_add_neq VarSet.incl_union_right.   Lemma allocate_var : forall v a prog s,     In (AbsAllocate v a) prog       -> VarSet.In v (pVars prog s) = true.   Lemma copy_var : forall v a prog s,     In (AbsCopy v a) prog       -> VarSet.In v (pVars prog s) = true.   Lemma read_var : forall v a prog s,     In (AbsRead v a) prog       -> VarSet.In v (pVars prog s) = true.   Lemma write_var : forall v a prog s,     In (AbsWrite v a) prog       -> VarSet.In v (pVars prog s) = true.   Lemma sel_write_valid : forall f s a ls h,     AllocMap.sel     (fold_left (fun known site => AllocMap.upd known site       (AllocSet.union (f site) s))     ls h) a     = if In_eq_dec eq_nat_dec a ls       then AllocSet.union (f a) s       else AllocMap.sel h a.   Lemma aexec' : forall ins abs, In ins program -> valid abs -> valid (abstract_exec ins abs).   Definition aexec : ainstruction -> astate -> astate.   Definition ainitState : astate.   Lemma ainstr_widen : forall h t,     {ins : abstract_instruction | In ins t}     -> {ins : abstract_instruction | In ins (h :: t)}.   Definition aprogram' : forall (prog : list abstract_instruction),     list (sig (fun ins => In ins prog)).   Definition aprogram := aprogram' program.        Theorem increasing : forall abs ins,     approx abs (aexec ins abs).    Hint Resolve increasing.   Theorem monotonic : forall abs abs' ins,     approx abs abs'     -> approx (aexec ins abs) (aexec ins abs').    Hint Resolve monotonic.   Theorem approx_refl : forall s, approx s s.    Hint Resolve approx_refl.   Theorem approx_trans : forall s1 s2 s3,     approx s1 s2 -> approx s2 s3 -> approx s1 s3.    Hint Resolve approx_trans.   Theorem approx_init : forall s, approx ainitState s.    Hint Resolve approx_init.    Hint Resolve AllocSet.incl_empty.   Theorem approxStrict_approx : forall s1 s2,     approx s2 s1     -> ~approxStrict s1 s2     -> approx s1 s2.    Hint Resolve approxStrict_approx.   Theorem approxStrict_trans : forall s1 s2 s3,     approx s2 s1 -> approxStrict s2 s3 -> approxStrict s1 s3.    Hint Resolve approxStrict_trans.   Definition approx_dec : forall abs1 abs2, {approx abs1 abs2} + {~approx abs1 abs2}.   Definition approxStrict_dec : forall abs1 abs2, {approxStrict abs1 abs2} + {~approxStrict abs1 abs2}.    Hint Resolve approxStrict_dec.   Fixpoint distinct (ls : list nat) : Prop :=     match ls with       | nil => True       | h::t => AllS (fun x => x <> h) t         /\ distinct t     end.   Definition cardinality_atLeast s n :=     exists ls, distinct ls       /\ length ls = n       /\ AllS (fun x => AllocSet.In x s = true) ls.      Definition cardinality s n :=     cardinality_atLeast s n     /\ forall n', cardinality_atLeast s n' -> n' <= n.   Definition bound := length (AllocSet.elems progSites).   Definition neq_nat_dec : forall (x y : nat), {x <> y} + {~x <> y}.   Definition distinctify : forall (ls : list allocation_site),     {ls' : list allocation_site | distinct ls'       /\ forall x, In x ls <-> In x ls'}.   Lemma incl_S : forall (ls : list allocation_site) a,     In a ls     -> exists ls', length ls = S (length ls')       /\ incl ls (a :: ls').   Lemma incl_trans' : forall (a : allocation_site) ls1 ls2,     distinct (a :: ls1)     -> incl (a :: ls1) (a :: ls2)     -> incl ls1 ls2.   Lemma incl_length : forall (ls1 ls2 : list allocation_site),     incl ls1 ls2     -> distinct ls1     -> length ls1 <= length ls2.   Lemma card : forall s,     AllocSet.incl s progSites = true     -> {n : nat       | n <= bound         /\ cardinality s n}.   Definition var_bounded : forall (abs : astate) (v : var),     AllocSet.incl (VarMap.sel (avars (proj1_sig abs)) v) progSites = true.   Definition site_bounded : forall (abs : astate) (s : allocation_site),     AllocSet.incl (AllocMap.sel (aheap (proj1_sig abs)) s) progSites = true.   Definition size (abs : astate) :=     fold_right plus 0 (map (fun x => proj1_sig (card _ (var_bounded abs x)))       (VarSet.elems progVars))     + fold_right plus 0 (map (fun x => proj1_sig (card _ (site_bounded abs x)))       (AllocSet.elems progSites)).      Lemma mult_le : forall n x m y,     x <= n * m     -> y <= n     -> y + x <= n * S m.   Lemma size_bounded : forall abs,     size abs <= bound * (length (VarSet.elems progVars) + length (AllocSet.elems progSites)).   Lemma fold_plus_ge : forall (A : Set) f1 f2 (ls : list A),     AllS (fun x => f1 x >= f2 x) ls     -> fold_right plus 0 (map f1 ls) >= fold_right plus 0 (map f2 ls).   Lemma fold_plus_gt : forall (A : Set) f1 f2 x,     f1 x > f2 x     -> forall (ls : list A), AllS (fun x => f1 x >= f2 x) ls     -> In x ls     -> fold_right plus 0 (map f1 ls) > fold_right plus 0 (map f2 ls).      Lemma sum_plus1 : forall x1 y1 x2 y2,     x1 > x2     -> y1 >= y2     -> x1 + y1 > x2 + y2.   Lemma sum_plus2 : forall x1 y1 x2 y2,     x1 >= x2     -> y1 > y2     -> x1 + y1 > x2 + y2.   Lemma incl_cardinality' : forall s1 s2 c,     AllocSet.incl s1 s2 = true     -> cardinality_atLeast s1 c     -> cardinality_atLeast s2 c.   Lemma incl_cardinality : forall s1 s2 c1 c2,     AllocSet.incl s1 s2 = true     -> cardinality s1 c1     -> cardinality s2 c2     -> c1 <= c2.   Lemma incl_gt : forall (x : allocation_site) ls2 ls1,     distinct ls1     -> incl ls1 ls2     -> ~In x ls1     -> In x ls2     -> length ls2 > length ls1.   Lemma set_grew : forall s1 s2 c1 c2,     AllocSet.incl s2 s1 = true     -> AllocSet.incl s1 s2 = false     -> cardinality s1 c1     -> cardinality s2 c2     -> c1 > c2.   Lemma size_approxStrict : forall abs abs',     approxStrict abs abs'     -> size abs > size abs'.   Lemma approxStrict_wf' : forall n a,     bound * (length (VarSet.elems progVars) + length (AllocSet.elems progSites)) - size a <= n     -> Acc approxStrict a.   Theorem approxStrict_wf : well_founded approxStrict.    Hint Resolve approxStrict_wf.   Definition fixed_point' : {fp : astate     | forall s, reachable_flowInsensitive aprogram aexec ainitState s       -> approx s fp}.   Lemma In_map : forall (A B : Set) x (f : A -> B) ls,     In x ls     -> In (f x) (map f ls).   Lemma in_aprogram' : forall i prog,     In i prog ->     exists H : In i prog,       In (exist (fun i0 => In i0 prog) i H)       (aprogram' prog).   Lemma in_aprogram : forall i,     In i program       -> exists H, In (exist (fun i => In i program) i H) aprogram.   Axiom valid_irrel : forall s (H1 H2 : valid s), H1 = H2.   Lemma reachable_a : forall s1 (Hv1 : valid s1) s2,     reachable_flowInsensitive program abstract_exec s1 s2       -> exists Hv2 : valid s2,         reachable_flowInsensitive aprogram aexec (exist _ _ Hv1) (exist _ _ Hv2).   Definition fixed_point : {fp : abstract_state     | forall s, reachable_flowInsensitive program abstract_exec abstract_initState s       -> approx' s fp}. End fixed_point. ```
Index