From 8c8fbc73afb29edbd303f4cac2a7300543c36d9c Mon Sep 17 00:00:00 2001 From: Nisarg Patel Date: Sun, 12 May 2024 02:25:24 -0400 Subject: [PATCH] complete flow_RA --- test/bugs/assume_false_bug.rav | 333 +++++++++++++++++++++++++ test/concurrent/templates/flows_ra.rav | 134 +++++++--- 2 files changed, 428 insertions(+), 39 deletions(-) create mode 100644 test/bugs/assume_false_bug.rav diff --git a/test/bugs/assume_false_bug.rav b/test/bugs/assume_false_bug.rav new file mode 100644 index 0000000..c65b6db --- /dev/null +++ b/test/bugs/assume_false_bug.rav @@ -0,0 +1,333 @@ +import Library.Type +import Library.CancellativeResourceAlgebra + +interface CCM : Type { + val id: T + func comp(a:T, b:T) returns (ret:T) + + func frame(a:T, b:T) returns (ret:T) + + func valid(a:T) returns (ret: Bool) + + auto lemma idValid() + ensures valid(id) + + auto lemma compAssoc() + ensures forall a:T, b:T, c:T :: {comp(comp(a, b), c)} {comp(a, comp(b, c))} (comp(comp(a, b), c) == comp(a, comp(b, c))) + + auto lemma compCommute() + ensures forall a:T, b:T :: {comp(a,b)} {comp(b,a)} comp(a, b) == comp(b, a) + + auto lemma compId() + ensures forall a:T :: {comp(a, id)} {comp(id, a)} comp(a, id) == a + + auto lemma compValid() + ensures forall a:T, b:T :: {comp(a,b)} valid(a) && valid(b) ==> valid(comp(a, b)) + + auto lemma frameCompInv() + ensures forall a:T, b:T:: {comp(a,b)} frame(comp(a, b), b) == a + + lemma frameId() + ensures forall a:T :: {frame(a,id)} frame(a, id) == a + { + } + + // lemma compFrameInv(a: T, b: T) + // ensures a == frame(comp(a, b), b) + // { + // } + + auto lemma frameFrame() + ensures forall a:T, b:T :: {valid(frame(a, b))} valid(frame(a, b)) ==> frame(a, frame(a, b)) == b + + // lemma misc1(a: T, b: T) + // requires valid(frame(a, b)) + // ensures frame(a, frame(a, b)) == b + // {} + + auto lemma compFrameInv() + ensures forall a:T, b:T :: {frame(a,b)} valid(frame(a, b)) ==> comp(frame(a, b), b) == a + + //auto lemma frameValid() + // ensures forall a:T, b:T :: {frame(a,b)} {valid(a), valid(b)} valid(frame(a,b)) ==> valid(a) && valid(b) + +} + +interface FlowsRA[M: CCM] : CancellativeResourceAlgebra { + rep type T = data { + case int(inf: Map[Ref, M], out: Map[Ref, M], dom: Set[Ref]) + case top + } + + /* The "all-zero" flow map */ + val zeroFlow: Map[Ref, M] = {| n: Ref :: M.id |} + + + /* The empty flow interface */ + val id: T = int(zeroFlow, zeroFlow, {||}) + + func valid(i: T) + returns (ret: Bool) + { + // not undefined + i != top + // Inflow and outflow properly defined + && (forall n: Ref :: i.inf[n] != M.id ==> n in i.dom) + && (forall n: Ref :: i.out[n] != M.id ==> n !in i.dom) + // Inflow and outflow are valid + && (forall n: Ref :: n in i.dom ==> M.valid(i.inf[n])) + && (forall n: Ref :: n !in i.dom ==> M.valid(i.out[n])) + // Empty domain ==> no outflow + && (i.dom == {||} ==> i.out == zeroFlow) + } + + // Condition ensuring that two flow interfaces compose + func composable(i1: T, i2: T) + returns (ret: Bool) + { + valid(i1) && valid(i2) && i1.dom ** i2.dom == {||} + && (forall n: Ref :: n in i1.dom ==> i1.inf[n] == M.comp(i2.out[n], M.frame(i1.inf[n], i2.out[n]))) + && (forall n: Ref :: n in i2.dom ==> i2.inf[n] == M.comp(i1.out[n], M.frame(i2.inf[n], i1.out[n]))) + && (forall n: Ref :: n in i1.dom ==> M.valid(M.frame(i1.inf[n], i2.out[n]))) + && (forall n: Ref :: n in i2.dom ==> M.valid(M.frame(i2.inf[n], i1.out[n]))) + } + + // Interface composition + func comp(i1: T, i2: T) returns (i: T) + { + composable(i1, i2) ? + int({| n: Ref :: n in i1.dom ? M.frame(i1.inf[n], i2.out[n]) : + (n in i2.dom ? M.frame(i2.inf[n], i1.out[n]) : M.id) |}, + {| n: Ref :: n !in i1.dom && n !in i2.dom ? M.comp(i1.out[n], i2.out[n]) : M.id |}, + i1.dom ++ i2.dom) : + (i1 == id ? i2 : (i2 == id ? i1 : top)) + } + + // Domain of interface composition is union of its component domains + auto lemma compDom() + ensures forall i1: T, i2: T :: {comp(i1, i2)} valid(comp(i1, i2)) ==> comp(i1, i2).dom == i1.dom ++ i2.dom + {} + + // Domains of composit interfaces must be disjoint + auto lemma compDisjoint() + ensures forall i1: T, i2: T :: {comp(i1, i2)} valid(comp(i1, i2)) ==> i1.dom ** i2.dom == {||} + {} + + // Valid interfaces are defined + auto lemma validDefined() + ensures forall i: T :: valid(i) ==> i != top + {} + + // The empty interface is valid */ + auto lemma idValid() + ensures valid(id) + { + M.idValid(); + } + + // top is an absorbing element + auto lemma compTop() + ensures forall i: T :: {comp(top, i)} comp(top, i) == top + {} + + // The empty interface is the unit of interface composition + auto lemma compId() + ensures forall i: T :: {comp(i, id)} comp(i, id) == i + { + + M.compCommute(); //idComposable(); + M.compId(); + M.frameId(); + } + + auto lemma compValid() + ensures forall i1: T, i2: T :: {comp(i1,i2)} valid(comp(i1, i2)) ==> valid(i1) && valid(i2) + {} + + + auto lemma compCommute() + ensures forall i1: T, i2: T :: {comp(i1,i2)} {comp(i2,i1)} comp(i1, i2) == comp(i2, i1) + { + M.compCommute(); + + assert forall i1: T, i2: T :: + (i1 == int(i1.inf, i1.out, i1.dom) && i2 == int(i2.inf, i2.out, i2.dom)) ==> + comp(i1, i2).inf == comp(i2, i1).inf; + + assert forall i1: T, i2: T :: + (i1 == int(i1.inf, i1.out, i1.dom) && i2 == int(i2.inf, i2.out, i2.dom)) ==> + comp(i1, i2).out == comp(i2, i1).out; + } + + // The empty interface composes with valid interfaces + lemma idComposable() + ensures forall i: T :: {valid(i)} valid(i) ==> composable(i, id) + { + M.compCommute(); + M.compId(); + M.frameId(); + } + + // Folds definition of interface composition, avoiding M.frame + lemma compFold(i1: T, i2: T, i: T) + requires i != top + requires i.dom == i1.dom ++ i2.dom + requires i1.dom ** i2.dom == {||} + requires valid(i1) && valid(i2) + requires forall n: Ref :: n in i.dom ==> M.valid(i.inf[n]) + requires forall n: Ref :: n in i1.dom ==> i1.inf[n] == M.comp(i.inf[n], i2.out[n]) + requires forall n: Ref :: n in i2.dom ==> i2.inf[n] == M.comp(i.inf[n], i1.out[n]) + requires forall n: Ref :: n !in i.dom ==> i.inf[n] == M.id + requires forall n: Ref :: n !in i.dom ==> i.out[n] == M.comp(i1.out[n], i2.out[n]) + requires forall n: Ref :: n in i.dom ==> i.out[n] == M.id + ensures comp(i1, i2) == i + { + assume false; + M.frameCompInv(); + M.compCommute(); + + assert i == int({| n: Ref :: + n in i1.dom ? M.frame(i1.inf[n], i2.out[n]) : + (n in i2.dom ? M.frame(i2.inf[n], i1.out[n]) : + M.id) |}, + {| n: Ref :: n !in i1.dom && n !in i2.dom ? M.comp(i1.out[n], i2.out[n]) : M.id |}, + i1.dom ++ i2.dom); + assert comp(i1, i2).inf == i.inf; + } + + // Unfolds definition of interface composition, avoiding M.frame + lemma compUnfold(i1: T, i2: T) + requires valid(comp(i1, i2)) + ensures comp(i1, i2).dom == i1.dom ++ i2.dom + ensures i1.dom ** i2.dom == {||} + ensures valid(i1) && valid(i2) + ensures forall n: Ref :: n in i1.dom ==> i1.inf[n] == M.comp(comp(i1, i2).inf[n], i2.out[n]) + ensures forall n: Ref :: n in i2.dom ==> i2.inf[n] == M.comp(comp(i1, i2).inf[n], i1.out[n]) + ensures forall n: Ref :: n !in comp(i1, i2).dom ==> comp(i1, i2).out[n] == M.comp(i1.out[n], i2.out[n]) + { + idComposable(); + M.compCommute(); + } + + + // Auxiliary lemma to prove that interface composition is associative + lemma compAssocValid(i1: T, i2: T, i3: T) + requires valid(comp(i1, comp(i2, i3))) + ensures comp(i1, comp(i2, i3)) == comp(comp(i1, i2), i3) + { + M.compId(); + M.frameId(); + M.compAssoc(); + M.compCommute(); + M.idValid(); + M.compValid(); + + val i23: T := comp(i2, i3); + val i: T := comp(i1, i23); + + compUnfold(i1, i23); + compUnfold(i2, i3); + + val i12: T := int({| n: Ref :: n in i1.dom ++ i2.dom ? M.comp(i.inf[n], i3.out[n]) : M.id |}, + {| n: Ref :: n !in i1.dom ++ i2.dom ? M.comp(i1.out[n], i2.out[n]) : M.id |}, + i1.dom ++ i2.dom); + + compFold(i1, i2, i12); + assert (forall n: Ref :: i12.inf[n] != M.id ==> n in i12.dom); + assert (forall n: Ref :: i12.out[n] != M.id ==> n !in i12.dom); + assert (forall n: Ref :: n in i12.dom ==> M.valid(i12.inf[n])); + assert (forall n: Ref :: n !in i12.dom ==> M.valid(i12.out[n])); + assume false; + assert (i12.dom == {||} ==> i12.out == zeroFlow); + assert i12 != top; + assume valid(i12); + assert valid(i3); + + assert forall n: Ref :: n in i3.dom ==> i3.inf[n] == M.comp(i.inf[n], i12.out[n]); + compFold(i12, i3, i); + } + + auto lemma compAssoc() + ensures forall a:T, b:T, c:T :: {comp(comp(a, b), c)} {comp(a, comp(b, c))} (comp(comp(a, b), c) == comp(a, comp(b, c))) + { + M.compCommute(); + M.compId(); + M.frameId(); + M.idValid(); + M.compValid(); + assert forall i1:T, i2:T, i3:T :: {comp(comp(i1, i2), i3)} {comp(i1, comp(i2, i3))} (comp(comp(i1, i2), i3) == comp(i1, comp(i2, i3))) with { + if (valid(comp(i1, comp(i2, i3)))) { + compAssocValid(i1, i2, i3); + } else if (valid(comp(comp(i1, i2), i3))) { + compAssocValid(i3, i2, i1); + } + } + } + + // Interface frame + func frame(i1: T, i2: T) returns (i: T) + { + i2 == id ? i1 : + (i1 != top && i2 != top && i2.dom subseteq i1.dom? + int({| n: Ref :: n in i1.dom && n !in i2.dom ? M.comp(i1.inf[n], i2.out[n]) : M.id |}, + {| n: Ref :: n in i2.dom ? M.frame(i2.inf[n], i1.inf[n]) : i1.out[n] |}, + i1.dom -- i2.dom) : + top) + } + + auto lemma frameId() + ensures forall a:T :: {frame(a,id)} frame(a, id) == a + { + M.frameId(); + M.frameCompInv(); + } + + func contextualExt(i1: T, i2: T) returns (ret: Bool) { + valid(i1) && valid(i2) && i1.dom subseteq i2.dom && + (forall n: Ref :: n in i1.dom ==> i1.inf[n] == i2.inf[n]) && + (forall n: Ref :: n !in i2.dom ==> i1.out[n] == i2.out[n]) + } + + func fpuAllowed(i1: T, i2: T) returns (ret: Bool) + { + i1 == i2 + // contextualExt(i1, i2) + } + + auto lemma compFrameInv() + ensures forall a:T, b:T :: {frame(a,b)} valid(frame(a, b)) ==> comp(frame(a, b), b) == a + { + M.frameCompInv(); + M.compCommute(); + // M.frameFrame(); + M.compFrameInv(); + assert forall a:T, b:T :: b == id ==> valid(frame(a,b)) ==> comp(frame(a,b), b) == a; + // assert (forall a:T, b:T, n: Ref :: b != id ==> valid(frame(a, b)) ==> n in b.dom ==> frame(a,b).out[n] == M.frame(b.inf[n], a.inf[n])); + // assert (forall a:T, b:T, n: Ref :: b != id ==> valid(frame(a, b)) ==> n in b.dom ==> b.inf[n] == M.comp(frame(a,b).out[n], M.frame(b.inf[n], frame(a,b).out[n]))); + assert forall a:T, b:T :: b != id ==> valid(frame(a, b)) ==> composable(frame(a, b), b); + assert forall a:T, b:T :: a == int(a.inf, a.out, a.dom) && b == int(b.inf, b.out, b.dom) ==> valid(frame(a, b)) ==> comp(frame(a, b), b).dom == a.dom; + // assert false; + } + + auto lemma fpuValid() + ensures forall a:T, b:T, c:T :: {fpuAllowed(a,b), comp(a,c)} {fpuAllowed(a,b), comp(b,c)} + (fpuAllowed(a,b) && valid(a) && valid(comp(a,c))) ==> valid(comp(b,c)) + {} + + // auto lemma fpuReflexive() + // ensures (forall a:T :: {valid(a)} valid(a) ==> fpuAllowed(a,a)) + // {} + + // auto lemma frameValid() + // ensures forall a:T, b:T :: {frame(a,b)} valid(frame(a,b)) ==> valid(a) && valid(b) + // {} + + // auto lemma weak_frameCompInv() + // ensures forall a:T, b:T:: {comp(a,b)} valid(comp(a, b)) ==> valid(frame(comp(a, b), b)) + // {} + + + // auto lemma frameCompInv() + // ensures forall a:T, b:T:: {comp(a,b)} valid(comp(a, b)) ==> frame(comp(a, b), b) == a + // {} +} diff --git a/test/concurrent/templates/flows_ra.rav b/test/concurrent/templates/flows_ra.rav index 6862cf3..4804882 100644 --- a/test/concurrent/templates/flows_ra.rav +++ b/test/concurrent/templates/flows_ra.rav @@ -29,16 +29,20 @@ interface CCM : Type { lemma frameId() ensures forall a:T :: {frame(a,id)} frame(a, id) == a - { - } + {} - lemma compFrameInv(a: T, b: T) - ensures a == frame(comp(a, b), b) - { - } + // Better name? + lemma frameInv() + ensures forall a:T :: frame(a, a) == id + {} + + auto lemma compFrameInv() + ensures forall a:T, b:T :: {frame(a,b)} valid(frame(a, b)) ==> comp(frame(a, b), b) == a + + lemma frameFrame() + ensures forall a:T, b:T :: {valid(frame(a, b))} valid(frame(a, b)) ==> frame(a, frame(a, b)) == b + {} - //auto lemma compFrameInv() - // ensures forall a:T, b:T :: {frame(a,b)} valid(frame(a, b)) ==> comp(frame(a, b), b) == a //auto lemma frameValid() // ensures forall a:T, b:T :: {frame(a,b)} {valid(a), valid(b)} valid(frame(a,b)) ==> valid(a) && valid(b) @@ -78,8 +82,8 @@ interface FlowsRA[M: CCM] : CancellativeResourceAlgebra { returns (ret: Bool) { valid(i1) && valid(i2) && i1.dom ** i2.dom == {||} - && (forall n: Ref :: n in i1.dom ==> i1.inf[n] == M.comp(i2.out[n], M.frame(i1.inf[n], i2.out[n]))) - && (forall n: Ref :: n in i2.dom ==> i2.inf[n] == M.comp(i1.out[n], M.frame(i2.inf[n], i1.out[n]))) + // && (forall n: Ref :: n in i1.dom ==> i1.inf[n] == M.comp(i2.out[n], M.frame(i1.inf[n], i2.out[n]))) + // && (forall n: Ref :: n in i2.dom ==> i2.inf[n] == M.comp(i1.out[n], M.frame(i2.inf[n], i1.out[n]))) && (forall n: Ref :: n in i1.dom ==> M.valid(M.frame(i1.inf[n], i2.out[n]))) && (forall n: Ref :: n in i2.dom ==> M.valid(M.frame(i2.inf[n], i1.out[n]))) } @@ -145,6 +149,10 @@ interface FlowsRA[M: CCM] : CancellativeResourceAlgebra { assert forall i1: T, i2: T :: (i1 == int(i1.inf, i1.out, i1.dom) && i2 == int(i2.inf, i2.out, i2.dom)) ==> comp(i1, i2).inf == comp(i2, i1).inf; + + assert forall i1: T, i2: T :: + (i1 == int(i1.inf, i1.out, i1.dom) && i2 == int(i2.inf, i2.out, i2.dom)) ==> + comp(i1, i2).out == comp(i2, i1).out; } // The empty interface composes with valid interfaces @@ -170,6 +178,7 @@ interface FlowsRA[M: CCM] : CancellativeResourceAlgebra { requires forall n: Ref :: n in i.dom ==> i.out[n] == M.id ensures comp(i1, i2) == i { + // assume false; M.frameCompInv(); M.compCommute(); @@ -179,6 +188,7 @@ interface FlowsRA[M: CCM] : CancellativeResourceAlgebra { M.id) |}, {| n: Ref :: n !in i1.dom && n !in i2.dom ? M.comp(i1.out[n], i2.out[n]) : M.id |}, i1.dom ++ i2.dom); + assert comp(i1, i2).inf == i.inf; } // Unfolds definition of interface composition, avoiding M.frame @@ -193,6 +203,7 @@ interface FlowsRA[M: CCM] : CancellativeResourceAlgebra { { idComposable(); M.compCommute(); + M.compFrameInv(); } @@ -223,8 +234,8 @@ interface FlowsRA[M: CCM] : CancellativeResourceAlgebra { assert (forall n: Ref :: i12.out[n] != M.id ==> n !in i12.dom); assert (forall n: Ref :: n in i12.dom ==> M.valid(i12.inf[n])); assert (forall n: Ref :: n !in i12.dom ==> M.valid(i12.out[n])); - // assert (i12.dom == {||} ==> i12.out == zeroFlow); - assert valid(i12); + assert (i12.dom == {||} ==> i12.out == zeroFlow); + assert i12 != top; assert valid(i3); assert forall n: Ref :: n in i3.dom ==> i3.inf[n] == M.comp(i.inf[n], i12.out[n]); @@ -252,9 +263,10 @@ interface FlowsRA[M: CCM] : CancellativeResourceAlgebra { func frame(i1: T, i2: T) returns (i: T) { i2 == id ? i1 : - (i1 != top && i2 != top ? + (valid(i1) && valid(i2) && i2.dom subseteq i1.dom? int({| n: Ref :: n in i1.dom && n !in i2.dom ? M.comp(i1.inf[n], i2.out[n]) : M.id |}, - {| n: Ref :: n in i2.dom ? M.frame(i2.inf[n], i1.inf[n]) : i1.out[n] |}, + {| n: Ref :: n in i2.dom ? M.frame(i2.inf[n], i1.inf[n]) : + (n in i1.dom ? M.id : M.frame(i1.out[n], i2.out[n])) |}, i1.dom -- i2.dom) : top) } @@ -265,6 +277,20 @@ interface FlowsRA[M: CCM] : CancellativeResourceAlgebra { M.frameId(); M.frameCompInv(); } + + lemma frameInv() + ensures forall a:T :: valid(a) ==> frame(a, a) == id + { + M.frameCompInv(); + M.compFrameInv(); + M.frameInv(); + M.frameFrame(); + assert forall a: T :: a == id ==> frame(a,a) == id; + assert forall a: T :: a != id ==> valid(a) ==> frame(a,a).dom == id.dom; + assert forall a: T :: a != id ==> valid(a) ==> frame(a,a).inf == id.inf; + assert forall a: T :: a != id ==> valid(a) ==> frame(a,a) == id; + } + func contextualExt(i1: T, i2: T) returns (ret: Bool) { valid(i1) && valid(i2) && i1.dom subseteq i2.dom && @@ -278,31 +304,61 @@ interface FlowsRA[M: CCM] : CancellativeResourceAlgebra { // contextualExt(i1, i2) } - // auto lemma compFrameInv() - // ensures forall a:T, b:T :: {frame(a,b)} valid(frame(a, b)) ==> comp(frame(a, b), b) == a - // { - // M.frameCompInv(); - // } - - // auto lemma fpuValid() - // ensures forall a:T, b:T, c:T :: {fpuAllowed(a,b), comp(a,c)} {fpuAllowed(a,b), comp(b,c)} - // (fpuAllowed(a,b) && valid(a) && valid(comp(a,c))) ==> valid(comp(b,c)) - // {} - - // auto lemma fpuReflexive() - // ensures (forall a:T :: {valid(a)} valid(a) ==> fpuAllowed(a,a)) - // {} - - // auto lemma frameValid() - // ensures forall a:T, b:T :: {frame(a,b)} valid(frame(a,b)) ==> valid(a) && valid(b) - // {} - - // auto lemma weak_frameCompInv() - // ensures forall a:T, b:T:: {comp(a,b)} valid(comp(a, b)) ==> valid(frame(comp(a, b), b)) - // {} + auto lemma compFrameInv() + ensures forall a:T, b:T :: {frame(a,b)} valid(frame(a, b)) ==> comp(frame(a, b), b) == a + { + M.frameCompInv(); + // M.compCommute(); + M.compFrameInv(); + M.frameInv(); + M.frameFrame(); + frameInv(); + assert forall a:T, b:T :: a == id || b == id ==> valid(frame(a,b)) ==> comp(frame(a,b), b) == a; + assert forall a:T, b:T :: a != id ==> b != id ==> valid(frame(a,b)) ==> comp(frame(a,b), b).dom == a.dom; + } + auto lemma fpuValid() + ensures forall a:T, b:T, c:T :: {fpuAllowed(a,b), comp(a,c)} {fpuAllowed(a,b), comp(b,c)} + (fpuAllowed(a,b) && valid(a) && valid(comp(a,c))) ==> valid(comp(b,c)) + {} + + auto lemma fpuReflexive() + ensures (forall a:T :: {valid(a)} valid(a) ==> fpuAllowed(a,a)) + {} + + auto lemma frameValid() + ensures forall a:T, b:T :: {frame(a,b)} valid(frame(a,b)) ==> valid(a) && valid(b) + {} + + auto lemma weak_frameCompInv() + ensures forall a:T, b:T:: {comp(a,b)} valid(comp(a, b)) ==> valid(frame(comp(a, b), b)) + { + M.frameCompInv(); + M.compCommute(); + // M.frameFrame(); + M.compFrameInv(); + // compId(); + M.frameInv(); + // assert forall a:T, b:T:: a == id || b == id ==> valid(comp(a, b)) ==> valid(frame(comp(a, b), b)); + // assert forall a:T, b:T:: a != id ==> b != id ==> valid(comp(a, b)) ==> valid(frame(comp(a, b), b)); + } - // auto lemma frameCompInv() - // ensures forall a:T, b:T:: {comp(a,b)} valid(comp(a, b)) ==> frame(comp(a, b), b) == a - // {} + auto lemma frameCompInv() + ensures forall a:T, b:T:: {comp(a,b)} valid(comp(a, b)) ==> frame(comp(a, b), b) == a + { + M.frameCompInv(); + M.compFrameInv(); + M.frameInv(); + M.frameFrame(); + frameInv(); + // assume forall a: M, b: M :: M.valid(M.frame(a, b)) ==> M.frame(a, M.frame(a,b)) == b; + assert forall a:T, b:T:: a == id || b == id ==> valid(comp(a, b)) ==> frame(comp(a, b), b) == a; + assert forall a:T, b:T:: a != id ==> b != id ==> valid(comp(a, b)) ==> frame(comp(a, b), b).dom == a.dom; + assert forall a:T, b:T, n: Ref :: a != id ==> b != id ==> n in a.dom ==> valid(comp(a, b)) ==> frame(comp(a, b), b).inf[n] == a.inf[n]; + assert forall a:T, b:T, n: Ref :: a != id ==> b != id ==> n !in a.dom ==> valid(comp(a, b)) ==> frame(comp(a, b), b).inf[n] == a.inf[n]; + assert forall a:T, b:T :: a != id ==> b != id ==> valid(comp(a, b)) ==> frame(comp(a, b), b).inf == a.inf; + assert forall a:T, b:T, n: Ref :: a != id ==> b != id ==> n in a.dom ==> valid(comp(a, b)) ==> frame(comp(a, b), b).out[n] == a.out[n]; + assert forall a:T, b:T, n: Ref :: a != id ==> b != id ==> n !in a.dom ==> valid(comp(a, b)) ==> frame(comp(a, b), b).out[n] == a.out[n]; + assert forall a:T, b:T :: a != id ==> b != id ==> valid(comp(a, b)) ==> frame(comp(a, b), b).out == a.out; + } }