From 8fff5363d9f60a3d8e499cd2f3f44d9b7c39fa18 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= Date: Tue, 20 Jan 2026 16:48:25 +0100 Subject: [PATCH 01/28] start work on this --- resalgebra2/auth.gobra | 154 +++++++++++++ resalgebra2/auth_test.gobra | 78 +++++++ resalgebra2/axioms.gobra | 43 ++++ resalgebra2/cooliomapio.gobra | 142 ++++++++++++ resalgebra2/cooliosetio.gobra | 129 +++++++++++ resalgebra2/doc.gobra | 19 ++ resalgebra2/loc.gobra | 385 +++++++++++++++++++++++++++++++++ resalgebra2/oneshot.gobra | 137 ++++++++++++ resalgebra2/oneshot_test.gobra | 102 +++++++++ resalgebra2/ra.gobra | 98 +++++++++ 10 files changed, 1287 insertions(+) create mode 100644 resalgebra2/auth.gobra create mode 100644 resalgebra2/auth_test.gobra create mode 100644 resalgebra2/axioms.gobra create mode 100644 resalgebra2/cooliomapio.gobra create mode 100644 resalgebra2/cooliosetio.gobra create mode 100644 resalgebra2/doc.gobra create mode 100644 resalgebra2/loc.gobra create mode 100644 resalgebra2/oneshot.gobra create mode 100644 resalgebra2/oneshot_test.gobra create mode 100644 resalgebra2/ra.gobra diff --git a/resalgebra2/auth.gobra b/resalgebra2/auth.gobra new file mode 100644 index 0000000..1e45ac3 --- /dev/null +++ b/resalgebra2/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 resalgebra2 + +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/resalgebra2/auth_test.gobra b/resalgebra2/auth_test.gobra new file mode 100644 index 0000000..33be7f5 --- /dev/null +++ b/resalgebra2/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 resalgebra2 + +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/resalgebra2/axioms.gobra b/resalgebra2/axioms.gobra new file mode 100644 index 0000000..9e47281 --- /dev/null +++ b/resalgebra2/axioms.gobra @@ -0,0 +1,43 @@ +// 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 + +// This file contains all facts assumed in this library, and thus, it +// is the only trusted part of our formalization of resource algebras +// and ghost locations (except for the assumptions about the language +// features). + +// The lemmas assumed below add support for introduction and elimination +// of existential quantifiers, and they are used to deal with Gobra's +// lack of support for existentially quantified permissions. + +package resalgebra2 + +// Same as `exists witness s.t. ghostLocationIdx(l, ra, e, witness)` +pred GhostLocation(l LocName, ra RA, e Elem) + +ghost +trusted +requires ghostLocationIdx(l, ra, e, witness) +ensures GhostLocation(l, ra, e) +decreases +func IntroExists(l LocName, ra RA, e Elem, witness UserFacingIdx) + +ghost +trusted +requires GhostLocation(l, ra, e) +ensures ghostLocationIdx(l, ra, e, witness) +decreases +func IntroElim(l LocName, ra RA, e Elem) (witness UserFacingIdx) \ No newline at end of file diff --git a/resalgebra2/cooliomapio.gobra b/resalgebra2/cooliomapio.gobra new file mode 100644 index 0000000..228d775 --- /dev/null +++ b/resalgebra2/cooliomapio.gobra @@ -0,0 +1,142 @@ +// 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 resalgebra2 + +// map that can only grow monotically. adding a new element to the map +// requires and ensures the map invariant, but checking that a key-pair value (or a key is in the map) is in the map +// should not require the map inv + +ghost type key = LocName +ghost type val = cooliosetio + +ghost type node ghost struct { + inUse bool + next gpointer[node] + k key + v val + p perm +} + +// todo: change +ghost type cooliomapio gpointer[node] + +pred inv(m cooliomapio) { + acc(m, 1/2) && + (m.next == nil ==> !m.inUse && acc(m, 1/2)) && + (m.next != nil ==> + m.inUse && + acc(&m.p, 1/2) && + inv(m.next) && + m.p > 0 && + acc(&m.inUse, m.p) && acc(&m.next, m.p) && acc(&m.k, m.p) && acc(&m.v, m.p)) +} + +ghost +ensures inv(m) +decreases +func allocMap() (m cooliomapio) { + var g@ node + fold inv(&g) + return &g +} + +ghost +requires inv(m) +decreases inv(m) +pure func toDict(m cooliomapio) dict[key]val { + return unfolding inv(m) in (m.inUse ? (let smallMap := toDict(m.next) in smallMap[m.k = m.v]) : dict[key]val{}) +} + +// ghost +// requires witness(m, k) +// decreases +// pure func getVal(m cooliomapio, k key) val + +pred witness(m cooliomapio, k key, v val) { + acc(&m.inUse, _) && acc(&m.next, _) && acc(&m.k, _) && acc(&m.v, _) && + (!m.inUse ==> false) && + (m.k == k && m.v != v ==> false) && + (m.k != k ==> witness(m.next, k, v)) +} + +ghost +requires inv(m) +requires !(k elem domain(toDict(m))) +ensures inv(m) +ensures witness(m, k, v) +// ensures getVal(m, k) === v +ensures toDict(m) === old(toDict(m))[k = v] +decreases inv(m) +func add(m cooliomapio, k key, v val) { + unfold inv(m) + if !m.inUse { + next@ := node{} + assert acc(m) + m.inUse = true + m.p = 1/4 + m.next = &next + m.k = k + m.v = v + fold inv(m.next) + fold inv(m) + assert toDict(m) === unfolding inv(m) in toDict(m.next)[m.k = m.v] + assert toDict(m) === dict[key]val{k : v} + fold witness(m, k, v) + } else { + add(m.next, k, v) + assert witness(m.next, k, v) + m.p = m.p/2 + fold inv(m) + fold witness(m, k, v) + } +} + +ghost +requires 0 < p +requires acc(inv(m), p) +//requires witness(m, k) +requires witness(m, k, v) +ensures acc(inv(m), p) +ensures witness(m, k, v) +ensures k elem domain(toDict(m)) +ensures toDict(m)[k] === v // v may not be comparable +decreases acc(inv(m), p) +func lemmaWitness(m cooliomapio, k key, v val, p perm) { + d := toDict(m) + unfold acc(inv(m), p) + unfold witness(m, k, v) + if m.k == k { + assert k elem domain(d) + } else { + lemmaWitness(m.next, k, v, p) + } + fold acc(inv(m), p) + fold witness(m, k, v) +} + +ghost +requires witness(m, k, v) +ensures witness(m, k, v) && witness(m, k, v) +decreases witness(m, k, v) +func dupWitness(m cooliomapio, k key, v val) { + unfold witness(m, k, v) + if m.k != k { + dupWitness(m.next, k, v) + } + fold witness(m, k, v) + fold witness(m, k, v) +} \ No newline at end of file diff --git a/resalgebra2/cooliosetio.gobra b/resalgebra2/cooliosetio.gobra new file mode 100644 index 0000000..2bba2fa --- /dev/null +++ b/resalgebra2/cooliosetio.gobra @@ -0,0 +1,129 @@ +// 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 resalgebra2 + +// sets that can only grow monotically. adding a new element to the set +// requires and ensures the set invariant, but checking that a value is in the set +// should not require the set inv + +ghost type valSet = idx + +ghost type nodeSet ghost struct { + inUse bool + next gpointer[nodeSet] + v valSet + p perm +} + +// todo: change +ghost type cooliosetio gpointer[nodeSet] + +pred (m cooliosetio) Inv() { + acc(m, 1/2) && + (m.next == nil ==> !m.inUse && acc(m, 1/2)) && + (m.next != nil ==> + m.inUse && + acc(&m.p, 1/2) && + cooliosetio(m.next).Inv() && + m.p > 0 && + acc(&m.inUse, m.p) && acc(&m.next, m.p) && acc(&m.v, m.p)) +} + +ghost +ensures m.Inv() +decreases +func allocSet() (m cooliosetio) { + var g@ nodeSet + var c cooliosetio = &g + fold c.Inv() + return c +} + +ghost +requires m.Inv() +decreases m.Inv() +pure func toCoolSet(m cooliosetio) set[valSet] { + return unfolding m.Inv() in (m.inUse ? (toCoolSet(m.next) union set[valSet]{m.v}) : set[valSet]{}) +} + +pred (m cooliosetio) witness(v valSet) { + acc(&m.inUse, _) && acc(&m.next, _) && acc(&m.v, _) && + (!m.inUse ==> false) && + (m.v != v ==> cooliosetio(m.next).witness(v)) +} + +ghost +requires m.Inv() +ensures m.Inv() +ensures m.witness(v) +ensures toCoolSet(m) === old(toCoolSet(m)) union set[valSet]{v} +decreases m.Inv() +func (m cooliosetio) add(v valSet) { + unfold m.Inv() + if !m.inUse { + next@ := nodeSet{} + assert acc(m) + m.inUse = true + m.p = 1/4 + m.next = &next + m.v = v + fold cooliosetio(m.next).Inv() + fold m.Inv() + fold m.witness(v) + } else { + cooliosetio(m.next).add(v) + assert cooliosetio(m.next).witness(v) + m.p = m.p/2 + fold m.Inv() + fold m.witness(v) + } +} + +ghost +requires 0 < p +requires acc(m.Inv(), p) +requires m.witness(v) +ensures acc(m.Inv(), p) +ensures m.witness(v) +ensures v elem toCoolSet(m) +decreases acc(m.Inv(), p) +func (m cooliosetio) lemmaWitness(v valSet, p perm) { + d := toCoolSet(m) + // here + unfold acc(m.Inv(), p) + unfold m.witness(v) + if m.v == v { + assert v elem d + } else { + cooliosetio(m.next).lemmaWitness(v, p) + } + fold acc(m.Inv(), p) + fold m.witness(v) +} + +ghost +requires m.witness(v) +ensures m.witness(v) && m.witness(v) +decreases m.witness(v) +func (m cooliosetio) dupWitness(v valSet) { + unfold m.witness(v) + if m.v != v { + cooliosetio(m.next).dupWitness(v) + } + fold m.witness(v) + fold m.witness(v) +} \ No newline at end of file diff --git a/resalgebra2/doc.gobra b/resalgebra2/doc.gobra new file mode 100644 index 0000000..78ad4eb --- /dev/null +++ b/resalgebra2/doc.gobra @@ -0,0 +1,19 @@ +// 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 resalgebra2 + +// TODO: explain differences \ No newline at end of file diff --git a/resalgebra2/loc.gobra b/resalgebra2/loc.gobra new file mode 100644 index 0000000..c8deb43 --- /dev/null +++ b/resalgebra2/loc.gobra @@ -0,0 +1,385 @@ +// 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 resalgebra2 + +// TODO: +// - move cooliosetio and coliomapio to another package, make them generic +// - use a cooliomapio for ras +// - adapt all documentation +// - provide a body for all operations without ghost idx +// - add triggers to invariants +// - drop all assumptions +// - come up with better names for everything + +// 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] + +// should be a coolio mappio from locname to (RA, set[idx]) +ghost var model cooliomapio +ghost var ras map[LocName]RA // probably needs to be monotonic as well + +ghost type idx gpointer[meta] + +ghost type UserFacingIdx ghost struct { + i idx + c cooliosetio +} + +// replace by infinite type for idx +ghost type meta ghost struct { + inUse bool + val Elem +} + +// TODO IsInv(ghostMem()) should be established by init +pred ghostMem() { + inv(model) && + acc(ras) && + // necessary for proving key freshness + (forall k LocName :: k elem domain(toDict(model)) ==> acc(k, 1/2)) && + (forall k LocName :: k elem domain(toDict(model)) ==> k elem domain(ras)) && + (forall k LocName :: k elem domain(ras) ==> ras[k] != RA(nil)) && + // injectivity + (forall k1, k2 LocName :: k1 elem domain(toDict(model)) && k2 elem domain(toDict(model)) && k1 != k2 ==> + toDict(model)[k1] != toDict(model)[k2]) && + (forall k LocName :: k elem domain(toDict(model)) ==> toDict(model)[k].Inv()) && + // injectivity + (forall k1, k2 LocName :: k1 elem domain(toDict(model)) && k2 elem domain(toDict(model)) && k1 != k2 ==> + (forall i idx :: i elem toCoolSet(toDict(model)[k1]) ==> !(i elem toCoolSet(toDict(model)[k2])))) && + (forall k LocName :: k elem domain(toDict(model)) ==> + (forall i idx :: i elem toCoolSet(toDict(model)[k]) ==> acc(i, 1/2))) && + (forall k LocName :: k elem domain(toDict(model)) ==> + (forall i idx :: i elem toCoolSet(toDict(model)[k]) ==> + i.inUse ==> (ras[k].IsElem(i.val) && ras[k].IsValid(i.val)))) && + (forall k LocName :: k elem domain(toDict(model)) ==> + (forall i idx :: i elem toCoolSet(toDict(model)[k]) ==> + i.inUse ==> ( + forall i2 idx :: i2 elem toCoolSet(toDict(model)[k]) && i2.inUse && i2 !== i ==> + ras[k].IsElem(ras[k].Compose(i.val, i2.val)) && + ras[k].IsValid(ras[k].Compose(i.val, i2.val))))) +} + // acc model + // for every member in model, we have half perm to In Use + +pred ghostLocationIdx(l LocName, ra RA, e Elem, i UserFacingIdx) { + acc(i.i, 1/2) && + witness(model, l, i.c) && + i.c.witness(i.i) && + ra != nil && + i.i.val === e && + ra.IsElem(i.i.val) && + ra.IsValid(i.i.val) + // and ra is in ras (we have a witness) +} +// IsInv(ghostMem()) && ra elem model.witness() + + + +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) +// adds a new key to the set, and a set to the model + +ghost +requires ra != nil +requires ra.IsElem(e) && ra.IsValid(e) +ensures l != nil +ensures ghostLocationIdx(l, ra, e, i) +decreases +func AllocWithIdx(ra RA, e Elem) (l LocName, i UserFacingIdx) { + // obtain pkg inv + inhale ghostMem() + unfold ghostMem() + + newl := new(int) + var cs cooliosetio = allocSet() + iii := &meta{true, e} + cs.add(iii) + add(model, newl, cs) + assert witness(model, newl, cs) + newi := UserFacingIdx {iii, cs} + exhale acc(ras) + inhale acc(ras) + assume ras[newl] === ra + // ras[newl] = ra // type system limitation, solved when swapping ras to a monotonic set + fold ghostLocationIdx(newl, ra, e, newi) + + assert acc(newl, 1/2) + // TODO: prolly missing triggers + assume forall k LocName :: k elem domain(toDict(model)) ==> acc(k, 1/2) + // TODO: fixed when we have a monotonic set and with permissions for showing injectivity + assume forall k LocName :: k elem domain(toDict(model)) ==> k elem domain(ras) + assume forall k LocName :: k elem domain(ras) ==> ras[k] != RA(nil) + assume forall k1, k2 LocName :: k1 elem domain(toDict(model)) && k2 elem domain(toDict(model)) && k1 != k2 ==> + (forall i idx :: i elem toCoolSet(toDict(model)[k1]) ==> !(i elem toCoolSet(toDict(model)[k2]))) + // problem with triggers? + assume forall k LocName :: k elem domain(toDict(model)) ==> + (forall i idx :: i elem toCoolSet(toDict(model)[k]) ==> acc(i, 1/2)) + assume forall k LocName :: k elem domain(toDict(model)) ==> + (forall i idx :: i elem toCoolSet(toDict(model)[k]) ==> + i.inUse ==> (ras[k].IsElem(i.val) && ras[k].IsValid(i.val))) + assume false + fold ghostMem() + // close pkg inv + exhale ghostMem() + + return newl, newi +} + +ghost +requires ra != nil +requires ra.IsElem(e1) +requires ra.IsElem(e2) +requires ghostLocationIdx(l, ra, ra.Compose(e1, e2), i) +ensures ghostLocationIdx(l, ra, e1, i1) && ghostLocationIdx(l, ra, e2, i2) +decreases +func GhostOp1WithIdx(l LocName, ra RA, e1 Elem, e2 Elem, i UserFacingIdx) (i1 UserFacingIdx, i2 UserFacingIdx) { + // obtain pkg inv + inhale ghostMem() + unfold ghostMem() + + unfold ghostLocationIdx(l, ra, ra.Compose(e1, e2), i) + + // todo: when we use monotonic maps + assume l elem ras && ras[l] === ra + assert witness(model, l, i.c) + lemmaWitness(model, l, i.c, 1/3) + assert toDict(model)[l] === i.c + assert i.c.witness(i.i) + i.c.lemmaWitness(i.i, 1/3) + assert i.i elem toCoolSet(i.c) + //assert i.i.inUse && i.i.val === a.Compose(e1, e2) + ra.ValidOp(e1, e2) + assert ra.IsValid(e1) + ra.ComposeComm(e1, e2) + ra.ValidOp(e2, e1) + assert ra.IsValid(e2) + + i.i.inUse = false + iii1 := &meta{true, e1} + dupWitness(model, l, i.c) + i.c.add(iii1) + i1 = UserFacingIdx {iii1, i.c} + fold ghostLocationIdx(l, ra, e1, i1) + + iii2 := &meta{true, e2} + i.c.add(iii2) + assert witness(model, l, i.c) + i2 = UserFacingIdx {iii2, i.c} + fold ghostLocationIdx(l, ra, e2, i2) + + assume forall k1, k2 LocName :: k1 elem domain(toDict(model)) && k2 elem domain(toDict(model)) && k1 != k2 ==> + (forall i idx :: i elem toCoolSet(toDict(model)[k1]) ==> !(i elem toCoolSet(toDict(model)[k2]))) + + // not hard to prove, requires applying commutativity and associativity to get (i1 x i2) x k == (i1 x k) x i2. Because the lhs is valid, the rhs is also valid, and by ValidOp, i1 x k is also valid + // TODO: requires changing the API of RAs so that all lemmas are universally quantified + assume forall k LocName :: k elem domain(toDict(model)) ==> + (forall i idx :: i elem toCoolSet(toDict(model)[k]) ==> + i.inUse ==> ( + forall i2 idx :: i2 elem toCoolSet(toDict(model)[k]) && i2.inUse && i2 !== i ==> + ras[k].IsElem(ras[k].Compose(i.val, i2.val)) && + ras[k].IsValid(ras[k].Compose(i.val, i2.val)))) + + fold ghostMem() + // close pkg inv + exhale ghostMem() +} +// modifies the set, removes one elem, adds two. should follow from axioms of RAs + +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 ghostLocationIdx(l, ra, e1, i1) && ghostLocationIdx(l, ra, e2, i2) +ensures ghostLocationIdx(l, ra, ra.Compose(e1, e2), i1) +decreases +func GhostOp2WithIdx(l LocName, ra RA, e1 Elem, e2 Elem, i1 UserFacingIdx, i2 UserFacingIdx) { + // obtain pkg inv + inhale ghostMem() + unfold ghostMem() + + unfold ghostLocationIdx(l, ra, e1, i1) + unfold ghostLocationIdx(l, ra, e2, i2) + lemmaWitness(model, l, i2.c, 1/3) + assert i2.c === toDict(model)[l] + i2.c.lemmaWitness(i2.i, 1/3) + assert i2.i elem toCoolSet(i2.c) + i2.i.inUse = false + + lemmaWitness(model, l, i1.c, 1/3) + i1.c.lemmaWitness(i1.i, 1/3) + i1.i.val = ra.Compose(e1, e2) + // triggering issue ? + assume ra.IsElem(ra.Compose(e1, e2)) && ra.IsValid(ra.Compose(e1, e2)) + fold ghostLocationIdx(l, ra, ra.Compose(e1, e2), i1) + + // triggering issue + assume forall k LocName :: k elem domain(toDict(model)) ==> + (forall i idx :: i elem toCoolSet(toDict(model)[k]) ==> + i.inUse ==> (ras[k].IsElem(i.val) && ras[k].IsValid(i.val))) + + // proof requires that all previous elems can be added to this one and become valid. + // actually, the proof should be very similar to that of GhostOp1WithIdx + assume forall k LocName :: k elem domain(toDict(model)) ==> + (forall i idx :: i elem toCoolSet(toDict(model)[k]) ==> + i.inUse ==> ( + forall i2 idx :: i2 elem toCoolSet(toDict(model)[k]) && i2.inUse && i2 !== i ==> + ras[k].IsElem(ras[k].Compose(i.val, i2.val)) && + ras[k].IsValid(ras[k].Compose(i.val, i2.val)))) + + + fold ghostMem() + // close pkg inv + exhale ghostMem() +} + +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) +// should follow from the invariant of the set + +ghost +requires ra != nil +requires ghostLocationIdx(l, ra, e, i) +ensures ghostLocationIdx(l, ra, e, i) +ensures ra.IsElem(e) && ra.IsValid(e) +decreases +func GhostValidWithIdx(l LocName, ra RA, e Elem, i UserFacingIdx) { + unfold ghostLocationIdx(l, ra, e, i) + fold ghostLocationIdx(l, ra, e, i) +} + +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) +// trivial from the inv + +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)) : + false // is this correct? +} + +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) +// should be trivial to prove too + +ghost +requires ra != nil +requires ra.IsElem(e1) +requires ra.IsElem(e2) +requires ghostLocationIdx(l, ra, e1, i) +requires IsFramePreservingUpdate(ra, e1, e2) +ensures ghostLocationIdx(l, ra, e2, i) +decreases +// slightly different from paper, improve +func GhostUpdateWithIdx(l LocName, ra RA, e1 Elem, e2 Elem, i UserFacingIdx) { + // obtain pkg inv + inhale ghostMem() + unfold ghostMem() + + unfold ghostLocationIdx(l, ra, e1, i) + lemmaWitness(model, l, i.c, 1/3) + i.c.lemmaWitness(i.i, 1/3) + i.i.val = e2 + + // TODO: can be proven easily once we require all RAs to be unital + // seems to require that ra is unital. + // idea: if e1 has a core, than e2 must be valid: e1 has core ==> + // ==> compose(e2, core(e1)) must be valid because compose(e1, core(e1)) is valid and e2 is a frame preserving update + // ==> e2 is valid because the compose(e2, core(e1)) is valid. + // what about the cases e1 does not have a core? + assume ra.IsValid(e2) + // TODO: drop when ras is a monotonic set + assume ras[l] === ra + // TODO: should be provable from the def of IsFramePreservingUpdate + assume forall k LocName :: k elem domain(toDict(model)) ==> + (forall i idx :: i elem toCoolSet(toDict(model)[k]) ==> + i.inUse ==> ( + forall i2 idx :: i2 elem toCoolSet(toDict(model)[k]) && i2.inUse && i2 !== i ==> + ras[k].IsElem(ras[k].Compose(i.val, i2.val)) && + ras[k].IsValid(ras[k].Compose(i.val, i2.val)))) + + fold ghostLocationIdx(l, ra, e2, i) + + fold ghostMem() + // close pkg inv + exhale ghostMem() +} + + + diff --git a/resalgebra2/oneshot.gobra b/resalgebra2/oneshot.gobra new file mode 100644 index 0000000..5b43dea --- /dev/null +++ b/resalgebra2/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 resalgebra2 + +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/resalgebra2/oneshot_test.gobra b/resalgebra2/oneshot_test.gobra new file mode 100644 index 0000000..dceac88 --- /dev/null +++ b/resalgebra2/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 resalgebra2 + +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/resalgebra2/ra.gobra b/resalgebra2/ra.gobra new file mode 100644 index 0000000..4184ce9 --- /dev/null +++ b/resalgebra2/ra.gobra @@ -0,0 +1,98 @@ +// 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 resalgebra2 + +// TODO: change to quantified lemmas, make the old lemmas available as a function +// defined outside the RA +// TODO: change RA to UnitResAlgebra +// TODO: rename "Compose" to "Op" +// TODO: make "core" a total func +// TODO: still include ResAlgebra as a type, but do not use it? + +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 3f67c3b2570266083c392a0df1563f0440603d2d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= Date: Tue, 20 Jan 2026 17:26:15 +0100 Subject: [PATCH 02/28] continue working on a model --- resalgebra2/doc.gobra | 2 -- resalgebra2/loc.gobra | 37 ++++++++++++++++++++++++++----------- resalgebra2/ra.gobra | 16 ++++++++++++---- 3 files changed, 38 insertions(+), 17 deletions(-) diff --git a/resalgebra2/doc.gobra b/resalgebra2/doc.gobra index 78ad4eb..b8b9c37 100644 --- a/resalgebra2/doc.gobra +++ b/resalgebra2/doc.gobra @@ -15,5 +15,3 @@ // +gobra package resalgebra2 - -// TODO: explain differences \ No newline at end of file diff --git a/resalgebra2/loc.gobra b/resalgebra2/loc.gobra index c8deb43..8dc3889 100644 --- a/resalgebra2/loc.gobra +++ b/resalgebra2/loc.gobra @@ -17,6 +17,7 @@ package resalgebra2 // TODO: +// - TODO: rename this package back to resalgebra, replace the old package // - move cooliosetio and coliomapio to another package, make them generic // - use a cooliomapio for ras // - adapt all documentation @@ -323,7 +324,7 @@ decreases pure func LiftedIsValid(ra RA, e option[Elem]) bool { return e !== none[Elem] ? ra.IsValid(get(e)) : - false // is this correct? + true } ghost @@ -357,13 +358,30 @@ func GhostUpdateWithIdx(l LocName, ra RA, e1 Elem, e2 Elem, i UserFacingIdx) { i.c.lemmaWitness(i.i, 1/3) i.i.val = e2 - // TODO: can be proven easily once we require all RAs to be unital - // seems to require that ra is unital. - // idea: if e1 has a core, than e2 must be valid: e1 has core ==> - // ==> compose(e2, core(e1)) must be valid because compose(e1, core(e1)) is valid and e2 is a frame preserving update - // ==> e2 is valid because the compose(e2, core(e1)) is valid. - // what about the cases e1 does not have a core? - assume ra.IsValid(e2) + // TODO: can be proven easily as long as I can introduce an existentially quantified variable + if forall e Elem :: ra.IsElem(e) ==> LiftedCompose(ra, some(e1), some(e)) === none[Elem] { + assert ra.IsValid(e2) + } else { + // idea: if e1 has a core, than e2 must be valid: e1 has core ==> + // ==> compose(e2, core(e1)) must be valid because compose(e1, core(e1)) is valid and e2 is a frame preserving update + // ==> e2 is valid because the compose(e2, core(e1)) is valid. + // what about the cases e1 does not have a core? + } + + // if ra.Core(e1) != none[Elem] { + // ra.CoreId(e1) + // assert ra.Compose(get(ra.Core(e1)), e1) === e1 + // ra.ComposeComm(get(ra.Core(e1)), e1) + // assert ra.Compose(e1, get(ra.Core(e1))) === e1 + // assert LiftedIsValid(ra, some(e1)) + // assert LiftedIsValid(ra, some(ra.Compose(e1, get(ra.Core(e1))))) + // IsFramePreservingUpdate(ra, e1, e2) + // assume false // TODO + // assert LiftedIsValid(ra, some(ra.Compose(e2, get(ra.Core(e1))))) // from def of frame-preserving update + // } else { + // // assume ra.IsValid(e2) + // } + // TODO: drop when ras is a monotonic set assume ras[l] === ra // TODO: should be provable from the def of IsFramePreservingUpdate @@ -380,6 +398,3 @@ func GhostUpdateWithIdx(l LocName, ra RA, e1 Elem, e2 Elem, i UserFacingIdx) { // close pkg inv exhale ghostMem() } - - - diff --git a/resalgebra2/ra.gobra b/resalgebra2/ra.gobra index 4184ce9..87593ae 100644 --- a/resalgebra2/ra.gobra +++ b/resalgebra2/ra.gobra @@ -18,10 +18,6 @@ package resalgebra2 // TODO: change to quantified lemmas, make the old lemmas available as a function // defined outside the RA -// TODO: change RA to UnitResAlgebra -// TODO: rename "Compose" to "Op" -// TODO: make "core" a total func -// TODO: still include ResAlgebra as a type, but do not use it? type Elem interface{} @@ -48,6 +44,11 @@ type RA interface { decreases pure Compose(e1 Elem, e2 Elem) (res Elem) + // ghost + // ensures IsElem(res) && IsValid(res) + // decreases + // pure Unit() (res Elem) + // Lemmas ghost @@ -95,4 +96,11 @@ type RA interface { ensures IsValid(e1) decreases ValidOp(e1 Elem, e2 Elem) + + // ghost + // requires IsElem(e) + // requires Compose(e, Unit()) === e + // requires Compose(Unit(), e) === e + // decreases + // ComposeUnit(e Elem) } \ No newline at end of file From 05f9026cc1d5eb2b270e3f802466157046fe9189 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= Date: Tue, 20 Jan 2026 17:33:37 +0100 Subject: [PATCH 03/28] change todos --- resalgebra2/loc.gobra | 7 +++++-- resalgebra2/ra.gobra | 3 --- 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/resalgebra2/loc.gobra b/resalgebra2/loc.gobra index 8dc3889..dbeffe7 100644 --- a/resalgebra2/loc.gobra +++ b/resalgebra2/loc.gobra @@ -17,11 +17,14 @@ package resalgebra2 // TODO: -// - TODO: rename this package back to resalgebra, replace the old package +// - rename this package to resalgebraNoAxioms +// - change to quantified lemmas, make the old lemmas available as a function defined outside the RA +// - rename "Idx" to "Witness", drop all lemmas without the witness and rename functions "WithIdx" to drop the suffix +// - drop axioms.gobra // - move cooliosetio and coliomapio to another package, make them generic // - use a cooliomapio for ras // - adapt all documentation -// - provide a body for all operations without ghost idx +// - change all functions to pass around the witnesses // - add triggers to invariants // - drop all assumptions // - come up with better names for everything diff --git a/resalgebra2/ra.gobra b/resalgebra2/ra.gobra index 87593ae..8272c6c 100644 --- a/resalgebra2/ra.gobra +++ b/resalgebra2/ra.gobra @@ -16,9 +16,6 @@ package resalgebra2 -// TODO: change to quantified lemmas, make the old lemmas available as a function -// defined outside the RA - type Elem interface{} type RA interface { From 76b439cd8fb3d3fc950a53365dce876ee942ebf4 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= Date: Tue, 20 Jan 2026 17:40:29 +0100 Subject: [PATCH 04/28] resalgebraNoAxioms --- {resalgebra2 => resalgebraNoAxioms}/auth.gobra | 2 +- {resalgebra2 => resalgebraNoAxioms}/auth_test.gobra | 2 +- {resalgebra2 => resalgebraNoAxioms}/axioms.gobra | 2 +- {resalgebra2 => resalgebraNoAxioms}/cooliomapio.gobra | 2 +- {resalgebra2 => resalgebraNoAxioms}/cooliosetio.gobra | 2 +- {resalgebra2 => resalgebraNoAxioms}/doc.gobra | 2 +- {resalgebra2 => resalgebraNoAxioms}/loc.gobra | 2 +- {resalgebra2 => resalgebraNoAxioms}/oneshot.gobra | 2 +- {resalgebra2 => resalgebraNoAxioms}/oneshot_test.gobra | 2 +- {resalgebra2 => resalgebraNoAxioms}/ra.gobra | 2 +- 10 files changed, 10 insertions(+), 10 deletions(-) rename {resalgebra2 => resalgebraNoAxioms}/auth.gobra (99%) rename {resalgebra2 => resalgebraNoAxioms}/auth_test.gobra (98%) rename {resalgebra2 => resalgebraNoAxioms}/axioms.gobra (98%) rename {resalgebra2 => resalgebraNoAxioms}/cooliomapio.gobra (99%) rename {resalgebra2 => resalgebraNoAxioms}/cooliosetio.gobra (99%) rename {resalgebra2 => resalgebraNoAxioms}/doc.gobra (95%) rename {resalgebra2 => resalgebraNoAxioms}/loc.gobra (99%) rename {resalgebra2 => resalgebraNoAxioms}/oneshot.gobra (99%) rename {resalgebra2 => resalgebraNoAxioms}/oneshot_test.gobra (98%) rename {resalgebra2 => resalgebraNoAxioms}/ra.gobra (98%) diff --git a/resalgebra2/auth.gobra b/resalgebraNoAxioms/auth.gobra similarity index 99% rename from resalgebra2/auth.gobra rename to resalgebraNoAxioms/auth.gobra index 1e45ac3..2b344c9 100644 --- a/resalgebra2/auth.gobra +++ b/resalgebraNoAxioms/auth.gobra @@ -14,7 +14,7 @@ // +gobra -package resalgebra2 +package resalgebraNoAxioms var _ RA = TypeAuthRA{} var AuthRA TypeAuthRA = TypeAuthRA{} diff --git a/resalgebra2/auth_test.gobra b/resalgebraNoAxioms/auth_test.gobra similarity index 98% rename from resalgebra2/auth_test.gobra rename to resalgebraNoAxioms/auth_test.gobra index 33be7f5..f6a0e99 100644 --- a/resalgebra2/auth_test.gobra +++ b/resalgebraNoAxioms/auth_test.gobra @@ -14,7 +14,7 @@ // +gobra -package resalgebra2 +package resalgebraNoAxioms import "sync" diff --git a/resalgebra2/axioms.gobra b/resalgebraNoAxioms/axioms.gobra similarity index 98% rename from resalgebra2/axioms.gobra rename to resalgebraNoAxioms/axioms.gobra index 9e47281..14c7f6f 100644 --- a/resalgebra2/axioms.gobra +++ b/resalgebraNoAxioms/axioms.gobra @@ -23,7 +23,7 @@ // of existential quantifiers, and they are used to deal with Gobra's // lack of support for existentially quantified permissions. -package resalgebra2 +package resalgebraNoAxioms // Same as `exists witness s.t. ghostLocationIdx(l, ra, e, witness)` pred GhostLocation(l LocName, ra RA, e Elem) diff --git a/resalgebra2/cooliomapio.gobra b/resalgebraNoAxioms/cooliomapio.gobra similarity index 99% rename from resalgebra2/cooliomapio.gobra rename to resalgebraNoAxioms/cooliomapio.gobra index 228d775..3046064 100644 --- a/resalgebra2/cooliomapio.gobra +++ b/resalgebraNoAxioms/cooliomapio.gobra @@ -14,7 +14,7 @@ // +gobra -package resalgebra2 +package resalgebraNoAxioms // map that can only grow monotically. adding a new element to the map // requires and ensures the map invariant, but checking that a key-pair value (or a key is in the map) is in the map diff --git a/resalgebra2/cooliosetio.gobra b/resalgebraNoAxioms/cooliosetio.gobra similarity index 99% rename from resalgebra2/cooliosetio.gobra rename to resalgebraNoAxioms/cooliosetio.gobra index 2bba2fa..d48eb3c 100644 --- a/resalgebra2/cooliosetio.gobra +++ b/resalgebraNoAxioms/cooliosetio.gobra @@ -14,7 +14,7 @@ // +gobra -package resalgebra2 +package resalgebraNoAxioms // sets that can only grow monotically. adding a new element to the set // requires and ensures the set invariant, but checking that a value is in the set diff --git a/resalgebra2/doc.gobra b/resalgebraNoAxioms/doc.gobra similarity index 95% rename from resalgebra2/doc.gobra rename to resalgebraNoAxioms/doc.gobra index b8b9c37..96aefe1 100644 --- a/resalgebra2/doc.gobra +++ b/resalgebraNoAxioms/doc.gobra @@ -14,4 +14,4 @@ // +gobra -package resalgebra2 +package resalgebraNoAxioms diff --git a/resalgebra2/loc.gobra b/resalgebraNoAxioms/loc.gobra similarity index 99% rename from resalgebra2/loc.gobra rename to resalgebraNoAxioms/loc.gobra index dbeffe7..5b7401e 100644 --- a/resalgebra2/loc.gobra +++ b/resalgebraNoAxioms/loc.gobra @@ -14,7 +14,7 @@ // +gobra -package resalgebra2 +package resalgebraNoAxioms // TODO: // - rename this package to resalgebraNoAxioms diff --git a/resalgebra2/oneshot.gobra b/resalgebraNoAxioms/oneshot.gobra similarity index 99% rename from resalgebra2/oneshot.gobra rename to resalgebraNoAxioms/oneshot.gobra index 5b43dea..23a9cbb 100644 --- a/resalgebra2/oneshot.gobra +++ b/resalgebraNoAxioms/oneshot.gobra @@ -14,7 +14,7 @@ // +gobra -package resalgebra2 +package resalgebraNoAxioms type Pending struct{} diff --git a/resalgebra2/oneshot_test.gobra b/resalgebraNoAxioms/oneshot_test.gobra similarity index 98% rename from resalgebra2/oneshot_test.gobra rename to resalgebraNoAxioms/oneshot_test.gobra index dceac88..cd34d8c 100644 --- a/resalgebra2/oneshot_test.gobra +++ b/resalgebraNoAxioms/oneshot_test.gobra @@ -14,7 +14,7 @@ // +gobra -package resalgebra2 +package resalgebraNoAxioms import "sync" diff --git a/resalgebra2/ra.gobra b/resalgebraNoAxioms/ra.gobra similarity index 98% rename from resalgebra2/ra.gobra rename to resalgebraNoAxioms/ra.gobra index 8272c6c..7382c7c 100644 --- a/resalgebra2/ra.gobra +++ b/resalgebraNoAxioms/ra.gobra @@ -14,7 +14,7 @@ // +gobra -package resalgebra2 +package resalgebraNoAxioms type Elem interface{} From 4e44225cec2b843b7da38ffdf0b18fdcecc44a54 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= Date: Tue, 20 Jan 2026 17:43:43 +0100 Subject: [PATCH 05/28] add assumption to make verification pass --- resalgebraNoAxioms/loc.gobra | 1 + 1 file changed, 1 insertion(+) diff --git a/resalgebraNoAxioms/loc.gobra b/resalgebraNoAxioms/loc.gobra index 5b7401e..e2498b2 100644 --- a/resalgebraNoAxioms/loc.gobra +++ b/resalgebraNoAxioms/loc.gobra @@ -369,6 +369,7 @@ func GhostUpdateWithIdx(l LocName, ra RA, e1 Elem, e2 Elem, i UserFacingIdx) { // ==> compose(e2, core(e1)) must be valid because compose(e1, core(e1)) is valid and e2 is a frame preserving update // ==> e2 is valid because the compose(e2, core(e1)) is valid. // what about the cases e1 does not have a core? + assume ra.IsValid(e2) // TODO } // if ra.Core(e1) != none[Elem] { From 9a5598a14bfc9065fdd91deb0dabe1acb92320c3 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= Date: Tue, 20 Jan 2026 17:48:34 +0100 Subject: [PATCH 06/28] backup --- resalgebraNoAxioms/axioms.gobra | 1 + resalgebraNoAxioms/loc.gobra | 21 +++++++++++---------- 2 files changed, 12 insertions(+), 10 deletions(-) diff --git a/resalgebraNoAxioms/axioms.gobra b/resalgebraNoAxioms/axioms.gobra index 14c7f6f..106e30f 100644 --- a/resalgebraNoAxioms/axioms.gobra +++ b/resalgebraNoAxioms/axioms.gobra @@ -25,6 +25,7 @@ package resalgebraNoAxioms +// TODO: move these axioms to package resalgebra, define that library on top of this one // Same as `exists witness s.t. ghostLocationIdx(l, ra, e, witness)` pred GhostLocation(l LocName, ra RA, e Elem) diff --git a/resalgebraNoAxioms/loc.gobra b/resalgebraNoAxioms/loc.gobra index e2498b2..24d9fa3 100644 --- a/resalgebraNoAxioms/loc.gobra +++ b/resalgebraNoAxioms/loc.gobra @@ -28,6 +28,7 @@ package resalgebraNoAxioms // - add triggers to invariants // - drop all assumptions // - come up with better names for everything +// - adapt package resalgebra to be an interface that redirects to this one, and introduces the existential elimination and introduction axioms // At the moment, all of these definitions are trusted, and this, // prone to mistakes. If possible, we should find a model for the @@ -41,7 +42,7 @@ ghost var ras map[LocName]RA // probably needs to be monotonic as well ghost type idx gpointer[meta] -ghost type UserFacingIdx ghost struct { +ghost type Witness ghost struct { i idx c cooliosetio } @@ -82,7 +83,7 @@ pred ghostMem() { // acc model // for every member in model, we have half perm to In Use -pred ghostLocationIdx(l LocName, ra RA, e Elem, i UserFacingIdx) { +pred ghostLocationIdx(l LocName, ra RA, e Elem, i Witness) { acc(i.i, 1/2) && witness(model, l, i.c) && i.c.witness(i.i) && @@ -111,7 +112,7 @@ requires ra.IsElem(e) && ra.IsValid(e) ensures l != nil ensures ghostLocationIdx(l, ra, e, i) decreases -func AllocWithIdx(ra RA, e Elem) (l LocName, i UserFacingIdx) { +func AllocWithIdx(ra RA, e Elem) (l LocName, i Witness) { // obtain pkg inv inhale ghostMem() unfold ghostMem() @@ -122,7 +123,7 @@ func AllocWithIdx(ra RA, e Elem) (l LocName, i UserFacingIdx) { cs.add(iii) add(model, newl, cs) assert witness(model, newl, cs) - newi := UserFacingIdx {iii, cs} + newi := Witness {iii, cs} exhale acc(ras) inhale acc(ras) assume ras[newl] === ra @@ -158,7 +159,7 @@ requires ra.IsElem(e2) requires ghostLocationIdx(l, ra, ra.Compose(e1, e2), i) ensures ghostLocationIdx(l, ra, e1, i1) && ghostLocationIdx(l, ra, e2, i2) decreases -func GhostOp1WithIdx(l LocName, ra RA, e1 Elem, e2 Elem, i UserFacingIdx) (i1 UserFacingIdx, i2 UserFacingIdx) { +func GhostOp1WithIdx(l LocName, ra RA, e1 Elem, e2 Elem, i Witness) (i1 Witness, i2 Witness) { // obtain pkg inv inhale ghostMem() unfold ghostMem() @@ -184,13 +185,13 @@ func GhostOp1WithIdx(l LocName, ra RA, e1 Elem, e2 Elem, i UserFacingIdx) (i1 Us iii1 := &meta{true, e1} dupWitness(model, l, i.c) i.c.add(iii1) - i1 = UserFacingIdx {iii1, i.c} + i1 = Witness {iii1, i.c} fold ghostLocationIdx(l, ra, e1, i1) iii2 := &meta{true, e2} i.c.add(iii2) assert witness(model, l, i.c) - i2 = UserFacingIdx {iii2, i.c} + i2 = Witness {iii2, i.c} fold ghostLocationIdx(l, ra, e2, i2) assume forall k1, k2 LocName :: k1 elem domain(toDict(model)) && k2 elem domain(toDict(model)) && k1 != k2 ==> @@ -227,7 +228,7 @@ requires ra.IsElem(e2) requires ghostLocationIdx(l, ra, e1, i1) && ghostLocationIdx(l, ra, e2, i2) ensures ghostLocationIdx(l, ra, ra.Compose(e1, e2), i1) decreases -func GhostOp2WithIdx(l LocName, ra RA, e1 Elem, e2 Elem, i1 UserFacingIdx, i2 UserFacingIdx) { +func GhostOp2WithIdx(l LocName, ra RA, e1 Elem, e2 Elem, i1 Witness, i2 Witness) { // obtain pkg inv inhale ghostMem() unfold ghostMem() @@ -283,7 +284,7 @@ requires ghostLocationIdx(l, ra, e, i) ensures ghostLocationIdx(l, ra, e, i) ensures ra.IsElem(e) && ra.IsValid(e) decreases -func GhostValidWithIdx(l LocName, ra RA, e Elem, i UserFacingIdx) { +func GhostValidWithIdx(l LocName, ra RA, e Elem, i Witness) { unfold ghostLocationIdx(l, ra, e, i) fold ghostLocationIdx(l, ra, e, i) } @@ -351,7 +352,7 @@ requires IsFramePreservingUpdate(ra, e1, e2) ensures ghostLocationIdx(l, ra, e2, i) decreases // slightly different from paper, improve -func GhostUpdateWithIdx(l LocName, ra RA, e1 Elem, e2 Elem, i UserFacingIdx) { +func GhostUpdateWithIdx(l LocName, ra RA, e1 Elem, e2 Elem, i Witness) { // obtain pkg inv inhale ghostMem() unfold ghostMem() From bdb8b6507d640c88fbda4885fd5122f612380ec8 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= Date: Tue, 20 Jan 2026 17:52:05 +0100 Subject: [PATCH 07/28] fix typo --- resalgebraNoAxioms/axioms.gobra | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/resalgebraNoAxioms/axioms.gobra b/resalgebraNoAxioms/axioms.gobra index 106e30f..49f25ad 100644 --- a/resalgebraNoAxioms/axioms.gobra +++ b/resalgebraNoAxioms/axioms.gobra @@ -34,11 +34,11 @@ trusted requires ghostLocationIdx(l, ra, e, witness) ensures GhostLocation(l, ra, e) decreases -func IntroExists(l LocName, ra RA, e Elem, witness UserFacingIdx) +func IntroExists(l LocName, ra RA, e Elem, witness Witness) ghost trusted requires GhostLocation(l, ra, e) ensures ghostLocationIdx(l, ra, e, witness) decreases -func IntroElim(l LocName, ra RA, e Elem) (witness UserFacingIdx) \ No newline at end of file +func IntroElim(l LocName, ra RA, e Elem) (witness Witness) \ No newline at end of file From 68dc6af85808cf86d82ca7b7e1a65eb1fd41408c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= Date: Tue, 20 Jan 2026 19:01:51 +0100 Subject: [PATCH 08/28] backup --- resalgebraNoAxioms/axioms.gobra | 44 ----------------- resalgebraNoAxioms/doc.gobra | 34 +++++++++++++ resalgebraNoAxioms/loc.gobra | 86 +++++++++++++++++---------------- 3 files changed, 78 insertions(+), 86 deletions(-) delete mode 100644 resalgebraNoAxioms/axioms.gobra diff --git a/resalgebraNoAxioms/axioms.gobra b/resalgebraNoAxioms/axioms.gobra deleted file mode 100644 index 49f25ad..0000000 --- a/resalgebraNoAxioms/axioms.gobra +++ /dev/null @@ -1,44 +0,0 @@ -// 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 - -// This file contains all facts assumed in this library, and thus, it -// is the only trusted part of our formalization of resource algebras -// and ghost locations (except for the assumptions about the language -// features). - -// The lemmas assumed below add support for introduction and elimination -// of existential quantifiers, and they are used to deal with Gobra's -// lack of support for existentially quantified permissions. - -package resalgebraNoAxioms - -// TODO: move these axioms to package resalgebra, define that library on top of this one -// Same as `exists witness s.t. ghostLocationIdx(l, ra, e, witness)` -pred GhostLocation(l LocName, ra RA, e Elem) - -ghost -trusted -requires ghostLocationIdx(l, ra, e, witness) -ensures GhostLocation(l, ra, e) -decreases -func IntroExists(l LocName, ra RA, e Elem, witness Witness) - -ghost -trusted -requires GhostLocation(l, ra, e) -ensures ghostLocationIdx(l, ra, e, witness) -decreases -func IntroElim(l LocName, ra RA, e Elem) (witness Witness) \ No newline at end of file diff --git a/resalgebraNoAxioms/doc.gobra b/resalgebraNoAxioms/doc.gobra index 96aefe1..2680366 100644 --- a/resalgebraNoAxioms/doc.gobra +++ b/resalgebraNoAxioms/doc.gobra @@ -14,4 +14,38 @@ // +gobra +// This package is shows that we can provide a model for ghost locations, similar to +// those of Iris entirely in Gobra. The public API of this package is very similar to +// that of `resalgebra` except that (1) we made some tweaks to the definition of RA that +// should be logically equivalent to those of the RA defined in `resalgebra` +// but which are easier to work with in Gobra (e.g., all lemmas in the +// interface RA are universally quantified, rather than requiring the user +// to provide the instantiations of the quantified variables), (2) all +// lemmas for ghost locations require a Witness value to be passed. +// This is due to a technicality in Gobra (we cannot existentially quantify +// over resources). Nonetheless, one may have the same API as that +// of `resalgebra/loc.gobra` if one axiomatizes the introduction and elimination +// rules for existential QPs: +// +// // Same as `exists w s.t. GhostLocationW(l, ra, e, w)` +// pred GhostLocation(l LocName, ra RA, e Elem) +// +// // Converting between GhostLocationW and GhostLocation by +// // introducing the existential quantifier. +// ghost +// trusted +// requires GhostLocationW(l, ra, e, w) +// ensures GhostLocation(l, ra, e) +// decreases +// func IntroExists(l LocName, ra RA, e Elem, w Witness) +// +// // Converting between GhostLocation and GhostLocationW by +// // eliminating the existential quantifier. +// ghost +// trusted +// requires GhostLocation(l, ra, e) +// ensures GhostLocationW(l, ra, e, w) +// decreases +// func IntroElim(l LocName, ra RA, e Elem) (w Witness) + package resalgebraNoAxioms diff --git a/resalgebraNoAxioms/loc.gobra b/resalgebraNoAxioms/loc.gobra index 24d9fa3..e1edfab 100644 --- a/resalgebraNoAxioms/loc.gobra +++ b/resalgebraNoAxioms/loc.gobra @@ -17,7 +17,6 @@ package resalgebraNoAxioms // TODO: -// - rename this package to resalgebraNoAxioms // - change to quantified lemmas, make the old lemmas available as a function defined outside the RA // - rename "Idx" to "Witness", drop all lemmas without the witness and rename functions "WithIdx" to drop the suffix // - drop axioms.gobra @@ -29,6 +28,7 @@ package resalgebraNoAxioms // - drop all assumptions // - come up with better names for everything // - adapt package resalgebra to be an interface that redirects to this one, and introduces the existential elimination and introduction axioms +// - add invs // At the moment, all of these definitions are trusted, and this, // prone to mistakes. If possible, we should find a model for the @@ -53,8 +53,8 @@ ghost type meta ghost struct { val Elem } -// TODO IsInv(ghostMem()) should be established by init -pred ghostMem() { +// TODO IsInv(GlobalMem()) should be established by init +pred GlobalMem() { inv(model) && acc(ras) && // necessary for proving key freshness @@ -83,7 +83,8 @@ pred ghostMem() { // acc model // for every member in model, we have half perm to In Use -pred ghostLocationIdx(l LocName, ra RA, e Elem, i Witness) { +// TODO: rename to GhostLocationW +pred GhostLocationW(l LocName, ra RA, e Elem, i Witness) { acc(i.i, 1/2) && witness(model, l, i.c) && i.c.witness(i.i) && @@ -93,9 +94,10 @@ pred ghostLocationIdx(l LocName, ra RA, e Elem, i Witness) { ra.IsValid(i.i.val) // and ra is in ras (we have a witness) } -// IsInv(ghostMem()) && ra elem model.witness() - +// IsInv(GlobalMem()) && ra elem model.witness() +// TODO: drop +pred GhostLocation(l LocName, ra RA, e Elem) ghost requires ra != nil @@ -110,12 +112,12 @@ ghost requires ra != nil requires ra.IsElem(e) && ra.IsValid(e) ensures l != nil -ensures ghostLocationIdx(l, ra, e, i) +ensures GhostLocationW(l, ra, e, i) decreases func AllocWithIdx(ra RA, e Elem) (l LocName, i Witness) { // obtain pkg inv - inhale ghostMem() - unfold ghostMem() + inhale GlobalMem() + unfold GlobalMem() newl := new(int) var cs cooliosetio = allocSet() @@ -128,7 +130,7 @@ func AllocWithIdx(ra RA, e Elem) (l LocName, i Witness) { inhale acc(ras) assume ras[newl] === ra // ras[newl] = ra // type system limitation, solved when swapping ras to a monotonic set - fold ghostLocationIdx(newl, ra, e, newi) + fold GhostLocationW(newl, ra, e, newi) assert acc(newl, 1/2) // TODO: prolly missing triggers @@ -145,9 +147,9 @@ func AllocWithIdx(ra RA, e Elem) (l LocName, i Witness) { (forall i idx :: i elem toCoolSet(toDict(model)[k]) ==> i.inUse ==> (ras[k].IsElem(i.val) && ras[k].IsValid(i.val))) assume false - fold ghostMem() + fold GlobalMem() // close pkg inv - exhale ghostMem() + exhale GlobalMem() return newl, newi } @@ -156,15 +158,15 @@ ghost requires ra != nil requires ra.IsElem(e1) requires ra.IsElem(e2) -requires ghostLocationIdx(l, ra, ra.Compose(e1, e2), i) -ensures ghostLocationIdx(l, ra, e1, i1) && ghostLocationIdx(l, ra, e2, i2) +requires GhostLocationW(l, ra, ra.Compose(e1, e2), i) +ensures GhostLocationW(l, ra, e1, i1) && GhostLocationW(l, ra, e2, i2) decreases func GhostOp1WithIdx(l LocName, ra RA, e1 Elem, e2 Elem, i Witness) (i1 Witness, i2 Witness) { // obtain pkg inv - inhale ghostMem() - unfold ghostMem() + inhale GlobalMem() + unfold GlobalMem() - unfold ghostLocationIdx(l, ra, ra.Compose(e1, e2), i) + unfold GhostLocationW(l, ra, ra.Compose(e1, e2), i) // todo: when we use monotonic maps assume l elem ras && ras[l] === ra @@ -186,13 +188,13 @@ func GhostOp1WithIdx(l LocName, ra RA, e1 Elem, e2 Elem, i Witness) (i1 Witness, dupWitness(model, l, i.c) i.c.add(iii1) i1 = Witness {iii1, i.c} - fold ghostLocationIdx(l, ra, e1, i1) + fold GhostLocationW(l, ra, e1, i1) iii2 := &meta{true, e2} i.c.add(iii2) assert witness(model, l, i.c) i2 = Witness {iii2, i.c} - fold ghostLocationIdx(l, ra, e2, i2) + fold GhostLocationW(l, ra, e2, i2) assume forall k1, k2 LocName :: k1 elem domain(toDict(model)) && k2 elem domain(toDict(model)) && k1 != k2 ==> (forall i idx :: i elem toCoolSet(toDict(model)[k1]) ==> !(i elem toCoolSet(toDict(model)[k2]))) @@ -206,9 +208,9 @@ func GhostOp1WithIdx(l LocName, ra RA, e1 Elem, e2 Elem, i Witness) (i1 Witness, ras[k].IsElem(ras[k].Compose(i.val, i2.val)) && ras[k].IsValid(ras[k].Compose(i.val, i2.val)))) - fold ghostMem() + fold GlobalMem() // close pkg inv - exhale ghostMem() + exhale GlobalMem() } // modifies the set, removes one elem, adds two. should follow from axioms of RAs @@ -225,16 +227,16 @@ ghost requires ra != nil requires ra.IsElem(e1) requires ra.IsElem(e2) -requires ghostLocationIdx(l, ra, e1, i1) && ghostLocationIdx(l, ra, e2, i2) -ensures ghostLocationIdx(l, ra, ra.Compose(e1, e2), i1) +requires GhostLocationW(l, ra, e1, i1) && GhostLocationW(l, ra, e2, i2) +ensures GhostLocationW(l, ra, ra.Compose(e1, e2), i1) decreases func GhostOp2WithIdx(l LocName, ra RA, e1 Elem, e2 Elem, i1 Witness, i2 Witness) { // obtain pkg inv - inhale ghostMem() - unfold ghostMem() + inhale GlobalMem() + unfold GlobalMem() - unfold ghostLocationIdx(l, ra, e1, i1) - unfold ghostLocationIdx(l, ra, e2, i2) + unfold GhostLocationW(l, ra, e1, i1) + unfold GhostLocationW(l, ra, e2, i2) lemmaWitness(model, l, i2.c, 1/3) assert i2.c === toDict(model)[l] i2.c.lemmaWitness(i2.i, 1/3) @@ -246,7 +248,7 @@ func GhostOp2WithIdx(l LocName, ra RA, e1 Elem, e2 Elem, i1 Witness, i2 Witness) i1.i.val = ra.Compose(e1, e2) // triggering issue ? assume ra.IsElem(ra.Compose(e1, e2)) && ra.IsValid(ra.Compose(e1, e2)) - fold ghostLocationIdx(l, ra, ra.Compose(e1, e2), i1) + fold GhostLocationW(l, ra, ra.Compose(e1, e2), i1) // triggering issue assume forall k LocName :: k elem domain(toDict(model)) ==> @@ -263,9 +265,9 @@ func GhostOp2WithIdx(l LocName, ra RA, e1 Elem, e2 Elem, i1 Witness, i2 Witness) ras[k].IsValid(ras[k].Compose(i.val, i2.val)))) - fold ghostMem() + fold GlobalMem() // close pkg inv - exhale ghostMem() + exhale GlobalMem() } ghost @@ -280,13 +282,13 @@ func GhostOp2(l LocName, ra RA, e1 Elem, e2 Elem) ghost requires ra != nil -requires ghostLocationIdx(l, ra, e, i) -ensures ghostLocationIdx(l, ra, e, i) +requires GhostLocationW(l, ra, e, i) +ensures GhostLocationW(l, ra, e, i) ensures ra.IsElem(e) && ra.IsValid(e) decreases func GhostValidWithIdx(l LocName, ra RA, e Elem, i Witness) { - unfold ghostLocationIdx(l, ra, e, i) - fold ghostLocationIdx(l, ra, e, i) + unfold GhostLocationW(l, ra, e, i) + fold GhostLocationW(l, ra, e, i) } ghost @@ -347,17 +349,17 @@ ghost requires ra != nil requires ra.IsElem(e1) requires ra.IsElem(e2) -requires ghostLocationIdx(l, ra, e1, i) +requires GhostLocationW(l, ra, e1, i) requires IsFramePreservingUpdate(ra, e1, e2) -ensures ghostLocationIdx(l, ra, e2, i) +ensures GhostLocationW(l, ra, e2, i) decreases // slightly different from paper, improve func GhostUpdateWithIdx(l LocName, ra RA, e1 Elem, e2 Elem, i Witness) { // obtain pkg inv - inhale ghostMem() - unfold ghostMem() + inhale GlobalMem() + unfold GlobalMem() - unfold ghostLocationIdx(l, ra, e1, i) + unfold GhostLocationW(l, ra, e1, i) lemmaWitness(model, l, i.c, 1/3) i.c.lemmaWitness(i.i, 1/3) i.i.val = e2 @@ -397,9 +399,9 @@ func GhostUpdateWithIdx(l LocName, ra RA, e1 Elem, e2 Elem, i Witness) { ras[k].IsElem(ras[k].Compose(i.val, i2.val)) && ras[k].IsValid(ras[k].Compose(i.val, i2.val)))) - fold ghostLocationIdx(l, ra, e2, i) + fold GhostLocationW(l, ra, e2, i) - fold ghostMem() + fold GlobalMem() // close pkg inv - exhale ghostMem() + exhale GlobalMem() } From db29a30bf3ad1d707ba43c2112103c228866d9ba Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= Date: Tue, 20 Jan 2026 22:06:47 +0100 Subject: [PATCH 09/28] clean-up --- resalgebraNoAxioms/auth_test.gobra | 4 +- resalgebraNoAxioms/doc.gobra | 54 +++-- resalgebraNoAxioms/loc.gobra | 376 +++++++++++++++++------------ resalgebraNoAxioms/oneshot.gobra | 1 - 4 files changed, 254 insertions(+), 181 deletions(-) diff --git a/resalgebraNoAxioms/auth_test.gobra b/resalgebraNoAxioms/auth_test.gobra index f6a0e99..e9771c5 100644 --- a/resalgebraNoAxioms/auth_test.gobra +++ b/resalgebraNoAxioms/auth_test.gobra @@ -16,6 +16,7 @@ package resalgebraNoAxioms +/* import "sync" type MonoCounter struct { @@ -75,4 +76,5 @@ func test(c *MonoCounter) { GhostOp2(c.loc, AuthRA, c.authRes, FragView(10)) GhostValid(c.loc, AuthRA, v) assert c.val >= 10 -} \ No newline at end of file +} +*/ \ No newline at end of file diff --git a/resalgebraNoAxioms/doc.gobra b/resalgebraNoAxioms/doc.gobra index 2680366..72564c7 100644 --- a/resalgebraNoAxioms/doc.gobra +++ b/resalgebraNoAxioms/doc.gobra @@ -14,7 +14,9 @@ // +gobra -// This package is shows that we can provide a model for ghost locations, similar to +package resalgebraNoAxioms + +// This package shows that we can provide a model for ghost locations, similar to // those of Iris entirely in Gobra. The public API of this package is very similar to // that of `resalgebra` except that (1) we made some tweaks to the definition of RA that // should be logically equivalent to those of the RA defined in `resalgebra` @@ -23,29 +25,29 @@ // to provide the instantiations of the quantified variables), (2) all // lemmas for ghost locations require a Witness value to be passed. // This is due to a technicality in Gobra (we cannot existentially quantify -// over resources). Nonetheless, one may have the same API as that -// of `resalgebra/loc.gobra` if one axiomatizes the introduction and elimination -// rules for existential QPs: -// -// // Same as `exists w s.t. GhostLocationW(l, ra, e, w)` -// pred GhostLocation(l LocName, ra RA, e Elem) -// -// // Converting between GhostLocationW and GhostLocation by -// // introducing the existential quantifier. -// ghost -// trusted -// requires GhostLocationW(l, ra, e, w) -// ensures GhostLocation(l, ra, e) -// decreases -// func IntroExists(l LocName, ra RA, e Elem, w Witness) -// -// // Converting between GhostLocation and GhostLocationW by -// // eliminating the existential quantifier. -// ghost -// trusted -// requires GhostLocation(l, ra, e) -// ensures GhostLocationW(l, ra, e, w) -// decreases -// func IntroElim(l LocName, ra RA, e Elem) (w Witness) +// over resources). -package resalgebraNoAxioms +// For the time being, to keep the same API for GhostLocations +// as the one found in `resalgebra/loc.gobra`, we axiomatize +// the introduction and elimination rules for existential QPs: + +// Same as `exists w s.t. GhostLocationW(l, ra, e, w)` +pred GhostLocation(l LocName, ra RA, e Elem) + +// Converting between GhostLocationW and GhostLocation by +// introducing the existential quantifier. +ghost +trusted +requires GhostLocationW(l, ra, e, w) +ensures GhostLocation(l, ra, e) +decreases +func IntroExists(l LocName, ra RA, e Elem, w Witness) + +// Converting between GhostLocation and GhostLocationW by +// eliminating the existential quantifier. +ghost +trusted +requires GhostLocation(l, ra, e) +ensures GhostLocationW(l, ra, e, w) +decreases +func ElimExists(l LocName, ra RA, e Elem) (w Witness) \ No newline at end of file diff --git a/resalgebraNoAxioms/loc.gobra b/resalgebraNoAxioms/loc.gobra index e1edfab..9ebe2d1 100644 --- a/resalgebraNoAxioms/loc.gobra +++ b/resalgebraNoAxioms/loc.gobra @@ -18,17 +18,10 @@ package resalgebraNoAxioms // TODO: // - change to quantified lemmas, make the old lemmas available as a function defined outside the RA -// - rename "Idx" to "Witness", drop all lemmas without the witness and rename functions "WithIdx" to drop the suffix -// - drop axioms.gobra -// - move cooliosetio and coliomapio to another package, make them generic +// - use Monoset and monomap, copy to this package if need be; delete cooliosetio and mapio // - use a cooliomapio for ras -// - adapt all documentation -// - change all functions to pass around the witnesses // - add triggers to invariants -// - drop all assumptions -// - come up with better names for everything -// - adapt package resalgebra to be an interface that redirects to this one, and introduces the existential elimination and introduction axioms -// - add invs +// - implement invs and atomic regions in Gobra // At the moment, all of these definitions are trusted, and this, // prone to mistakes. If possible, we should find a model for the @@ -36,24 +29,114 @@ package resalgebraNoAxioms ghost type LocName gpointer[int] -// should be a coolio mappio from locname to (RA, set[idx]) -ghost var model cooliomapio -ghost var ras map[LocName]RA // probably needs to be monotonic as well +/***** GhostLocation *****/ -ghost type idx gpointer[meta] +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) { + l, w := AllocW(ra, e) + assert GhostLocationW(l, ra, e, w) + IntroExists(l, ra, e, w) +} -ghost type Witness ghost struct { - i idx - c cooliosetio +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) { + w := ElimExists(l, ra, ra.Compose(e1, e2)) + w1, w2 := GhostOp1W(l, ra, e1, e2, w) + IntroExists(l, ra, e1, w1) + IntroExists(l, ra, e2, w2) } -// replace by infinite type for idx -ghost type meta ghost struct { - inUse bool - val 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) { + w1 := ElimExists(l, ra, e1) + w2 := ElimExists(l, ra, e2) + GhostOp2W(l, ra, e1, e2, w1, w2) + IntroExists(l, ra, ra.Compose(e1, e2), w1) +} + +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) { + w := ElimExists(l, ra, e) + GhostValidW(l, ra, e, w) + IntroExists(l, ra, e, w) +} + +// Slightly different from paper, only captures a deterministic update. +// Non-deterministic update can be easily supported too. +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 +func GhostUpdate(l LocName, ra RA, e1 Elem, e2 Elem) { + w := ElimExists(l, ra, e1) + GhostUpdateW(l, ra, e1, e2, w) + IntroExists(l, ra, e2, w) +} + +/***** Frame-Preserving Updates *****/ + +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 } -// TODO IsInv(GlobalMem()) should be established by init +/***** Model: Global State *****/ + +// TODO: IsInv(GlobalMem()) should be established by init pred GlobalMem() { inv(model) && acc(ras) && @@ -80,43 +163,47 @@ pred GlobalMem() { ras[k].IsElem(ras[k].Compose(i.val, i2.val)) && ras[k].IsValid(ras[k].Compose(i.val, i2.val))))) } - // acc model - // for every member in model, we have half perm to In Use - -// TODO: rename to GhostLocationW -pred GhostLocationW(l LocName, ra RA, e Elem, i Witness) { - acc(i.i, 1/2) && - witness(model, l, i.c) && - i.c.witness(i.i) && + +ghost var model cooliomapio + +ghost var ras map[LocName]RA // TODO: make monotonic + +/***** Model *****/ + +ghost type idx gpointer[meta] + +ghost type Witness ghost struct { + i idx + c cooliosetio +} + +ghost type meta ghost struct { + inUse bool + val Elem +} + +pred GhostLocationW(l LocName, ra RA, e Elem, w Witness) { + acc(w.i, 1/2) && + witness(model, l, w.c) && + w.c.witness(w.i) && ra != nil && - i.i.val === e && - ra.IsElem(i.i.val) && - ra.IsValid(i.i.val) + w.i.val === e && + ra.IsElem(w.i.val) && + ra.IsValid(w.i.val) // and ra is in ras (we have a witness) } -// IsInv(GlobalMem()) && ra elem model.witness() - -// TODO: drop -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) -// adds a new key to the set, and a set to the model +/***** Model: functions that do not acquire global invariant; these functions may be called from critical regions *****/ ghost +requires GlobalMem() requires ra != nil requires ra.IsElem(e) && ra.IsValid(e) +ensures GlobalMem() ensures l != nil -ensures GhostLocationW(l, ra, e, i) +ensures GhostLocationW(l, ra, e, w) decreases -func AllocWithIdx(ra RA, e Elem) (l LocName, i Witness) { - // obtain pkg inv - inhale GlobalMem() +func AllocWI(ra RA, e Elem) (l LocName, w Witness) { unfold GlobalMem() newl := new(int) @@ -148,22 +235,21 @@ func AllocWithIdx(ra RA, e Elem) (l LocName, i Witness) { i.inUse ==> (ras[k].IsElem(i.val) && ras[k].IsValid(i.val))) assume false fold GlobalMem() - // close pkg inv - exhale GlobalMem() return newl, newi } ghost +requires GlobalMem() requires ra != nil requires ra.IsElem(e1) requires ra.IsElem(e2) -requires GhostLocationW(l, ra, ra.Compose(e1, e2), i) -ensures GhostLocationW(l, ra, e1, i1) && GhostLocationW(l, ra, e2, i2) +requires GhostLocationW(l, ra, ra.Compose(e1, e2), w) +ensures GlobalMem() +ensures GhostLocationW(l, ra, e1, w1) && GhostLocationW(l, ra, e2, w2) decreases -func GhostOp1WithIdx(l LocName, ra RA, e1 Elem, e2 Elem, i Witness) (i1 Witness, i2 Witness) { - // obtain pkg inv - inhale GlobalMem() +func GhostOp1WI(l LocName, ra RA, e1 Elem, e2 Elem, w Witness) (w1 Witness, w2 Witness) { + i := w unfold GlobalMem() unfold GhostLocationW(l, ra, ra.Compose(e1, e2), i) @@ -187,13 +273,13 @@ func GhostOp1WithIdx(l LocName, ra RA, e1 Elem, e2 Elem, i Witness) (i1 Witness, iii1 := &meta{true, e1} dupWitness(model, l, i.c) i.c.add(iii1) - i1 = Witness {iii1, i.c} + i1 := Witness {iii1, i.c} fold GhostLocationW(l, ra, e1, i1) iii2 := &meta{true, e2} i.c.add(iii2) assert witness(model, l, i.c) - i2 = Witness {iii2, i.c} + i2 := Witness {iii2, i.c} fold GhostLocationW(l, ra, e2, i2) assume forall k1, k2 LocName :: k1 elem domain(toDict(model)) && k2 elem domain(toDict(model)) && k1 != k2 ==> @@ -209,30 +295,22 @@ func GhostOp1WithIdx(l LocName, ra RA, e1 Elem, e2 Elem, i Witness) (i1 Witness, ras[k].IsValid(ras[k].Compose(i.val, i2.val)))) fold GlobalMem() - // close pkg inv - exhale GlobalMem() + return i1, i2 } -// modifies the set, removes one elem, adds two. should follow from axioms of RAs ghost +requires GlobalMem() 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) +requires GhostLocationW(l, ra, e1, w1) && GhostLocationW(l, ra, e2, w2) +ensures GlobalMem() +ensures GhostLocationW(l, ra, ra.Compose(e1, e2), w1) decreases -func GhostOp1(l LocName, ra RA, e1 Elem, e2 Elem) +func GhostOp2WI(l LocName, ra RA, e1 Elem, e2 Elem, w1 Witness, w2 Witness) { + i1 := w1 + i2 := w2 -ghost -requires ra != nil -requires ra.IsElem(e1) -requires ra.IsElem(e2) -requires GhostLocationW(l, ra, e1, i1) && GhostLocationW(l, ra, e2, i2) -ensures GhostLocationW(l, ra, ra.Compose(e1, e2), i1) -decreases -func GhostOp2WithIdx(l LocName, ra RA, e1 Elem, e2 Elem, i1 Witness, i2 Witness) { - // obtain pkg inv - inhale GlobalMem() unfold GlobalMem() unfold GhostLocationW(l, ra, e1, i1) @@ -256,7 +334,7 @@ func GhostOp2WithIdx(l LocName, ra RA, e1 Elem, e2 Elem, i1 Witness, i2 Witness) i.inUse ==> (ras[k].IsElem(i.val) && ras[k].IsValid(i.val))) // proof requires that all previous elems can be added to this one and become valid. - // actually, the proof should be very similar to that of GhostOp1WithIdx + // actually, the proof should be very similar to that of GhostOp1W assume forall k LocName :: k elem domain(toDict(model)) ==> (forall i idx :: i elem toCoolSet(toDict(model)[k]) ==> i.inUse ==> ( @@ -266,97 +344,31 @@ func GhostOp2WithIdx(l LocName, ra RA, e1 Elem, e2 Elem, i1 Witness, i2 Witness) fold GlobalMem() - // close pkg inv - exhale GlobalMem() -} - -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) -// should follow from the invariant of the set - -ghost -requires ra != nil -requires GhostLocationW(l, ra, e, i) -ensures GhostLocationW(l, ra, e, i) -ensures ra.IsElem(e) && ra.IsValid(e) -decreases -func GhostValidWithIdx(l LocName, ra RA, e Elem, i Witness) { - unfold GhostLocationW(l, ra, e, i) - fold GhostLocationW(l, ra, e, i) } ghost requires ra != nil -requires GhostLocation(l, ra, e) -ensures GhostLocation(l, ra, e) +requires GhostLocationW(l, ra, e, w) +ensures GhostLocationW(l, ra, e, w) ensures ra.IsElem(e) && ra.IsValid(e) decreases -func GhostValid(l LocName, ra RA, e Elem) -// trivial from the inv - -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 +func GhostValidW(l LocName, ra RA, e Elem, w Witness) { + unfold GhostLocationW(l, ra, e, w) + fold GhostLocationW(l, ra, e, w) } ghost +requires GlobalMem() requires ra != nil requires ra.IsElem(e1) requires ra.IsElem(e2) -requires GhostLocation(l, ra, e1) +requires GhostLocationW(l, ra, e1, w) requires IsFramePreservingUpdate(ra, e1, e2) -ensures GhostLocation(l, ra, e2) +ensures GlobalMem() +ensures GhostLocationW(l, ra, e2, w) decreases -// slightly different from paper, improve -func GhostUpdate(l LocName, ra RA, e1 Elem, e2 Elem) -// should be trivial to prove too - -ghost -requires ra != nil -requires ra.IsElem(e1) -requires ra.IsElem(e2) -requires GhostLocationW(l, ra, e1, i) -requires IsFramePreservingUpdate(ra, e1, e2) -ensures GhostLocationW(l, ra, e2, i) -decreases -// slightly different from paper, improve -func GhostUpdateWithIdx(l LocName, ra RA, e1 Elem, e2 Elem, i Witness) { - // obtain pkg inv - inhale GlobalMem() +func GhostUpdateWI(l LocName, ra RA, e1 Elem, e2 Elem, w Witness) { + i := w unfold GlobalMem() unfold GhostLocationW(l, ra, e1, i) @@ -402,6 +414,64 @@ func GhostUpdateWithIdx(l LocName, ra RA, e1 Elem, e2 Elem, i Witness) { fold GhostLocationW(l, ra, e2, i) fold GlobalMem() - // close pkg inv - exhale GlobalMem() } + +/***** Model: wrappers that acquire the global invariant; these functions may not be called from critical regions *****/ + +// TODO: IsInv(GlobalMem()) should be a duplicable invariant + +ghost +// opensInvariants +requires ra != nil +requires ra.IsElem(e) && ra.IsValid(e) +ensures l != nil +ensures GhostLocationW(l, ra, e, w) +decreases +func AllocW(ra RA, e Elem) (l LocName, w Witness) { + inhale GlobalMem() // acquire dup pkg invariant && open invariant + l, w = AllocWI(ra, e) + exhale GlobalMem() // close invariant +} + +ghost +// opensInvariants +requires ra != nil +requires ra.IsElem(e1) +requires ra.IsElem(e2) +requires GhostLocationW(l, ra, ra.Compose(e1, e2), w) +ensures GhostLocationW(l, ra, e1, w1) && GhostLocationW(l, ra, e2, w2) +decreases +func GhostOp1W(l LocName, ra RA, e1 Elem, e2 Elem, w Witness) (w1 Witness, w2 Witness) { + inhale GlobalMem() // acquire dup pkg invariant && open invariant + w1, w2 = GhostOp1WI(l, ra, e1, e2, w) + exhale GlobalMem() // close invariant +} + +ghost +// opensInvariants +requires ra != nil +requires ra.IsElem(e1) +requires ra.IsElem(e2) +requires GhostLocationW(l, ra, e1, w1) && GhostLocationW(l, ra, e2, w2) +ensures GhostLocationW(l, ra, ra.Compose(e1, e2), w1) +decreases +func GhostOp2W(l LocName, ra RA, e1 Elem, e2 Elem, w1 Witness, w2 Witness) { + inhale GlobalMem() // acquire dup pkg invariant && open invariant + GhostOp2WI(l, ra, e1, e2, w1, w2) + exhale GlobalMem() // close invariant +} + +ghost +// opensInvariants +requires ra != nil +requires ra.IsElem(e1) +requires ra.IsElem(e2) +requires GhostLocationW(l, ra, e1, w) +requires IsFramePreservingUpdate(ra, e1, e2) +ensures GhostLocationW(l, ra, e2, w) +decreases +func GhostUpdateW(l LocName, ra RA, e1 Elem, e2 Elem, w Witness) { + inhale GlobalMem() // acquire dup pkg invariant && open invariant + GhostUpdateWI(l, ra, e1, e2, w) + exhale GlobalMem() // close invariant +} \ No newline at end of file diff --git a/resalgebraNoAxioms/oneshot.gobra b/resalgebraNoAxioms/oneshot.gobra index 23a9cbb..12bda1a 100644 --- a/resalgebraNoAxioms/oneshot.gobra +++ b/resalgebraNoAxioms/oneshot.gobra @@ -42,7 +42,6 @@ func (ra TypeOneShotRA) IsElem(e Elem) (res bool) { (e === Fail{}) } - ghost requires ra.IsElem(e) decreases From 46da2e406a7d115b74b4893f08a02804ae5a1bf6 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= Date: Tue, 20 Jan 2026 22:30:20 +0100 Subject: [PATCH 10/28] backup --- genericmonomap/monomap.gobra | 15 +++++++++++++++ resalgebraNoAxioms/loc.gobra | 25 ++++++++++++++----------- 2 files changed, 29 insertions(+), 11 deletions(-) diff --git a/genericmonomap/monomap.gobra b/genericmonomap/monomap.gobra index a8ec218..1cdd029 100644 --- a/genericmonomap/monomap.gobra +++ b/genericmonomap/monomap.gobra @@ -66,6 +66,21 @@ pure func (m MonoMap) ToDict() dict[Key]Val { (m.inUse ? (let smallMap := MonoMap(m.next).ToDict() in smallMap[m.k = m.v]) : dict[Key]Val{}) } +ghost +requires m.Inv() +decreases m.Inv() +pure func (m MonoMap) KeySet() set[Key] { + return domain(m.ToDict()) +} + +ghost +requires m.Inv() +requires k elem domain(m.ToDict()) +decreases m.Inv() +pure func (m MonoMap) Get(k Key) Val { + return let d := m.ToDict() in Val(d[k]) +} + pred (m MonoMap) Witness(k Key, v Val) { acc(&m.inUse, _) && acc(&m.next, _) && acc(&m.k, _) && acc(&m.v, _) && isComparable(k) && diff --git a/resalgebraNoAxioms/loc.gobra b/resalgebraNoAxioms/loc.gobra index 9ebe2d1..f1185bd 100644 --- a/resalgebraNoAxioms/loc.gobra +++ b/resalgebraNoAxioms/loc.gobra @@ -167,6 +167,7 @@ pred GlobalMem() { ghost var model cooliomapio ghost var ras map[LocName]RA // TODO: make monotonic +// ghost var ras genericmonomap.MonoMap /***** Model *****/ @@ -346,17 +347,6 @@ func GhostOp2WI(l LocName, ra RA, e1 Elem, e2 Elem, w1 Witness, w2 Witness) { fold GlobalMem() } -ghost -requires ra != nil -requires GhostLocationW(l, ra, e, w) -ensures GhostLocationW(l, ra, e, w) -ensures ra.IsElem(e) && ra.IsValid(e) -decreases -func GhostValidW(l LocName, ra RA, e Elem, w Witness) { - unfold GhostLocationW(l, ra, e, w) - fold GhostLocationW(l, ra, e, w) -} - ghost requires GlobalMem() requires ra != nil @@ -416,6 +406,19 @@ func GhostUpdateWI(l LocName, ra RA, e1 Elem, e2 Elem, w Witness) { fold GlobalMem() } +/***** Model: functions that do not depend on the global invariant *****/ + +ghost +requires ra != nil +requires GhostLocationW(l, ra, e, w) +ensures GhostLocationW(l, ra, e, w) +ensures ra.IsElem(e) && ra.IsValid(e) +decreases +func GhostValidW(l LocName, ra RA, e Elem, w Witness) { + unfold GhostLocationW(l, ra, e, w) + fold GhostLocationW(l, ra, e, w) +} + /***** Model: wrappers that acquire the global invariant; these functions may not be called from critical regions *****/ // TODO: IsInv(GlobalMem()) should be a duplicable invariant From 37734fff8e6fc14377009b5d0698b92f1dc92fd1 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= Date: Tue, 20 Jan 2026 22:46:25 +0100 Subject: [PATCH 11/28] add init code --- resalgebraNoAxioms/cooliomapio.gobra | 1 + resalgebraNoAxioms/loc.gobra | 17 +++++++++++++++-- 2 files changed, 16 insertions(+), 2 deletions(-) diff --git a/resalgebraNoAxioms/cooliomapio.gobra b/resalgebraNoAxioms/cooliomapio.gobra index 3046064..1444304 100644 --- a/resalgebraNoAxioms/cooliomapio.gobra +++ b/resalgebraNoAxioms/cooliomapio.gobra @@ -46,6 +46,7 @@ pred inv(m cooliomapio) { } ghost +mayInit ensures inv(m) decreases func allocMap() (m cooliomapio) { diff --git a/resalgebraNoAxioms/loc.gobra b/resalgebraNoAxioms/loc.gobra index f1185bd..5c60dbb 100644 --- a/resalgebraNoAxioms/loc.gobra +++ b/resalgebraNoAxioms/loc.gobra @@ -14,6 +14,7 @@ // +gobra +pkgInvariant GlobalMem() // todo: replace this by a dup invariant that GlobalMem() is an invariant package resalgebraNoAxioms // TODO: @@ -164,11 +165,23 @@ pred GlobalMem() { ras[k].IsValid(ras[k].Compose(i.val, i2.val))))) } -ghost var model cooliomapio +// ghost +// requires ras.Inv() +// requires l elem domain(ras.ToDict()) +// requires forall k LocName :: { k elem domain(ras.ToDict()) }{ k.ToDict()[k] } k elem domain(ras.ToDict()) ==> +// typeOf(k.ToDict()[k]) == type[RA] +// decreases +// pure func getRA(l LocName) RA -ghost var ras map[LocName]RA // TODO: make monotonic +ghost var model cooliomapio = allocMap() +ghost var ras map[LocName]RA = map[LocName]RA{} // TODO: make monotonic // ghost var ras genericmonomap.MonoMap +func init() { + assume false // todo + fold GlobalMem() +} + /***** Model *****/ ghost type idx gpointer[meta] From 0647c0358f243e868ace9e33cdcad90a1919f339 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= Date: Tue, 20 Jan 2026 23:39:06 +0100 Subject: [PATCH 12/28] progress with proof --- resalgebraNoAxioms/loc.gobra | 77 ++++++++-------- resalgebraNoAxioms/ras-map.gobra | 150 +++++++++++++++++++++++++++++++ 2 files changed, 186 insertions(+), 41 deletions(-) create mode 100644 resalgebraNoAxioms/ras-map.gobra diff --git a/resalgebraNoAxioms/loc.gobra b/resalgebraNoAxioms/loc.gobra index 5c60dbb..3c00a8d 100644 --- a/resalgebraNoAxioms/loc.gobra +++ b/resalgebraNoAxioms/loc.gobra @@ -140,11 +140,11 @@ pure func LiftedIsValid(ra RA, e option[Elem]) bool { // TODO: IsInv(GlobalMem()) should be established by init pred GlobalMem() { inv(model) && - acc(ras) && + ras.Inv() && // necessary for proving key freshness (forall k LocName :: k elem domain(toDict(model)) ==> acc(k, 1/2)) && - (forall k LocName :: k elem domain(toDict(model)) ==> k elem domain(ras)) && - (forall k LocName :: k elem domain(ras) ==> ras[k] != RA(nil)) && + (forall k LocName :: k elem domain(toDict(model)) ==> k elem domain(ras.ToDict())) && + (forall k LocName :: k elem domain(ras.ToDict()) ==> ras.ToDict()[k] != RA(nil)) && // injectivity (forall k1, k2 LocName :: k1 elem domain(toDict(model)) && k2 elem domain(toDict(model)) && k1 != k2 ==> toDict(model)[k1] != toDict(model)[k2]) && @@ -156,26 +156,17 @@ pred GlobalMem() { (forall i idx :: i elem toCoolSet(toDict(model)[k]) ==> acc(i, 1/2))) && (forall k LocName :: k elem domain(toDict(model)) ==> (forall i idx :: i elem toCoolSet(toDict(model)[k]) ==> - i.inUse ==> (ras[k].IsElem(i.val) && ras[k].IsValid(i.val)))) && + i.inUse ==> (ras.ToDict()[k].IsElem(i.val) && ras.ToDict()[k].IsValid(i.val)))) && (forall k LocName :: k elem domain(toDict(model)) ==> (forall i idx :: i elem toCoolSet(toDict(model)[k]) ==> i.inUse ==> ( forall i2 idx :: i2 elem toCoolSet(toDict(model)[k]) && i2.inUse && i2 !== i ==> - ras[k].IsElem(ras[k].Compose(i.val, i2.val)) && - ras[k].IsValid(ras[k].Compose(i.val, i2.val))))) + ras.ToDict()[k].IsElem(ras.ToDict()[k].Compose(i.val, i2.val)) && + ras.ToDict()[k].IsValid(ras.ToDict()[k].Compose(i.val, i2.val))))) } -// ghost -// requires ras.Inv() -// requires l elem domain(ras.ToDict()) -// requires forall k LocName :: { k elem domain(ras.ToDict()) }{ k.ToDict()[k] } k elem domain(ras.ToDict()) ==> -// typeOf(k.ToDict()[k]) == type[RA] -// decreases -// pure func getRA(l LocName) RA - ghost var model cooliomapio = allocMap() -ghost var ras map[LocName]RA = map[LocName]RA{} // TODO: make monotonic -// ghost var ras genericmonomap.MonoMap +ghost var ras rasMap = rasMapAlloc() func init() { assume false // todo @@ -197,14 +188,14 @@ ghost type meta ghost struct { } pred GhostLocationW(l LocName, ra RA, e Elem, w Witness) { - acc(w.i, 1/2) && + acc(w.i, 1/2) && witness(model, l, w.c) && - w.c.witness(w.i) && - ra != nil && - w.i.val === e && - ra.IsElem(w.i.val) && - ra.IsValid(w.i.val) - // and ra is in ras (we have a witness) + w.c.witness(w.i) && + ra != nil && + w.i.val === e && + ra.IsElem(w.i.val) && + ra.IsValid(w.i.val) && + ras.Witness(l, ra) } /***** Model: functions that do not acquire global invariant; these functions may be called from critical regions *****/ @@ -226,10 +217,13 @@ func AllocWI(ra RA, e Elem) (l LocName, w Witness) { cs.add(iii) add(model, newl, cs) assert witness(model, newl, cs) - newi := Witness {iii, cs} - exhale acc(ras) - inhale acc(ras) - assume ras[newl] === ra + newi := Witness{iii, cs} + rasDict := ras.ToDict() + assume !(newl elem domain(rasDict)) + ras.Insert(newl, ra) + // exhale acc(ras) + // inhale acc(ras) + // assume ras.ToDict()[newl] === ra // ras[newl] = ra // type system limitation, solved when swapping ras to a monotonic set fold GhostLocationW(newl, ra, e, newi) @@ -237,8 +231,8 @@ func AllocWI(ra RA, e Elem) (l LocName, w Witness) { // TODO: prolly missing triggers assume forall k LocName :: k elem domain(toDict(model)) ==> acc(k, 1/2) // TODO: fixed when we have a monotonic set and with permissions for showing injectivity - assume forall k LocName :: k elem domain(toDict(model)) ==> k elem domain(ras) - assume forall k LocName :: k elem domain(ras) ==> ras[k] != RA(nil) + assume forall k LocName :: k elem domain(toDict(model)) ==> k elem domain(ras.ToDict()) + assume forall k LocName :: k elem domain(ras.ToDict()) ==> ras.ToDict()[k] != RA(nil) assume forall k1, k2 LocName :: k1 elem domain(toDict(model)) && k2 elem domain(toDict(model)) && k1 != k2 ==> (forall i idx :: i elem toCoolSet(toDict(model)[k1]) ==> !(i elem toCoolSet(toDict(model)[k2]))) // problem with triggers? @@ -246,7 +240,7 @@ func AllocWI(ra RA, e Elem) (l LocName, w Witness) { (forall i idx :: i elem toCoolSet(toDict(model)[k]) ==> acc(i, 1/2)) assume forall k LocName :: k elem domain(toDict(model)) ==> (forall i idx :: i elem toCoolSet(toDict(model)[k]) ==> - i.inUse ==> (ras[k].IsElem(i.val) && ras[k].IsValid(i.val))) + i.inUse ==> (ras.ToDict()[k].IsElem(i.val) && ras.ToDict()[k].IsValid(i.val))) assume false fold GlobalMem() @@ -269,7 +263,7 @@ func GhostOp1WI(l LocName, ra RA, e1 Elem, e2 Elem, w Witness) (w1 Witness, w2 W unfold GhostLocationW(l, ra, ra.Compose(e1, e2), i) // todo: when we use monotonic maps - assume l elem ras && ras[l] === ra + assume l elem domain(ras.ToDict()) && ras.ToDict()[l] === ra assert witness(model, l, i.c) lemmaWitness(model, l, i.c, 1/3) assert toDict(model)[l] === i.c @@ -287,13 +281,14 @@ func GhostOp1WI(l LocName, ra RA, e1 Elem, e2 Elem, w Witness) (w1 Witness, w2 W iii1 := &meta{true, e1} dupWitness(model, l, i.c) i.c.add(iii1) - i1 := Witness {iii1, i.c} + i1 := Witness{iii1, i.c} + ras.DupWitness(l, ra) fold GhostLocationW(l, ra, e1, i1) iii2 := &meta{true, e2} i.c.add(iii2) assert witness(model, l, i.c) - i2 := Witness {iii2, i.c} + i2 := Witness{iii2, i.c} fold GhostLocationW(l, ra, e2, i2) assume forall k1, k2 LocName :: k1 elem domain(toDict(model)) && k2 elem domain(toDict(model)) && k1 != k2 ==> @@ -305,8 +300,8 @@ func GhostOp1WI(l LocName, ra RA, e1 Elem, e2 Elem, w Witness) (w1 Witness, w2 W (forall i idx :: i elem toCoolSet(toDict(model)[k]) ==> i.inUse ==> ( forall i2 idx :: i2 elem toCoolSet(toDict(model)[k]) && i2.inUse && i2 !== i ==> - ras[k].IsElem(ras[k].Compose(i.val, i2.val)) && - ras[k].IsValid(ras[k].Compose(i.val, i2.val)))) + ras.ToDict()[k].IsElem( ras.ToDict()[k].Compose(i.val, i2.val)) && + ras.ToDict()[k].IsValid(ras.ToDict()[k].Compose(i.val, i2.val)))) fold GlobalMem() return i1, i2 @@ -345,7 +340,7 @@ func GhostOp2WI(l LocName, ra RA, e1 Elem, e2 Elem, w1 Witness, w2 Witness) { // triggering issue assume forall k LocName :: k elem domain(toDict(model)) ==> (forall i idx :: i elem toCoolSet(toDict(model)[k]) ==> - i.inUse ==> (ras[k].IsElem(i.val) && ras[k].IsValid(i.val))) + i.inUse ==> (ras.ToDict()[k].IsElem(i.val) && ras.ToDict()[k].IsValid(i.val))) // proof requires that all previous elems can be added to this one and become valid. // actually, the proof should be very similar to that of GhostOp1W @@ -353,8 +348,8 @@ func GhostOp2WI(l LocName, ra RA, e1 Elem, e2 Elem, w1 Witness, w2 Witness) { (forall i idx :: i elem toCoolSet(toDict(model)[k]) ==> i.inUse ==> ( forall i2 idx :: i2 elem toCoolSet(toDict(model)[k]) && i2.inUse && i2 !== i ==> - ras[k].IsElem(ras[k].Compose(i.val, i2.val)) && - ras[k].IsValid(ras[k].Compose(i.val, i2.val)))) + ras.ToDict()[k].IsElem(ras.ToDict()[k].Compose(i.val, i2.val)) && + ras.ToDict()[k].IsValid(ras.ToDict()[k].Compose(i.val, i2.val)))) fold GlobalMem() @@ -405,14 +400,14 @@ func GhostUpdateWI(l LocName, ra RA, e1 Elem, e2 Elem, w Witness) { // } // TODO: drop when ras is a monotonic set - assume ras[l] === ra + assume ras.ToDict()[l] === ra // TODO: should be provable from the def of IsFramePreservingUpdate assume forall k LocName :: k elem domain(toDict(model)) ==> (forall i idx :: i elem toCoolSet(toDict(model)[k]) ==> i.inUse ==> ( forall i2 idx :: i2 elem toCoolSet(toDict(model)[k]) && i2.inUse && i2 !== i ==> - ras[k].IsElem(ras[k].Compose(i.val, i2.val)) && - ras[k].IsValid(ras[k].Compose(i.val, i2.val)))) + ras.ToDict()[k].IsElem(ras.ToDict()[k].Compose(i.val, i2.val)) && + ras.ToDict()[k].IsValid(ras.ToDict()[k].Compose(i.val, i2.val)))) fold GhostLocationW(l, ra, e2, i) diff --git a/resalgebraNoAxioms/ras-map.gobra b/resalgebraNoAxioms/ras-map.gobra new file mode 100644 index 0000000..623adbd --- /dev/null +++ b/resalgebraNoAxioms/ras-map.gobra @@ -0,0 +1,150 @@ +// 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 + +// Instantiation of genericmonomap for `ras` (Key is LocName and Val is RA). +// Copying this is easier than implementing wrappers around MonoMap. + +package resalgebraNoAxioms + +ghost type keyRasMap = LocName +type valRasMap = RA + +ghost type nodeRasMap ghost struct { + inUse bool + next gpointer[nodeRasMap] + k keyRasMap + v valRasMap + p perm +} + +ghost type rasMap gpointer[nodeRasMap] + +pred (m rasMap) Inv() { + acc(m, 1/2) && + (m.next == nil ==> !m.inUse && acc(m, 1/2)) && + (m.next != nil ==> + m.inUse && + acc(&m.p, 1/2) && + rasMap(m.next).Inv() && + m.p > 0 && + acc(&m.inUse, m.p) && acc(&m.next, m.p) && acc(&m.k, m.p) && acc(&m.v, m.p)) +} + +ghost +mayInit +ensures m.Inv() +decreases +func rasMapAlloc() (m rasMap) { + var g@ nodeRasMap + fold rasMap(&g).Inv() + return &g +} + +ghost +requires m.Inv() +decreases m.Inv() +pure func (m rasMap) ToDict() dict[keyRasMap]valRasMap { + return unfolding m.Inv() in + (m.inUse ? (let smallMap := rasMap(m.next).ToDict() in smallMap[m.k = m.v]) : dict[keyRasMap]valRasMap{}) +} + +ghost +requires m.Inv() +decreases m.Inv() +pure func (m rasMap) KeySet() set[keyRasMap] { + return domain(m.ToDict()) +} + +ghost +requires m.Inv() +requires k elem domain(m.ToDict()) +decreases m.Inv() +pure func (m rasMap) Get(k keyRasMap) valRasMap { + return let d := m.ToDict() in valRasMap(d[k]) +} + +pred (m rasMap) Witness(k keyRasMap, v valRasMap) { + acc(&m.inUse, _) && acc(&m.next, _) && acc(&m.k, _) && acc(&m.v, _) && + (!m.inUse ==> false) && + (m.k === k && m.v !== v ==> false) && + (m.k != k ==> rasMap(m.next).Witness(k, v)) +} + +ghost +requires m.Inv() +requires !(k elem domain(m.ToDict())) +ensures m.Inv() +ensures m.Witness(k, v) +ensures m.ToDict() === old(m.ToDict())[k = v] +decreases m.Inv() +func (m rasMap) Insert(k keyRasMap, v valRasMap) { + unfold m.Inv() + if !m.inUse { + next@ := nodeRasMap{} + assert acc(m) + m.inUse = true + m.p = 1/4 + m.next = &next + m.k = k + m.v = v + fold rasMap(m.next).Inv() + fold m.Inv() + assert m.ToDict() === unfolding m.Inv() in rasMap(m.next).ToDict()[m.k = m.v] + assert m.ToDict() === dict[keyRasMap]valRasMap{k : v} + fold m.Witness(k, v) + } else { + rasMap(m.next).Insert(k, v) + assert rasMap(m.next).Witness(k, v) + m.p = m.p/2 + fold m.Inv() + fold m.Witness(k, v) + } +} + +ghost +requires 0 < p +requires acc(m.Inv(), p) +requires m.Witness(k, v) +ensures acc(m.Inv(), p) +ensures m.Witness(k, v) +ensures k elem domain(m.ToDict()) +ensures m.ToDict()[k] === v +decreases acc(m.Inv(), p) +func (m rasMap) WitnessInMap(k keyRasMap, v valRasMap, p perm) { + d := m.ToDict() + unfold acc(m.Inv(), p) + unfold m.Witness(k, v) + if m.k == k { + assert k elem domain(d) + } else { + rasMap(m.next).WitnessInMap(k, v, p) + } + fold acc(m.Inv(), p) + fold m.Witness(k, v) +} + +ghost +requires m.Witness(k, v) +ensures m.Witness(k, v) && m.Witness(k, v) +decreases m.Witness(k, v) +func (m rasMap) DupWitness(k keyRasMap, v valRasMap) { + unfold m.Witness(k, v) + if m.k != k { + rasMap(m.next).DupWitness(k, v) + } + fold m.Witness(k, v) + fold m.Witness(k, v) +} \ No newline at end of file From a41cb2024c84c379f18800deedb4b309857d021f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= Date: Tue, 20 Jan 2026 23:42:38 +0100 Subject: [PATCH 13/28] drop duplicated code --- resalgebraNoAxioms/auth.gobra | 154 -------------------------- resalgebraNoAxioms/auth_test.gobra | 80 ------------- resalgebraNoAxioms/oneshot.gobra | 136 ----------------------- resalgebraNoAxioms/oneshot_test.gobra | 102 ----------------- 4 files changed, 472 deletions(-) delete mode 100644 resalgebraNoAxioms/auth.gobra delete mode 100644 resalgebraNoAxioms/auth_test.gobra delete mode 100644 resalgebraNoAxioms/oneshot.gobra delete mode 100644 resalgebraNoAxioms/oneshot_test.gobra diff --git a/resalgebraNoAxioms/auth.gobra b/resalgebraNoAxioms/auth.gobra deleted file mode 100644 index 2b344c9..0000000 --- a/resalgebraNoAxioms/auth.gobra +++ /dev/null @@ -1,154 +0,0 @@ -// 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 resalgebraNoAxioms - -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/resalgebraNoAxioms/auth_test.gobra b/resalgebraNoAxioms/auth_test.gobra deleted file mode 100644 index e9771c5..0000000 --- a/resalgebraNoAxioms/auth_test.gobra +++ /dev/null @@ -1,80 +0,0 @@ -// 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 resalgebraNoAxioms - -/* -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/resalgebraNoAxioms/oneshot.gobra b/resalgebraNoAxioms/oneshot.gobra deleted file mode 100644 index 12bda1a..0000000 --- a/resalgebraNoAxioms/oneshot.gobra +++ /dev/null @@ -1,136 +0,0 @@ -// 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 resalgebraNoAxioms - -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/resalgebraNoAxioms/oneshot_test.gobra b/resalgebraNoAxioms/oneshot_test.gobra deleted file mode 100644 index cd34d8c..0000000 --- a/resalgebraNoAxioms/oneshot_test.gobra +++ /dev/null @@ -1,102 +0,0 @@ -// 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 resalgebraNoAxioms - -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() -} From 2a7ff7f24d90620b4be501aa7a567597f1f21b8a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= Date: Wed, 21 Jan 2026 00:54:25 +0100 Subject: [PATCH 14/28] drop assumptions --- resalgebraNoAxioms/cooliomapio.gobra | 1 + resalgebraNoAxioms/loc.gobra | 32 +++---- resalgebraNoAxioms/oneshot.gobra | 136 +++++++++++++++++++++++++++ resalgebraNoAxioms/ras-map.gobra | 1 + 4 files changed, 151 insertions(+), 19 deletions(-) create mode 100644 resalgebraNoAxioms/oneshot.gobra diff --git a/resalgebraNoAxioms/cooliomapio.gobra b/resalgebraNoAxioms/cooliomapio.gobra index 1444304..becca86 100644 --- a/resalgebraNoAxioms/cooliomapio.gobra +++ b/resalgebraNoAxioms/cooliomapio.gobra @@ -48,6 +48,7 @@ pred inv(m cooliomapio) { ghost mayInit ensures inv(m) +ensures toDict(m) == dict[key]val{} decreases func allocMap() (m cooliomapio) { var g@ node diff --git a/resalgebraNoAxioms/loc.gobra b/resalgebraNoAxioms/loc.gobra index 3c00a8d..4f0739f 100644 --- a/resalgebraNoAxioms/loc.gobra +++ b/resalgebraNoAxioms/loc.gobra @@ -22,7 +22,6 @@ package resalgebraNoAxioms // - use Monoset and monomap, copy to this package if need be; delete cooliosetio and mapio // - use a cooliomapio for ras // - add triggers to invariants -// - implement invs and atomic regions in Gobra // At the moment, all of these definitions are trusted, and this, // prone to mistakes. If possible, we should find a model for the @@ -143,8 +142,10 @@ pred GlobalMem() { ras.Inv() && // necessary for proving key freshness (forall k LocName :: k elem domain(toDict(model)) ==> acc(k, 1/2)) && - (forall k LocName :: k elem domain(toDict(model)) ==> k elem domain(ras.ToDict())) && - (forall k LocName :: k elem domain(ras.ToDict()) ==> ras.ToDict()[k] != RA(nil)) && + (forall k LocName :: { k elem domain(toDict(model)) } { ras.ToDict()[k] } k elem domain(toDict(model)) ==> + k elem domain(ras.ToDict())) && + (forall k LocName :: { k elem domain(ras.ToDict()) }{ ras.ToDict()[k] } k elem domain(ras.ToDict()) ==> + ras.ToDict()[k] != RA(nil)) && // injectivity (forall k1, k2 LocName :: k1 elem domain(toDict(model)) && k2 elem domain(toDict(model)) && k1 != k2 ==> toDict(model)[k1] != toDict(model)[k2]) && @@ -169,7 +170,6 @@ ghost var model cooliomapio = allocMap() ghost var ras rasMap = rasMapAlloc() func init() { - assume false // todo fold GlobalMem() } @@ -221,10 +221,6 @@ func AllocWI(ra RA, e Elem) (l LocName, w Witness) { rasDict := ras.ToDict() assume !(newl elem domain(rasDict)) ras.Insert(newl, ra) - // exhale acc(ras) - // inhale acc(ras) - // assume ras.ToDict()[newl] === ra - // ras[newl] = ra // type system limitation, solved when swapping ras to a monotonic set fold GhostLocationW(newl, ra, e, newi) assert acc(newl, 1/2) @@ -232,7 +228,7 @@ func AllocWI(ra RA, e Elem) (l LocName, w Witness) { assume forall k LocName :: k elem domain(toDict(model)) ==> acc(k, 1/2) // TODO: fixed when we have a monotonic set and with permissions for showing injectivity assume forall k LocName :: k elem domain(toDict(model)) ==> k elem domain(ras.ToDict()) - assume forall k LocName :: k elem domain(ras.ToDict()) ==> ras.ToDict()[k] != RA(nil) + assume forall k LocName :: k elem domain(ras.ToDict()) ==> ras.ToDict()[k] != RA(nil) assume forall k1, k2 LocName :: k1 elem domain(toDict(model)) && k2 elem domain(toDict(model)) && k1 != k2 ==> (forall i idx :: i elem toCoolSet(toDict(model)[k1]) ==> !(i elem toCoolSet(toDict(model)[k2]))) // problem with triggers? @@ -241,7 +237,6 @@ func AllocWI(ra RA, e Elem) (l LocName, w Witness) { assume forall k LocName :: k elem domain(toDict(model)) ==> (forall i idx :: i elem toCoolSet(toDict(model)[k]) ==> i.inUse ==> (ras.ToDict()[k].IsElem(i.val) && ras.ToDict()[k].IsValid(i.val))) - assume false fold GlobalMem() return newl, newi @@ -259,18 +254,16 @@ decreases func GhostOp1WI(l LocName, ra RA, e1 Elem, e2 Elem, w Witness) (w1 Witness, w2 Witness) { i := w unfold GlobalMem() - unfold GhostLocationW(l, ra, ra.Compose(e1, e2), i) - // todo: when we use monotonic maps - assume l elem domain(ras.ToDict()) && ras.ToDict()[l] === ra + ras.DupWitness(l, ra) + ras.WitnessInMap(l, ra, 1/10) assert witness(model, l, i.c) lemmaWitness(model, l, i.c, 1/3) assert toDict(model)[l] === i.c assert i.c.witness(i.i) i.c.lemmaWitness(i.i, 1/3) assert i.i elem toCoolSet(i.c) - //assert i.i.inUse && i.i.val === a.Compose(e1, e2) ra.ValidOp(e1, e2) assert ra.IsValid(e1) ra.ComposeComm(e1, e2) @@ -283,13 +276,13 @@ func GhostOp1WI(l LocName, ra RA, e1 Elem, e2 Elem, w Witness) (w1 Witness, w2 W i.c.add(iii1) i1 := Witness{iii1, i.c} ras.DupWitness(l, ra) - fold GhostLocationW(l, ra, e1, i1) + fold GhostLocationW(l, ra, e1, i1) iii2 := &meta{true, e2} i.c.add(iii2) assert witness(model, l, i.c) i2 := Witness{iii2, i.c} - fold GhostLocationW(l, ra, e2, i2) + fold GhostLocationW(l, ra, e2, i2) assume forall k1, k2 LocName :: k1 elem domain(toDict(model)) && k2 elem domain(toDict(model)) && k1 != k2 ==> (forall i idx :: i elem toCoolSet(toDict(model)[k1]) ==> !(i elem toCoolSet(toDict(model)[k2]))) @@ -301,7 +294,7 @@ func GhostOp1WI(l LocName, ra RA, e1 Elem, e2 Elem, w Witness) (w1 Witness, w2 W i.inUse ==> ( forall i2 idx :: i2 elem toCoolSet(toDict(model)[k]) && i2.inUse && i2 !== i ==> ras.ToDict()[k].IsElem( ras.ToDict()[k].Compose(i.val, i2.val)) && - ras.ToDict()[k].IsValid(ras.ToDict()[k].Compose(i.val, i2.val)))) + ras.ToDict()[k].IsValid(ras.ToDict()[k].Compose(i.val, i2.val)))) fold GlobalMem() return i1, i2 @@ -399,8 +392,9 @@ func GhostUpdateWI(l LocName, ra RA, e1 Elem, e2 Elem, w Witness) { // // assume ra.IsValid(e2) // } - // TODO: drop when ras is a monotonic set - assume ras.ToDict()[l] === ra + ras.DupWitness(l, ra) + ras.WitnessInMap(l, ra, 1/10) + // TODO: should be provable from the def of IsFramePreservingUpdate assume forall k LocName :: k elem domain(toDict(model)) ==> (forall i idx :: i elem toCoolSet(toDict(model)[k]) ==> diff --git a/resalgebraNoAxioms/oneshot.gobra b/resalgebraNoAxioms/oneshot.gobra new file mode 100644 index 0000000..12bda1a --- /dev/null +++ b/resalgebraNoAxioms/oneshot.gobra @@ -0,0 +1,136 @@ +// 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 resalgebraNoAxioms + +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/resalgebraNoAxioms/ras-map.gobra b/resalgebraNoAxioms/ras-map.gobra index 623adbd..d57a360 100644 --- a/resalgebraNoAxioms/ras-map.gobra +++ b/resalgebraNoAxioms/ras-map.gobra @@ -46,6 +46,7 @@ pred (m rasMap) Inv() { ghost mayInit ensures m.Inv() +ensures m.ToDict() == dict[keyRasMap]valRasMap{} decreases func rasMapAlloc() (m rasMap) { var g@ nodeRasMap From c9472c8c27147c475b1b1a37f9a19f02790b0d0e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= Date: Wed, 21 Jan 2026 01:33:43 +0100 Subject: [PATCH 15/28] clean-up, verify some assumptions --- resalgebraNoAxioms/auth.gobra | 133 +++++++++++++++++++++++++++++++ resalgebraNoAxioms/loc.gobra | 33 ++++---- resalgebraNoAxioms/oneshot.gobra | 41 +++------- resalgebraNoAxioms/ra.gobra | 124 +++++++++++++++++++--------- 4 files changed, 244 insertions(+), 87 deletions(-) create mode 100644 resalgebraNoAxioms/auth.gobra diff --git a/resalgebraNoAxioms/auth.gobra b/resalgebraNoAxioms/auth.gobra new file mode 100644 index 0000000..601885b --- /dev/null +++ b/resalgebraNoAxioms/auth.gobra @@ -0,0 +1,133 @@ +// 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 resalgebraNoAxioms + +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 +} + +// all lemmas proven automatically + +ghost +decreases +func (ra TypeAuthRA) ComposeAssocQ() { + // proved +} + +ghost +decreases +func (ra TypeAuthRA) ComposeCommQ() { + // proved +} + +ghost +decreases +func (ra TypeAuthRA) CoreIdQ() { + // proved +} + +ghost +decreases +func (ra TypeAuthRA) CoreIdemQ() { + // proved +} + +ghost +decreases +func (ra TypeAuthRA) CoreMonoQ() { + // proved +} + +ghost +decreases +func (ra TypeAuthRA) ValidOpQ() { + // proved +} \ No newline at end of file diff --git a/resalgebraNoAxioms/loc.gobra b/resalgebraNoAxioms/loc.gobra index 4f0739f..0719bd4 100644 --- a/resalgebraNoAxioms/loc.gobra +++ b/resalgebraNoAxioms/loc.gobra @@ -18,9 +18,7 @@ pkgInvariant GlobalMem() // todo: replace this by a dup invariant that GlobalMem package resalgebraNoAxioms // TODO: -// - change to quantified lemmas, make the old lemmas available as a function defined outside the RA -// - use Monoset and monomap, copy to this package if need be; delete cooliosetio and mapio -// - use a cooliomapio for ras +// - use Monoset and monomap for the model, copy to this package if need be; delete cooliosetio and mapio // - add triggers to invariants // At the moment, all of these definitions are trusted, and this, @@ -224,17 +222,16 @@ func AllocWI(ra RA, e Elem) (l LocName, w Witness) { fold GhostLocationW(newl, ra, e, newi) assert acc(newl, 1/2) - // TODO: prolly missing triggers - assume forall k LocName :: k elem domain(toDict(model)) ==> acc(k, 1/2) - // TODO: fixed when we have a monotonic set and with permissions for showing injectivity - assume forall k LocName :: k elem domain(toDict(model)) ==> k elem domain(ras.ToDict()) - assume forall k LocName :: k elem domain(ras.ToDict()) ==> ras.ToDict()[k] != RA(nil) + assert forall k LocName :: k elem domain(toDict(model)) ==> acc(k, 1/2) + assert forall k LocName :: k elem domain(toDict(model)) ==> k elem domain(ras.ToDict()) + assert forall k LocName :: k elem domain(ras.ToDict()) ==> ras.ToDict()[k] != RA(nil) + + // problem with triggers? assume forall k1, k2 LocName :: k1 elem domain(toDict(model)) && k2 elem domain(toDict(model)) && k1 != k2 ==> (forall i idx :: i elem toCoolSet(toDict(model)[k1]) ==> !(i elem toCoolSet(toDict(model)[k2]))) - // problem with triggers? assume forall k LocName :: k elem domain(toDict(model)) ==> (forall i idx :: i elem toCoolSet(toDict(model)[k]) ==> acc(i, 1/2)) - assume forall k LocName :: k elem domain(toDict(model)) ==> + assert forall k LocName :: k elem domain(toDict(model)) ==> (forall i idx :: i elem toCoolSet(toDict(model)[k]) ==> i.inUse ==> (ras.ToDict()[k].IsElem(i.val) && ras.ToDict()[k].IsValid(i.val))) fold GlobalMem() @@ -264,10 +261,10 @@ func GhostOp1WI(l LocName, ra RA, e1 Elem, e2 Elem, w Witness) (w1 Witness, w2 W assert i.c.witness(i.i) i.c.lemmaWitness(i.i, 1/3) assert i.i elem toCoolSet(i.c) - ra.ValidOp(e1, e2) + ValidOp(ra, e1, e2) assert ra.IsValid(e1) - ra.ComposeComm(e1, e2) - ra.ValidOp(e2, e1) + ComposeComm(ra, e1, e2) + ValidOp(ra, e2, e1) assert ra.IsValid(e2) i.i.inUse = false @@ -290,11 +287,11 @@ func GhostOp1WI(l LocName, ra RA, e1 Elem, e2 Elem, w Witness) (w1 Witness, w2 W // not hard to prove, requires applying commutativity and associativity to get (i1 x i2) x k == (i1 x k) x i2. Because the lhs is valid, the rhs is also valid, and by ValidOp, i1 x k is also valid // TODO: requires changing the API of RAs so that all lemmas are universally quantified assume forall k LocName :: k elem domain(toDict(model)) ==> - (forall i idx :: i elem toCoolSet(toDict(model)[k]) ==> - i.inUse ==> ( - forall i2 idx :: i2 elem toCoolSet(toDict(model)[k]) && i2.inUse && i2 !== i ==> - ras.ToDict()[k].IsElem( ras.ToDict()[k].Compose(i.val, i2.val)) && - ras.ToDict()[k].IsValid(ras.ToDict()[k].Compose(i.val, i2.val)))) + (forall i idx :: i elem toCoolSet(toDict(model)[k]) ==> + i.inUse ==> ( + forall i2 idx :: i2 elem toCoolSet(toDict(model)[k]) && i2.inUse && i2 !== i ==> + ras.ToDict()[k].IsElem( ras.ToDict()[k].Compose(i.val, i2.val)) && + ras.ToDict()[k].IsValid(ras.ToDict()[k].Compose(i.val, i2.val)))) fold GlobalMem() return i1, i2 diff --git a/resalgebraNoAxioms/oneshot.gobra b/resalgebraNoAxioms/oneshot.gobra index 12bda1a..b49c396 100644 --- a/resalgebraNoAxioms/oneshot.gobra +++ b/resalgebraNoAxioms/oneshot.gobra @@ -74,63 +74,40 @@ func (ra TypeOneShotRA) Compose(e1 Elem, e2 Elem) (res Elem) { Elem(Fail{}) } +// all of the following properties are proven automatically + 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) { +func (ra TypeOneShotRA) ComposeAssocQ() { // 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) { +func (ra TypeOneShotRA) ComposeCommQ() { // 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) { +func (ra TypeOneShotRA) CoreIdQ() { // 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) { +func (ra TypeOneShotRA) CoreIdemQ() { // 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) { +func (ra TypeOneShotRA) CoreMonoQ() { // 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) { +func (ra TypeOneShotRA) ValidOpQ() { // proved -} - - - +} \ No newline at end of file diff --git a/resalgebraNoAxioms/ra.gobra b/resalgebraNoAxioms/ra.gobra index 7382c7c..cd30460 100644 --- a/resalgebraNoAxioms/ra.gobra +++ b/resalgebraNoAxioms/ra.gobra @@ -41,63 +41,113 @@ type RA interface { decreases pure Compose(e1 Elem, e2 Elem) (res Elem) - // ghost - // ensures IsElem(res) && IsValid(res) - // decreases - // pure Unit() (res Elem) - // Lemmas ghost - requires IsElem(e1) && IsElem(e2) && IsElem(e3) - ensures Compose(Compose(e1, e2), e3) === Compose(e1, Compose(e2, e3)) + ensures forall e1, e2, e3 Elem :: { Compose(Compose(e1, e2), e3) } { Compose(e1, Compose(e2, e3)) } IsElem(e1) && + IsElem(e2) && IsElem(e3) ==> + Compose(Compose(e1, e2), e3) === Compose(e1, Compose(e2, e3)) decreases - ComposeAssoc(e1 Elem, e2 Elem, e3 Elem) + ComposeAssocQ() ghost - requires IsElem(e1) && IsElem(e2) - ensures Compose(e1, e2) === Compose(e2, e1) + ensures forall e1, e2 Elem :: { Compose(e1, e2) } { Compose(e2, e1) } IsElem(e1) && IsElem(e2) ==> + Compose(e1, e2) === Compose(e2, e1) decreases - ComposeComm(e1 Elem, e2 Elem) + ComposeCommQ() ghost - requires IsElem(e) - ensures let c := Core(e) in - c !== none[Elem] ==> Compose(get(c), e) === e + ensures forall e Elem :: { Core(e) } IsElem(e) ==> + let c := Core(e) in + c !== none[Elem] ==> Compose(get(c), e) === e decreases - CoreId(e Elem) + CoreIdQ() ghost - requires IsElem(e) - requires Core(e) !== none[Elem] - ensures let c := Core(e) in + ensures forall e Elem :: { Core(e) } IsElem(e) && Core(e) !== none[Elem] ==> + let c := Core(e) in let cc := Core(get(c)) in cc !== none[Elem] && get(cc) === get(c) decreases - CoreIdem(e Elem) + CoreIdemQ() 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) + ensures forall e1, e2 Elem :: { Core(e1), Core(e2) } IsElem(e1) && IsElem(e2) && Core(e1) !== none[Elem] && + // fully expanded version of <= due to Gobra's lack of `Self` in interface specs + (exists e3 Elem :: { IsElem(e3) } IsElem(e3) && e2 === Compose(e1, e3)) ==> + Core(e2) !== none[Elem] && + exists e4 Elem :: { IsElem(e4) } IsElem(e4) && get(Core(e2)) === Compose(get(Core(e1)), e4) decreases - CoreMono(e1 Elem, e2 Elem) + CoreMonoQ() ghost - requires IsElem(e1) && IsElem(e2) - requires IsValid(Compose(e1, e2)) - ensures IsValid(e1) + ensures forall e1, e2 Elem :: { Compose(e1, e2) } IsElem(e1) && IsElem(e2) && IsValid(Compose(e1, e2)) ==> + IsValid(e1) decreases - ValidOp(e1 Elem, e2 Elem) - - // ghost - // requires IsElem(e) - // requires Compose(e, Unit()) === e - // requires Compose(Unit(), e) === e - // decreases - // ComposeUnit(e Elem) + ValidOpQ() +} + +ghost +requires ra != nil +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 ComposeAssoc(ra RA, e1 Elem, e2 Elem, e3 Elem) { + ra.ComposeAssocQ() +} + +ghost +requires ra != nil +requires ra.IsElem(e1) && ra.IsElem(e2) +ensures ra.Compose(e1, e2) === ra.Compose(e2, e1) +decreases +func ComposeComm(ra RA, e1 Elem, e2 Elem) { + ra.ComposeCommQ() +} + +ghost +requires ra != nil +requires ra.IsElem(e) +ensures let c := ra.Core(e) in + c !== none[Elem] ==> ra.Compose(get(c), e) === e +decreases +func CoreId(ra RA, e Elem) { + ra.CoreIdQ() +} + +ghost +requires ra != nil +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 CoreIdem(ra RA, e Elem) { + ra.CoreIdemQ() +} + +ghost +requires ra != nil +requires ra.IsElem(e1) && ra.IsElem(e2) +requires ra.Core(e1) !== none[Elem] +// fully expanded version of <= due to Gobra's lack of `Self` in interface specs +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 CoreMono(ra RA, e1 Elem, e2 Elem) { + ra.CoreMonoQ() +} + +ghost +requires ra != nil +requires ra.IsElem(e1) && ra.IsElem(e2) +requires ra.IsValid(ra.Compose(e1, e2)) +ensures ra.IsValid(e1) +decreases +func ValidOp(ra RA, e1 Elem, e2 Elem) { + ra.ValidOpQ() } \ No newline at end of file From 3ad5e997682500163249628b44bd6c29b3b420d1 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= Date: Wed, 21 Jan 2026 01:56:46 +0100 Subject: [PATCH 16/28] another assumption proven --- resalgebraNoAxioms/loc.gobra | 21 ++++++++++++++------- 1 file changed, 14 insertions(+), 7 deletions(-) diff --git a/resalgebraNoAxioms/loc.gobra b/resalgebraNoAxioms/loc.gobra index 0719bd4..e47581e 100644 --- a/resalgebraNoAxioms/loc.gobra +++ b/resalgebraNoAxioms/loc.gobra @@ -134,14 +134,16 @@ pure func LiftedIsValid(ra RA, e option[Elem]) bool { /***** Model: Global State *****/ -// TODO: IsInv(GlobalMem()) should be established by init pred GlobalMem() { inv(model) && ras.Inv() && // necessary for proving key freshness - (forall k LocName :: k elem domain(toDict(model)) ==> acc(k, 1/2)) && + (forall k LocName :: { k elem domain(toDict(model)) } k elem domain(toDict(model)) ==> acc(k, 1/2)) && + // complicated way of saying that the domains of model and ras are the same: (forall k LocName :: { k elem domain(toDict(model)) } { ras.ToDict()[k] } k elem domain(toDict(model)) ==> k elem domain(ras.ToDict())) && + (forall k LocName :: { k elem domain(toDict(model)) } k elem domain(ras.ToDict()) ==> + k elem domain(toDict(model))) && (forall k LocName :: { k elem domain(ras.ToDict()) }{ ras.ToDict()[k] } k elem domain(ras.ToDict()) ==> ras.ToDict()[k] != RA(nil)) && // injectivity @@ -153,10 +155,10 @@ pred GlobalMem() { (forall i idx :: i elem toCoolSet(toDict(model)[k1]) ==> !(i elem toCoolSet(toDict(model)[k2])))) && (forall k LocName :: k elem domain(toDict(model)) ==> (forall i idx :: i elem toCoolSet(toDict(model)[k]) ==> acc(i, 1/2))) && - (forall k LocName :: k elem domain(toDict(model)) ==> + (forall k LocName :: { k elem domain(toDict(model)) }{ toDict(model)[k] } k elem domain(toDict(model)) ==> (forall i idx :: i elem toCoolSet(toDict(model)[k]) ==> i.inUse ==> (ras.ToDict()[k].IsElem(i.val) && ras.ToDict()[k].IsValid(i.val)))) && - (forall k LocName :: k elem domain(toDict(model)) ==> + (forall k LocName :: { k elem domain(toDict(model)) } { toDict(model)[k] } k elem domain(toDict(model)) ==> (forall i idx :: i elem toCoolSet(toDict(model)[k]) ==> i.inUse ==> ( forall i2 idx :: i2 elem toCoolSet(toDict(model)[k]) && i2.inUse && i2 !== i ==> @@ -213,12 +215,17 @@ func AllocWI(ra RA, e Elem) (l LocName, w Witness) { var cs cooliosetio = allocSet() iii := &meta{true, e} cs.add(iii) + if (newl elem domain(toDict(model))) { + assert acc(newl, 3/2) + } + assert !(newl elem domain(toDict(model))) + rasDict := ras.ToDict() + assert !(newl elem domain(rasDict)) + ras.Insert(newl, ra) add(model, newl, cs) assert witness(model, newl, cs) newi := Witness{iii, cs} - rasDict := ras.ToDict() - assume !(newl elem domain(rasDict)) - ras.Insert(newl, ra) + fold GhostLocationW(newl, ra, e, newi) assert acc(newl, 1/2) From 545d5826b0086683ca9e754cfa6084e1c3f04f5d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= Date: Wed, 21 Jan 2026 14:21:56 +0100 Subject: [PATCH 17/28] anoda one --- resalgebraNoAxioms/loc.gobra | 37 ++++++++++++++++-------------------- 1 file changed, 16 insertions(+), 21 deletions(-) diff --git a/resalgebraNoAxioms/loc.gobra b/resalgebraNoAxioms/loc.gobra index e47581e..02282e3 100644 --- a/resalgebraNoAxioms/loc.gobra +++ b/resalgebraNoAxioms/loc.gobra @@ -371,31 +371,27 @@ func GhostUpdateWI(l LocName, ra RA, e1 Elem, e2 Elem, w Witness) { i.c.lemmaWitness(i.i, 1/3) i.i.val = e2 - // TODO: can be proven easily as long as I can introduce an existentially quantified variable if forall e Elem :: ra.IsElem(e) ==> LiftedCompose(ra, some(e1), some(e)) === none[Elem] { assert ra.IsValid(e2) + } else if forall e Elem :: { ra.Compose(e1, e) } ra.IsElem(e) ==> !ra.IsValid(ra.Compose(e1, e)) { + assert IsFramePreservingUpdate(ra, e1, e2) + assert 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))) + assert 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)) ==> c === none[Elem]) + assert LiftedIsValid(ra, LiftedCompose(ra, some(e2), none[Elem])) + assert ra.IsValid(e2) } else { - // idea: if e1 has a core, than e2 must be valid: e1 has core ==> - // ==> compose(e2, core(e1)) must be valid because compose(e1, core(e1)) is valid and e2 is a frame preserving update - // ==> e2 is valid because the compose(e2, core(e1)) is valid. - // what about the cases e1 does not have a core? - assume ra.IsValid(e2) // TODO + assert exists e Elem :: { ra.IsElem(e) } { LiftedCompose(ra, some(e1), some(e)) } ra.IsElem(e) && + LiftedCompose(ra, some(e1), some(e)) !== none[Elem] + ra.ValidOpQ() + assert exists e Elem :: { ra.IsElem(e) } { LiftedCompose(ra, some(e1), some(e)) } ra.IsElem(e) && + LiftedIsValid(ra, LiftedCompose(ra, some(e1), some(e))) && + ra.IsValid(ra.Compose(e1, e)) && + ra.IsValid(ra.Compose(e2, e)) && + ra.IsValid(e2) } - // if ra.Core(e1) != none[Elem] { - // ra.CoreId(e1) - // assert ra.Compose(get(ra.Core(e1)), e1) === e1 - // ra.ComposeComm(get(ra.Core(e1)), e1) - // assert ra.Compose(e1, get(ra.Core(e1))) === e1 - // assert LiftedIsValid(ra, some(e1)) - // assert LiftedIsValid(ra, some(ra.Compose(e1, get(ra.Core(e1))))) - // IsFramePreservingUpdate(ra, e1, e2) - // assume false // TODO - // assert LiftedIsValid(ra, some(ra.Compose(e2, get(ra.Core(e1))))) // from def of frame-preserving update - // } else { - // // assume ra.IsValid(e2) - // } - ras.DupWitness(l, ra) ras.WitnessInMap(l, ra, 1/10) @@ -408,7 +404,6 @@ func GhostUpdateWI(l LocName, ra RA, e1 Elem, e2 Elem, w Witness) { ras.ToDict()[k].IsValid(ras.ToDict()[k].Compose(i.val, i2.val)))) fold GhostLocationW(l, ra, e2, i) - fold GlobalMem() } From 35a7232d3595e5bcf991e54f6df3affa51b7df0d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= Date: Wed, 21 Jan 2026 14:42:00 +0100 Subject: [PATCH 18/28] prove another assumption --- resalgebraNoAxioms/loc.gobra | 28 +++++++++++++++++++++------- 1 file changed, 21 insertions(+), 7 deletions(-) diff --git a/resalgebraNoAxioms/loc.gobra b/resalgebraNoAxioms/loc.gobra index 02282e3..92e4a13 100644 --- a/resalgebraNoAxioms/loc.gobra +++ b/resalgebraNoAxioms/loc.gobra @@ -158,10 +158,10 @@ pred GlobalMem() { (forall k LocName :: { k elem domain(toDict(model)) }{ toDict(model)[k] } k elem domain(toDict(model)) ==> (forall i idx :: i elem toCoolSet(toDict(model)[k]) ==> i.inUse ==> (ras.ToDict()[k].IsElem(i.val) && ras.ToDict()[k].IsValid(i.val)))) && - (forall k LocName :: { k elem domain(toDict(model)) } { toDict(model)[k] } k elem domain(toDict(model)) ==> - (forall i idx :: i elem toCoolSet(toDict(model)[k]) ==> + (forall k LocName :: { k elem domain(toDict(model)) } { toDict(model)[k] }{ ras.ToDict()[k] } k elem domain(toDict(model)) ==> + (forall i idx :: { i elem toCoolSet(toDict(model)[k]) } { i.inUse } i elem toCoolSet(toDict(model)[k]) ==> i.inUse ==> ( - forall i2 idx :: i2 elem toCoolSet(toDict(model)[k]) && i2.inUse && i2 !== i ==> + forall i2 idx :: { ras.ToDict()[k].Compose(i.val, i2.val) } i2 elem toCoolSet(toDict(model)[k]) && i2.inUse && i2 !== i ==> ras.ToDict()[k].IsElem(ras.ToDict()[k].Compose(i.val, i2.val)) && ras.ToDict()[k].IsValid(ras.ToDict()[k].Compose(i.val, i2.val))))) } @@ -189,6 +189,7 @@ ghost type meta ghost struct { pred GhostLocationW(l LocName, ra RA, e Elem, w Witness) { acc(w.i, 1/2) && + w.i.inUse && witness(model, l, w.c) && w.c.witness(w.i) && ra != nil && @@ -322,16 +323,29 @@ func GhostOp2WI(l LocName, ra RA, e1 Elem, e2 Elem, w1 Witness, w2 Witness) { unfold GhostLocationW(l, ra, e1, i1) unfold GhostLocationW(l, ra, e2, i2) lemmaWitness(model, l, i2.c, 1/3) + assert forall i idx :: { i elem toCoolSet(toDict(model)[l]) } { i.inUse } i elem toCoolSet(toDict(model)[l]) ==> + i.inUse ==> ( + forall i2 idx :: { ras.ToDict()[l].Compose(i.val, i2.val) } i2 elem toCoolSet(toDict(model)[l]) && i2.inUse && i2 !== i ==> + ras.ToDict()[l].IsElem(ras.ToDict()[l].Compose(i.val, i2.val)) && + ras.ToDict()[l].IsValid(ras.ToDict()[l].Compose(i.val, i2.val))) assert i2.c === toDict(model)[l] i2.c.lemmaWitness(i2.i, 1/3) assert i2.i elem toCoolSet(i2.c) - i2.i.inUse = false - lemmaWitness(model, l, i1.c, 1/3) i1.c.lemmaWitness(i1.i, 1/3) + + ras.DupWitness(l, ra) + ras.WitnessInMap(l, ra, 1/10) + assert ra === ras.ToDict()[l] + + assert i1.i elem toCoolSet(toDict(model)[l]) && i1.i.inUse + assert i2.i elem toCoolSet(toDict(model)[l]) && i2.i.inUse + assert ra.IsElem(ra.Compose(i1.i.val, i2.i.val)) + assert ra.IsValid(ra.Compose(i1.i.val, i2.i.val)) + + assert ra.IsElem(ra.Compose(e1, e2)) && ra.IsValid(ra.Compose(e1, e2)) i1.i.val = ra.Compose(e1, e2) - // triggering issue ? - assume ra.IsElem(ra.Compose(e1, e2)) && ra.IsValid(ra.Compose(e1, e2)) + i2.i.inUse = false fold GhostLocationW(l, ra, ra.Compose(e1, e2), i1) // triggering issue From 71a44b3454539ebe9b744cd4cdcb1b64431099bb Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= Date: Wed, 21 Jan 2026 14:44:43 +0100 Subject: [PATCH 19/28] prove another assumption --- resalgebraNoAxioms/loc.gobra | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/resalgebraNoAxioms/loc.gobra b/resalgebraNoAxioms/loc.gobra index 92e4a13..6c7d71c 100644 --- a/resalgebraNoAxioms/loc.gobra +++ b/resalgebraNoAxioms/loc.gobra @@ -348,10 +348,9 @@ func GhostOp2WI(l LocName, ra RA, e1 Elem, e2 Elem, w1 Witness, w2 Witness) { i2.i.inUse = false fold GhostLocationW(l, ra, ra.Compose(e1, e2), i1) - // triggering issue - assume forall k LocName :: k elem domain(toDict(model)) ==> - (forall i idx :: i elem toCoolSet(toDict(model)[k]) ==> - i.inUse ==> (ras.ToDict()[k].IsElem(i.val) && ras.ToDict()[k].IsValid(i.val))) + assert forall k LocName :: k elem domain(toDict(model)) ==> + (forall i idx :: i elem toCoolSet(toDict(model)[k]) ==> + i.inUse ==> (ras.ToDict()[k].IsElem(i.val) && ras.ToDict()[k].IsValid(i.val))) // proof requires that all previous elems can be added to this one and become valid. // actually, the proof should be very similar to that of GhostOp1W From aa13f671b04658fcc017669a8bfa507a35ae85a2 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= Date: Wed, 21 Jan 2026 14:58:27 +0100 Subject: [PATCH 20/28] prove two more assumptions --- resalgebraNoAxioms/cooliosetio.gobra | 1 + resalgebraNoAxioms/loc.gobra | 22 +++++++++++----------- 2 files changed, 12 insertions(+), 11 deletions(-) diff --git a/resalgebraNoAxioms/cooliosetio.gobra b/resalgebraNoAxioms/cooliosetio.gobra index d48eb3c..4270bb2 100644 --- a/resalgebraNoAxioms/cooliosetio.gobra +++ b/resalgebraNoAxioms/cooliosetio.gobra @@ -45,6 +45,7 @@ pred (m cooliosetio) Inv() { ghost ensures m.Inv() +ensures toCoolSet(m) == set[valSet]{} decreases func allocSet() (m cooliosetio) { var g@ nodeSet diff --git a/resalgebraNoAxioms/loc.gobra b/resalgebraNoAxioms/loc.gobra index 6c7d71c..48fd996 100644 --- a/resalgebraNoAxioms/loc.gobra +++ b/resalgebraNoAxioms/loc.gobra @@ -227,6 +227,11 @@ func AllocWI(ra RA, e Elem) (l LocName, w Witness) { assert witness(model, newl, cs) newi := Witness{iii, cs} + assert forall k LocName :: k elem domain(toDict(model)) && k != newl ==> + !(iii elem toCoolSet(toDict(model)[k])) + assert forall k1, k2 LocName :: k1 elem domain(toDict(model)) && k2 elem domain(toDict(model)) && k1 != k2 ==> + (forall i idx :: i elem toCoolSet(toDict(model)[k1]) ==> !(i elem toCoolSet(toDict(model)[k2]))) + fold GhostLocationW(newl, ra, e, newi) assert acc(newl, 1/2) @@ -234,10 +239,7 @@ func AllocWI(ra RA, e Elem) (l LocName, w Witness) { assert forall k LocName :: k elem domain(toDict(model)) ==> k elem domain(ras.ToDict()) assert forall k LocName :: k elem domain(ras.ToDict()) ==> ras.ToDict()[k] != RA(nil) - // problem with triggers? - assume forall k1, k2 LocName :: k1 elem domain(toDict(model)) && k2 elem domain(toDict(model)) && k1 != k2 ==> - (forall i idx :: i elem toCoolSet(toDict(model)[k1]) ==> !(i elem toCoolSet(toDict(model)[k2]))) - assume forall k LocName :: k elem domain(toDict(model)) ==> + assert forall k LocName :: k elem domain(toDict(model)) ==> (forall i idx :: i elem toCoolSet(toDict(model)[k]) ==> acc(i, 1/2)) assert forall k LocName :: k elem domain(toDict(model)) ==> (forall i idx :: i elem toCoolSet(toDict(model)[k]) ==> @@ -410,11 +412,11 @@ func GhostUpdateWI(l LocName, ra RA, e1 Elem, e2 Elem, w Witness) { // TODO: should be provable from the def of IsFramePreservingUpdate assume forall k LocName :: k elem domain(toDict(model)) ==> - (forall i idx :: i elem toCoolSet(toDict(model)[k]) ==> - i.inUse ==> ( - forall i2 idx :: i2 elem toCoolSet(toDict(model)[k]) && i2.inUse && i2 !== i ==> - ras.ToDict()[k].IsElem(ras.ToDict()[k].Compose(i.val, i2.val)) && - ras.ToDict()[k].IsValid(ras.ToDict()[k].Compose(i.val, i2.val)))) + (forall i idx :: i elem toCoolSet(toDict(model)[k]) ==> + i.inUse ==> ( + forall i2 idx :: i2 elem toCoolSet(toDict(model)[k]) && i2.inUse && i2 !== i ==> + ras.ToDict()[k].IsElem(ras.ToDict()[k].Compose(i.val, i2.val)) && + ras.ToDict()[k].IsValid(ras.ToDict()[k].Compose(i.val, i2.val)))) fold GhostLocationW(l, ra, e2, i) fold GlobalMem() @@ -435,8 +437,6 @@ func GhostValidW(l LocName, ra RA, e Elem, w Witness) { /***** Model: wrappers that acquire the global invariant; these functions may not be called from critical regions *****/ -// TODO: IsInv(GlobalMem()) should be a duplicable invariant - ghost // opensInvariants requires ra != nil From 4709ed059b8d751d4b511126ed8182b829b14f8b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= Date: Wed, 21 Jan 2026 15:04:27 +0100 Subject: [PATCH 21/28] prove one more assumption --- resalgebraNoAxioms/loc.gobra | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) diff --git a/resalgebraNoAxioms/loc.gobra b/resalgebraNoAxioms/loc.gobra index 48fd996..3791e88 100644 --- a/resalgebraNoAxioms/loc.gobra +++ b/resalgebraNoAxioms/loc.gobra @@ -283,15 +283,23 @@ func GhostOp1WI(l LocName, ra RA, e1 Elem, e2 Elem, w Witness) (w1 Witness, w2 W i.c.add(iii1) i1 := Witness{iii1, i.c} ras.DupWitness(l, ra) + assert forall k LocName :: k elem domain(toDict(model)) && k != l ==> + !(iii1 elem toCoolSet(toDict(model)[k])) + assert forall k1, k2 LocName :: k1 elem domain(toDict(model)) && k2 elem domain(toDict(model)) && k1 != k2 ==> + (forall i idx :: i elem toCoolSet(toDict(model)[k1]) ==> !(i elem toCoolSet(toDict(model)[k2]))) fold GhostLocationW(l, ra, e1, i1) iii2 := &meta{true, e2} i.c.add(iii2) assert witness(model, l, i.c) i2 := Witness{iii2, i.c} + assert forall k LocName :: k elem domain(toDict(model)) && k != l ==> + !(iii2 elem toCoolSet(toDict(model)[k])) + assert forall k1, k2 LocName :: k1 elem domain(toDict(model)) && k2 elem domain(toDict(model)) && k1 != k2 ==> + (forall i idx :: i elem toCoolSet(toDict(model)[k1]) ==> !(i elem toCoolSet(toDict(model)[k2]))) fold GhostLocationW(l, ra, e2, i2) - assume forall k1, k2 LocName :: k1 elem domain(toDict(model)) && k2 elem domain(toDict(model)) && k1 != k2 ==> + assert forall k1, k2 LocName :: k1 elem domain(toDict(model)) && k2 elem domain(toDict(model)) && k1 != k2 ==> (forall i idx :: i elem toCoolSet(toDict(model)[k1]) ==> !(i elem toCoolSet(toDict(model)[k2]))) // not hard to prove, requires applying commutativity and associativity to get (i1 x i2) x k == (i1 x k) x i2. Because the lhs is valid, the rhs is also valid, and by ValidOp, i1 x k is also valid From 0eb67835697d3d8bffecc623274fe415bd343922 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= Date: Wed, 21 Jan 2026 16:59:42 +0100 Subject: [PATCH 22/28] simplify proof obligation --- resalgebraNoAxioms/loc.gobra | 134 ++++++++++++++++++++++++++++++++--- 1 file changed, 124 insertions(+), 10 deletions(-) diff --git a/resalgebraNoAxioms/loc.gobra b/resalgebraNoAxioms/loc.gobra index 3791e88..fd5410a 100644 --- a/resalgebraNoAxioms/loc.gobra +++ b/resalgebraNoAxioms/loc.gobra @@ -14,7 +14,8 @@ // +gobra -pkgInvariant GlobalMem() // todo: replace this by a dup invariant that GlobalMem() is an invariant +// todo: replace this by a dup invariant that GlobalMem() is an invariant +pkgInvariant GlobalMem() package resalgebraNoAxioms // TODO: @@ -302,19 +303,134 @@ func GhostOp1WI(l LocName, ra RA, e1 Elem, e2 Elem, w Witness) (w1 Witness, w2 W assert forall k1, k2 LocName :: k1 elem domain(toDict(model)) && k2 elem domain(toDict(model)) && k1 != k2 ==> (forall i idx :: i elem toCoolSet(toDict(model)[k1]) ==> !(i elem toCoolSet(toDict(model)[k2]))) + assert ras.ToDict()[l] === ra + + // assume (forall i idx :: { ra.Compose(iii1.val, i.val) } i elem toCoolSet(toDict(model)[l]) ==> + // i != iii1 && i.inUse ==> ( + // ra.IsElem(ra.Compose(iii1.val, i.val)) && + // ra.IsValid(ra.Compose(iii1.val, i.val)))) + // assume (forall i idx :: { ra.Compose(iii2.val, i.val) } i elem toCoolSet(toDict(model)[l]) ==> + // i != iii2 && i.inUse ==> ( + // ra.IsElem(ra.Compose(iii2.val, i.val)) && + // ra.IsValid(ra.Compose(iii2.val, i.val)))) + // assume ra.IsElem(ra.Compose(iii2.val, iii1.val)) && + // ra.IsValid(ra.Compose(iii2.val, iii1.val)) + // assume ra.IsElem(ra.Compose(iii1.val, iii2.val)) && + // ra.IsValid(ra.Compose(iii1.val, iii2.val)) + +/* + assert forall k LocName :: k elem domain(toDict(model)) && k != l ==> + (forall i idx :: i elem toCoolSet(toDict(model)[k]) ==> + i.inUse ==> ( + forall i2 idx :: i2 elem toCoolSet(toDict(model)[k]) && i2.inUse && i2 !== i ==> + ras.ToDict()[k].IsElem(ras.ToDict()[k].Compose(i.val, i2.val)) && + ras.ToDict()[k].IsValid(ras.ToDict()[k].Compose(i.val, i2.val)))) + + assert forall i idx :: i elem toCoolSet(toDict(model)[l]) ==> + i.inUse && i != iii1 && i != iii2 ==> ( + forall i2 idx :: i2 elem toCoolSet(toDict(model)[l]) && i2.inUse && i2 !== i && i2 != iii1 && i2 != iii2 ==> + ras.ToDict()[l].IsElem(ras.ToDict()[l].Compose(i.val, i2.val)) && + ras.ToDict()[l].IsValid(ras.ToDict()[l].Compose(i.val, i2.val))) + + assert forall i idx :: i elem toCoolSet(toDict(model)[l]) ==> + i.inUse && i != iii1 && i != iii2 ==> ( + forall i2 idx :: i2 elem toCoolSet(toDict(model)[l]) && i2.inUse && i2 !== i && i2 != iii1 && i2 != iii2 ==> + ras.ToDict()[l].IsElem(ras.ToDict()[l].Compose(i.val, i2.val)) && + ras.ToDict()[l].IsValid(ras.ToDict()[l].Compose(i.val, i2.val))) +*/ + /* + assert forall i2 idx :: i2 elem toCoolSet(toDict(model)[l]) && i2.inUse && i2 != iii1 && i2 != iii2 ==> + ras.ToDict()[l].IsElem(ras.ToDict()[l].Compose(ras.ToDict()[l].Compose(iii1.val, iii2.val), i2.val)) && + ras.ToDict()[l].IsValid(ras.ToDict()[l].Compose(ras.ToDict()[l].Compose(iii1.val, iii2.val), i2.val)) + ra.ValidOpQ() + ra.ComposeAssocQ() + assert forall i2 idx :: i2 elem toCoolSet(toDict(model)[l]) && i2.inUse && i2 != iii1 && i2 != iii2 ==> + ras.ToDict()[l].IsElem(ras.ToDict()[l].Compose(iii1.val, ras.ToDict()[l].Compose(iii2.val, i2.val))) && + ras.ToDict()[l].IsValid(ras.ToDict()[l].Compose(iii1.val, ras.ToDict()[l].Compose(iii2.val, i2.val))) + ra.ComposeCommQ() + assert forall i2 idx :: i2 elem toCoolSet(toDict(model)[l]) && i2.inUse && i2 != iii1 && i2 != iii2 ==> + ras.ToDict()[l].IsElem(ras.ToDict()[l].Compose(iii1.val, ras.ToDict()[l].Compose(i2.val, iii2.val))) && + ras.ToDict()[l].IsValid(ras.ToDict()[l].Compose(iii1.val, ras.ToDict()[l].Compose(i2.val, iii2.val))) + assert forall i2 idx :: i2 elem toCoolSet(toDict(model)[l]) && i2.inUse && i2 != iii1 && i2 != iii2 ==> + ras.ToDict()[l].IsElem(ras.ToDict()[l].Compose(ras.ToDict()[l].Compose(iii1.val, i2.val), iii2.val)) && + ras.ToDict()[l].IsValid(ras.ToDict()[l].Compose(ras.ToDict()[l].Compose(iii1.val, i2.val), iii2.val)) + /// + assert false + assert forall i2 idx :: i2 elem toCoolSet(toDict(model)[l]) && i2.inUse && i2 != iii1 ==> + ras.ToDict()[l].IsElem(ras.ToDict()[l].Compose(iii1.val, i2.val)) && + ras.ToDict()[l].IsValid(ras.ToDict()[l].Compose(iii1.val, i2.val)) + + ///// + + assert forall i idx :: i elem toCoolSet(toDict(model)[l]) ==> + i.inUse && i != iii1 && i != iii2 ==> ( + forall i2 idx :: i2 elem toCoolSet(toDict(model)[l]) && i2.inUse && i2 !== i && i2 != iii1 && i2 != iii2 ==> + ras.ToDict()[l].IsElem(ras.ToDict()[l].Compose(i.val, i2.val)) && + ras.ToDict()[l].IsValid(ras.ToDict()[l].Compose(i.val, i2.val))) + + assert forall i idx :: i elem toCoolSet(toDict(model)[l]) ==> + i.inUse ==> ( + forall i2 idx :: i2 elem toCoolSet(toDict(model)[l]) && i2.inUse && i2 !== i ==> + ras.ToDict()[l].IsElem(ras.ToDict()[l].Compose(i.val, i2.val)) && + ras.ToDict()[l].IsValid(ras.ToDict()[l].Compose(i.val, i2.val))) + */ // not hard to prove, requires applying commutativity and associativity to get (i1 x i2) x k == (i1 x k) x i2. Because the lhs is valid, the rhs is also valid, and by ValidOp, i1 x k is also valid - // TODO: requires changing the API of RAs so that all lemmas are universally quantified - assume forall k LocName :: k elem domain(toDict(model)) ==> + + ghostOp1WIAux(ra, iii1.val, iii2.val) + + assert forall k LocName :: k elem domain(toDict(model)) ==> (forall i idx :: i elem toCoolSet(toDict(model)[k]) ==> i.inUse ==> ( forall i2 idx :: i2 elem toCoolSet(toDict(model)[k]) && i2.inUse && i2 !== i ==> - ras.ToDict()[k].IsElem( ras.ToDict()[k].Compose(i.val, i2.val)) && + ras.ToDict()[k].IsElem(ras.ToDict()[k].Compose(i.val, i2.val)) && ras.ToDict()[k].IsValid(ras.ToDict()[k].Compose(i.val, i2.val)))) fold GlobalMem() return i1, i2 } +ghost +requires ra != nil +requires ra.IsElem(e1) && ra.IsElem(e2) +requires ra.IsValid(ra.Compose(e1, e2)) +ensures forall e Elem :: { ra.Compose(e1, e) } ra.IsElem(e) && ra.IsValid(ra.Compose(ra.Compose(e1, e2), e)) ==> + ra.IsValid(ra.Compose(e1, e)) +ensures forall e Elem :: { ra.Compose(e2, e) } ra.IsElem(e) && ra.IsValid(ra.Compose(ra.Compose(e1, e2), e)) ==> + ra.IsValid(ra.Compose(e2, e)) +ensures forall e Elem :: { ra.Compose(e, e1) } ra.IsElem(e) && ra.IsValid(ra.Compose(ra.Compose(e1, e2), e)) ==> + ra.IsValid(ra.Compose(e, e1)) +ensures forall e Elem :: { ra.Compose(e, e2) } ra.IsElem(e) && ra.IsValid(ra.Compose(ra.Compose(e1, e2), e)) ==> + ra.IsValid(ra.Compose(e, e2)) +decreases +func ghostOp1WIAux(ra RA, e1 Elem, e2 Elem) { + assume false + /* + requires ra != nil + requires ra.IsElem(e1) && ra.IsElem(e2) + requires ra.IsValid(ra.Compose(e1, e2)) + ensures forall e Elem :: { ra.Compose(e1, e) } ra.IsElem(e) && ra.IsValid(ra.Compose(ra.Compose(e1, e2), e)) ==> + ra.IsValid(ra.Compose(e1, e)) + decreases + outline( + assume false + ra.ComposeAssocQ() + assert forall e Elem :: { ra.Compose(e1, e) } ra.IsElem(e) && ra.IsValid(ra.Compose(ra.Compose(e1, e2), e)) ==> + ra.IsValid(ra.Compose(e1, ra.Compose(e2, e))) + ra.ComposeCommQ() + assert forall e Elem :: { ra.Compose(e1, e) } ra.IsElem(e) && ra.IsValid(ra.Compose(e1, ra.Compose(e2, e))) ==> + ra.IsValid(ra.Compose(e1, ra.Compose(e, e2))) + assert forall e Elem :: { ra.Compose(e1, e) } ra.IsElem(e) && ra.IsValid(ra.Compose(e1, ra.Compose(e, e2))) ==> + ra.IsValid(ra.Compose(ra.Compose(e1, e), e2)) + ra.ValidOpQ() + assert forall e Elem :: { ra.Compose(e1, e) } ra.IsElem(e) && ra.IsValid(ra.Compose(ra.Compose(e1, e), e2)) ==> + ra.IsValid(ra.Compose(e1, e)) + ) + */ + // ra.ValidOpQ() + // ra.ComposeAssocQ() + // ra.ComposeCommQ() +} + ghost requires GlobalMem() requires ra != nil @@ -366,12 +482,10 @@ func GhostOp2WI(l LocName, ra RA, e1 Elem, e2 Elem, w1 Witness, w2 Witness) { // actually, the proof should be very similar to that of GhostOp1W assume forall k LocName :: k elem domain(toDict(model)) ==> (forall i idx :: i elem toCoolSet(toDict(model)[k]) ==> - i.inUse ==> ( - forall i2 idx :: i2 elem toCoolSet(toDict(model)[k]) && i2.inUse && i2 !== i ==> - ras.ToDict()[k].IsElem(ras.ToDict()[k].Compose(i.val, i2.val)) && - ras.ToDict()[k].IsValid(ras.ToDict()[k].Compose(i.val, i2.val)))) - - + i.inUse ==> ( + forall i2 idx :: i2 elem toCoolSet(toDict(model)[k]) && i2.inUse && i2 !== i ==> + ras.ToDict()[k].IsElem(ras.ToDict()[k].Compose(i.val, i2.val)) && + ras.ToDict()[k].IsValid(ras.ToDict()[k].Compose(i.val, i2.val)))) fold GlobalMem() } From 7015069ec6ad34adc0194983e2a1d835a9029b7c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= Date: Wed, 21 Jan 2026 17:02:19 +0100 Subject: [PATCH 23/28] cleanup --- resalgebraNoAxioms/loc.gobra | 69 ------------------------------------ 1 file changed, 69 deletions(-) diff --git a/resalgebraNoAxioms/loc.gobra b/resalgebraNoAxioms/loc.gobra index fd5410a..936ab81 100644 --- a/resalgebraNoAxioms/loc.gobra +++ b/resalgebraNoAxioms/loc.gobra @@ -304,76 +304,7 @@ func GhostOp1WI(l LocName, ra RA, e1 Elem, e2 Elem, w Witness) (w1 Witness, w2 W (forall i idx :: i elem toCoolSet(toDict(model)[k1]) ==> !(i elem toCoolSet(toDict(model)[k2]))) assert ras.ToDict()[l] === ra - - // assume (forall i idx :: { ra.Compose(iii1.val, i.val) } i elem toCoolSet(toDict(model)[l]) ==> - // i != iii1 && i.inUse ==> ( - // ra.IsElem(ra.Compose(iii1.val, i.val)) && - // ra.IsValid(ra.Compose(iii1.val, i.val)))) - // assume (forall i idx :: { ra.Compose(iii2.val, i.val) } i elem toCoolSet(toDict(model)[l]) ==> - // i != iii2 && i.inUse ==> ( - // ra.IsElem(ra.Compose(iii2.val, i.val)) && - // ra.IsValid(ra.Compose(iii2.val, i.val)))) - // assume ra.IsElem(ra.Compose(iii2.val, iii1.val)) && - // ra.IsValid(ra.Compose(iii2.val, iii1.val)) - // assume ra.IsElem(ra.Compose(iii1.val, iii2.val)) && - // ra.IsValid(ra.Compose(iii1.val, iii2.val)) - -/* - assert forall k LocName :: k elem domain(toDict(model)) && k != l ==> - (forall i idx :: i elem toCoolSet(toDict(model)[k]) ==> - i.inUse ==> ( - forall i2 idx :: i2 elem toCoolSet(toDict(model)[k]) && i2.inUse && i2 !== i ==> - ras.ToDict()[k].IsElem(ras.ToDict()[k].Compose(i.val, i2.val)) && - ras.ToDict()[k].IsValid(ras.ToDict()[k].Compose(i.val, i2.val)))) - assert forall i idx :: i elem toCoolSet(toDict(model)[l]) ==> - i.inUse && i != iii1 && i != iii2 ==> ( - forall i2 idx :: i2 elem toCoolSet(toDict(model)[l]) && i2.inUse && i2 !== i && i2 != iii1 && i2 != iii2 ==> - ras.ToDict()[l].IsElem(ras.ToDict()[l].Compose(i.val, i2.val)) && - ras.ToDict()[l].IsValid(ras.ToDict()[l].Compose(i.val, i2.val))) - - assert forall i idx :: i elem toCoolSet(toDict(model)[l]) ==> - i.inUse && i != iii1 && i != iii2 ==> ( - forall i2 idx :: i2 elem toCoolSet(toDict(model)[l]) && i2.inUse && i2 !== i && i2 != iii1 && i2 != iii2 ==> - ras.ToDict()[l].IsElem(ras.ToDict()[l].Compose(i.val, i2.val)) && - ras.ToDict()[l].IsValid(ras.ToDict()[l].Compose(i.val, i2.val))) -*/ - /* - assert forall i2 idx :: i2 elem toCoolSet(toDict(model)[l]) && i2.inUse && i2 != iii1 && i2 != iii2 ==> - ras.ToDict()[l].IsElem(ras.ToDict()[l].Compose(ras.ToDict()[l].Compose(iii1.val, iii2.val), i2.val)) && - ras.ToDict()[l].IsValid(ras.ToDict()[l].Compose(ras.ToDict()[l].Compose(iii1.val, iii2.val), i2.val)) - ra.ValidOpQ() - ra.ComposeAssocQ() - assert forall i2 idx :: i2 elem toCoolSet(toDict(model)[l]) && i2.inUse && i2 != iii1 && i2 != iii2 ==> - ras.ToDict()[l].IsElem(ras.ToDict()[l].Compose(iii1.val, ras.ToDict()[l].Compose(iii2.val, i2.val))) && - ras.ToDict()[l].IsValid(ras.ToDict()[l].Compose(iii1.val, ras.ToDict()[l].Compose(iii2.val, i2.val))) - ra.ComposeCommQ() - assert forall i2 idx :: i2 elem toCoolSet(toDict(model)[l]) && i2.inUse && i2 != iii1 && i2 != iii2 ==> - ras.ToDict()[l].IsElem(ras.ToDict()[l].Compose(iii1.val, ras.ToDict()[l].Compose(i2.val, iii2.val))) && - ras.ToDict()[l].IsValid(ras.ToDict()[l].Compose(iii1.val, ras.ToDict()[l].Compose(i2.val, iii2.val))) - assert forall i2 idx :: i2 elem toCoolSet(toDict(model)[l]) && i2.inUse && i2 != iii1 && i2 != iii2 ==> - ras.ToDict()[l].IsElem(ras.ToDict()[l].Compose(ras.ToDict()[l].Compose(iii1.val, i2.val), iii2.val)) && - ras.ToDict()[l].IsValid(ras.ToDict()[l].Compose(ras.ToDict()[l].Compose(iii1.val, i2.val), iii2.val)) - /// - assert false - assert forall i2 idx :: i2 elem toCoolSet(toDict(model)[l]) && i2.inUse && i2 != iii1 ==> - ras.ToDict()[l].IsElem(ras.ToDict()[l].Compose(iii1.val, i2.val)) && - ras.ToDict()[l].IsValid(ras.ToDict()[l].Compose(iii1.val, i2.val)) - - ///// - - assert forall i idx :: i elem toCoolSet(toDict(model)[l]) ==> - i.inUse && i != iii1 && i != iii2 ==> ( - forall i2 idx :: i2 elem toCoolSet(toDict(model)[l]) && i2.inUse && i2 !== i && i2 != iii1 && i2 != iii2 ==> - ras.ToDict()[l].IsElem(ras.ToDict()[l].Compose(i.val, i2.val)) && - ras.ToDict()[l].IsValid(ras.ToDict()[l].Compose(i.val, i2.val))) - - assert forall i idx :: i elem toCoolSet(toDict(model)[l]) ==> - i.inUse ==> ( - forall i2 idx :: i2 elem toCoolSet(toDict(model)[l]) && i2.inUse && i2 !== i ==> - ras.ToDict()[l].IsElem(ras.ToDict()[l].Compose(i.val, i2.val)) && - ras.ToDict()[l].IsValid(ras.ToDict()[l].Compose(i.val, i2.val))) - */ // not hard to prove, requires applying commutativity and associativity to get (i1 x i2) x k == (i1 x k) x i2. Because the lhs is valid, the rhs is also valid, and by ValidOp, i1 x k is also valid ghostOp1WIAux(ra, iii1.val, iii2.val) From 142427db6fe9aabdcb7a116afdb6ec2da6dfdcc1 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= Date: Wed, 21 Jan 2026 20:38:37 +0100 Subject: [PATCH 24/28] made RA lemmas pure to make them easier to work with --- resalgebraNoAxioms/auth.gobra | 19 +++-- resalgebraNoAxioms/loc.gobra | 73 ++++++++++------- resalgebraNoAxioms/oneshot.gobra | 18 +++-- resalgebraNoAxioms/ra.gobra | 129 ++++++++++++++++++------------- 4 files changed, 143 insertions(+), 96 deletions(-) diff --git a/resalgebraNoAxioms/auth.gobra b/resalgebraNoAxioms/auth.gobra index 601885b..8c68e36 100644 --- a/resalgebraNoAxioms/auth.gobra +++ b/resalgebraNoAxioms/auth.gobra @@ -96,38 +96,45 @@ pure func max(a int, b int) int { // all lemmas proven automatically + ghost decreases -func (ra TypeAuthRA) ComposeAssocQ() { +pure func (ra TypeAuthRA) ComposeAssoc(e1 Elem, e2 Elem, e3 Elem) Unit { // proved + return Unit{} } ghost decreases -func (ra TypeAuthRA) ComposeCommQ() { +pure func (ra TypeAuthRA) ComposeComm(e1 Elem, e2 Elem) Unit { // proved + return Unit{} } ghost decreases -func (ra TypeAuthRA) CoreIdQ() { +pure func (ra TypeAuthRA) CoreId(e Elem) Unit { // proved + return Unit{} } ghost decreases -func (ra TypeAuthRA) CoreIdemQ() { +pure func (ra TypeAuthRA) CoreIdem(e Elem) Unit { // proved + return Unit{} } ghost decreases -func (ra TypeAuthRA) CoreMonoQ() { +pure func (ra TypeAuthRA) CoreMono(e1 Elem, e2 Elem) Unit { // proved + return Unit{} } ghost decreases -func (ra TypeAuthRA) ValidOpQ() { +pure func (ra TypeAuthRA) ValidOp(e1 Elem, e2 Elem) Unit { // proved + return Unit{} } \ No newline at end of file diff --git a/resalgebraNoAxioms/loc.gobra b/resalgebraNoAxioms/loc.gobra index 936ab81..24a868b 100644 --- a/resalgebraNoAxioms/loc.gobra +++ b/resalgebraNoAxioms/loc.gobra @@ -272,10 +272,10 @@ func GhostOp1WI(l LocName, ra RA, e1 Elem, e2 Elem, w Witness) (w1 Witness, w2 W assert i.c.witness(i.i) i.c.lemmaWitness(i.i, 1/3) assert i.i elem toCoolSet(i.c) - ValidOp(ra, e1, e2) + ra.ValidOp(e1, e2) assert ra.IsValid(e1) - ComposeComm(ra, e1, e2) - ValidOp(ra, e2, e1) + ra.ComposeComm(e1, e2) + ra.ValidOp(e2, e1) assert ra.IsValid(e2) i.i.inUse = false @@ -334,32 +334,47 @@ ensures forall e Elem :: { ra.Compose(e, e2) } ra.IsElem(e) && ra.IsValid(ra.Co ra.IsValid(ra.Compose(e, e2)) decreases func ghostOp1WIAux(ra RA, e1 Elem, e2 Elem) { - assume false - /* - requires ra != nil - requires ra.IsElem(e1) && ra.IsElem(e2) - requires ra.IsValid(ra.Compose(e1, e2)) - ensures forall e Elem :: { ra.Compose(e1, e) } ra.IsElem(e) && ra.IsValid(ra.Compose(ra.Compose(e1, e2), e)) ==> + ghostOp1WIAux1(ra, e1, e2) + ghostOp1WIAux2(ra, e1, e2) + ComposeCommQ(ra) +} + +ghost +requires ra != nil +requires ra.IsElem(e1) && ra.IsElem(e2) +requires ra.IsValid(ra.Compose(e1, e2)) +ensures forall e Elem :: { ra.Compose(e1, e) } ra.IsElem(e) && ra.IsValid(ra.Compose(ra.Compose(e1, e2), e)) ==> + ra.IsValid(ra.Compose(e1, e)) +decreases +func ghostOp1WIAux1(ra RA, e1 Elem, e2 Elem) { + assert forall e Elem :: ra.IsElem(e) && ra.IsValid(ra.Compose(ra.Compose(e1, e2), e)) ==> + let _ := ra.ComposeAssoc(e1, e2, e) in + ra.IsValid(ra.Compose(e1, ra.Compose(e2, e))) && + let _ := ra.ComposeComm(e2, e) in + ra.Compose(e, e2) === ra.Compose(e2, e) && + ra.IsValid(ra.Compose(e1, ra.Compose(e, e2))) && + let _ := ra.ComposeAssoc(e1, e, e2) in + ra.Compose(e1, ra.Compose(e, e2)) === ra.Compose(ra.Compose(e1, e), e2) && + ra.IsValid(ra.Compose(ra.Compose(e1, e), e2)) && + let _ := ra.ValidOp(ra.Compose(e1, e), e2) in ra.IsValid(ra.Compose(e1, e)) - decreases - outline( - assume false - ra.ComposeAssocQ() - assert forall e Elem :: { ra.Compose(e1, e) } ra.IsElem(e) && ra.IsValid(ra.Compose(ra.Compose(e1, e2), e)) ==> - ra.IsValid(ra.Compose(e1, ra.Compose(e2, e))) - ra.ComposeCommQ() - assert forall e Elem :: { ra.Compose(e1, e) } ra.IsElem(e) && ra.IsValid(ra.Compose(e1, ra.Compose(e2, e))) ==> - ra.IsValid(ra.Compose(e1, ra.Compose(e, e2))) - assert forall e Elem :: { ra.Compose(e1, e) } ra.IsElem(e) && ra.IsValid(ra.Compose(e1, ra.Compose(e, e2))) ==> - ra.IsValid(ra.Compose(ra.Compose(e1, e), e2)) - ra.ValidOpQ() - assert forall e Elem :: { ra.Compose(e1, e) } ra.IsElem(e) && ra.IsValid(ra.Compose(ra.Compose(e1, e), e2)) ==> - ra.IsValid(ra.Compose(e1, e)) - ) - */ - // ra.ValidOpQ() - // ra.ComposeAssocQ() - // ra.ComposeCommQ() +} + +ghost +requires ra != nil +requires ra.IsElem(e1) && ra.IsElem(e2) +requires ra.IsValid(ra.Compose(e1, e2)) +ensures forall e Elem :: { ra.Compose(e1, e) } ra.IsElem(e) && ra.IsValid(ra.Compose(ra.Compose(e1, e2), e)) ==> + ra.IsValid(ra.Compose(e2, e)) +decreases +func ghostOp1WIAux2(ra RA, e1 Elem, e2 Elem) { + assert forall e Elem :: ra.IsElem(e) && ra.IsValid(ra.Compose(ra.Compose(e1, e2), e)) ==> + let _ := ra.ComposeAssoc(e1, e2, e) in + ra.IsValid(ra.Compose(e1, ra.Compose(e2, e))) && + let _ := ra.ComposeComm(e1, ra.Compose(e2, e)) in + ra.IsValid(ra.Compose(ra.Compose(e2, e), e1)) && + let _ := ra.ValidOp(ra.Compose(e2, e), e1) in + ra.IsValid(ra.Compose(e2, e)) } ghost @@ -452,7 +467,7 @@ func GhostUpdateWI(l LocName, ra RA, e1 Elem, e2 Elem, w Witness) { } else { assert exists e Elem :: { ra.IsElem(e) } { LiftedCompose(ra, some(e1), some(e)) } ra.IsElem(e) && LiftedCompose(ra, some(e1), some(e)) !== none[Elem] - ra.ValidOpQ() + ValidOpQ(ra) assert exists e Elem :: { ra.IsElem(e) } { LiftedCompose(ra, some(e1), some(e)) } ra.IsElem(e) && LiftedIsValid(ra, LiftedCompose(ra, some(e1), some(e))) && ra.IsValid(ra.Compose(e1, e)) && diff --git a/resalgebraNoAxioms/oneshot.gobra b/resalgebraNoAxioms/oneshot.gobra index b49c396..7765c23 100644 --- a/resalgebraNoAxioms/oneshot.gobra +++ b/resalgebraNoAxioms/oneshot.gobra @@ -78,36 +78,42 @@ func (ra TypeOneShotRA) Compose(e1 Elem, e2 Elem) (res Elem) { ghost decreases -func (ra TypeOneShotRA) ComposeAssocQ() { +pure func (ra TypeOneShotRA) ComposeAssoc(e1 Elem, e2 Elem, e3 Elem) Unit { // proved + return Unit{} } ghost decreases -func (ra TypeOneShotRA) ComposeCommQ() { +pure func (ra TypeOneShotRA) ComposeComm(e1 Elem, e2 Elem) Unit { // proved + return Unit{} } ghost decreases -func (ra TypeOneShotRA) CoreIdQ() { +pure func (ra TypeOneShotRA) CoreId(e Elem) Unit { // proved + return Unit{} } ghost decreases -func (ra TypeOneShotRA) CoreIdemQ() { +pure func (ra TypeOneShotRA) CoreIdem(e Elem) Unit { // proved + return Unit{} } ghost decreases -func (ra TypeOneShotRA) CoreMonoQ() { +pure func (ra TypeOneShotRA) CoreMono(e1 Elem, e2 Elem) Unit { // proved + return Unit{} } ghost decreases -func (ra TypeOneShotRA) ValidOpQ() { +pure func (ra TypeOneShotRA) ValidOp(e1 Elem, e2 Elem) Unit { // proved + return Unit{} } \ No newline at end of file diff --git a/resalgebraNoAxioms/ra.gobra b/resalgebraNoAxioms/ra.gobra index cd30460..8c15f8d 100644 --- a/resalgebraNoAxioms/ra.gobra +++ b/resalgebraNoAxioms/ra.gobra @@ -18,6 +18,8 @@ package resalgebraNoAxioms type Elem interface{} +type Unit struct{} + type RA interface { // defines the set of elements of the RA ghost @@ -44,110 +46,127 @@ type RA interface { // Lemmas ghost - ensures forall e1, e2, e3 Elem :: { Compose(Compose(e1, e2), e3) } { Compose(e1, Compose(e2, e3)) } IsElem(e1) && - IsElem(e2) && IsElem(e3) ==> - Compose(Compose(e1, e2), e3) === Compose(e1, Compose(e2, e3)) + requires IsElem(e1) && IsElem(e2) && IsElem(e3) + ensures Compose(Compose(e1, e2), e3) === Compose(e1, Compose(e2, e3)) decreases - ComposeAssocQ() + pure ComposeAssoc(e1 Elem, e2 Elem, e3 Elem) Unit ghost - ensures forall e1, e2 Elem :: { Compose(e1, e2) } { Compose(e2, e1) } IsElem(e1) && IsElem(e2) ==> - Compose(e1, e2) === Compose(e2, e1) + requires IsElem(e1) && IsElem(e2) + ensures Compose(e1, e2) === Compose(e2, e1) decreases - ComposeCommQ() + pure ComposeComm(e1 Elem, e2 Elem) Unit ghost - ensures forall e Elem :: { Core(e) } IsElem(e) ==> - let c := Core(e) in - c !== none[Elem] ==> Compose(get(c), e) === e + requires IsElem(e) + ensures let c := Core(e) in + c !== none[Elem] ==> Compose(get(c), e) === e decreases - CoreIdQ() + pure CoreId(e Elem) Unit ghost - ensures forall e Elem :: { Core(e) } IsElem(e) && Core(e) !== none[Elem] ==> - let c := Core(e) in + 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 - CoreIdemQ() + pure CoreIdem(e Elem) Unit ghost - ensures forall e1, e2 Elem :: { Core(e1), Core(e2) } IsElem(e1) && IsElem(e2) && Core(e1) !== none[Elem] && - // fully expanded version of <= due to Gobra's lack of `Self` in interface specs - (exists e3 Elem :: { IsElem(e3) } IsElem(e3) && e2 === Compose(e1, e3)) ==> - Core(e2) !== none[Elem] && - exists e4 Elem :: { IsElem(e4) } IsElem(e4) && get(Core(e2)) === Compose(get(Core(e1)), e4) + 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 - CoreMonoQ() + pure CoreMono(e1 Elem, e2 Elem) Unit ghost - ensures forall e1, e2 Elem :: { Compose(e1, e2) } IsElem(e1) && IsElem(e2) && IsValid(Compose(e1, e2)) ==> - IsValid(e1) + requires IsElem(e1) && IsElem(e2) + requires IsValid(Compose(e1, e2)) + ensures IsValid(e1) decreases - ValidOpQ() + pure ValidOp(e1 Elem, e2 Elem) Unit } +// The following wrappers should be treated as automatically generated code, their implementation +// is not to be read closely + ghost +opaque requires ra != nil -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)) +ensures forall e1, e2, e3 Elem :: { ra.Compose(ra.Compose(e1, e2), e3) } { ra.Compose(e1, ra.Compose(e2, e3)) } ra.IsElem(e1) && + ra.IsElem(e2) && ra.IsElem(e3) ==> + ra.Compose(ra.Compose(e1, e2), e3) === ra.Compose(e1, ra.Compose(e2, e3)) decreases -func ComposeAssoc(ra RA, e1 Elem, e2 Elem, e3 Elem) { - ra.ComposeAssocQ() +pure func ComposeAssocQ(ra RA) Unit { + return asserting(forall e1, e2, e3 Elem :: { ra.Compose(ra.Compose(e1, e2), e3) } { ra.Compose(e1, ra.Compose(e2, e3)) } ra.IsElem(e1) && ra.IsElem(e2) && ra.IsElem(e3) ==> let _ := ra.ComposeAssoc(e1, e2, e3) in ra.Compose(ra.Compose(e1, e2), e3) === ra.Compose(e1, ra.Compose(e2, e3))) } ghost +opaque requires ra != nil -requires ra.IsElem(e1) && ra.IsElem(e2) -ensures ra.Compose(e1, e2) === ra.Compose(e2, e1) +ensures forall e1, e2 Elem :: { ra.Compose(e1, e2) } { ra.Compose(e2, e1) } ra.IsElem(e1) && ra.IsElem(e2) ==> + ra.Compose(e1, e2) === ra.Compose(e2, e1) decreases -func ComposeComm(ra RA, e1 Elem, e2 Elem) { - ra.ComposeCommQ() +pure func ComposeCommQ(ra RA) Unit { + return asserting(forall e1, e2 Elem :: { ra.Compose(e1, e2) } { ra.Compose(e2, e1) } ra.IsElem(e1) && ra.IsElem(e2) ==> let _ := ra.ComposeComm(e1, e2) in ra.Compose(e1, e2) === ra.Compose(e2, e1)) } ghost +opaque requires ra != nil -requires ra.IsElem(e) -ensures let c := ra.Core(e) in - c !== none[Elem] ==> ra.Compose(get(c), e) === e +ensures forall e Elem :: { ra.Core(e) } ra.IsElem(e) ==> + let c := ra.Core(e) in + c !== none[Elem] ==> ra.Compose(get(c), e) === e decreases -func CoreId(ra RA, e Elem) { - ra.CoreIdQ() +pure func CoreIdQ(ra RA) Unit { + return asserting(forall e Elem :: { ra.Core(e) } ra.IsElem(e) ==> let _ := ra.CoreId(e) in ra.Core(e) !== none[Elem] ==> ra.Compose(get(ra.Core(e)), e) === e) } ghost +opaque requires ra != nil -requires ra.IsElem(e) -requires ra.Core(e) !== none[Elem] -ensures let c := ra.Core(e) in +ensures forall e Elem :: { ra.Core(e) } ra.IsElem(e) && ra.Core(e) !== none[Elem] ==> + let c := ra.Core(e) in let cc := ra.Core(get(c)) in cc !== none[Elem] && get(cc) === get(c) decreases -func CoreIdem(ra RA, e Elem) { - ra.CoreIdemQ() +pure func CoreIdemQ(ra RA) Unit { + return asserting(forall e Elem :: { ra.Core(e) } ra.IsElem(e) && ra.Core(e) !== none[Elem] ==> let _ := ra.CoreIdem(e) in let c := ra.Core(e) in let cc := ra.Core(get(c)) in cc !== none[Elem] && get(cc) === get(c)) } ghost +opaque requires ra != nil -requires ra.IsElem(e1) && ra.IsElem(e2) -requires ra.Core(e1) !== none[Elem] -// fully expanded version of <= due to Gobra's lack of `Self` in interface specs -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) +ensures forall e1, e2 Elem :: { ra.Core(e1), ra.Core(e2) } ra.IsElem(e1) && ra.IsElem(e2) && ra.Core(e1) !== none[Elem] && + // fully expanded version of <= due to Gobra's lack of `Self` in interface specs + (exists e3 Elem :: { ra.IsElem(e3) } ra.IsElem(e3) && e2 === ra.Compose(e1, e3)) ==> + ra.Core(e2) !== none[Elem] && + exists e4 Elem :: { ra.IsElem(e4) } ra.IsElem(e4) && get(ra.Core(e2)) === ra.Compose(get(ra.Core(e1)), e4) decreases -func CoreMono(ra RA, e1 Elem, e2 Elem) { - ra.CoreMonoQ() +pure func CoreMonoQ(ra RA) Unit { + return asserting(forall e1, e2 Elem :: { ra.Core(e1), ra.Core(e2) } ra.IsElem(e1) && ra.IsElem(e2) && ra.Core(e1) !== none[Elem] && (exists e3 Elem :: { ra.IsElem(e3) } ra.IsElem(e3) && e2 === ra.Compose(e1, e3)) ==> let _ := ra.CoreMono(e1, e2) in ra.Core(e2) !== none[Elem] && + exists e4 Elem :: { ra.IsElem(e4) } ra.IsElem(e4) && get(ra.Core(e2)) === ra.Compose(get(ra.Core(e1)), e4)) } ghost +opaque requires ra != nil -requires ra.IsElem(e1) && ra.IsElem(e2) -requires ra.IsValid(ra.Compose(e1, e2)) -ensures ra.IsValid(e1) +ensures forall e1, e2 Elem :: { ra.Compose(e1, e2) } ra.IsElem(e1) && ra.IsElem(e2) && ra.IsValid(ra.Compose(e1, e2)) ==> + ra.IsValid(e1) +decreases +pure func ValidOpQ(ra RA) Unit { + return asserting(forall e1, e2 Elem :: { ra.Compose(e1, e2) } ra.IsElem(e1) && ra.IsElem(e2) && ra.IsValid(ra.Compose(e1, e2)) ==> let _ := ra.ValidOp(e1, e2) in ra.IsValid(e1)) +} + +ghost +requires b decreases -func ValidOp(ra RA, e1 Elem, e2 Elem) { - ra.ValidOpQ() -} \ No newline at end of file +pure func asserting(ghost b bool) Unit { + return Unit{} +} From ed9e7c1944165f40c3240fd7d7ed3e5c40b293c6 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= Date: Wed, 21 Jan 2026 22:14:20 +0100 Subject: [PATCH 25/28] One more assumption proved --- resalgebraNoAxioms/loc.gobra | 55 ++++++++++++++++++++++++++++++------ 1 file changed, 46 insertions(+), 9 deletions(-) diff --git a/resalgebraNoAxioms/loc.gobra b/resalgebraNoAxioms/loc.gobra index 24a868b..78186a9 100644 --- a/resalgebraNoAxioms/loc.gobra +++ b/resalgebraNoAxioms/loc.gobra @@ -452,6 +452,19 @@ func GhostUpdateWI(l LocName, ra RA, e1 Elem, e2 Elem, w Witness) { unfold GhostLocationW(l, ra, e1, i) lemmaWitness(model, l, i.c, 1/3) i.c.lemmaWitness(i.i, 1/3) + + ras.DupWitness(l, ra) + ras.WitnessInMap(l, ra, 1/10) + + assert forall i2 idx :: i2 elem toCoolSet(toDict(model)[l]) && i2.inUse && i2 !== i.i ==> + ras.ToDict()[l].IsElem(ras.ToDict()[l].Compose(i.i.val, i2.val)) && + ras.ToDict()[l].IsValid(ras.ToDict()[l].Compose(i.i.val, i2.val)) + + assert forall i2 idx :: i2 elem toCoolSet(toDict(model)[l]) && i2.inUse && i2 !== i.i ==> + let _ := updateFrameLemma(ra, i.i.val, i2.val, e2) in + ras.ToDict()[l].IsElem(ras.ToDict()[l].Compose(e2, i2.val)) && + ras.ToDict()[l].IsValid(ras.ToDict()[l].Compose(e2, i2.val)) + i.i.val = e2 if forall e Elem :: ra.IsElem(e) ==> LiftedCompose(ra, some(e1), some(e)) === none[Elem] { @@ -475,21 +488,45 @@ func GhostUpdateWI(l LocName, ra RA, e1 Elem, e2 Elem, w Witness) { ra.IsValid(e2) } - ras.DupWitness(l, ra) - ras.WitnessInMap(l, ra, 1/10) - // TODO: should be provable from the def of IsFramePreservingUpdate - assume forall k LocName :: k elem domain(toDict(model)) ==> - (forall i idx :: i elem toCoolSet(toDict(model)[k]) ==> - i.inUse ==> ( - forall i2 idx :: i2 elem toCoolSet(toDict(model)[k]) && i2.inUse && i2 !== i ==> - ras.ToDict()[k].IsElem(ras.ToDict()[k].Compose(i.val, i2.val)) && - ras.ToDict()[k].IsValid(ras.ToDict()[k].Compose(i.val, i2.val)))) + assert forall i2 idx :: i2 elem toCoolSet(toDict(model)[l]) && i2.inUse && i2 !== i.i ==> + ras.ToDict()[l].IsElem(ras.ToDict()[l].Compose(i.i.val, i2.val)) && + ras.ToDict()[l].IsValid(ras.ToDict()[l].Compose(i.i.val, i2.val)) + assert forall i2 idx :: i2 elem toCoolSet(toDict(model)[l]) && i2.inUse && i2 !== i.i ==> + let _ := ra.ComposeComm(i2.val, i.i.val) in + ras.ToDict()[l].IsElem(ras.ToDict()[l].Compose(i2.val, i.i.val)) && + ras.ToDict()[l].IsValid(ras.ToDict()[l].Compose(i2.val, i.i.val)) fold GhostLocationW(l, ra, e2, i) fold GlobalMem() } +ghost +opaque +requires ra != nil +requires ra.IsElem(e1) && ra.IsElem(e2) && ra.IsElem(e3) +requires ra.IsElem(ra.Compose(e1, e2)) +requires ra.IsValid(ra.Compose(e1, e2)) +requires IsFramePreservingUpdate(ra, e1, e3) +ensures ra.IsElem(ra.Compose(e3, e2)) +ensures ra.IsValid(ra.Compose(e3, e2)) +decreases +pure func updateFrameLemma(ra RA, e1 Elem, e2 Elem, e3 Elem) Unit { + return let _ := asserting(ra.IsValid(ra.Compose(e1, e2))) in + let _ := asserting(IsFramePreservingUpdate(ra, e1, e3)) in + let _ := asserting(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(e3), c)))) in + let _ := asserting(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)) === ra.IsValid(ra.Compose(e1, get(c)))) in + let _ := asserting(forall c option[Elem] :: { LiftedCompose(ra, some(e1), c) } { ra.Compose(e3, get(c)) } (c !== none[Elem] && ra.IsElem(get(c))) ==> + LiftedIsValid(ra, LiftedCompose(ra, some(e3), c)) === ra.IsValid(ra.Compose(e3, get(c)))) in + let _ := asserting(forall c option[Elem] :: { LiftedCompose(ra, some(e1), c) } { ra.Compose(e3, get(c)) } (c !== none[Elem] && ra.IsElem(get(c))) ==> + ra.IsValid(ra.Compose(e1, get(c))) ==> ra.IsValid(ra.Compose(e3, get(c)))) in + // the term `get(some(e2))` is used to trigger the previous quantifier + let _ := asserting(ra.IsElem(ra.Compose(e3, get(some(e2))))) in + Unit{} +} + /***** Model: functions that do not depend on the global invariant *****/ ghost From a6cf4f1de6f635458ea051303bb55fca5faaace3 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= Date: Wed, 21 Jan 2026 23:03:29 +0100 Subject: [PATCH 26/28] last assumption --- resalgebraNoAxioms/loc.gobra | 36 ++++++++++++++++++------------------ 1 file changed, 18 insertions(+), 18 deletions(-) diff --git a/resalgebraNoAxioms/loc.gobra b/resalgebraNoAxioms/loc.gobra index 78186a9..9a0b10c 100644 --- a/resalgebraNoAxioms/loc.gobra +++ b/resalgebraNoAxioms/loc.gobra @@ -18,10 +18,6 @@ pkgInvariant GlobalMem() package resalgebraNoAxioms -// TODO: -// - use Monoset and monomap for the model, copy to this package if need be; delete cooliosetio and mapio -// - add triggers to invariants - // 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. @@ -167,6 +163,7 @@ pred GlobalMem() { ras.ToDict()[k].IsValid(ras.ToDict()[k].Compose(i.val, i2.val))))) } +// TODO: use MonoSet and MonoMap for the model; delete cooliosetio and mapio ghost var model cooliomapio = allocMap() ghost var ras rasMap = rasMapAlloc() @@ -391,8 +388,12 @@ func GhostOp2WI(l LocName, ra RA, e1 Elem, e2 Elem, w1 Witness, w2 Witness) { i2 := w2 unfold GlobalMem() - unfold GhostLocationW(l, ra, e1, i1) + + ras.DupWitness(l, ra) + ras.WitnessInMap(l, ra, 1/10) + assert ra === ras.ToDict()[l] + unfold GhostLocationW(l, ra, e2, i2) lemmaWitness(model, l, i2.c, 1/3) assert forall i idx :: { i elem toCoolSet(toDict(model)[l]) } { i.inUse } i elem toCoolSet(toDict(model)[l]) ==> @@ -406,15 +407,16 @@ func GhostOp2WI(l LocName, ra RA, e1 Elem, e2 Elem, w1 Witness, w2 Witness) { lemmaWitness(model, l, i1.c, 1/3) i1.c.lemmaWitness(i1.i, 1/3) - ras.DupWitness(l, ra) - ras.WitnessInMap(l, ra, 1/10) - assert ra === ras.ToDict()[l] - assert i1.i elem toCoolSet(toDict(model)[l]) && i1.i.inUse assert i2.i elem toCoolSet(toDict(model)[l]) && i2.i.inUse assert ra.IsElem(ra.Compose(i1.i.val, i2.i.val)) assert ra.IsValid(ra.Compose(i1.i.val, i2.i.val)) + assume forall ii idx :: ii elem toCoolSet(toDict(model)[l]) && ii.inUse && ii !== i1.i && ii != i2.i ==> + // let _ := ghostOp2WIaux(ra, e1, e2, ii.val) in + ras.ToDict()[l].IsElem(ras.ToDict()[l].Compose(ra.Compose(e1, e2), ii.val)) && + ras.ToDict()[l].IsValid(ras.ToDict()[l].Compose(ra.Compose(e1, e2), ii.val)) + assert ra.IsElem(ra.Compose(e1, e2)) && ra.IsValid(ra.Compose(e1, e2)) i1.i.val = ra.Compose(e1, e2) i2.i.inUse = false @@ -424,14 +426,13 @@ func GhostOp2WI(l LocName, ra RA, e1 Elem, e2 Elem, w1 Witness, w2 Witness) { (forall i idx :: i elem toCoolSet(toDict(model)[k]) ==> i.inUse ==> (ras.ToDict()[k].IsElem(i.val) && ras.ToDict()[k].IsValid(i.val))) - // proof requires that all previous elems can be added to this one and become valid. - // actually, the proof should be very similar to that of GhostOp1W - assume forall k LocName :: k elem domain(toDict(model)) ==> - (forall i idx :: i elem toCoolSet(toDict(model)[k]) ==> - i.inUse ==> ( - forall i2 idx :: i2 elem toCoolSet(toDict(model)[k]) && i2.inUse && i2 !== i ==> - ras.ToDict()[k].IsElem(ras.ToDict()[k].Compose(i.val, i2.val)) && - ras.ToDict()[k].IsValid(ras.ToDict()[k].Compose(i.val, i2.val)))) + assert forall i2 idx :: i2 elem toCoolSet(toDict(model)[l]) && i2.inUse && i2 !== i1.i ==> + ras.ToDict()[l].IsElem(ras.ToDict()[l].Compose(i1.i.val, i2.val)) && + ras.ToDict()[l].IsValid(ras.ToDict()[l].Compose(i1.i.val, i2.val)) + assert forall i2 idx :: i2 elem toCoolSet(toDict(model)[l]) && i2.inUse && i2 !== i1.i ==> + let _ := ra.ComposeComm(i2.val, i1.i.val) in + ras.ToDict()[l].IsElem(ras.ToDict()[l].Compose(i2.val, i1.i.val)) && + ras.ToDict()[l].IsValid(ras.ToDict()[l].Compose(i2.val, i1.i.val)) fold GlobalMem() } @@ -488,7 +489,6 @@ func GhostUpdateWI(l LocName, ra RA, e1 Elem, e2 Elem, w Witness) { ra.IsValid(e2) } - // TODO: should be provable from the def of IsFramePreservingUpdate assert forall i2 idx :: i2 elem toCoolSet(toDict(model)[l]) && i2.inUse && i2 !== i.i ==> ras.ToDict()[l].IsElem(ras.ToDict()[l].Compose(i.i.val, i2.val)) && ras.ToDict()[l].IsValid(ras.ToDict()[l].Compose(i.i.val, i2.val)) From 1047c699ff5131f6229f8443dbe0e6eea5b45ca5 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= Date: Wed, 21 Jan 2026 23:56:51 +0100 Subject: [PATCH 27/28] add explanation on missing invariant --- resalgebraNoAxioms/loc.gobra | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/resalgebraNoAxioms/loc.gobra b/resalgebraNoAxioms/loc.gobra index 9a0b10c..fba20ca 100644 --- a/resalgebraNoAxioms/loc.gobra +++ b/resalgebraNoAxioms/loc.gobra @@ -161,6 +161,9 @@ pred GlobalMem() { forall i2 idx :: { ras.ToDict()[k].Compose(i.val, i2.val) } i2 elem toCoolSet(toDict(model)[k]) && i2.inUse && i2 !== i ==> ras.ToDict()[k].IsElem(ras.ToDict()[k].Compose(i.val, i2.val)) && ras.ToDict()[k].IsValid(ras.ToDict()[k].Compose(i.val, i2.val))))) + // MISSING: the product of all inUse elements is valid. requires proving all kinds of facts + // about the updates to the set of values inUse and the order in which the multiplication is performed. + // this is easy to show ghostOp1 and ghostOp2 and frame-preserving updates } // TODO: use MonoSet and MonoMap for the model; delete cooliosetio and mapio @@ -412,6 +415,8 @@ func GhostOp2WI(l LocName, ra RA, e1 Elem, e2 Elem, w1 Witness, w2 Witness) { assert ra.IsElem(ra.Compose(i1.i.val, i2.i.val)) assert ra.IsValid(ra.Compose(i1.i.val, i2.i.val)) + // TODO: this is where the invariant of Validity of the product of all elements comes in handy + // to prove this assumption assume forall ii idx :: ii elem toCoolSet(toDict(model)[l]) && ii.inUse && ii !== i1.i && ii != i2.i ==> // let _ := ghostOp2WIaux(ra, e1, e2, ii.val) in ras.ToDict()[l].IsElem(ras.ToDict()[l].Compose(ra.Compose(e1, e2), ii.val)) && From fd169f487888ce316eefcc07fc8ac11bf7bf361c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= Date: Sun, 25 Jan 2026 17:09:48 +0100 Subject: [PATCH 28/28] add body to all functions that depend on the invariant --- resalgebraNoAxioms/loc.gobra | 60 +++++++++++++++++++++++++++--------- 1 file changed, 45 insertions(+), 15 deletions(-) diff --git a/resalgebraNoAxioms/loc.gobra b/resalgebraNoAxioms/loc.gobra index fba20ca..2100d72 100644 --- a/resalgebraNoAxioms/loc.gobra +++ b/resalgebraNoAxioms/loc.gobra @@ -14,8 +14,7 @@ // +gobra -// todo: replace this by a dup invariant that GlobalMem() is an invariant -pkgInvariant GlobalMem() +dup pkgInvariant Invariant(GlobalMem!) package resalgebraNoAxioms // At the moment, all of these definitions are trusted, and this, @@ -171,7 +170,8 @@ ghost var model cooliomapio = allocMap() ghost var ras rasMap = rasMapAlloc() func init() { - fold GlobalMem() + fold GlobalMem!() + EstablishInvariant(GlobalMem!) } /***** Model *****/ @@ -548,20 +548,23 @@ func GhostValidW(l LocName, ra RA, e Elem, w Witness) { /***** Model: wrappers that acquire the global invariant; these functions may not be called from critical regions *****/ ghost -// opensInvariants +opensInvariants requires ra != nil requires ra.IsElem(e) && ra.IsValid(e) ensures l != nil ensures GhostLocationW(l, ra, e, w) decreases func AllocW(ra RA, e Elem) (l LocName, w Witness) { - inhale GlobalMem() // acquire dup pkg invariant && open invariant + openDupPkgInv + critical GlobalMem! ( + changeView1() l, w = AllocWI(ra, e) - exhale GlobalMem() // close invariant + changeView2() + ) } ghost -// opensInvariants +opensInvariants requires ra != nil requires ra.IsElem(e1) requires ra.IsElem(e2) @@ -569,13 +572,16 @@ requires GhostLocationW(l, ra, ra.Compose(e1, e2), w) ensures GhostLocationW(l, ra, e1, w1) && GhostLocationW(l, ra, e2, w2) decreases func GhostOp1W(l LocName, ra RA, e1 Elem, e2 Elem, w Witness) (w1 Witness, w2 Witness) { - inhale GlobalMem() // acquire dup pkg invariant && open invariant + openDupPkgInv + critical GlobalMem! ( + changeView1() w1, w2 = GhostOp1WI(l, ra, e1, e2, w) - exhale GlobalMem() // close invariant + changeView2() + ) } ghost -// opensInvariants +opensInvariants requires ra != nil requires ra.IsElem(e1) requires ra.IsElem(e2) @@ -583,13 +589,16 @@ requires GhostLocationW(l, ra, e1, w1) && GhostLocationW(l, ra, e2, w2) ensures GhostLocationW(l, ra, ra.Compose(e1, e2), w1) decreases func GhostOp2W(l LocName, ra RA, e1 Elem, e2 Elem, w1 Witness, w2 Witness) { - inhale GlobalMem() // acquire dup pkg invariant && open invariant + openDupPkgInv + critical GlobalMem! ( + changeView1() GhostOp2WI(l, ra, e1, e2, w1, w2) - exhale GlobalMem() // close invariant + changeView2() + ) } ghost -// opensInvariants +opensInvariants requires ra != nil requires ra.IsElem(e1) requires ra.IsElem(e2) @@ -598,7 +607,28 @@ requires IsFramePreservingUpdate(ra, e1, e2) ensures GhostLocationW(l, ra, e2, w) decreases func GhostUpdateW(l LocName, ra RA, e1 Elem, e2 Elem, w Witness) { - inhale GlobalMem() // acquire dup pkg invariant && open invariant + openDupPkgInv + critical GlobalMem! ( + changeView1() GhostUpdateWI(l, ra, e1, e2, w) - exhale GlobalMem() // close invariant + changeView2() + ) +} + +ghost +requires GlobalMem!() +ensures GlobalMem() +decreases +func changeView1() { + unfold GlobalMem!() + fold GlobalMem() +} + +ghost +requires GlobalMem() +ensures GlobalMem!() +decreases +func changeView2() { + unfold GlobalMem() + fold GlobalMem!() } \ No newline at end of file