diff --git a/router/dataplane_concurrency_model.gobra b/router/dataplane_concurrency_model.gobra index 65ea156c7..1b8207c17 100644 --- a/router/dataplane_concurrency_model.gobra +++ b/router/dataplane_concurrency_model.gobra @@ -18,6 +18,7 @@ package router import ( gsync "verification/utils/ghost_sync" + "verification/utils/resalgebra" io "verification/io" ) @@ -245,32 +246,439 @@ func multiElemWitnessConvAux(y ElemRA, k Key, es seq[io.Val], i int) { /**** End of MultiElemWitness helper functions ****/ /////////////////////////////////////// RA definitions /////////////////////////////////////// + ghost type Key = option[io.Ifs] ghost type Val = set[io.Pkt] ghost type Elem = io.Pkt -ghost type ElemRA domain{} +type DictWithTopBot interface {} +ghost type Top ghost struct{} +ghost type Bottom ghost struct{} +ghost type Dict ghost struct { + V dict[Key]Val +} + +Dict implements DictWithTopBot + +ghost type TypeAuthRA ghost struct{} + +ghost type AuthCarrier ghost struct { + fst DictWithTopBot + snd Dict +} + +ghost +decreases +pure func AuthView(m Dict) resalgebra.Elem { + return AuthCarrier{m, Dict{}} +} + +ghost +decreases +pure func FragView(m Dict) resalgebra.Elem { + return AuthCarrier{Bottom{}, m} +} + +TypeAuthRA implements resalgebra.RA + +ghost +decreases +pure func (ra TypeAuthRA) IsElem(e resalgebra.Elem) (res bool) { + return typeOf(e) == type[AuthCarrier] && + let c := e.(AuthCarrier) in + c.fst === Bottom{} || + c.fst === Top{} || + typeOf(c.fst) == type[Dict] +} + +ghost +requires ra.IsElem(e) +decreases +pure func (ra TypeAuthRA) IsValid(e resalgebra.Elem) bool { + return let x := e.(AuthCarrier) in + x.fst === Bottom{} || + (typeOf(x.fst) == type[Dict] && dictLessThan(x.snd.V, x.fst.(Dict).V)) +} + +ghost +decreases +pure func dictLessThan(d1 dict[Key]Val, d2 dict[Key]Val) bool { + return (forall k Key :: k elem domain(d1) ==> k elem domain(d2) && AsSet(d1[k]) union AsSet(d2[k]) == AsSet(d2[k])) +} + +ghost +ensures forall d1 dict[Key]Val, d2 dict[Key]Val, d3 dict[Key]Val :: {dictLessThan(d1, d2), dictLessThan(d2, d3)} dictLessThan(d1, d2) && dictLessThan(d2, d3) ==> + dictLessThan(d1, d3) +decreases +func dictLessThanTransitiveQ() { + // proven +} + +ghost +ensures dictLessThan(d1, d3) && dictLessThan(d2, d3) ==> dictLessThan(dictMax(d1, d2), d3) +decreases +pure func dictMaxIsLessThan(d1 dict[Key]Val, d2 dict[Key]Val, d3 dict[Key]Val) U { + return dictUnionIsLessThan(d1, d2, d3) +} + +ghost +decreases +pure func dictMax(d1 dict[Key]Val, d2 dict[Key]Val) dict[Key]Val { + // logically redundant but it simplifies automated reasoning when + // either dictLessThan(d1, d2) or dictLessThan(d2, d1) is known. + return dictLessThan(d1, d2) ? d2 : dictLessThan(d2, d1) ? d1 : dictUnion(d1, d2) +} + +ghost +requires dictLessThan(d1, d2) && dictLessThan(d2, d1) +ensures d1 === d2 +decreases +func dictLessEq(d1 dict[Key]Val, d2 dict[Key]Val) { + assert forall k Key :: k elem domain(d1) ==> k elem domain(d2) && AsSet(d1[k]) union AsSet(d2[k]) == AsSet(d2[k]) + assert forall k Key :: k elem domain(d2) ==> k elem domain(d1) && AsSet(d1[k]) union AsSet(d2[k]) == AsSet(d1[k]) + assert domain(d1) == domain(d2) +} + +ghost +decreases +pure func keyInDict(d dict[Key]Val, k Key, v io.Pkt) bool { + return k elem domain(d) && v elem AsSet(d[k]) +} + +ghost +ensures domain(dictMax(d1, d2)) == domain(d1) union domain(d2) +ensures let d := dictMax(d1, d2) in + forall k Key, v io.Pkt :: !keyInDict(d, k, v) == !(keyInDict(d1, k, v) || keyInDict(d2, k, v)) +decreases +func dictMaxAssocLemma0(d1 dict[Key]Val, d2 dict[Key]Val) { + reveal dictUnion(d1, d2) +} + +ghost +ensures domain(dictMax(d1, dictMax(d2, d3))) == domain(d1) union domain(d2) union domain(d3) +ensures let d := dictMax(d1, dictMax(d2, d3)) in + forall k Key, v io.Pkt :: keyInDict(d, k, v) == (keyInDict(d1, k, v) || keyInDict(d2, k, v) || keyInDict(d3, k, v)) +decreases +func dictMaxAssocLemma1(d1 dict[Key]Val, d2 dict[Key]Val, d3 dict[Key]Val) { + d := dictMax(d1, dictMax(d2, d3)) + assert forall k Key, v io.Pkt :: (keyInDict(d1, k, v) || keyInDict(d2, k, v) || keyInDict(d3, k, v)) ==> keyInDict(d, k, v) + dictMaxAssocLemma0(d2, d3) + dictMaxAssocLemma0(d1, dictMax(d2, d3)) + assert forall k Key, v io.Pkt :: keyInDict(d, k, v) ==> (keyInDict(d1, k, v) || keyInDict(d2, k, v) || keyInDict(d3, k, v)) +} -pred ElemAuth(ghost m dict[Key]Val, ghost y ElemRA) +ghost +ensures domain(dictMax(dictMax(d1, d2), d3)) == domain(d1) union domain(d2) union domain(d3) +ensures let d := dictMax(dictMax(d1, d2), d3) in + forall k Key, v io.Pkt :: keyInDict(d, k, v) == (keyInDict(d1, k, v) || keyInDict(d2, k, v) || keyInDict(d3, k, v)) +decreases +func dictMaxAssocLemma2(d1 dict[Key]Val, d2 dict[Key]Val, d3 dict[Key]Val) { + d := dictMax(dictMax(d1, d2), d3) + assert forall k Key, v io.Pkt :: (keyInDict(d1, k, v) || keyInDict(d2, k, v) || keyInDict(d3, k, v)) ==> keyInDict(d, k, v) + dictMaxAssocLemma0(d1, d2) + dictMaxAssocLemma0(dictMax(d1, d2), d3) + assert forall k Key, v io.Pkt :: keyInDict(d, k, v) ==> (keyInDict(d1, k, v) || keyInDict(d2, k, v) || keyInDict(d3, k, v)) +} -pred ElemWitness(ghost y ElemRA, ghost k Key, ghost e Elem) +ghost +requires domain(d1) === domain(d2) // requirement necessary, as some keys might point to an empty set +requires forall k Key, v io.Pkt :: { keyInDict(d1, k, v) }{ keyInDict(d2, k, v) } keyInDict(d1, k, v) == keyInDict(d2, k, v) +ensures d1 === d2 +decreases +func dictExtensionality(d1 dict[Key]Val, d2 dict[Key]Val) { + assert (d1 === d2) ==> (forall k Key, v io.Pkt :: keyInDict(d1, k, v) == keyInDict(d2, k, v)) + assert forall k Key :: k elem domain(d1) ==> forall e io.Pkt :: e elem AsSet(d1[k]) == keyInDict(d1, k, e) + assert forall k Key :: k elem domain(d1) ==> forall e io.Pkt :: e elem AsSet(d1[k]) ==> e elem AsSet(d2[k]) + assert forall k Key :: k elem domain(d2) ==> forall e io.Pkt :: e elem AsSet(d2[k]) ==> e elem AsSet(d1[k]) + lemmaSubSet() + assert forall k Key :: k elem domain(d1) ==> AsSet(d1[k]) union AsSet(d2[k]) == AsSet(d2[k]) + assert forall k Key :: k elem domain(d2) ==> AsSet(d2[k]) union AsSet(d1[k]) == AsSet(d1[k]) + assert dictLessThan(d1, d2) + assert dictLessThan(d2, d1) + dictLessEq(d1, d2) +} + +ghost +ensures forall s1 Val, s2 Val :: {s1 union s2} (forall e io.Pkt :: e elem s1 ==> e elem s2) ==> s1 union s2 == s2 +decreases +func lemmaSubSet() { + // proven +} + +ghost +ensures dictMax(d1, dictMax(d2, d3)) === dictMax(dictMax(d1, d2), d3) +decreases +func dictMaxAssoc(d1 dict[Key]Val, d2 dict[Key]Val, d3 dict[Key]Val) { + dictMaxAssocLemma1(d1, d2, d3) + dictMaxAssocLemma2(d1, d2, d3) + dictExtensionality(dictMax(d1, dictMax(d2, d3)), dictMax(dictMax(d1, d2), d3)) +} + +ghost +ensures dictMax(d1, d2) == dictMax(d2, d1) +decreases +func dictMaxIsComm(d1 dict[Key]Val, d2 dict[Key]Val) { + if dictLessThan(d1, d2) && dictLessThan(d2, d1) { + dictLessEq(d1, d2) + } + assert d1 != d2 && dictLessThan(d1, d2) ==> !dictLessThan(d2, d1) + assert dictLessThan(d1, d2) ==> dictMax(d1, d2) == d2 + assert dictLessThan(d1, d2) ==> dictMax(d2, d1) == d2 + assert dictLessThan(d2, d1) ==> dictMax(d1, d2) == d1 + assert dictLessThan(d2, d1) ==> dictMax(d2, d1) == d1 + dictUnionIsComm(d1, d2) +} + +ghost +requires ra.IsElem(e) +ensures res !== none[resalgebra.Elem] ==> ra.IsElem(get(res)) +decreases +pure func (ra TypeAuthRA) Core(e resalgebra.Elem) (ghost res option[resalgebra.Elem]) { + return let x := e.(AuthCarrier) in + some(resalgebra.Elem(AuthCarrier{Bottom{}, x.snd})) +} ghost +requires ra.IsElem(e1) && ra.IsElem(e2) +ensures ra.IsElem(res) decreases +pure func (ra TypeAuthRA) Compose(e1 resalgebra.Elem, e2 resalgebra.Elem) (res resalgebra.Elem) { + return let c1 := e1.(AuthCarrier) in + let c2 := e2.(AuthCarrier) in + (c1.fst === Bottom{} ? + AuthCarrier{c2.fst, Dict{dictMax(c1.snd.V, c2.snd.V)}} : + (c2.fst === Bottom{} ? + AuthCarrier{c1.fst, Dict{dictMax(c1.snd.V, c2.snd.V)}} : + AuthCarrier{Top{}, Dict{dictMax(c1.snd.V, c2.snd.V)}})) +} + +ghost +requires ra.IsElem(e1) && ra.IsElem(e2) && ra.IsElem(e3) +ensures ra.Compose(ra.Compose(e1, e2), e3) === ra.Compose(e1, ra.Compose(e2, e3)) +decreases +func (ra TypeAuthRA) ComposeAssoc(e1 resalgebra.Elem, e2 resalgebra.Elem, e3 resalgebra.Elem) { + c1 := e1.(AuthCarrier) + c2 := e2.(AuthCarrier) + c3 := e3.(AuthCarrier) + + comp1 := ra.Compose(ra.Compose(e1, e2), e3).(AuthCarrier) + comp2 := ra.Compose(e1, ra.Compose(e2, e3)).(AuthCarrier) + + assert comp1.fst === comp2.fst + dictMaxAssoc(c1.snd.V, c2.snd.V, c3.snd.V) +} + +ghost +requires ra.IsElem(e1) && ra.IsElem(e2) +ensures ra.Compose(e1, e2) === ra.Compose(e2, e1) +decreases +func (ra TypeAuthRA) ComposeComm(e1 resalgebra.Elem, e2 resalgebra.Elem) { + c1 := e1.(AuthCarrier) + c2 := e2.(AuthCarrier) + dictMaxIsComm(c1.snd.V, c2.snd.V) +} + +ghost +requires ra.IsElem(e) +ensures let c := ra.Core(e) in + c !== none[resalgebra.Elem] ==> ra.Compose(get(c), e) === e +decreases +func (ra TypeAuthRA) CoreId(e resalgebra.Elem) { + // proven +} + +ghost +requires ra.IsElem(e) +requires ra.Core(e) !== none[resalgebra.Elem] +ensures let c := ra.Core(e) in + let cc := ra.Core(get(c)) in + cc !== none[resalgebra.Elem] && + get(cc) === get(c) +decreases +func (ra TypeAuthRA) CoreIdem(e resalgebra.Elem) { + // proven +} + +ghost +requires ra.IsElem(e1) && ra.IsElem(e2) +requires ra.Core(e1) !== none[resalgebra.Elem] +// fully expanded version of <= due to Gobra's lack of `Self` in interface specs +requires exists e3 resalgebra.Elem :: { ra.IsElem(e3) } ra.IsElem(e3) && e2 === ra.Compose(e1, e3) +ensures ra.Core(e2) !== none[resalgebra.Elem] +ensures exists e4 resalgebra.Elem :: { ra.IsElem(e4) } ra.IsElem(e4) && get(ra.Core(e2)) === ra.Compose(get(ra.Core(e1)), e4) +decreases +func (ra TypeAuthRA) CoreMono(e1 resalgebra.Elem, e2 resalgebra.Elem) { + // proven +} + +ghost +requires ra.IsElem(e1) && ra.IsElem(e2) +requires ra.IsValid(ra.Compose(e1, e2)) +ensures ra.IsValid(e1) +decreases +func (ra TypeAuthRA) ValidOp(e1 resalgebra.Elem, e2 resalgebra.Elem) { + c := ra.Compose(e1, e2).(AuthCarrier) + c1 := e1.(AuthCarrier) + c2 := e2.(AuthCarrier) + if (c1.fst !== Bottom{}) { + fst := c.fst.(Dict).V + snd := c.snd.V + assert dictLessThan(snd, fst) + assert snd === dictMax(c1.snd.V, c2.snd.V) + } +} + +ghost type ElemRA = resalgebra.LocName + +pred ElemAuth(ghost m dict[Key]Val, ghost y ElemRA) { + resalgebra.GhostLocation(y, TypeAuthRA{}, AuthView(Dict{m})) +} + +pred ElemWitness(ghost y ElemRA, ghost k Key, ghost e Elem) { + let d := Dict{dict[Key]Val{k: set[io.Pkt]{e}}} in + resalgebra.GhostLocation(y, TypeAuthRA{}, FragView(d)) +} + +ghost requires ElemAuth(m, y) && ElemWitness(y, k, e) ensures ElemAuth(m, y) && ElemWitness(y, k, e) && k elem domain(m) && e elem AsSet(m[k]) -func ApplyElemWitness(m dict[Key]Val, y ElemRA, k Key, e Elem) +decreases +func ApplyElemWitness(m dict[Key]Val, y ElemRA, k Key, e Elem) { + unfold ElemAuth(m, y) + unfold ElemWitness(y, k, e) + d := Dict{dict[Key]Val{k: set[io.Pkt]{e}}} + resalgebra.GhostOp2(y, TypeAuthRA{}, AuthView(Dict{m}), FragView(d)) + c := (TypeAuthRA{}).Compose(AuthView(Dict{m}), FragView(d)) + resalgebra.GhostValid(y, TypeAuthRA{}, c) + // The composition must be valid, which implies the element of the FragView must be in m + resalgebra.GhostOp1(y, TypeAuthRA{}, AuthView(Dict{m}), FragView(d)) + fold ElemAuth(m, y) + fold ElemWitness(y, k, e) +} ghost -decreases requires ElemAuth(m, y) -ensures ElemAuth(io.insert(m, k, e), y) && ElemWitness(y, k, e) -func UpdateElemWitness(m dict[Key]Val, y ElemRA, k Key, e Elem) +ensures ElemAuth(io.insert(m, k, e), y) +ensures ElemWitness(y, k, e) +decreases +func UpdateElemWitness(m dict[Key]Val, y ElemRA, k Key, e Elem) { + unfold ElemAuth(m, y) + d := Dict{dict[Key]Val{k: set[io.Pkt]{e}}} + c := (TypeAuthRA{}).Compose(AuthView(Dict{io.insert(m, k, e)}), FragView(d)) + updateElemWitnessAuxLemma(m, k, e) + assert resalgebra.IsFramePreservingUpdate(TypeAuthRA{}, AuthView(Dict{m}), c) + resalgebra.GhostUpdate(y, TypeAuthRA{}, AuthView(Dict{m}), c) + assert resalgebra.GhostLocation(y, TypeAuthRA{}, c) + resalgebra.GhostOp1(y, TypeAuthRA{}, AuthView(Dict{io.insert(m, k, e)}), FragView(d)) + fold ElemAuth(io.insert(m, k, e), y) + fold ElemWitness(y, k, e) +} +// by far, the slowest lemma to prove atm ghost +ensures let d := Dict{dict[Key]Val{k: set[io.Pkt]{e}}} in + let c := (TypeAuthRA{}).Compose(AuthView(Dict{io.insert(m, k, e)}), FragView(d)) in + resalgebra.IsFramePreservingUpdate(TypeAuthRA{}, AuthView(Dict{m}), c) decreases +func updateElemWitnessAuxLemma(m dict[Key]Val, k Key, e Elem) { + ra := TypeAuthRA{} + a := AuthView(Dict{m}) + d := Dict{dict[Key]Val{k: set[io.Pkt]{e}}} + c := ra.Compose(AuthView(Dict{io.insert(m, k, e)}), FragView(d)) + assert ra.IsValid(a) ==> ra.IsValid(c) + assert forall ee resalgebra.Elem :: ra.IsElem(ee) && ra.IsValid(ra.Compose(a, ee)) ==> + (let ae := ra.Compose(a, ee).(AuthCarrier) in + (ae.fst == Bottom{} || dictLessThan(ae.snd.V, m))) + dictLessThanTransitiveQ() + assert forall ee resalgebra.Elem :: ra.IsElem(ee) && ra.IsValid(ra.Compose(a, ee)) ==> + ee.(AuthCarrier).fst === Bottom{} && + dictLessThan(ee.(AuthCarrier).snd.V, m) && + dictLessThan(m, io.insert(m, k, e)) && + dictLessThan(ee.(AuthCarrier).snd.V, io.insert(m, k, e)) + assert forall ee resalgebra.Elem :: ra.IsElem(ee) && ra.IsValid(ra.Compose(a, ee)) ==> + ee.(AuthCarrier).fst === Bottom{} && + let ce := ra.Compose(c, ee).(AuthCarrier) in + ce.fst.(Dict).V === io.insert(m, k, e) + assert forall ee resalgebra.Elem :: ra.IsElem(ee) && ra.IsValid(ra.Compose(a, ee)) ==> + ee.(AuthCarrier).fst === Bottom{} && + let ce := ra.Compose(c, ee).(AuthCarrier) in + ce.snd.V == dictMax(d.V, ee.(AuthCarrier).snd.V) && + dictLessThan(d.V, io.insert(m, k, e)) && + dictLessThan(ee.(AuthCarrier).snd.V, io.insert(m, k, e)) && + let _ := dictMaxIsLessThan(d.V, ee.(AuthCarrier).snd.V, io.insert(m, k, e)) in + true +} + +ghost ensures ElemAuth(m, y) -func InitElemAuth(m dict[Key]Val) (y ElemRA) +decreases +func InitElemAuth(m dict[Key]Val) (y ElemRA) { + l := resalgebra.Alloc(TypeAuthRA{}, AuthView(Dict{m})) + fold ElemAuth(m, l) + return l +} + +/////////////////////////////////////// Dict Ops /////////////////////////////////////// + +ghost +opaque +ensures dictLessThan(d1, res) && dictLessThan(d2, res) +decreases +pure func dictUnion(d1 dict[Key]Val, d2 dict[Key]Val) (res dict[Key]Val) { + return dictUnionAux(d1, d2) +} + +ghost +ensures domain(res) == domain(d1) union domain(d2) +ensures forall k Key :: k elem domain(d1) && k elem domain(d2) ==> k elem domain(res) && res[k] == AsSet(d1[k]) union AsSet(d2[k]) +ensures forall k Key :: k elem domain(d1) && !(k elem domain(d2)) ==> k elem domain(res) && res[k] == d1[k] +ensures forall k Key :: !(k elem domain(d1)) && (k elem domain(d2)) ==> k elem domain(res) && res[k] == d2[k] +ensures forall k Key :: !(k elem domain(d1)) && !(k elem domain(d2)) ==> !(k elem domain(res)) +decreases +pure func dictUnionAux(d1 dict[Key]Val, d2 dict[Key]Val) (res dict[Key]Val) { + return dictUnionAuxIter(d1, d2, set[Key]{}) +} + +ghost +opaque +requires visitedKeys union (domain(d1) union domain(d2)) === (domain(d1) union domain(d2)) +ensures domain(res) === (domain(d1) union domain(d2)) setminus visitedKeys +ensures forall k Key :: k elem domain(res) && k elem domain(d1) && k elem domain(d2) ==> k elem domain(res) && res[k] == AsSet(d1[k]) union AsSet(d2[k]) +ensures forall k Key :: k elem domain(res) && k elem domain(d1) && !(k elem domain(d2)) ==> k elem domain(res) && res[k] == d1[k] +ensures forall k Key :: k elem domain(res) && !(k elem domain(d1)) && (k elem domain(d2)) ==> k elem domain(res) && res[k] == d2[k] +ensures forall k Key :: !(k elem domain(d1)) && !(k elem domain(d2)) ==> !(k elem domain(res)) +decreases len((domain(d1) union domain(d2)) setminus visitedKeys) +pure func dictUnionAuxIter(d1 dict[Key]Val, d2 dict[Key]Val, visitedKeys set[Key]) (res dict[Key]Val) { + return visitedKeys === (domain(d1) union domain(d2)) ? + dict[Key]Val{} : + let _ := lemmaSetInclusion(visitedKeys, domain(d1) union domain(d2)) in + let c := choose((domain(d1) union domain(d2)) setminus visitedKeys) in + let v := (c elem domain(d1) && c elem domain(d2) ? AsSet(d1[c]) union AsSet(d2[c]) : (c elem domain(d1) ? d1[c] : d2[c])) in + let d := dictUnionAuxIter(d1, d2, visitedKeys union set[Key]{c}) in + d[c = v] +} + +ghost +ensures dictUnion(d1, d2) === dictUnion(d2, d1) +decreases +func dictUnionIsComm(d1 dict[Key]Val, d2 dict[Key]Val) { + u1 := reveal dictUnion(d1, d2) + u2 := reveal dictUnion(d2, d1) + assert domain(u1) === domain(u2) + assert forall k Key :: k elem domain(u1) ==> u1[k] == u2[k] +} + +// dictUnion(d1, d2) is the smallest dict that is bigger than both d1 and d2 +ghost +ensures dictLessThan(d1, d3) && dictLessThan(d2, d3) ==> dictLessThan(dictUnion(d1, d2), d3) +decreases +pure func dictUnionIsLessThan(d1 dict[Key]Val, d2 dict[Key]Val, d3 dict[Key]Val) U { + return let u1 := reveal dictUnion(d1, d2) in + let u2 := reveal dictUnion(d2, d1) in + let _ := domain(u1) === domain(u2) in + let _ := forall k Key :: k elem domain(u1) ==> u1[k] == u2[k] in + U{} +} /////////////////////////////////////// Utility /////////////////////////////////////// // needed for typechecking @@ -278,4 +686,23 @@ ghost decreases pure func AsSet(s set[Elem]) set[Elem] { return s -} \ No newline at end of file +} + +type U struct{} + +ghost +requires (s1 union s2) === s2 && s1 !== s2 +ensures 0 < len(s2 setminus s1) +decreases +pure func lemmaSetInclusion(s1 set[Key], s2 set[Key]) U { + return U{} +} + + +// Hilbert's choice operator, cannot be proven in Gobra yet. +ghost +trusted +requires 0 < len(s) +ensures res elem s +decreases +pure func choose(s set[Key]) (res Key) \ No newline at end of file diff --git a/verification/utils/resalgebra/auth.gobra b/verification/utils/resalgebra/auth.gobra new file mode 100644 index 000000000..96ba158ab --- /dev/null +++ b/verification/utils/resalgebra/auth.gobra @@ -0,0 +1,154 @@ +// Copyright 2025 ETH Zurich +// +// Licensed under the Apache License, Version 2.0 (the "License"); +// you may not use this file except in compliance with the License. +// You may obtain a copy of the License at +// +// http://www.apache.org/licenses/LICENSE-2.0 +// +// Unless required by applicable law or agreed to in writing, software +// distributed under the License is distributed on an "AS IS" BASIS, +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +// See the License for the specific language governing permissions and +// limitations under the License. + +// +gobra + +package resalgebra + +var _ RA = TypeAuthRA{} +var AuthRA TypeAuthRA = TypeAuthRA{} + +type IntWithTopBot interface {} +type Top struct{} +type Bottom struct{} +type Int struct { + V int +} + +type AuthCarrier struct { + Fst IntWithTopBot + Snd int +} + +type TypeAuthRA struct{} + +ghost +decreases +pure func AuthView(m int) Elem { + return AuthCarrier{Int{m}, 0} +} + +ghost +decreases +pure func FragView(m int) Elem { + return AuthCarrier{Bottom{}, m} +} + + +ghost +decreases +pure func (ra TypeAuthRA) IsElem(e Elem) (res bool) { + return typeOf(e) == type[AuthCarrier] && + let c := e.(AuthCarrier) in + c.Fst === Bottom{} || + c.Fst === Top{} || + typeOf(c.Fst) == type[Int] +} + +ghost +requires ra.IsElem(e) +decreases +pure func (ra TypeAuthRA) IsValid(e Elem) bool { + return let x := e.(AuthCarrier) in + x.Fst === Bottom{} || + (typeOf(x.Fst) == type[Int] && x.Fst.(Int).V >= x.Snd) +} + +ghost +requires ra.IsElem(e) +ensures res !== none[Elem] ==> ra.IsElem(get(res)) +decreases +pure func (ra TypeAuthRA) Core(e Elem) (ghost res option[Elem]) { + return let x := e.(AuthCarrier) in + some(Elem(AuthCarrier{Bottom{}, x.Snd})) +} + +ghost +requires ra.IsElem(e1) && ra.IsElem(e2) +ensures ra.IsElem(res) +decreases +pure func (ra TypeAuthRA) Compose(e1 Elem, e2 Elem) (res Elem) { + return let c1 := e1.(AuthCarrier) in + let c2 := e2.(AuthCarrier) in + (c1.Fst === Bottom{} ? + AuthCarrier{c2.Fst, max(c1.Snd, c2.Snd)} : + (c2.Fst === Bottom{} ? + AuthCarrier{c1.Fst, max(c1.Snd, c2.Snd)} : + AuthCarrier{Top{}, max(c1.Snd, c2.Snd)})) +} + +ghost +decreases +pure func max(a int, b int) int { + return a > b ? a : b +} + +// proofs commented out, termiation is a problem +ghost +requires ra.IsElem(e1) && ra.IsElem(e2) && ra.IsElem(e3) +ensures ra.Compose(ra.Compose(e1, e2), e3) === ra.Compose(e1, ra.Compose(e2, e3)) +decreases +func (ra TypeAuthRA) ComposeAssoc(e1 Elem, e2 Elem, e3 Elem) { + // proved +} + +ghost +requires ra.IsElem(e1) && ra.IsElem(e2) +ensures ra.Compose(e1, e2) === ra.Compose(e2, e1) +decreases +func (ra TypeAuthRA) ComposeComm(e1 Elem, e2 Elem) { + // proved +} + +ghost +requires ra.IsElem(e) +ensures let c := ra.Core(e) in + c !== none[Elem] ==> ra.Compose(get(c), e) === e +decreases +func (ra TypeAuthRA) CoreId(e Elem) { + // proved +} + +ghost +requires ra.IsElem(e) +requires ra.Core(e) !== none[Elem] +ensures let c := ra.Core(e) in + let cc := ra.Core(get(c)) in + cc !== none[Elem] && + get(cc) === get(c) +decreases +func (ra TypeAuthRA) CoreIdem(e Elem) { + // proved +} + +// perf problems, body left out; check triggers everywhere for this def +ghost +requires ra.IsElem(e1) && ra.IsElem(e2) +requires ra.Core(e1) !== none[Elem] +requires exists e3 Elem :: { ra.IsElem(e3) } ra.IsElem(e3) && e2 === ra.Compose(e1, e3) +ensures ra.Core(e2) !== none[Elem] +ensures exists e4 Elem :: { ra.IsElem(e4) } ra.IsElem(e4) && get(ra.Core(e2)) === ra.Compose(get(ra.Core(e1)), e4) +decreases +func (ra TypeAuthRA) CoreMono(e1 Elem, e2 Elem) { + // proved +} + +ghost +requires ra.IsElem(e1) && ra.IsElem(e2) +requires ra.IsValid(ra.Compose(e1, e2)) +ensures ra.IsValid(e1) +decreases +func (ra TypeAuthRA) ValidOp(e1 Elem, e2 Elem) { + // proved +} \ No newline at end of file diff --git a/verification/utils/resalgebra/auth_test.gobra b/verification/utils/resalgebra/auth_test.gobra new file mode 100644 index 000000000..61f279ac6 --- /dev/null +++ b/verification/utils/resalgebra/auth_test.gobra @@ -0,0 +1,78 @@ +// Copyright 2025 ETH Zurich +// +// Licensed under the Apache License, Version 2.0 (the "License"); +// you may not use this file except in compliance with the License. +// You may obtain a copy of the License at +// +// http://www.apache.org/licenses/LICENSE-2.0 +// +// Unless required by applicable law or agreed to in writing, software +// distributed under the License is distributed on an "AS IS" BASIS, +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +// See the License for the specific language governing permissions and +// limitations under the License. + +// +gobra + +package resalgebra + +import "sync" + +type MonoCounter struct { + val int + ghost authRes AuthCarrier + ghost loc LocName +} + +pred (c *MonoCounter) Mem() { + acc(c) && + c.authRes === AuthView(c.val) && + AuthRA.IsElem(c.authRes) && + AuthRA.IsValid(c.authRes) && + GhostLocation(c.loc, AuthRA, c.authRes) +} + +ghost +requires c.Mem() +decreases +pure func (c *MonoCounter) GetLocName() LocName { + return unfolding c.Mem() in c.loc +} + +ensures c.Mem() +decreases +func AllocMonotonicCounter() (c *MonoCounter) { + c = new(MonoCounter) + c.loc = Alloc(AuthRA, AuthView(0)) + c.authRes = AuthView(0).(AuthCarrier) + fold c.Mem() +} + +requires c.Mem() +ensures c.Mem() +ensures GhostLocation(c.GetLocName(), AuthRA, FragView(res)) +func (c *MonoCounter) ReadVal() (res int) { + unfold c.Mem() + defer fold c.Mem() + ghost auth := c.authRes + ghost frag := FragView(c.val).(AuthCarrier) + ghost comp := AuthRA.Compose(auth, frag).(AuthCarrier) + GhostUpdate(c.loc, AuthRA, auth, comp) + assert GhostLocation(c.loc, AuthRA, comp) + assert AuthRA.Core(comp) === some(Elem(frag)) + GhostOp1(c.loc, AuthRA, comp, frag) + assert GhostLocation(c.loc, AuthRA, comp) && GhostLocation(c.loc, AuthRA, frag) + GhostOp1(c.loc, AuthRA, auth, frag) + assert GhostLocation(c.loc, AuthRA, auth) && GhostLocation(c.loc, AuthRA, frag) && GhostLocation(c.loc, AuthRA, frag) + return c.val +} + +requires c.Mem() +requires GhostLocation(c.GetLocName(), AuthRA, FragView(10)) +func test(c *MonoCounter) { + unfold c.Mem() + ghost v := AuthRA.Compose(c.authRes, FragView(10)) + GhostOp2(c.loc, AuthRA, c.authRes, FragView(10)) + GhostValid(c.loc, AuthRA, v) + assert c.val >= 10 +} \ No newline at end of file diff --git a/verification/utils/resalgebra/loc.gobra b/verification/utils/resalgebra/loc.gobra new file mode 100644 index 000000000..62bcb086b --- /dev/null +++ b/verification/utils/resalgebra/loc.gobra @@ -0,0 +1,111 @@ +// Copyright 2025 ETH Zurich +// +// Licensed under the Apache License, Version 2.0 (the "License"); +// you may not use this file except in compliance with the License. +// You may obtain a copy of the License at +// +// http://www.apache.org/licenses/LICENSE-2.0 +// +// Unless required by applicable law or agreed to in writing, software +// distributed under the License is distributed on an "AS IS" BASIS, +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +// See the License for the specific language governing permissions and +// limitations under the License. + +// +gobra + +// Rules for ghost locations as presented in the paper "Iris from the ground up" (pp. 10) +// (https://people.mpi-sws.org/~dreyer/papers/iris-ground-up/paper.pdf). +// At the moment, the rules for manipulating ghost locations are trusted. +// If at all possible, we should find a model for the predicate GhostLocation and for +// all lemmas, but it is not clear that this can be done in Gobra itself. + +package resalgebra + +ghost type LocName gpointer[int] + +pred GhostLocation(l LocName, ra RA, e Elem) + +ghost +trusted +requires ra != nil +requires ra.IsElem(e) && ra.IsValid(e) +ensures l != nil +ensures GhostLocation(l, ra, e) +decreases +func Alloc(ra RA, e Elem) (l LocName) + +ghost +trusted +requires ra != nil +requires ra.IsElem(e1) +requires ra.IsElem(e2) +requires GhostLocation(l, ra, ra.Compose(e1, e2)) +ensures GhostLocation(l, ra, e1) && GhostLocation(l, ra, e2) +decreases +func GhostOp1(l LocName, ra RA, e1 Elem, e2 Elem) + +ghost +trusted +requires ra != nil +requires ra.IsElem(e1) +requires ra.IsElem(e2) +requires GhostLocation(l, ra, e1) && GhostLocation(l, ra, e2) +ensures GhostLocation(l, ra, ra.Compose(e1, e2)) +decreases +func GhostOp2(l LocName, ra RA, e1 Elem, e2 Elem) + +ghost +trusted +requires ra != nil +requires GhostLocation(l, ra, e) +ensures GhostLocation(l, ra, e) +ensures ra.IsElem(e) && ra.IsValid(e) +decreases +func GhostValid(l LocName, ra RA, e Elem) + +ghost +requires ra != nil +requires ra.IsElem(e1) +requires ra.IsElem(e2) +decreases +pure func IsFramePreservingUpdate(ra RA, e1 Elem, e2 Elem) bool { + return forall c option[Elem] :: { LiftedCompose(ra, some(e1), c) } { LiftedCompose(ra, some(e2), c) } (c !== none[Elem] ==> ra.IsElem(get(c))) ==> + (LiftedIsValid(ra, LiftedCompose(ra, some(e1), c)) ==> LiftedIsValid(ra, LiftedCompose(ra, some(e2), c))) +} + +ghost +requires ra != nil +requires e1 !== none[Elem] ==> ra.IsElem(get(e1)) +requires e2 !== none[Elem] ==> ra.IsElem(get(e2)) +decreases +pure func LiftedCompose(ra RA, e1 option[Elem], e2 option[Elem]) option[Elem] { + return e1 === none[Elem] ? + e2 : + (e2 === none[Elem] ? + e1 : + some(ra.Compose(get(e1), get(e2)))) +} + +ghost +requires ra != nil +requires e !== none[Elem] ==> ra.IsElem(get(e)) +decreases +pure func LiftedIsValid(ra RA, e option[Elem]) bool { + return e !== none[Elem] ? + ra.IsValid(get(e)) : + true +} + +ghost +trusted +requires ra != nil +requires ra.IsElem(e1) +requires ra.IsElem(e2) +requires GhostLocation(l, ra, e1) +requires IsFramePreservingUpdate(ra, e1, e2) +ensures GhostLocation(l, ra, e2) +decreases +// this rule is less powerful than the one presented in the paper, here we +// only have a deterministic update. +func GhostUpdate(l LocName, ra RA, e1 Elem, e2 Elem) \ No newline at end of file diff --git a/verification/utils/resalgebra/oneshot.gobra b/verification/utils/resalgebra/oneshot.gobra new file mode 100644 index 000000000..19475a959 --- /dev/null +++ b/verification/utils/resalgebra/oneshot.gobra @@ -0,0 +1,137 @@ +// Copyright 2025 ETH Zurich +// +// Licensed under the Apache License, Version 2.0 (the "License"); +// you may not use this file except in compliance with the License. +// You may obtain a copy of the License at +// +// http://www.apache.org/licenses/LICENSE-2.0 +// +// Unless required by applicable law or agreed to in writing, software +// distributed under the License is distributed on an "AS IS" BASIS, +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +// See the License for the specific language governing permissions and +// limitations under the License. + +// +gobra + +package resalgebra + +type Pending struct{} + +type Shot struct { + N int +} + +type Fail struct{} + +type TypeOneShotRA struct{} + +TypeOneShotRA implements RA + +var OneShotRA TypeOneShotRA = TypeOneShotRA{} + +ghost +decreases +pure +func (ra TypeOneShotRA) IsElem(e Elem) (res bool) { + return e != nil && + // using typeOf here leads to unexpected incompletnesses + (e === Elem(Pending{})) || + typeOf(e) == type[Shot] || + // using typeOf here leads to unexpected incompletnesses + (e === Fail{}) +} + + +ghost +requires ra.IsElem(e) +decreases +pure +func (ra TypeOneShotRA) IsValid(e Elem) bool { + return e != nil && + (typeOf(e) == type[Pending] || typeOf(e) == type[Shot]) +} + +ghost +requires ra.IsElem(e) +ensures res !== none[Elem] ==> ra.IsElem(get(res)) +decreases +pure +func (ra TypeOneShotRA) Core(e Elem) (ghost res option[Elem]) { + return typeOf(e) == type[Pending] ? + none[Elem] : + some(e) +} + + +ghost +requires ra.IsElem(e1) && ra.IsElem(e2) +ensures ra.IsElem(res) +decreases +pure +func (ra TypeOneShotRA) Compose(e1 Elem, e2 Elem) (res Elem) { + return typeOf(e1) == type[Shot] && typeOf(e2) == type[Shot] && e1 === e2 ? + e1 : + Elem(Fail{}) +} + +ghost +requires ra.IsElem(e1) && ra.IsElem(e2) && ra.IsElem(e3) +ensures ra.Compose(ra.Compose(e1, e2), e3) === ra.Compose(e1, ra.Compose(e2, e3)) +decreases +func (ra TypeOneShotRA) ComposeAssoc(e1 Elem, e2 Elem, e3 Elem) { + // proved +} + +ghost +requires ra.IsElem(e1) && ra.IsElem(e2) +ensures ra.Compose(e1, e2) === ra.Compose(e2, e1) +decreases +func (ra TypeOneShotRA) ComposeComm(e1 Elem, e2 Elem) { + // proved +} + +ghost +requires ra.IsElem(e) +ensures let c := ra.Core(e) in + c !== none[Elem] ==> ra.Compose(get(c), e) === e +decreases +func (ra TypeOneShotRA) CoreId(e Elem) { + // proved +} + +ghost +requires ra.IsElem(e) +requires ra.Core(e) !== none[Elem] +ensures let c := ra.Core(e) in + c !== none[Elem] && + let cc := ra.Core(get(c)) in + cc !== none[Elem] && + get(cc) === get(c) +decreases +func (ra TypeOneShotRA) CoreIdem(e Elem) { + // proved +} + +ghost +requires ra.IsElem(e1) && ra.IsElem(e2) +requires ra.Core(e1) !== none[Elem] +requires exists e3 Elem :: { ra.IsElem(e3) } ra.IsElem(e3) && e2 === ra.Compose(e1, e3) +ensures ra.Core(e2) !== none[Elem] +ensures exists e4 Elem :: { ra.IsElem(e4) } ra.IsElem(e4) && get(ra.Core(e2)) === ra.Compose(get(ra.Core(e1)), e4) +decreases +func (ra TypeOneShotRA) CoreMono(e1 Elem, e2 Elem) { + // proved +} + +ghost +requires ra.IsElem(e1) && ra.IsElem(e2) +requires ra.IsValid(ra.Compose(e1, e2)) +ensures ra.IsValid(e1) +decreases +func (ra TypeOneShotRA) ValidOp(e1 Elem, e2 Elem) { + // proved +} + + + diff --git a/verification/utils/resalgebra/oneshot_test.gobra b/verification/utils/resalgebra/oneshot_test.gobra new file mode 100644 index 000000000..475fc403d --- /dev/null +++ b/verification/utils/resalgebra/oneshot_test.gobra @@ -0,0 +1,102 @@ +// Copyright 2025 ETH Zurich +// +// Licensed under the Apache License, Version 2.0 (the "License"); +// you may not use this file except in compliance with the License. +// You may obtain a copy of the License at +// +// http://www.apache.org/licenses/LICENSE-2.0 +// +// Unless required by applicable law or agreed to in writing, software +// distributed under the License is distributed on an "AS IS" BASIS, +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +// See the License for the specific language governing permissions and +// limitations under the License. + +// +gobra + +package resalgebra + +import "sync" + +type oneshot struct { + V int + isInit bool + ghost e Elem +} + +pred oneshotInv(o *oneshot, l LocName) { + acc(o) && + GhostLocation(l, OneShotRA, o.e) && + (!o.isInit ==> o.e == Pending{} && o.V == 0) && + (o.isInit ==> o.e == Shot{o.V}) +} + +ensures oneshotInv(o, l) +decreases +func mkOneShot() (o *oneshot, ghost l LocName) { + o = new(oneshot) + l = Alloc(OneShotRA, Pending{}) + o.e = Pending{} + fold oneshotInv(o, l) + return o, l +} + +requires m.LockP() +requires m.LockInv() == oneshotInv! +requires n != 0 +func (o *oneshot) trySet(n int, m *sync.Mutex, ghost l LocName) bool { + m.Lock() + defer m.Unlock() + unfold oneshotInv!() + defer fold oneshotInv!() + if o.isInit { + return false + } + GhostUpdate(l, OneShotRA, Pending{}, Shot{n}) + o.V = n + o.isInit = true + ghost o.e = Shot{n} + return true +} + +requires m.LockP() +requires m.LockInv() == oneshotInv! +func (o *oneshot) check(m *sync.Mutex, ghost l LocName) { + m.Lock() + unfold oneshotInv!() + y1 := o.V + ghost e1 := o.e + ghost isInit1 := o.isInit + ghost if isInit1 { + assert e1 == Shot{y1} + assert OneShotRA.Compose(e1, e1) == e1 + assert GhostLocation(l, OneShotRA, e1) + GhostOp1(l, OneShotRA, e1, e1) + assert GhostLocation(l, OneShotRA, e1) && GhostLocation(l, OneShotRA, e1) + } + fold oneshotInv!() + m.Unlock() + + m.Lock() + unfold oneshotInv!() + y2 := o.V + ghost e2 := o.e + ghost isInit2 := o.isInit + ghost if isInit1 && !isInit2 { + assert GhostLocation(l, OneShotRA, Shot{y1}) + assert GhostLocation(l, OneShotRA, Pending{}) + GhostOp2(l, OneShotRA, Shot{y1}, Pending{}) + GhostValid(l, OneShotRA, OneShotRA.Compose(Shot{y1}, Pending{})) + assert false // Unreachable + } + ghost if isInit1 && isInit2 { + assert GhostLocation(l, OneShotRA, e1) && GhostLocation(l, OneShotRA, e2) + GhostValid(l, OneShotRA, e1) + GhostValid(l, OneShotRA, e2) + GhostOp2(l, OneShotRA, e1, e2) + GhostValid(l, OneShotRA, OneShotRA.Compose(e1, e2)) + assert e1 == e2 + } + fold oneshotInv!() + m.Unlock() +} diff --git a/verification/utils/resalgebra/ra.gobra b/verification/utils/resalgebra/ra.gobra new file mode 100644 index 000000000..430f6e925 --- /dev/null +++ b/verification/utils/resalgebra/ra.gobra @@ -0,0 +1,95 @@ +// Copyright 2025 ETH Zurich +// +// Licensed under the Apache License, Version 2.0 (the "License"); +// you may not use this file except in compliance with the License. +// You may obtain a copy of the License at +// +// http://www.apache.org/licenses/LICENSE-2.0 +// +// Unless required by applicable law or agreed to in writing, software +// distributed under the License is distributed on an "AS IS" BASIS, +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +// See the License for the specific language governing permissions and +// limitations under the License. + +// +gobra + +// Rules for resource algebras as presented in the paper "Iris from the ground up" (pp. 9) +// (https://people.mpi-sws.org/~dreyer/papers/iris-ground-up/paper.pdf). + +package resalgebra + +type Elem interface{} + +type RA interface { + // Defines the set of elements of the RA. This overcomes + // Go's and Gobra's limitations with generics. + ghost + decreases + pure IsElem(e Elem) (res bool) + + ghost + requires IsElem(e) + decreases + pure IsValid(e Elem) bool + + ghost + requires IsElem(e) + ensures res !== none[Elem] ==> IsElem(get(res)) + decreases + pure Core(e Elem) (ghost res option[Elem]) + + ghost + requires IsElem(e1) && IsElem(e2) + ensures IsElem(res) + decreases + pure Compose(e1 Elem, e2 Elem) (res Elem) + + // Lemmas + + ghost + requires IsElem(e1) && IsElem(e2) && IsElem(e3) + ensures Compose(Compose(e1, e2), e3) === Compose(e1, Compose(e2, e3)) + decreases + ComposeAssoc(e1 Elem, e2 Elem, e3 Elem) + + ghost + requires IsElem(e1) && IsElem(e2) + ensures Compose(e1, e2) === Compose(e2, e1) + decreases + ComposeComm(e1 Elem, e2 Elem) + + ghost + requires IsElem(e) + ensures let c := Core(e) in + c !== none[Elem] ==> Compose(get(c), e) === e + decreases + CoreId(e Elem) + + ghost + requires IsElem(e) + requires Core(e) !== none[Elem] + ensures let c := Core(e) in + let cc := Core(get(c)) in + cc !== none[Elem] && + get(cc) === get(c) + decreases + CoreIdem(e Elem) + + ghost + requires IsElem(e1) && IsElem(e2) + requires Core(e1) !== none[Elem] + // fully expanded version of <= due to Gobra's lack of `Self` in interface specs + requires exists e3 Elem :: { IsElem(e3) } IsElem(e3) && e2 === Compose(e1, e3) + ensures Core(e2) !== none[Elem] + ensures exists e4 Elem :: { IsElem(e4) } IsElem(e4) && get(Core(e2)) === Compose(get(Core(e1)), e4) + decreases + CoreMono(e1 Elem, e2 Elem) + + ghost + requires IsElem(e1) && IsElem(e2) + requires IsValid(Compose(e1, e2)) + ensures IsValid(e1) + decreases + ValidOp(e1 Elem, e2 Elem) +} \ No newline at end of file