Replace resalgebra with resalgebraNoAxioms

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 |

resalgebraNoAxioms/CLAUDE.md → 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
 

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{}
 }

resalgebraNoAxioms/cooliomapio.gobra → 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

resalgebraNoAxioms/cooliosetio.gobra → 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

resalgebraNoAxioms/doc.gobra → 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)`