Skip to content

Commit

Permalink
Changed Auth RA to work with any resource algebra, not just cancellat…
Browse files Browse the repository at this point in the history 
…ive RAs
  • Loading branch information
@EkanshdeepGupta
EkanshdeepGupta committed May 8, 2024
1 parent e4733e3 commit 041f4d5
Showing 1 changed file with 84 additions and 76 deletions.
160 changes: 84 additions & 76 deletions lib/library/resource_algebra.rav
View file
Original file line number Diff line number Diff line change
Expand Up @@ -180,7 +180,7 @@ module Nat : CancellativeResourceAlgebra {
//{}
}

module Auth[M: CancellativeResourceAlgebra] : ResourceAlgebra {
module Auth[M: ResourceAlgebra] : ResourceAlgebra {
rep type T = data {
case frag(f_proj1: M);
case auth_frag(af_proj1: M, af_proj2: M);
Expand Down Expand Up @@ -229,7 +229,11 @@ module Auth[M: CancellativeResourceAlgebra] : ResourceAlgebra {

(a == auth_frag(a.af_proj1, a.af_proj2) && b == auth_frag(b.af_proj1, b.af_proj2) ?
(M.valid(M.frame(b.af_proj1, a.af_proj1)) &&
M.valid(M.frame(M.frame(b.af_proj1, b.af_proj2), M.frame(a.af_proj1, a.af_proj2)))) :
// M.valid(M.frame(M.frame(b.af_proj1, b.af_proj2), M.frame(a.af_proj1, a.af_proj2)))
M.valid(M.frame(a.af_proj2, b.af_proj2))
)

:

false)
}
Expand All @@ -252,7 +256,12 @@ module Auth[M: CancellativeResourceAlgebra] : ResourceAlgebra {

auto lemma compValid()
ensures forall a:T, b:T :: {comp(a,b)} valid(comp(a, b)) ==> valid(a) && valid(b)
{ M.compValid(); M.compAssoc(); M.frameCompInv(); M.compFrameInv(); }
{
M.compValid(); M.compAssoc(); M.compFrameInv();
M.weak_frameCompInv();


}

auto lemma frameId()
ensures forall a:T :: {frame(a,id)} frame(a, id) == a
Expand All @@ -264,7 +273,6 @@ module Auth[M: CancellativeResourceAlgebra] : ResourceAlgebra {
M.compCommute();
M.compId();
M.compValid();
M.frameCompInv();
M.compFrameInv();
}

Expand All @@ -273,7 +281,7 @@ module Auth[M: CancellativeResourceAlgebra] : ResourceAlgebra {
(fpuAllowed(a,b) && valid(a) && valid(comp(a,c))) ==> valid(comp(b,c))
{
M.idValid(); M.compAssoc(); M.compCommute(); M.compId(); M.compValid(); M.frameId(); M.compFrameInv();
M.fpuValid(); M.fpuReflexive(); M.frameValid(); M.weak_frameCompInv(); M.frameCompInv(); M.frameReflexive();
M.fpuValid(); M.fpuReflexive(); M.frameValid(); M.weak_frameCompInv();
}


Expand All @@ -285,15 +293,15 @@ module Auth[M: CancellativeResourceAlgebra] : ResourceAlgebra {
ensures forall a:T, b:T :: {frame(a,b)} valid(frame(a,b)) ==> valid(a) && valid(b)
{
M.idValid(); M.compAssoc(); M.compCommute(); M.compId(); M.compValid(); M.frameId(); M.compFrameInv();
M.fpuValid(); M.fpuReflexive(); M.frameValid(); M.weak_frameCompInv(); M.frameCompInv(); M.frameReflexive();
M.fpuValid(); M.fpuReflexive(); M.frameValid(); M.weak_frameCompInv();

}

auto lemma weak_frameCompInv()
ensures forall a:T, b:T:: {comp(a,b)} valid(comp(a, b)) ==> valid(frame(comp(a, b), b))
{
M.idValid(); M.compAssoc(); M.compCommute(); M.compId(); M.compValid(); M.frameId(); M.compFrameInv();
M.fpuValid(); M.fpuReflexive(); M.frameValid(); M.weak_frameCompInv(); M.frameCompInv(); M.frameReflexive();
M.fpuValid(); M.fpuReflexive(); M.frameValid(); M.weak_frameCompInv();
}

}
Expand Down Expand Up @@ -983,92 +991,92 @@ module AtomicTokenRA[InArg: Type, RetArg: Type] : ResourceAlgebra {
{}
}

module InvRA[X: Type] : ResourceAlgebra {
rep type T = data {
case inv_null;
case inv_closed(inv_closed_proj1: X);
case inv_open(inv_open_proj1: X);
case inv_top
}
// module InvRA[X: Type] : ResourceAlgebra {
// rep type T = data {
// case inv_null;
// case inv_closed(inv_closed_proj1: X);
// case inv_open(inv_open_proj1: X);
// case inv_top
// }

val id: T = inv_null()
// val id: T = inv_null()

func valid(n:T)
returns (ret:Bool)
{
n == inv_closed(n.inv_closed_proj1) || n == inv_open(n.inv_open_proj1) || n == inv_null()
}
// func valid(n:T)
// returns (ret:Bool)
// {
// n == inv_closed(n.inv_closed_proj1) || n == inv_open(n.inv_open_proj1) || n == inv_null()
// }

func comp(a:T, b:T) returns (ret:T) {
a == id ? b :
(b == id ? a :
(a == inv_closed(a.inv_closed_proj1) && b == a ? a :
(a == inv_closed(a.inv_closed_proj1) && b == inv_open(a.inv_closed_proj1) ? b :
(a == inv_open(a.inv_open_proj1) && b == inv_closed(a.inv_open_proj1) ? a : inv_top))))
}
// func comp(a:T, b:T) returns (ret:T) {
// a == id ? b :
// (b == id ? a :
// (a == inv_closed(a.inv_closed_proj1) && b == a ? a :
// (a == inv_closed(a.inv_closed_proj1) && b == inv_open(a.inv_closed_proj1) ? b :
// (a == inv_open(a.inv_open_proj1) && b == inv_closed(a.inv_open_proj1) ? a : inv_top))))
// }

func frame(a:T, b:T) returns (ret:T) {
b == id ? a :
(a == inv_closed(a.inv_closed_proj1) && a == b ? a :
(a == inv_open(a.inv_open_proj1) && a == b ? id :
(a == inv_open(a.inv_open_proj1) && b == inv_closed(a.inv_open_proj1) ?
inv_open(a.inv_open_proj1) : inv_top())))
}
// func frame(a:T, b:T) returns (ret:T) {
// b == id ? a :
// (a == inv_closed(a.inv_closed_proj1) && a == b ? a :
// (a == inv_open(a.inv_open_proj1) && a == b ? id :
// (a == inv_open(a.inv_open_proj1) && b == inv_closed(a.inv_open_proj1) ?
// inv_open(a.inv_open_proj1) : inv_top())))
// }

func fpuAllowed(a:T, b:T) returns (ret: Bool) {
a == b ? true :
(a == inv_open(a.inv_open_proj1) && b == inv_closed(b.inv_closed_proj1) ?
a.inv_open_proj1 == b.inv_closed_proj1 :
false
)
// func fpuAllowed(a:T, b:T) returns (ret: Bool) {
// a == b ? true :
// (a == inv_open(a.inv_open_proj1) && b == inv_closed(b.inv_closed_proj1) ?
// a.inv_open_proj1 == b.inv_closed_proj1 :
// false
// )

}
// }

auto lemma idValid()
ensures valid(id)
{}
// 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 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)
{ assert forall a:T, b:T :: (a == inv_closed(a.inv_closed_proj1)) ==> (comp(a, b) == comp(b, a)); }
// auto lemma compCommute()
// ensures forall a:T, b:T :: {comp(a,b)} {comp(b,a)} comp(a, b) == comp(b, a)
// { assert forall a:T, b:T :: (a == inv_closed(a.inv_closed_proj1)) ==> (comp(a, b) == comp(b, a)); }

auto lemma compId()
ensures forall a:T :: {comp(a, id)} comp(a, id) == a
{}
// auto lemma compId()
// ensures forall a:T :: {comp(a, id)} comp(a, id) == a
// {}

auto lemma compValid()
ensures forall a:T, b:T :: {comp(a,b)} valid(comp(a, b)) ==> valid(a) && valid(b)
{}
// auto lemma compValid()
// ensures forall a:T, b:T :: {comp(a,b)} valid(comp(a, b)) ==> valid(a) && valid(b)
// {}

auto lemma frameId()
ensures forall a:T :: {frame(a,id)} frame(a, id) == a
{}
// auto lemma frameId()
// ensures forall a:T :: {frame(a,id)} frame(a, id) == a
// {}

auto lemma compFrameInv()
ensures forall a:T, b:T :: {comp(frame(a, b), b)} valid(frame(a, b)) ==> comp(frame(a, b), b) == a
{}
// auto lemma compFrameInv()
// ensures forall a:T, b:T :: {comp(frame(a, b), b)} valid(frame(a, b)) ==> comp(frame(a, b), b) == a
// {}

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 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 :: {fpuAllowed(a,a)} valid(a) ==> fpuAllowed(a,a))
{}
// auto lemma fpuReflexive()
// ensures (forall a:T :: {fpuAllowed(a,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 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:: {frame(comp(a, b), b)} valid(comp(a, b)) ==> valid(frame(comp(a, b), b))
{ assert forall a:T, b:T:: (a == inv_closed(a.inv_closed_proj1)) ==> (valid(comp(a, b)) ==> valid(frame(comp(a, b), b))); }
}
// auto lemma weak_frameCompInv()
// ensures forall a:T, b:T:: {frame(comp(a, b), b)} valid(comp(a, b)) ==> valid(frame(comp(a, b), b))
// { assert forall a:T, b:T:: (a == inv_closed(a.inv_closed_proj1)) ==> (valid(comp(a, b)) ==> valid(frame(comp(a, b), b))); }
// }



Expand Down

0 comments on commit 041f4d5

Please sign in to comment.