Skip to content

Commit

Permalink
complete flow_RA
Browse files Browse the repository at this point in the history
  • Loading branch information
@nrp364
nrp364 committed May 12, 2024
1 parent c4ac315 commit 8c8fbc7
Show file tree
Hide file tree
Showing 2 changed files with 428 additions and 39 deletions.
333 changes: 333 additions & 0 deletions test/bugs/assume_false_bug.rav
View file
Original file line number Diff line number Diff line change
@@ -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
// {}
}
Loading

0 comments on commit 8c8fbc7

Please sign in to comment.