From 634d8226a9b0a0b512dd564b448d8371f68a2ef0 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= Date: Wed, 31 Dec 2025 15:11:41 +0100 Subject: [PATCH 1/6] Formalize Authoritative RA in terms of RA from the standard lib --- router/dataplane_concurrency_model.gobra | 432 +++++++++++++++++- verification/utils/resalgebra/auth.gobra | 154 +++++++ verification/utils/resalgebra/auth_test.gobra | 78 ++++ verification/utils/resalgebra/loc.gobra | 103 +++++ verification/utils/resalgebra/oneshot.gobra | 137 ++++++ .../utils/resalgebra/oneshot_test.gobra | 102 +++++ verification/utils/resalgebra/ra.gobra | 91 ++++ 7 files changed, 1088 insertions(+), 9 deletions(-) create mode 100644 verification/utils/resalgebra/auth.gobra create mode 100644 verification/utils/resalgebra/auth_test.gobra create mode 100644 verification/utils/resalgebra/loc.gobra create mode 100644 verification/utils/resalgebra/oneshot.gobra create mode 100644 verification/utils/resalgebra/oneshot_test.gobra create mode 100644 verification/utils/resalgebra/ra.gobra diff --git a/router/dataplane_concurrency_model.gobra b/router/dataplane_concurrency_model.gobra index 65ea156c7..c5d7178c6 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,427 @@ 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 +requires DictLessThan(d1, d2) +requires DictLessThan(d2, d3) +ensures DictLessThan(d1, d3) +decreases +func DictLessThanTransitive(d1 dict[Key]Val, d2 dict[Key]Val, d3 dict[Key]Val) { + // proven +} + +ghost +requires DictLessThan(d1, d2) +requires DictLessThan(d2, d3) +requires !DictLessThan(d2, d1) || !DictLessThan(d3, d2) +ensures DictLessThan(d1, d3) +ensures !DictLessThan(d3, d1) +decreases +func StrictDictLessThanTransitive(d1 dict[Key]Val, d2 dict[Key]Val, d3 dict[Key]Val) { + assume false +} + +ghost +ensures forall d1 dict[Key]Val, d2 dict[Key]Val, d3 dict[Key]Val :: DictLessThan(d1, d2) && DictLessThan(d2, d3) ==> + DictLessThan(d1, d3) +decreases +func DictLessThanTransitiveQ() { + // proven +} + +ghost +ensures DictLessThan(m, io.insert(m, k, e)) +decreases +func DictLessThanInsert(m dict[Key]Val, k Key, e Elem) { + // proven +} + +ghost +ensures DictLessThan(d1, d3) && DictLessThan(d2, d3) ==> DictLessThan(DictMax(d1, d2), d3) +decreases +func DictMaxIsLessThan(d1 dict[Key]Val, d2 dict[Key]Val, d3 dict[Key]Val) { + 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 +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) { + m1 := DictMax(d1, DictMax(d2, d3)) + m2 := DictMax(DictMax(d1, d2), d3) + assert m1 === d1 || m1 === DictMax(d2, d3) || m1 === DictUnion(d1, DictMax(d2, d3)) + + if DictLessThan(d1, d2) { + DictLessThanTransitive(d1, d2, DictMax(d2, d3)) + assert DictMax(d1, DictMax(d2, d3)) === DictMax(d2, d3) + assert DictMax(DictMax(d1, d2), d3) === DictMax(d2, d3) + } else if DictLessThan(d2, d1) { + assert DictMax(DictMax(d1, d2), d3) === DictMax(d1, d3) + if DictLessThan(d2, d3) { + // proven + } else if DictLessThan(d3, d2) { + assert DictMax(d2, d3) === d2 + assert DictMax(d1, DictMax(d2, d3)) === DictMax(d1, d2) + assert DictMax(d1, d2) === d1 + assert DictMax(DictMax(d1, d2), d3) === DictMax(d1, d3) + StrictDictLessThanTransitive(d3, d2, d1) + assert DictLessThan(d3, d1) + assert DictMax(d1, d3) === d1 || DictMax(d1, d3) === d3 + assert !DictLessThan(d1, d3) + assert DictMax(d1, d3) === d1 + } else { + assert DictMax(d2, d3) === DictUnion(d2, d3) + assert DictLessThan(d1, DictMax(d1, d3)) + if DictLessThan(d1, d3) { + // d1 <= d3 && d2 <= d1 && !(d2 <= d3) && !(d3 <= d2) + assert DictMax(DictMax(d1, d2), d3) === DictMax(d1, d3) + assert DictMax(d1, d3) === d3 + DictLessThanTransitive(d2, d1, d3) // Shows contradiction + assert false // Unreachable + } else if DictLessThan(d3, d1) { + // d3 <= d1 && !(d1 <= d3) && d2 <= d1 && !(d2 <= d3) && !(d3 <= d2) + assert DictMax(DictMax(d1, d2), d3) === d1 + DictMaxIsLessThan(d2, d3, d1) + DictMaxIsComm(d1, DictMax(d2, d3)) + assert DictMax(d1, DictMax(d2, d3)) === d1 + } else { + assume false + } + } + } else { + assume false + } +} + +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 DictMax(d2, d1) === DictLessThan(d2, d1) ? d1 : DictLessThan(d2, d1) ? d1 : DictUnion(d1, 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) +} -pred ElemAuth(ghost m dict[Key]Val, ghost y ElemRA) +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) +} -pred ElemWitness(ghost y ElemRA, ghost k Key, ghost e Elem) +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) +} 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) { + d := Dict{dict[Key]Val{k: set[io.Pkt]{e}}} + c := (TypeAuthRA{}).Compose(AuthView(Dict{io.insert(m, k, e)}), FragView(d)) + assert (TypeAuthRA{}).IsValid(AuthView(Dict{m})) ==> + (TypeAuthRA{}).IsValid(c) + //assert forall e resalgebra.Elem :: (TypeAuthRA{}).IsValid(AuthView(Dict{m})) + assume false +} + +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] +} + +ghost +ensures DictUnion(DictUnion(d1, d2), d3) === DictUnion(d1, DictUnion(d2, d3)) +decreases +func DictUnionIsAssoc(d1 dict[Key]Val, d2 dict[Key]Val, d3 dict[Key]Val) { + assume false +} + +// 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 +func DictUnionIsLessThan(d1 dict[Key]Val, d2 dict[Key]Val, d3 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] +} /////////////////////////////////////// Utility /////////////////////////////////////// // needed for typechecking @@ -278,4 +674,22 @@ 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 +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..4573836d2 --- /dev/null +++ b/verification/utils/resalgebra/loc.gobra @@ -0,0 +1,103 @@ +// 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 + +// At the moment, all of these definitions are trusted, and this, +// prone to mistakes. If possible, we should find a model for the +// predicate GhostLocation and for all lemmas. + +ghost type LocName gpointer[int] + +pred GhostLocation(l LocName, ra RA, e Elem) + +ghost +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 +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 +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 +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 +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 +// slightly different from paper, improve +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..85fded73b --- /dev/null +++ b/verification/utils/resalgebra/ra.gobra @@ -0,0 +1,91 @@ +// 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 Elem interface{} + +type RA interface { + // defines the set of elements of the RA + 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 From bc8432678bdc6c5219585330929f3834348da295 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= Date: Thu, 1 Jan 2026 23:14:04 +0100 Subject: [PATCH 2/6] only two outstanding goals --- router/dataplane_concurrency_model.gobra | 115 ++++++++++++----------- 1 file changed, 62 insertions(+), 53 deletions(-) diff --git a/router/dataplane_concurrency_model.gobra b/router/dataplane_concurrency_model.gobra index c5d7178c6..2e7e2b56e 100644 --- a/router/dataplane_concurrency_model.gobra +++ b/router/dataplane_concurrency_model.gobra @@ -323,7 +323,14 @@ ensures DictLessThan(d1, d3) ensures !DictLessThan(d3, d1) decreases func StrictDictLessThanTransitive(d1 dict[Key]Val, d2 dict[Key]Val, d3 dict[Key]Val) { - assume false + DictLessThanTransitive(d1, d2, d3) + assert DictLessThan(d1, d3) + assert d1 !== d3 + + if DictLessThan(d3, d1) { + DictLessEq(d1, d3) + assert false // Unreachable + } } ghost @@ -366,54 +373,64 @@ func DictLessEq(d1 dict[Key]Val, d2 dict[Key]Val) { 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 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 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)) +} + +ghost +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)) +} + +ghost +ensures (forall k Key, v io.Pkt :: keyInDict(d1, k, v) == keyInDict(d2, k, v)) == (d1 === d2) +decreases +func dictMaxExtensionality(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)) + assume false + assert forall k Key, v io.Pkt :: keyInDict(d1, k, v) == keyInDict(d2, k, v) ==> + domain(d1) == domain(d2) + // assert forall k Key :: k elem domain(d1) ==> + // ((forall v io.Pkt :: keyInDict(d1, k, v) == keyInDict(d2, k, v)) == + // (k elem domain(d2) && d1[k] == d2[k])) +} + 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) { - m1 := DictMax(d1, DictMax(d2, d3)) - m2 := DictMax(DictMax(d1, d2), d3) - assert m1 === d1 || m1 === DictMax(d2, d3) || m1 === DictUnion(d1, DictMax(d2, d3)) - - if DictLessThan(d1, d2) { - DictLessThanTransitive(d1, d2, DictMax(d2, d3)) - assert DictMax(d1, DictMax(d2, d3)) === DictMax(d2, d3) - assert DictMax(DictMax(d1, d2), d3) === DictMax(d2, d3) - } else if DictLessThan(d2, d1) { - assert DictMax(DictMax(d1, d2), d3) === DictMax(d1, d3) - if DictLessThan(d2, d3) { - // proven - } else if DictLessThan(d3, d2) { - assert DictMax(d2, d3) === d2 - assert DictMax(d1, DictMax(d2, d3)) === DictMax(d1, d2) - assert DictMax(d1, d2) === d1 - assert DictMax(DictMax(d1, d2), d3) === DictMax(d1, d3) - StrictDictLessThanTransitive(d3, d2, d1) - assert DictLessThan(d3, d1) - assert DictMax(d1, d3) === d1 || DictMax(d1, d3) === d3 - assert !DictLessThan(d1, d3) - assert DictMax(d1, d3) === d1 - } else { - assert DictMax(d2, d3) === DictUnion(d2, d3) - assert DictLessThan(d1, DictMax(d1, d3)) - if DictLessThan(d1, d3) { - // d1 <= d3 && d2 <= d1 && !(d2 <= d3) && !(d3 <= d2) - assert DictMax(DictMax(d1, d2), d3) === DictMax(d1, d3) - assert DictMax(d1, d3) === d3 - DictLessThanTransitive(d2, d1, d3) // Shows contradiction - assert false // Unreachable - } else if DictLessThan(d3, d1) { - // d3 <= d1 && !(d1 <= d3) && d2 <= d1 && !(d2 <= d3) && !(d3 <= d2) - assert DictMax(DictMax(d1, d2), d3) === d1 - DictMaxIsLessThan(d2, d3, d1) - DictMaxIsComm(d1, DictMax(d2, d3)) - assert DictMax(d1, DictMax(d2, d3)) === d1 - } else { - assume false - } - } - } else { - assume false - } + dictMaxAssocLemma1(d1, d2, d3) + dictMaxAssocLemma2(d1, d2, d3) + dictMaxExtensionality(DictMax(d1, DictMax(d2, d3)), DictMax(DictMax(d1, d2), d3)) } ghost @@ -425,7 +442,6 @@ func DictMaxIsComm(d1 dict[Key]Val, d2 dict[Key]Val) { } assert d1 != d2 && DictLessThan(d1, d2) ==> !DictLessThan(d2, d1) assert DictLessThan(d1, d2) ==> DictMax(d1, d2) == d2 - //assert DictMax(d2, d1) === DictLessThan(d2, d1) ? d1 : DictLessThan(d2, d1) ? d1 : DictUnion(d1, 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 @@ -650,13 +666,6 @@ func DictUnionIsComm(d1 dict[Key]Val, d2 dict[Key]Val) { assert forall k Key :: k elem domain(u1) ==> u1[k] == u2[k] } -ghost -ensures DictUnion(DictUnion(d1, d2), d3) === DictUnion(d1, DictUnion(d2, d3)) -decreases -func DictUnionIsAssoc(d1 dict[Key]Val, d2 dict[Key]Val, d3 dict[Key]Val) { - assume false -} - // 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) From 4312ee0fa9fe460e6cd4c30d9f231b73b5efb0e3 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= Date: Fri, 2 Jan 2026 00:13:41 +0100 Subject: [PATCH 3/6] Adapt shape of theorems --- router/dataplane_concurrency_model.gobra | 19 +++++++++++-------- verification/utils/resalgebra/loc.gobra | 10 ++++++++-- 2 files changed, 19 insertions(+), 10 deletions(-) diff --git a/router/dataplane_concurrency_model.gobra b/router/dataplane_concurrency_model.gobra index 2e7e2b56e..5f6a25e47 100644 --- a/router/dataplane_concurrency_model.gobra +++ b/router/dataplane_concurrency_model.gobra @@ -380,6 +380,7 @@ pure func keyInDict(d dict[Key]Val, k Key, v io.Pkt) bool { } 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 @@ -388,6 +389,7 @@ func dictMaxAssocLemma0(d1 dict[Key]Val, d2 dict[Key]Val) { } 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 @@ -400,6 +402,7 @@ func dictMaxAssocLemma1(d1 dict[Key]Val, d2 dict[Key]Val, d3 dict[Key]Val) { } 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 @@ -412,16 +415,16 @@ func dictMaxAssocLemma2(d1 dict[Key]Val, d2 dict[Key]Val, d3 dict[Key]Val) { } ghost -ensures (forall k Key, v io.Pkt :: keyInDict(d1, k, v) == keyInDict(d2, k, v)) == (d1 === d2) +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) +ensures d1 === d2 decreases -func dictMaxExtensionality(d1 dict[Key]Val, d2 dict[Key]Val) { +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)) assume false - assert forall k Key, v io.Pkt :: keyInDict(d1, k, v) == keyInDict(d2, k, v) ==> - domain(d1) == domain(d2) - // assert forall k Key :: k elem domain(d1) ==> - // ((forall v io.Pkt :: keyInDict(d1, k, v) == keyInDict(d2, k, v)) == - // (k elem domain(d2) && d1[k] == d2[k])) + // TODO + // assert forall k Key :: (k elem domain(d1) && forall v io.Pkt :: !keyInDict(d1, k, v)) ==> AsSet(d1[k]) == set[io.Pkt]{} + // assert forall k Key :: k elem domain(d1) && AsSet(d1[k]) == set[io.Pkt]{} ==> AsSet(d2[k]) == set[io.Pkt]{} } ghost @@ -430,7 +433,7 @@ decreases func DictMaxAssoc(d1 dict[Key]Val, d2 dict[Key]Val, d3 dict[Key]Val) { dictMaxAssocLemma1(d1, d2, d3) dictMaxAssocLemma2(d1, d2, d3) - dictMaxExtensionality(DictMax(d1, DictMax(d2, d3)), DictMax(DictMax(d1, d2), d3)) + dictExtensionality(DictMax(d1, DictMax(d2, d3)), DictMax(DictMax(d1, d2), d3)) } ghost diff --git a/verification/utils/resalgebra/loc.gobra b/verification/utils/resalgebra/loc.gobra index 4573836d2..63c83ced9 100644 --- a/verification/utils/resalgebra/loc.gobra +++ b/verification/utils/resalgebra/loc.gobra @@ -17,14 +17,16 @@ package resalgebra // At the moment, all of these definitions are trusted, and this, -// prone to mistakes. If possible, we should find a model for the -// predicate GhostLocation and for all lemmas. +// prone to mistakes. 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. 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 @@ -33,6 +35,7 @@ decreases func Alloc(ra RA, e Elem) (l LocName) ghost +trusted requires ra != nil requires ra.IsElem(e1) requires ra.IsElem(e2) @@ -42,6 +45,7 @@ decreases func GhostOp1(l LocName, ra RA, e1 Elem, e2 Elem) ghost +trusted requires ra != nil requires ra.IsElem(e1) requires ra.IsElem(e2) @@ -51,6 +55,7 @@ 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) @@ -92,6 +97,7 @@ pure func LiftedIsValid(ra RA, e option[Elem]) bool { } ghost +trusted requires ra != nil requires ra.IsElem(e1) requires ra.IsElem(e2) From 5d5fe4665f5927450e987d396e88fbbe7f5ffd01 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= Date: Fri, 2 Jan 2026 00:33:41 +0100 Subject: [PATCH 4/6] prove extensionality --- router/dataplane_concurrency_model.gobra | 22 +++++++++++++++++----- 1 file changed, 17 insertions(+), 5 deletions(-) diff --git a/router/dataplane_concurrency_model.gobra b/router/dataplane_concurrency_model.gobra index 5f6a25e47..36aba3566 100644 --- a/router/dataplane_concurrency_model.gobra +++ b/router/dataplane_concurrency_model.gobra @@ -416,15 +416,27 @@ func dictMaxAssocLemma2(d1 dict[Key]Val, d2 dict[Key]Val, d3 dict[Key]Val) { 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) +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)) - assume false - // TODO - // assert forall k Key :: (k elem domain(d1) && forall v io.Pkt :: !keyInDict(d1, k, v)) ==> AsSet(d1[k]) == set[io.Pkt]{} - // assert forall k Key :: k elem domain(d1) && AsSet(d1[k]) == set[io.Pkt]{} ==> AsSet(d2[k]) == set[io.Pkt]{} + 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 From 9dfa7e7634e2e3023d704a02068eb47bfc0297b4 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= Date: Fri, 2 Jan 2026 01:58:38 +0100 Subject: [PATCH 5/6] cleanup, finish last lemma --- router/dataplane_concurrency_model.gobra | 191 +++++++++++------------ 1 file changed, 90 insertions(+), 101 deletions(-) diff --git a/router/dataplane_concurrency_model.gobra b/router/dataplane_concurrency_model.gobra index 36aba3566..1b8207c17 100644 --- a/router/dataplane_concurrency_model.gobra +++ b/router/dataplane_concurrency_model.gobra @@ -297,77 +297,43 @@ 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)) + (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 { +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 -requires DictLessThan(d1, d2) -requires DictLessThan(d2, d3) -ensures DictLessThan(d1, d3) +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 DictLessThanTransitive(d1 dict[Key]Val, d2 dict[Key]Val, d3 dict[Key]Val) { +func dictLessThanTransitiveQ() { // proven } ghost -requires DictLessThan(d1, d2) -requires DictLessThan(d2, d3) -requires !DictLessThan(d2, d1) || !DictLessThan(d3, d2) -ensures DictLessThan(d1, d3) -ensures !DictLessThan(d3, d1) +ensures dictLessThan(d1, d3) && dictLessThan(d2, d3) ==> dictLessThan(dictMax(d1, d2), d3) decreases -func StrictDictLessThanTransitive(d1 dict[Key]Val, d2 dict[Key]Val, d3 dict[Key]Val) { - DictLessThanTransitive(d1, d2, d3) - assert DictLessThan(d1, d3) - assert d1 !== d3 - - if DictLessThan(d3, d1) { - DictLessEq(d1, d3) - assert false // Unreachable - } -} - -ghost -ensures forall d1 dict[Key]Val, d2 dict[Key]Val, d3 dict[Key]Val :: DictLessThan(d1, d2) && DictLessThan(d2, d3) ==> - DictLessThan(d1, d3) -decreases -func DictLessThanTransitiveQ() { - // proven +pure func dictMaxIsLessThan(d1 dict[Key]Val, d2 dict[Key]Val, d3 dict[Key]Val) U { + return dictUnionIsLessThan(d1, d2, d3) } ghost -ensures DictLessThan(m, io.insert(m, k, e)) decreases -func DictLessThanInsert(m dict[Key]Val, k Key, e Elem) { - // proven -} - -ghost -ensures DictLessThan(d1, d3) && DictLessThan(d2, d3) ==> DictLessThan(DictMax(d1, d2), d3) -decreases -func DictMaxIsLessThan(d1 dict[Key]Val, d2 dict[Key]Val, d3 dict[Key]Val) { - DictUnionIsLessThan(d1, d2, d3) -} - -ghost -decreases -pure func DictMax(d1 dict[Key]Val, d2 dict[Key]Val) dict[Key]Val { +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) + // 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) +requires dictLessThan(d1, d2) && dictLessThan(d2, d1) ensures d1 === d2 decreases -func DictLessEq(d1 dict[Key]Val, d2 dict[Key]Val) { +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) @@ -380,37 +346,37 @@ pure func keyInDict(d dict[Key]Val, k Key, v io.Pkt) bool { } ghost -ensures domain(DictMax(d1, d2)) == domain(d1) union domain(d2) -ensures let d := DictMax(d1, d2) in +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) + 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 +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)) + 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)) + 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)) } 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 +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) + 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) + 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)) } @@ -427,9 +393,9 @@ func dictExtensionality(d1 dict[Key]Val, d2 dict[Key]Val) { 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) + assert dictLessThan(d1, d2) + assert dictLessThan(d2, d1) + dictLessEq(d1, d2) } ghost @@ -440,27 +406,27 @@ func lemmaSubSet() { } ghost -ensures DictMax(d1, DictMax(d2, d3)) === DictMax(DictMax(d1, d2), d3) +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) { +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)) + dictExtensionality(dictMax(d1, dictMax(d2, d3)), dictMax(dictMax(d1, d2), d3)) } ghost -ensures DictMax(d1, d2) == DictMax(d2, d1) +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) +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) + 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 @@ -480,10 +446,10 @@ pure func (ra TypeAuthRA) Compose(e1 resalgebra.Elem, e2 resalgebra.Elem) (res r 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)}} : + 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)}})) + AuthCarrier{c1.fst, Dict{dictMax(c1.snd.V, c2.snd.V)}} : + AuthCarrier{Top{}, Dict{dictMax(c1.snd.V, c2.snd.V)}})) } ghost @@ -499,7 +465,7 @@ func (ra TypeAuthRA) ComposeAssoc(e1 resalgebra.Elem, e2 resalgebra.Elem, e3 res comp2 := ra.Compose(e1, ra.Compose(e2, e3)).(AuthCarrier) assert comp1.fst === comp2.fst - DictMaxAssoc(c1.snd.V, c2.snd.V, c3.snd.V) + dictMaxAssoc(c1.snd.V, c2.snd.V, c3.snd.V) } ghost @@ -509,7 +475,7 @@ decreases func (ra TypeAuthRA) ComposeComm(e1 resalgebra.Elem, e2 resalgebra.Elem) { c1 := e1.(AuthCarrier) c2 := e2.(AuthCarrier) - DictMaxIsComm(c1.snd.V, c2.snd.V) + dictMaxIsComm(c1.snd.V, c2.snd.V) } ghost @@ -557,8 +523,8 @@ func (ra TypeAuthRA) ValidOp(e1 resalgebra.Elem, e2 resalgebra.Elem) { 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) + assert dictLessThan(snd, fst) + assert snd === dictMax(c1.snd.V, c2.snd.V) } } @@ -608,18 +574,39 @@ func UpdateElemWitness(m dict[Key]Val, y ElemRA, k Key, e Elem) { 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 := (TypeAuthRA{}).Compose(AuthView(Dict{io.insert(m, k, e)}), FragView(d)) - assert (TypeAuthRA{}).IsValid(AuthView(Dict{m})) ==> - (TypeAuthRA{}).IsValid(c) - //assert forall e resalgebra.Elem :: (TypeAuthRA{}).IsValid(AuthView(Dict{m})) - assume false + 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 @@ -635,9 +622,9 @@ func InitElemAuth(m dict[Key]Val) (y ElemRA) { ghost opaque -ensures DictLessThan(d1, res) && DictLessThan(d2, res) +ensures dictLessThan(d1, res) && dictLessThan(d2, res) decreases -pure func DictUnion(d1 dict[Key]Val, d2 dict[Key]Val) (res dict[Key]Val) { +pure func dictUnion(d1 dict[Key]Val, d2 dict[Key]Val) (res dict[Key]Val) { return dictUnionAux(d1, d2) } @@ -664,7 +651,7 @@ 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 _ := 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 @@ -672,24 +659,25 @@ pure func dictUnionAuxIter(d1 dict[Key]Val, d2 dict[Key]Val, visitedKeys set[Key } ghost -ensures DictUnion(d1, d2) === DictUnion(d2, d1) +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) +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 +// 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) +ensures dictLessThan(d1, d3) && dictLessThan(d2, d3) ==> dictLessThan(dictUnion(d1, d2), d3) decreases -func DictUnionIsLessThan(d1 dict[Key]Val, d2 dict[Key]Val, d3 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] +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 /////////////////////////////////////// @@ -706,13 +694,14 @@ 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 { +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 From ca8ff62abca37c48d763ca75faae2df21a042bd2 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= Date: Fri, 2 Jan 2026 17:37:40 +0100 Subject: [PATCH 6/6] update comments --- verification/utils/resalgebra/loc.gobra | 14 ++++++++------ verification/utils/resalgebra/ra.gobra | 6 +++++- 2 files changed, 13 insertions(+), 7 deletions(-) diff --git a/verification/utils/resalgebra/loc.gobra b/verification/utils/resalgebra/loc.gobra index 63c83ced9..62bcb086b 100644 --- a/verification/utils/resalgebra/loc.gobra +++ b/verification/utils/resalgebra/loc.gobra @@ -14,12 +14,13 @@ // +gobra -package resalgebra +// 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. -// At the moment, all of these definitions are trusted, and this, -// prone to mistakes. 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] @@ -105,5 +106,6 @@ requires GhostLocation(l, ra, e1) requires IsFramePreservingUpdate(ra, e1, e2) ensures GhostLocation(l, ra, e2) decreases -// slightly different from paper, improve +// 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/ra.gobra b/verification/utils/resalgebra/ra.gobra index 85fded73b..430f6e925 100644 --- a/verification/utils/resalgebra/ra.gobra +++ b/verification/utils/resalgebra/ra.gobra @@ -14,12 +14,16 @@ // +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 + // 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)