diff --git a/CLAUDE.md b/CLAUDE.md index b35ed0c..30e40e7 100644 --- a/CLAUDE.md +++ b/CLAUDE.md @@ -19,8 +19,7 @@ Each top-level directory is a Gobra package: | `runeslice/` | Rune slice helper functions | | `math/` | Natural numbers and math utilities | | `util/` | General utility functions | -| `resalgebra/` | Resource algebra framework (with axioms) (deprecated) | -| `resalgebraNoAxioms/` | Resource algebra framework (without axioms) | +| `resalgebra/` | Resource algebra framework | | `refinement/` | Refinement type support (deprecated) | | `refinementguard/` | Refinement with guards and LIIs | | `genericmonomap/` | Generic monotonic map | diff --git a/resalgebraNoAxioms/CLAUDE.md b/resalgebra/CLAUDE.md similarity index 80% rename from resalgebraNoAxioms/CLAUDE.md rename to resalgebra/CLAUDE.md index 6517832..7e9f938 100644 --- a/resalgebraNoAxioms/CLAUDE.md +++ b/resalgebra/CLAUDE.md @@ -4,9 +4,7 @@ This file provides guidance to Claude Code (claude.ai/code) when working with co ## Project Overview -This package (`resalgebraNoAxioms`) is part of the `gobra-libs` project—a collection of reusable Gobra verification libraries. It provides a **verified model of ghost locations and relational algebras without axioms**, inspired by the Iris separation logic framework but implemented entirely in Gobra. - -Key distinction from the `resalgebra` sibling package: all lemmas are proven within Gobra using pure functions rather than relying on axioms (hence "NoAxioms"). +This package (`resalgebra`) is part of the `gobra-libs` project—a collection of reusable Gobra verification libraries. It provides a **verified model of ghost locations and relational algebras**, inspired by the Iris separation logic framework but implemented entirely in Gobra. All RA lemmas are proven within Gobra using pure functions rather than relying on axioms. ## Architecture diff --git a/resalgebra/auth.gobra b/resalgebra/auth.gobra index 5f7102c..1f32a66 100644 --- a/resalgebra/auth.gobra +++ b/resalgebra/auth.gobra @@ -16,8 +16,8 @@ package resalgebra -var _ RA = TypeAuthRA{} -var AuthRA TypeAuthRA = TypeAuthRA{} +ghost var _ RA = TypeAuthRA{} +ghost var AuthRA TypeAuthRA = TypeAuthRA{} type IntWithTopBot interface {} type Top struct{} @@ -45,6 +45,7 @@ pure func FragView(m int) Elem { return AuthCarrier{Bottom{}, m} } + ghost decreases pure func (ra TypeAuthRA) IsElem(e Elem) (res bool) { @@ -93,59 +94,47 @@ pure func max(a int, b int) int { return a > b ? a : b } +// all lemmas 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 TypeAuthRA) ComposeAssoc(e1 Elem, e2 Elem, e3 Elem) { +pure func (ra TypeAuthRA) ComposeAssoc(e1 Elem, e2 Elem, e3 Elem) Unit { // proved + return Unit{} } 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) { +pure func (ra TypeAuthRA) ComposeComm(e1 Elem, e2 Elem) Unit { // proved + return Unit{} } 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) { +pure func (ra TypeAuthRA) CoreId(e Elem) Unit { // proved + return Unit{} } 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) { +pure func (ra TypeAuthRA) CoreIdem(e Elem) Unit { // proved + return Unit{} } 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) { +pure func (ra TypeAuthRA) CoreMono(e1 Elem, e2 Elem) Unit { // proved + return Unit{} } 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) { +pure func (ra TypeAuthRA) ValidOp(e1 Elem, e2 Elem) Unit { // proved + return Unit{} } diff --git a/resalgebraNoAxioms/cooliomapio.gobra b/resalgebra/cooliomapio.gobra similarity index 99% rename from resalgebraNoAxioms/cooliomapio.gobra rename to resalgebra/cooliomapio.gobra index becca86..9bf2154 100644 --- a/resalgebraNoAxioms/cooliomapio.gobra +++ b/resalgebra/cooliomapio.gobra @@ -14,7 +14,7 @@ // +gobra -package resalgebraNoAxioms +package resalgebra // 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/resalgebraNoAxioms/cooliosetio.gobra b/resalgebra/cooliosetio.gobra similarity index 99% rename from resalgebraNoAxioms/cooliosetio.gobra rename to resalgebra/cooliosetio.gobra index 4270bb2..ccc1f29 100644 --- a/resalgebraNoAxioms/cooliosetio.gobra +++ b/resalgebra/cooliosetio.gobra @@ -14,7 +14,7 @@ // +gobra -package resalgebraNoAxioms +package resalgebra // 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/resalgebraNoAxioms/doc.gobra b/resalgebra/doc.gobra similarity index 63% rename from resalgebraNoAxioms/doc.gobra rename to resalgebra/doc.gobra index 72564c7..b0db999 100644 --- a/resalgebraNoAxioms/doc.gobra +++ b/resalgebra/doc.gobra @@ -14,21 +14,16 @@ // +gobra -package resalgebraNoAxioms +package resalgebra // 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` -// 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). +// those of Iris entirely in Gobra. All lemmas in the interface RA are universally +// quantified (rather than requiring the user to provide instantiations of the +// quantified variables), and all lemmas for ghost locations are formulated in +// terms of an explicit Witness value. This is due to a technicality in Gobra: +// we cannot existentially quantify over resources. -// For the time being, to keep the same API for GhostLocations -// as the one found in `resalgebra/loc.gobra`, we axiomatize +// To keep the public API for GhostLocations free of witnesses, we axiomatize // the introduction and elimination rules for existential QPs: // Same as `exists w s.t. GhostLocationW(l, ra, e, w)` diff --git a/resalgebra/loc.gobra b/resalgebra/loc.gobra index 4573836..db0e0d1 100644 --- a/resalgebra/loc.gobra +++ b/resalgebra/loc.gobra @@ -14,6 +14,8 @@ // +gobra +// todo: replace this by a dup invariant that GlobalMem() is an invariant +pkgInvariant GlobalMem() package resalgebra // At the moment, all of these definitions are trusted, and this, @@ -22,7 +24,7 @@ package resalgebra ghost type LocName gpointer[int] -pred GhostLocation(l LocName, ra RA, e Elem) +/***** GhostLocation *****/ ghost requires ra != nil @@ -30,7 +32,11 @@ requires ra.IsElem(e) && ra.IsValid(e) ensures l != nil ensures GhostLocation(l, ra, e) decreases -func Alloc(ra RA, e Elem) (l LocName) +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 requires ra != nil @@ -39,7 +45,12 @@ 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) +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) +} ghost requires ra != nil @@ -48,7 +59,12 @@ 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) +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 @@ -56,7 +72,29 @@ 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) +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 @@ -91,13 +129,593 @@ pure func LiftedIsValid(ra RA, e option[Elem]) bool { true } +/***** Model: Global State *****/ + +pred GlobalMem() { + inv(model) && + ras.Inv() && + acc(&inUseIdx) && + acc(&inUseVal) && + // necessary for proving key freshness + (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 + (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)) }{ 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] }{ 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 :: { 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))))) && + // In-use value tracking: per-location seqs of currently-in-use idx pointers and their + // values. + domain(toDict(model)) subset domain(inUseIdx) && + domain(toDict(model)) subset domain(inUseVal) && + (forall k LocName :: k elem domain(toDict(model)) ==> + len(getIdxAt(k)) >= 1) && + (forall k LocName :: k elem domain(toDict(model)) ==> + len(getValAt(k)) >= 1) && + (forall k LocName :: k elem domain(toDict(model)) ==> + len(getIdxAt(k)) == len(getValAt(k))) && + (forall k LocName :: k elem domain(toDict(model)) ==> + (forall i idx :: i elem toCoolSet(toDict(model)[k]) && i.inUse ==> + i elem getIdxAt(k))) && + (forall k LocName :: k elem domain(toDict(model)) ==> + (forall j int :: 0 <= j && j < len(getIdxAt(k)) ==> + getIdxAt(k)[j] elem toCoolSet(toDict(model)[k]))) && + (forall k LocName :: k elem domain(toDict(model)) ==> + (forall j1, j2 int :: 0 <= j1 && j1 < j2 && j2 < len(getIdxAt(k)) ==> + getIdxAt(k)[j1] !== getIdxAt(k)[j2])) && + (forall k LocName :: k elem domain(toDict(model)) ==> + (forall j int :: 0 <= j && j < len(getIdxAt(k)) ==> + getIdxAt(k)[j].val === getValAt(k)[j])) && + (forall k LocName :: k elem domain(toDict(model)) ==> + (forall j int :: 0 <= j && j < len(getValAt(k)) ==> + ras.ToDict()[k].IsElem(getValAt(k)[j]))) && + // Product validity: the composition of all in-use values at k is valid under ras[k]. + (forall k LocName :: k elem domain(toDict(model)) ==> + ras.ToDict()[k].IsValid(ProductOfSeq(getValAt(k), ras.ToDict()[k]))) +} + +// Returns the sequence of active elements for a given reference. +ghost +requires acc(&inUseIdx) +decreases +pure func getIdxAt(k LocName) seq[idx] { + return idxSeqLookup(inUseIdx, k) +} + +ghost +requires acc(&inUseVal) +decreases +pure func getValAt(k LocName) seq[Elem] { + return valSeqLookup(inUseVal, k) +} + ghost +decreases +pure func idxSeqLookup(d dict[LocName](seq[idx]), k LocName) seq[idx] { + return k elem domain(d) ? d[k] : seq[idx]{} +} + +ghost +decreases +pure func valSeqLookup(d dict[LocName](seq[Elem]), k LocName) seq[Elem] { + return k elem domain(d) ? d[k] : seq[Elem]{} +} + +// Find the (first) position of x in s. Requires x to be present in s. +ghost +requires x elem s +ensures 0 <= res && res < len(s) +ensures s[res] === x +decreases len(s) +pure func idxPos(s seq[idx], x idx) (res int) { + return (s[0] === x) ? 0 : 1 + idxPos(s[1:], x) +} + +// TODO: use MonoSet and MonoMap for the model; delete cooliosetio and mapio +ghost var model cooliomapio = allocMap() +ghost var ras rasMap = rasMapAlloc() + +// Per-location sequences of currently-in-use idx pointers and their values. +// Maintained in lockstep with the in-use indices in `model`. These are used +// by `GlobalMem()` to state the product-of-all-in-use-values invariant. +ghost var inUseIdx@ dict[LocName](seq[idx]) +ghost var inUseVal@ dict[LocName](seq[Elem]) + +func init() { + fold GlobalMem() +} + +/***** 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) && + w.i.inUse && + 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) && + ras.Witness(l, ra) +} + +/***** 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, w) +decreases +func AllocWI(ra RA, e Elem) (l LocName, w Witness) { + unfold GlobalMem() + + newl := new(int) + 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} + + 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) + 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) + + 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]) ==> + i.inUse ==> (ras.ToDict()[k].IsElem(i.val) && ras.ToDict()[k].IsValid(i.val))) + + inUseIdx[newl] = seq[idx]{iii} + inUseVal[newl] = seq[Elem]{e} + fold GlobalMem() + + return newl, newi +} + +ghost +requires GlobalMem() requires ra != nil requires ra.IsElem(e1) requires ra.IsElem(e2) -requires GhostLocation(l, ra, e1) +requires GhostLocationW(l, ra, ra.Compose(e1, e2), w) +ensures GlobalMem() +ensures GhostLocationW(l, ra, e1, w1) && GhostLocationW(l, ra, e2, w2) +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) + + 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) + 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 := 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) + + 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 + + // 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) + + 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].IsValid(ras.ToDict()[k].Compose(i.val, i2.val)))) + + // Replace i.i's slot in the seqs with iii1 (val e1) and append iii2 (val e2). + // i.i is no longer in-use, but by the completeness invariant it was in getIdxAt(l) while still in-use. + posI := idxPos(getIdxAt(l), i.i) + oldVals := getValAt(l) + pre := oldVals[:posI] + post := oldVals[posI+1:] + assert oldVals[posI] === ra.Compose(e1, e2) + assert oldVals === pre ++ seq[Elem]{ra.Compose(e1, e2)} ++ post + ProductSplitEq(pre, post, e1, e2, ra) + inUseIdx[l] = getIdxAt(l)[:posI] ++ seq[idx]{iii1} ++ getIdxAt(l)[posI+1:] ++ seq[idx]{iii2} + inUseVal[l] = pre ++ seq[Elem]{e1} ++ post ++ seq[Elem]{e2} + 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) { + 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)) +} + +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 +requires GlobalMem() +requires ra != nil +requires ra.IsElem(e1) +requires ra.IsElem(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 GhostOp2WI(l LocName, ra RA, e1 Elem, e2 Elem, w1 Witness, w2 Witness) { + i1 := w1 + 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]) ==> + 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) + lemmaWitness(model, l, i1.c, 1/3) + i1.c.lemmaWitness(i1.i, 1/3) + + 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)) + + // Capture seq positions and values BEFORE mutating i1.i.val or i2.i.inUse. + posI1 := idxPos(getIdxAt(l), i1.i) + posI2 := idxPos(getIdxAt(l), i2.i) + pmin, pmax := posI1, posI2 + if posI1 > posI2 { + pmin, pmax = posI2, posI1 + } + oldVals := getValAt(l) + oldIdxs := getIdxAt(l) + assert oldVals[posI1] === e1 + assert oldVals[posI2] === e2 + ProductMergeAt(oldVals, posI1, posI2, ra) + // ProductMergeAt yields IsValid of the merged seq: + // oldVals[:pmin] ++ [Compose(e1,e2)] ++ oldVals[pmin+1:pmax] ++ oldVals[pmax+1:] + + // Discharge: derive `IsValid(Compose(Compose(e1, e2), ii.val))` for any other in-use ii at l. + // By completeness, every in-use i at l appears in inUseIdx[l] (= oldIdxs). + // By distinctness, the positions of i1.i, i2.i, and any third ii are all distinct. + // By IsElem invariant on values, all entries of oldVals are RA elements. + // By the product-validity invariant, ProductOfSeq(oldVals, ra) is valid, so by + // `ExtractThreeValid` (pure, in product.gobra) any triple of values has its triple-Compose valid. + assert forall ii idx :: ii elem toCoolSet(toDict(model)[l]) && ii.inUse && ii !== i1.i && ii != i2.i ==> + let posIi := idxPos(oldIdxs, ii) in + let _ := ExtractThreeValid(oldVals, ra, posI1, posI2, posIi) 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 + fold GhostLocationW(l, ra, ra.Compose(e1, e2), i1) + + 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))) + + 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)) + + inUseVal[l] = oldVals[:pmin] ++ seq[Elem]{ra.Compose(e1, e2)} ++ oldVals[pmin+1:pmax] ++ oldVals[pmax+1:] + inUseIdx[l] = oldIdxs[:pmin] ++ seq[idx]{i1.i} ++ oldIdxs[pmin+1:pmax] ++ oldIdxs[pmax+1:] + + fold GlobalMem() +} + +ghost +requires GlobalMem() +requires ra != nil +requires ra.IsElem(e1) +requires ra.IsElem(e2) +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 +func GhostUpdateWI(l LocName, ra RA, e1 Elem, e2 Elem, w Witness) { + i := w + unfold GlobalMem() + + 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)) + + // Capture seq position and apply product FPU lemma BEFORE mutating i.i.val. + posI := idxPos(getIdxAt(l), i.i) + oldVals := getValAt(l) + assert oldVals[posI] === e1 + ProductFPUEq(oldVals, posI, e1, e2, ra) + + i.i.val = e2 + + 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 { + assert exists e Elem :: { ra.IsElem(e) } { LiftedCompose(ra, some(e1), some(e)) } ra.IsElem(e) && + LiftedCompose(ra, some(e1), some(e)) !== none[Elem] + 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)) && + ra.IsValid(ra.Compose(e2, e)) && + ra.IsValid(e2) + } + + 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)) + + // Update inUseVal[l] at i.i's position to the new value e2 using the captured oldVals. + inUseVal[l] = oldVals[:posI] ++ seq[Elem]{e2} ++ oldVals[posI+1:] + + 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 +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 *****/ + +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 -// slightly different from paper, improve -func GhostUpdate(l LocName, ra RA, e1 Elem, e2 Elem) \ No newline at end of file +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/resalgebra/oneshot.gobra b/resalgebra/oneshot.gobra index 19475a9..06cfedc 100644 --- a/resalgebra/oneshot.gobra +++ b/resalgebra/oneshot.gobra @@ -28,7 +28,7 @@ type TypeOneShotRA struct{} TypeOneShotRA implements RA -var OneShotRA TypeOneShotRA = TypeOneShotRA{} +ghost var OneShotRA TypeOneShotRA = TypeOneShotRA{} ghost decreases @@ -42,7 +42,6 @@ func (ra TypeOneShotRA) IsElem(e Elem) (res bool) { (e === Fail{}) } - ghost requires ra.IsElem(e) decreases @@ -75,63 +74,46 @@ 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) { +pure func (ra TypeOneShotRA) ComposeAssoc(e1 Elem, e2 Elem, e3 Elem) Unit { // proved + return Unit{} } 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) { +pure func (ra TypeOneShotRA) ComposeComm(e1 Elem, e2 Elem) Unit { // proved + return Unit{} } 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) { +pure func (ra TypeOneShotRA) CoreId(e Elem) Unit { // proved + return Unit{} } 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) { +pure func (ra TypeOneShotRA) CoreIdem(e Elem) Unit { // proved + return Unit{} } 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) { +pure func (ra TypeOneShotRA) CoreMono(e1 Elem, e2 Elem) Unit { // proved + return Unit{} } 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) { +pure func (ra TypeOneShotRA) ValidOp(e1 Elem, e2 Elem) Unit { // proved + return Unit{} } - - - diff --git a/resalgebraNoAxioms/product.gobra b/resalgebra/product.gobra similarity index 99% rename from resalgebraNoAxioms/product.gobra rename to resalgebra/product.gobra index 413fb44..f0920c7 100644 --- a/resalgebraNoAxioms/product.gobra +++ b/resalgebra/product.gobra @@ -14,7 +14,7 @@ // +gobra -package resalgebraNoAxioms +package resalgebra // ProductOfSeq composes all elements of `s` under `ra`. ghost diff --git a/resalgebra/ra.gobra b/resalgebra/ra.gobra index 85fded7..9e748ef 100644 --- a/resalgebra/ra.gobra +++ b/resalgebra/ra.gobra @@ -18,6 +18,8 @@ package resalgebra type Elem interface{} +type Unit struct{} + type RA interface { // defines the set of elements of the RA ghost @@ -47,20 +49,20 @@ type RA interface { 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) + pure ComposeAssoc(e1 Elem, e2 Elem, e3 Elem) Unit ghost requires IsElem(e1) && IsElem(e2) ensures Compose(e1, e2) === Compose(e2, e1) decreases - ComposeComm(e1 Elem, e2 Elem) + pure ComposeComm(e1 Elem, e2 Elem) Unit ghost requires IsElem(e) ensures let c := Core(e) in c !== none[Elem] ==> Compose(get(c), e) === e decreases - CoreId(e Elem) + pure CoreId(e Elem) Unit ghost requires IsElem(e) @@ -70,7 +72,7 @@ type RA interface { cc !== none[Elem] && get(cc) === get(c) decreases - CoreIdem(e Elem) + pure CoreIdem(e Elem) Unit ghost requires IsElem(e1) && IsElem(e2) @@ -80,12 +82,91 @@ type RA interface { 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) + pure CoreMono(e1 Elem, e2 Elem) Unit 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 + 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 +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 +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 +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 +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 +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 +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 +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 +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 +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 +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 +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 +pure func asserting(ghost b bool) Unit { + return Unit{} +} diff --git a/resalgebraNoAxioms/ras-map.gobra b/resalgebra/ras-map.gobra similarity index 99% rename from resalgebraNoAxioms/ras-map.gobra rename to resalgebra/ras-map.gobra index d57a360..7e206ed 100644 --- a/resalgebraNoAxioms/ras-map.gobra +++ b/resalgebra/ras-map.gobra @@ -17,7 +17,7 @@ // Instantiation of genericmonomap for `ras` (Key is LocName and Val is RA). // Copying this is easier than implementing wrappers around MonoMap. -package resalgebraNoAxioms +package resalgebra ghost type keyRasMap = LocName type valRasMap = RA diff --git a/resalgebraNoAxioms/auth.gobra b/resalgebraNoAxioms/auth.gobra deleted file mode 100644 index 2841be5..0000000 --- a/resalgebraNoAxioms/auth.gobra +++ /dev/null @@ -1,140 +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 - -ghost var _ RA = TypeAuthRA{} -ghost 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 -pure func (ra TypeAuthRA) ComposeAssoc(e1 Elem, e2 Elem, e3 Elem) Unit { - // proved - return Unit{} -} - -ghost -decreases -pure func (ra TypeAuthRA) ComposeComm(e1 Elem, e2 Elem) Unit { - // proved - return Unit{} -} - -ghost -decreases -pure func (ra TypeAuthRA) CoreId(e Elem) Unit { - // proved - return Unit{} -} - -ghost -decreases -pure func (ra TypeAuthRA) CoreIdem(e Elem) Unit { - // proved - return Unit{} -} - -ghost -decreases -pure func (ra TypeAuthRA) CoreMono(e1 Elem, e2 Elem) Unit { - // proved - return Unit{} -} - -ghost -decreases -pure func (ra TypeAuthRA) ValidOp(e1 Elem, e2 Elem) Unit { - // proved - return Unit{} -} diff --git a/resalgebraNoAxioms/loc.gobra b/resalgebraNoAxioms/loc.gobra deleted file mode 100644 index 404a2f1..0000000 --- a/resalgebraNoAxioms/loc.gobra +++ /dev/null @@ -1,721 +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 - -// todo: replace this by a dup invariant that GlobalMem() is an invariant -pkgInvariant GlobalMem() -package resalgebraNoAxioms - -// 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] - -/***** GhostLocation *****/ - -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 -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) -} - -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 -} - -/***** Model: Global State *****/ - -pred GlobalMem() { - inv(model) && - ras.Inv() && - acc(&inUseIdx) && - acc(&inUseVal) && - // necessary for proving key freshness - (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 - (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)) }{ 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] }{ 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 :: { 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))))) && - // In-use value tracking: per-location seqs of currently-in-use idx pointers and their - // values. - domain(toDict(model)) subset domain(inUseIdx) && - domain(toDict(model)) subset domain(inUseVal) && - (forall k LocName :: k elem domain(toDict(model)) ==> - len(getIdxAt(k)) >= 1) && - (forall k LocName :: k elem domain(toDict(model)) ==> - len(getValAt(k)) >= 1) && - (forall k LocName :: k elem domain(toDict(model)) ==> - len(getIdxAt(k)) == len(getValAt(k))) && - (forall k LocName :: k elem domain(toDict(model)) ==> - (forall i idx :: i elem toCoolSet(toDict(model)[k]) && i.inUse ==> - i elem getIdxAt(k))) && - (forall k LocName :: k elem domain(toDict(model)) ==> - (forall j int :: 0 <= j && j < len(getIdxAt(k)) ==> - getIdxAt(k)[j] elem toCoolSet(toDict(model)[k]))) && - (forall k LocName :: k elem domain(toDict(model)) ==> - (forall j1, j2 int :: 0 <= j1 && j1 < j2 && j2 < len(getIdxAt(k)) ==> - getIdxAt(k)[j1] !== getIdxAt(k)[j2])) && - (forall k LocName :: k elem domain(toDict(model)) ==> - (forall j int :: 0 <= j && j < len(getIdxAt(k)) ==> - getIdxAt(k)[j].val === getValAt(k)[j])) && - (forall k LocName :: k elem domain(toDict(model)) ==> - (forall j int :: 0 <= j && j < len(getValAt(k)) ==> - ras.ToDict()[k].IsElem(getValAt(k)[j]))) && - // Product validity: the composition of all in-use values at k is valid under ras[k]. - (forall k LocName :: k elem domain(toDict(model)) ==> - ras.ToDict()[k].IsValid(ProductOfSeq(getValAt(k), ras.ToDict()[k]))) -} - -// Returns the sequence of active elements for a given reference. -ghost -requires acc(&inUseIdx) -decreases -pure func getIdxAt(k LocName) seq[idx] { - return idxSeqLookup(inUseIdx, k) -} - -ghost -requires acc(&inUseVal) -decreases -pure func getValAt(k LocName) seq[Elem] { - return valSeqLookup(inUseVal, k) -} - -ghost -decreases -pure func idxSeqLookup(d dict[LocName](seq[idx]), k LocName) seq[idx] { - return k elem domain(d) ? d[k] : seq[idx]{} -} - -ghost -decreases -pure func valSeqLookup(d dict[LocName](seq[Elem]), k LocName) seq[Elem] { - return k elem domain(d) ? d[k] : seq[Elem]{} -} - -// Find the (first) position of x in s. Requires x to be present in s. -ghost -requires x elem s -ensures 0 <= res && res < len(s) -ensures s[res] === x -decreases len(s) -pure func idxPos(s seq[idx], x idx) (res int) { - return (s[0] === x) ? 0 : 1 + idxPos(s[1:], x) -} - -// TODO: use MonoSet and MonoMap for the model; delete cooliosetio and mapio -ghost var model cooliomapio = allocMap() -ghost var ras rasMap = rasMapAlloc() - -// Per-location sequences of currently-in-use idx pointers and their values. -// Maintained in lockstep with the in-use indices in `model`. These are used -// by `GlobalMem()` to state the product-of-all-in-use-values invariant. -ghost var inUseIdx@ dict[LocName](seq[idx]) -ghost var inUseVal@ dict[LocName](seq[Elem]) - -func init() { - fold GlobalMem() -} - -/***** 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) && - w.i.inUse && - 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) && - ras.Witness(l, ra) -} - -/***** 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, w) -decreases -func AllocWI(ra RA, e Elem) (l LocName, w Witness) { - unfold GlobalMem() - - newl := new(int) - 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} - - 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) - 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) - - 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]) ==> - i.inUse ==> (ras.ToDict()[k].IsElem(i.val) && ras.ToDict()[k].IsValid(i.val))) - - inUseIdx[newl] = seq[idx]{iii} - inUseVal[newl] = seq[Elem]{e} - fold 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), w) -ensures GlobalMem() -ensures GhostLocationW(l, ra, e1, w1) && GhostLocationW(l, ra, e2, w2) -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) - - 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) - 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 := 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) - - 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 - - // 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) - - 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].IsValid(ras.ToDict()[k].Compose(i.val, i2.val)))) - - // Replace i.i's slot in the seqs with iii1 (val e1) and append iii2 (val e2). - // i.i is no longer in-use, but by the completeness invariant it was in getIdxAt(l) while still in-use. - posI := idxPos(getIdxAt(l), i.i) - oldVals := getValAt(l) - pre := oldVals[:posI] - post := oldVals[posI+1:] - assert oldVals[posI] === ra.Compose(e1, e2) - assert oldVals === pre ++ seq[Elem]{ra.Compose(e1, e2)} ++ post - ProductSplitEq(pre, post, e1, e2, ra) - inUseIdx[l] = getIdxAt(l)[:posI] ++ seq[idx]{iii1} ++ getIdxAt(l)[posI+1:] ++ seq[idx]{iii2} - inUseVal[l] = pre ++ seq[Elem]{e1} ++ post ++ seq[Elem]{e2} - 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) { - 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)) -} - -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 -requires GlobalMem() -requires ra != nil -requires ra.IsElem(e1) -requires ra.IsElem(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 GhostOp2WI(l LocName, ra RA, e1 Elem, e2 Elem, w1 Witness, w2 Witness) { - i1 := w1 - 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]) ==> - 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) - lemmaWitness(model, l, i1.c, 1/3) - i1.c.lemmaWitness(i1.i, 1/3) - - 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)) - - // Capture seq positions and values BEFORE mutating i1.i.val or i2.i.inUse. - posI1 := idxPos(getIdxAt(l), i1.i) - posI2 := idxPos(getIdxAt(l), i2.i) - pmin, pmax := posI1, posI2 - if posI1 > posI2 { - pmin, pmax = posI2, posI1 - } - oldVals := getValAt(l) - oldIdxs := getIdxAt(l) - assert oldVals[posI1] === e1 - assert oldVals[posI2] === e2 - ProductMergeAt(oldVals, posI1, posI2, ra) - // ProductMergeAt yields IsValid of the merged seq: - // oldVals[:pmin] ++ [Compose(e1,e2)] ++ oldVals[pmin+1:pmax] ++ oldVals[pmax+1:] - - // Discharge: derive `IsValid(Compose(Compose(e1, e2), ii.val))` for any other in-use ii at l. - // By completeness, every in-use i at l appears in inUseIdx[l] (= oldIdxs). - // By distinctness, the positions of i1.i, i2.i, and any third ii are all distinct. - // By IsElem invariant on values, all entries of oldVals are RA elements. - // By the product-validity invariant, ProductOfSeq(oldVals, ra) is valid, so by - // `ExtractThreeValid` (pure, in product.gobra) any triple of values has its triple-Compose valid. - assert forall ii idx :: ii elem toCoolSet(toDict(model)[l]) && ii.inUse && ii !== i1.i && ii != i2.i ==> - let posIi := idxPos(oldIdxs, ii) in - let _ := ExtractThreeValid(oldVals, ra, posI1, posI2, posIi) 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 - fold GhostLocationW(l, ra, ra.Compose(e1, e2), i1) - - 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))) - - 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)) - - inUseVal[l] = oldVals[:pmin] ++ seq[Elem]{ra.Compose(e1, e2)} ++ oldVals[pmin+1:pmax] ++ oldVals[pmax+1:] - inUseIdx[l] = oldIdxs[:pmin] ++ seq[idx]{i1.i} ++ oldIdxs[pmin+1:pmax] ++ oldIdxs[pmax+1:] - - fold GlobalMem() -} - -ghost -requires GlobalMem() -requires ra != nil -requires ra.IsElem(e1) -requires ra.IsElem(e2) -requires GhostLocationW(l, ra, e1, w) -requires IsFramePreservingUpdate(ra, e1, e2) -ensures GlobalMem() -ensures GhostLocationW(l, ra, e2, w) -decreases -func GhostUpdateWI(l LocName, ra RA, e1 Elem, e2 Elem, w Witness) { - i := w - unfold GlobalMem() - - 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)) - - // Capture seq position and apply product FPU lemma BEFORE mutating i.i.val. - posI := idxPos(getIdxAt(l), i.i) - oldVals := getValAt(l) - assert oldVals[posI] === e1 - ProductFPUEq(oldVals, posI, e1, e2, ra) - - i.i.val = e2 - - 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 { - assert exists e Elem :: { ra.IsElem(e) } { LiftedCompose(ra, some(e1), some(e)) } ra.IsElem(e) && - LiftedCompose(ra, some(e1), some(e)) !== none[Elem] - 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)) && - ra.IsValid(ra.Compose(e2, e)) && - ra.IsValid(e2) - } - - 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)) - - // Update inUseVal[l] at i.i's position to the new value e2 using the captured oldVals. - inUseVal[l] = oldVals[:posI] ++ seq[Elem]{e2} ++ oldVals[posI+1:] - - 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 -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 *****/ - -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 deleted file mode 100644 index 3adee1e..0000000 --- a/resalgebraNoAxioms/oneshot.gobra +++ /dev/null @@ -1,119 +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 - -ghost 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{}) -} - -// all of the following properties are proven automatically - -ghost -decreases -pure func (ra TypeOneShotRA) ComposeAssoc(e1 Elem, e2 Elem, e3 Elem) Unit { - // proved - return Unit{} -} - -ghost -decreases -pure func (ra TypeOneShotRA) ComposeComm(e1 Elem, e2 Elem) Unit { - // proved - return Unit{} -} - -ghost -decreases -pure func (ra TypeOneShotRA) CoreId(e Elem) Unit { - // proved - return Unit{} -} - -ghost -decreases -pure func (ra TypeOneShotRA) CoreIdem(e Elem) Unit { - // proved - return Unit{} -} - -ghost -decreases -pure func (ra TypeOneShotRA) CoreMono(e1 Elem, e2 Elem) Unit { - // proved - return Unit{} -} - -ghost -decreases -pure func (ra TypeOneShotRA) ValidOp(e1 Elem, e2 Elem) Unit { - // proved - return Unit{} -} diff --git a/resalgebraNoAxioms/ra.gobra b/resalgebraNoAxioms/ra.gobra deleted file mode 100644 index 8c15f8d..0000000 --- a/resalgebraNoAxioms/ra.gobra +++ /dev/null @@ -1,172 +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 Elem interface{} - -type Unit struct{} - -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 - pure ComposeAssoc(e1 Elem, e2 Elem, e3 Elem) Unit - - ghost - requires IsElem(e1) && IsElem(e2) - ensures Compose(e1, e2) === Compose(e2, e1) - decreases - pure ComposeComm(e1 Elem, e2 Elem) Unit - - ghost - requires IsElem(e) - ensures let c := Core(e) in - c !== none[Elem] ==> Compose(get(c), e) === e - decreases - pure CoreId(e Elem) Unit - - 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 - pure CoreIdem(e Elem) Unit - - 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 - pure CoreMono(e1 Elem, e2 Elem) Unit - - ghost - requires IsElem(e1) && IsElem(e2) - requires IsValid(Compose(e1, e2)) - ensures IsValid(e1) - decreases - 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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -pure func asserting(ghost b bool) Unit { - return Unit{} -}