diff --git a/.zenodo.json b/.zenodo.json index b36710a..1f58a4f 100644 --- a/.zenodo.json +++ b/.zenodo.json @@ -1,6 +1,6 @@ { - "title": "RSH v4.0.0: Epistemic and Conformance Governance for Deterministic Robitaille–Slade Helix Evidence", - "description": "RSH v4.0.0 adds RSH-EPISTEMIC-V1 and RSH-CONFORMANCE-V1: machine-readable evidence/claim classification, explicit runtime identity, no-silent-fallback rules, deterministic SHA-256 experiment receipts, and a sealed Python/Rust cross-runtime governance vector. The v3.0.0 Lean theorem surface RSH-FORMAL-V1, geometry model contract 2.0.0, tissue contract 1.0.0, and scientific authority hierarchy remain unchanged. GLUBALL integration is deliberately deferred to a later additive release.", + "title": "RSH v4.1.0: Additive GLUBALL Lean 4 Formalization for the Robitaille–Slade Helix Evidence Framework", + "description": "RSH v4.1.0 adds the separately versioned theorem surface RSH-GLUBALL-FORMAL-V1, pinned to RSH v4.0.0 and GLUBALL v1.0.0. Lean 4 machine-checks the frozen GLUBALL parameter inequalities, componentwise derivative linkage to the declared centreline, squared-speed positivity and regularity, host-torus normal and frame orthogonality, tube-radius invariance, tube-angle periodicity, centreline closure, exact C3 rotational symmetry, uniform-floor sampling bounds, and mesh-index wrap bounds. The existing RSH-FORMAL-V1 theorem surface and the RSH-EPISTEMIC-V1 / RSH-CONFORMANCE-V1 governance contracts remain intact. The release does not claim global thick-tube embeddedness, IEEE-754 or browser/runtime identity, accelerator correctness beyond declared conformance surfaces, or empirical physical, biological, consciousness, sentience, or qualia validation.", "upload_type": "software", "creators": [ {"name": "Dr. J. Robitaille"}, @@ -9,22 +9,26 @@ "contributors": [ {"name": "ChatGPT 5.6 Sol", "type": "Other", "affiliation": "OpenAI"} ], - "version": "4.0.0", + "version": "4.1.0", "license": "MPL-2.0", "keywords": [ "Robitaille-Slade Helix", - "epistemic governance", - "deterministic evidence", - "cross-runtime conformance", - "no silent fallback", - "SHA-256 receipts", + "GLUBALL", + "RSH-GLUBALL-FORMAL-V1", "Lean 4", "formal verification", + "torus-curve geometry", + "C3 rotational symmetry", + "deterministic sampling", + "epistemic governance", + "cross-runtime conformance", + "deterministic evidence", "Frenet-Serret", "curvature", "torsion" ], "related_identifiers": [ - {"identifier": "https://github.com/QSOLKCB/RSH", "relation": "isSupplementTo", "scheme": "url"} + {"identifier": "https://github.com/QSOLKCB/RSH", "relation": "isSupplementTo", "scheme": "url"}, + {"identifier": "https://github.com/QSOLKCB/GLUBALL/releases/tag/v1.0.0", "relation": "references", "scheme": "url"} ] } diff --git a/CITATION.cff b/CITATION.cff index a35e0d2..d04769d 100644 --- a/CITATION.cff +++ b/CITATION.cff @@ -1,7 +1,7 @@ cff-version: 1.2.0 message: "If you use RSH, please cite this software." title: "RSH: Robitaille–Slade Helix Geometry and Evidence Runner" -version: 4.0.0 +version: 4.1.0 type: software authors: - family-names: Robitaille @@ -22,6 +22,10 @@ keywords: - SHA-256 receipts - Lean 4 - formal verification + - RSH-FORMAL-V1 + - RSH-GLUBALL-FORMAL-V1 + - GLUBALL + - torus-curve geometry - exact rational geometry - Sierpinski inversive witness - geometric tissue diff --git a/Cargo.lock b/Cargo.lock index b356cc0..2f98913 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -94,7 +94,7 @@ dependencies = [ [[package]] name = "rsh-cli" -version = "4.0.0" +version = "4.1.0" dependencies = [ "rsh-core", "serde_json", @@ -102,7 +102,7 @@ dependencies = [ [[package]] name = "rsh-core" -version = "4.0.0" +version = "4.1.0" dependencies = [ "serde", "serde_json", @@ -111,14 +111,14 @@ dependencies = [ [[package]] name = "rsh-ffi" -version = "4.0.0" +version = "4.1.0" dependencies = [ "rsh-core", ] [[package]] name = "rsh-governance" -version = "4.0.0" +version = "4.1.0" dependencies = [ "serde", "serde_json", @@ -127,7 +127,7 @@ dependencies = [ [[package]] name = "rsh-numerics" -version = "4.0.0" +version = "4.1.0" dependencies = [ "rsh-core", "serde", @@ -136,7 +136,7 @@ dependencies = [ [[package]] name = "rsh-numerics-cli" -version = "4.0.0" +version = "4.1.0" dependencies = [ "rsh-core", "rsh-numerics", @@ -145,7 +145,7 @@ dependencies = [ [[package]] name = "rsh-numerics-wasm" -version = "4.0.0" +version = "4.1.0" dependencies = [ "rsh-core", "rsh-numerics", @@ -155,7 +155,7 @@ dependencies = [ [[package]] name = "rsh-parallel" -version = "4.0.0" +version = "4.1.0" dependencies = [ "rsh-core", "serde", @@ -164,7 +164,7 @@ dependencies = [ [[package]] name = "rsh-parallel-cli" -version = "4.0.0" +version = "4.1.0" dependencies = [ "rsh-core", "rsh-parallel", @@ -173,7 +173,7 @@ dependencies = [ [[package]] name = "rsh-parallel-wasm" -version = "4.0.0" +version = "4.1.0" dependencies = [ "rsh-core", "rsh-parallel", @@ -183,7 +183,7 @@ dependencies = [ [[package]] name = "rsh-tissue" -version = "4.0.0" +version = "4.1.0" dependencies = [ "rsh-core", "serde", @@ -193,7 +193,7 @@ dependencies = [ [[package]] name = "rsh-tissue-cli" -version = "4.0.0" +version = "4.1.0" dependencies = [ "rsh-tissue", "serde_json", @@ -201,7 +201,7 @@ dependencies = [ [[package]] name = "rsh-tissue-wasm" -version = "4.0.0" +version = "4.1.0" dependencies = [ "rsh-tissue", "serde", @@ -210,7 +210,7 @@ dependencies = [ [[package]] name = "rsh-wasm" -version = "4.0.0" +version = "4.1.0" dependencies = [ "rsh-core", "serde", diff --git a/Cargo.toml b/Cargo.toml index a60cf42..c0a3ca2 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -18,7 +18,7 @@ members = [ resolver = "2" [workspace.package] -version = "4.0.0" +version = "4.1.0" edition = "2021" license = "MPL-2.0" repository = "https://github.com/QSOLKCB/RSH" diff --git a/FORMALIZATION.md b/FORMALIZATION.md index dc1ebdd..b5159ab 100644 --- a/FORMALIZATION.md +++ b/FORMALIZATION.md @@ -14,6 +14,8 @@ RSH-GLUBALL-FORMAL-V1 The two surfaces coexist. The GLUBALL work does **not** replace, reinterpret, or weaken `RSH-FORMAL-V1`. +`RSH-GLUBALL-FORMAL-V1` is packaged for archival release in RSH v4.1.0. The release number is software/archive metadata; the theorem-surface identifiers remain the authority boundary for the propositions Lean actually checks. + ## Authors and contribution - **Dr. J. Robitaille** — author @@ -91,7 +93,7 @@ and C(t)=(A(t)\cos(pt),A(t)\sin(pt),r\sin(qt)), \] -Lean formalizes the declared derivative and proves the squared-speed identity +Lean formalizes the declared derivative, proves `HasDerivAt` for each centreline component, and therefore connects the closed-form derivative to the actual curve rather than treating it as an independent trusted definition. It also proves the squared-speed identity \[ \|C'(t)\|^2=p^2A(t)^2+q^2r^2. diff --git a/README.md b/README.md index 2cba355..d0a6251 100644 --- a/README.md +++ b/README.md @@ -7,19 +7,19 @@ inside explicit Robitaille bounds, integrating the Frenet–Serret frame, and translating the exact discrete midpoint to the coordinate origin. **Authors:** J. Robitaille (DeltaKingZero) and Trent Slade / QSOL-IMC -**Release:** 4.0.0 -**Implementations:** Python geometry oracle, tissue reference, and v4 governance reference + Rust geometry/tissue/governance cores and CLIs + canonical geometry and tissue WASM bridges + WGSL schedule field + versioned C ABI/C++ adapter + optional CUDA schedule kernel + Tier 2 NPU evidence profile + separate Rust/WASM/WGSL full-path and parallel-prefix research stacks +**Release:** 4.1.0 +**Implementations:** Python geometry oracle, tissue reference, and v4 governance reference + Rust geometry/tissue/governance cores and CLIs + canonical geometry and tissue WASM bridges + WGSL schedule field + versioned C ABI/C++ adapter + optional CUDA schedule kernel + Tier 2 NPU evidence profile + separate Rust/WASM/WGSL full-path and parallel-prefix research stacks + additive Lean 4 GLUBALL theorem surface ## Contract and interface versions | Surface | Version / identifier | |---|---| -| RSH software release / workspace crates | `4.0.0` | +| RSH software release / workspace crates | `4.1.0` | | Geometry model contract | `2.0.0` | | Tissue contract | `1.0.0` | | Epistemic governance contract | `RSH-EPISTEMIC-V1` | | Conformance governance contract | `RSH-CONFORMANCE-V1` | -| Lean theorem surface | `RSH-FORMAL-V1` (unchanged from v3.0.0) | +| Lean theorem surfaces | `RSH-FORMAL-V1` + additive `RSH-GLUBALL-FORMAL-V1` | | Frenet numerical research contract | `1.0.0` / `RSH-FRENET-NUMERICS-V1` | | Parallel Frenet research contract | `RSH-FRENET-PARALLEL-V1` | | Geometry, numerical, parallel, and tissue raw WASM ABIs | `1` | @@ -47,10 +47,19 @@ vector in `conformance/rsh_v4_governance_vector_v1.json`. See [`docs/V4_GOVERNANCE.md`](docs/V4_GOVERNANCE.md) and the normative contracts in [`contracts/`](contracts/). -GLUBALL is deliberately **not** integrated in v4.0.0. After v4 is merged, -validated, and tagged, a later additive release may pin GLUBALL v1.0.0 and add -`RSH-GLUBALL-FORMAL-V1` without replacing the Robitaille–Slade helix or -`RSH-FORMAL-V1`. +## GLUBALL integration + +RSH v4.1.0 adds `RSH-GLUBALL-FORMAL-V1` as a separate Lean theorem surface pinned +to GLUBALL v1.0.0 at commit +`80941183d14531093117e122da0fc32c13d2464b`. The integration is additive: it +does not replace or reinterpret the Robitaille–Slade helix or `RSH-FORMAL-V1`. + +The theorem-facing GLUBALL modules prove exact parameter admissibility, +componentwise derivative linkage, squared-speed regularity, host-torus frame +properties, the tube-radius invariant, centreline closure, exact C3 rotational +symmetry, and deterministic uniform-floor sampling/index bounds. The browser +renderer remains outside mathematical authority, and global thick-tube +embeddedness remains an explicit nonclaim. ## Browser laboratories @@ -661,6 +670,7 @@ crates/rsh-parallel-wasm/ Parallel-prefix raw WASM ABI crates/rsh-tissue/ Shared Rust tissue runtime crates/rsh-tissue-cli/ Native tissue runner and conformance CLI crates/rsh-tissue-wasm/ Raw tissue WASM ABI over `rsh-tissue` +formal/lean/RSH/Gluball/ Additive RSH-GLUBALL-FORMAL-V1 theorem modules contracts/ Machine-readable v4 epistemic/conformance contracts release/ Machine-readable release manifests include/rsh_ffi.h Public ABI-v1 C/C++ header @@ -731,7 +741,7 @@ theory, biological organism, consciousness, or subjective experience. 9. **Single-device parallel Frenet research** — implemented under `RSH-FRENET-PARALLEL-V1` with native Rust, compiled WASM, multi-pass WGSL, complete readback, and scoped benchmark policy. 10. **Lean 4 theorem surface** — frozen in v3.0.0 as `RSH-FORMAL-V1`. 11. **Epistemic and conformance governance** — implemented in v4.0.0 as `RSH-EPISTEMIC-V1` and `RSH-CONFORMANCE-V1`. -12. **GLUBALL integration** — next additive release after the v4.0.0 tag; planned theorem surface `RSH-GLUBALL-FORMAL-V1`. +12. **GLUBALL integration** — implemented additively in v4.1.0 as `RSH-GLUBALL-FORMAL-V1`, pinned to GLUBALL v1.0.0. 13. **Multi-device and distributed parallel execution** — future research; current shard summaries provide ordered deterministic groundwork only. Performance, compositional complexity, anthropomorphic language, or a visually diff --git a/RELEASE_NOTES_v4.1.0.md b/RELEASE_NOTES_v4.1.0.md new file mode 100644 index 0000000..e30e835 --- /dev/null +++ b/RELEASE_NOTES_v4.1.0.md @@ -0,0 +1,119 @@ +# RSH v4.1.0 — GLUBALL Machine-Checked Geometry + +RSH v4.1.0 adds the additive Lean theorem surface `RSH-GLUBALL-FORMAL-V1` while preserving the existing Robitaille–Slade theorem surface, geometry contracts, governance contracts, numerical research contracts, and implementation authority boundaries. + +This release is pinned to: + +- RSH v4.0.0: `79b8481639fb4187c41035de4e707545db93f59a` +- GLUBALL v1.0.0: `80941183d14531093117e122da0fc32c13d2464b` +- merged GLUBALL formalization: `124af8283dd69f78031d3a92249fdd7ea4a60508` + +## New theorem surface + +The new theorem surface is: + +```text +RSH-GLUBALL-FORMAL-V1 +``` + +It coexists with, and does not replace or reinterpret: + +```text +RSH-FORMAL-V1 +``` + +The GLUBALL theorem modules live under `formal/lean/RSH/Gluball/` and are included in the existing proof-hole, project-axiom, build, and axiom-report audit. + +## Machine-checked results + +For the frozen GLUBALL `(2,3)` torus-curve contract with exact rational parameters corresponding to `R = 2.10`, `r = 0.85`, `rho = 0.34`, `p = 2`, and `q = 3`, Lean checks: + +- exact parameter admissibility; +- the declared centreline and its componentwise derivatives; +- `HasDerivAt` linkage between the declared derivative and the actual centreline coordinates; +- the exact squared-speed identity; +- strict positivity of squared speed and non-vanishing derivative; +- host-torus normal unit norm; +- tangent/normal orthogonality; +- normalized tangent and binormal unit-norm properties; +- pairwise frame orthogonality; +- the exact squared tube-radius invariant; +- periodicity in the tube-angle coordinate; +- centreline closure; +- exact C3 rotational symmetry; +- exact uniform-floor sampling bounds; +- adjacent rendered-sample collision freedom when rendered cardinality does not exceed logical cardinality; +- finite `96 × 18` mesh-index wrap bounds. + +## Derivative linkage hardening + +The formalization does not merely define a vector and call it the derivative. Following review, the Lean development proves `radial_hasDerivAt`, the x/y/z centreline component derivative theorems, `centerline_hasComponentDerivAt`, and `centerline_regular_componentwise`. + +This closes the gap between the written closed-form derivative and the actual curve being formalized. + +## Audit provenance hardening + +The theorem audit retains the immutable RSH v4 base pin and additionally records the actual audited source revision and workflow checkout revision. Pull-request workflows pass the PR head SHA explicitly so a synthetic GitHub merge ref cannot obscure which source revision was audited. + +The audit continues to reject: + +- `sorry`; +- `admit`; +- project-defined `axiom` declarations; +- project-defined `constant` declarations. + +Lean remains pinned to 4.32.1 and Mathlib remains pinned to commit `520045ab14e26149ee970e2e617ca04b09bde5d6`. + +## Preserved governance and scientific authority + +RSH v4.1.0 preserves: + +- geometry model contract `2.0.0`; +- tissue contract `1.0.0`; +- `RSH-FORMAL-V1`; +- `RSH-EPISTEMIC-V1`; +- `RSH-CONFORMANCE-V1`; +- `RSH-FRENET-NUMERICS-V1`; +- `RSH-FRENET-PARALLEL-V1`; +- the Python geometry oracle; +- runtime-specific conformance and accelerator residual-sidecar boundaries. + +The GLUBALL browser renderer is not promoted to mathematical authority. + +## Deliberate nonclaims + +This release does not claim that Lean has proved: + +- global thick-tube embeddedness or non-self-intersection; +- IEEE-754 or binary64 equivalence across runtimes; +- bit-identical browser rendering; +- GPU, WASM, Android, CUDA, WebGPU, or NPU implementation correctness outside their declared conformance surfaces; +- experimental or empirical physics; +- biological interpretation; +- consciousness, sentience, subjective awareness, or qualia; +- ternary/triality topology. + +A proof receipt certifies the proposition checked by Lean. It does not silently become an empirical measurement. + +## Release and archival metadata + +The Python package and Rust workspace advance to `4.1.0`. `CITATION.cff`, `.zenodo.json`, and `release/manifest-v4.1.0.json` describe the additive formalization and preserve the exact RSH/GLUBALL source boundaries. + +The v4.1.0 tag must resolve to the final merge commit containing the release manifest after portable CI and the Lean theorem audit are green. + +## Reproduce the theorem audit + +```bash +cd formal/lean +lake update +lake exe cache get +bash audit.sh +``` + +## Authors and contribution + +- **Dr. J. Robitaille** — author +- **Trent Slade** — author +- **ChatGPT 5.6 Sol** — contributor (formalization implementation and proof-engineering assistance) + +The AI contribution is recorded as a contributor role rather than a human creator/author. diff --git a/pyproject.toml b/pyproject.toml index 9657bdb..cdd32d5 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -4,8 +4,8 @@ build-backend = "setuptools.build_meta" [project] name = "rsh-geometry" -version = "4.0.0" -description = "Bounded Frenet-Serret geometry, deterministic evidence, epistemic governance, cross-runtime conformance, and Lean 4 formal verification" +version = "4.1.0" +description = "Bounded Frenet-Serret geometry, deterministic evidence, epistemic governance, cross-runtime conformance, and additive Lean 4 formal verification including RSH-GLUBALL-FORMAL-V1" readme = "README.md" requires-python = ">=3.10" license = {text = "MPL-2.0"} @@ -13,7 +13,7 @@ authors = [ {name = "Dr. J. Robitaille"}, {name = "Trent Slade", email = "qsolimc@users.noreply.github.com"}, ] -keywords = ["geometry", "frenet-serret", "deterministic", "verification", "epistemic-governance", "conformance", "formal-verification", "lean4", "helix", "tissue-simulation", "functional-cohesion", "constitutional-governance", "rust-tissue", "tissue-conformance", "webassembly", "webgpu", "wgsl", "ffi", "cpp", "cuda", "npu", "hardware-validation", "lie-group-integration", "fuzz-testing", "gpu-path-integration"] +keywords = ["geometry", "frenet-serret", "deterministic", "verification", "epistemic-governance", "conformance", "formal-verification", "lean4", "gluball", "torus-curve", "helix", "tissue-simulation", "functional-cohesion", "constitutional-governance", "rust-tissue", "tissue-conformance", "webassembly", "webgpu", "wgsl", "ffi", "cpp", "cuda", "npu", "hardware-validation", "lie-group-integration", "fuzz-testing", "gpu-path-integration"] classifiers = [ "Programming Language :: Python :: 3", "Programming Language :: Python :: 3 :: Only", diff --git a/release/manifest-v4.1.0.json b/release/manifest-v4.1.0.json new file mode 100644 index 0000000..a64a5e9 --- /dev/null +++ b/release/manifest-v4.1.0.json @@ -0,0 +1,68 @@ +{ + "schema": "rsh-release-manifest/1", + "release": { + "version": "4.1.0", + "tag": "v4.1.0", + "status": "release-ready", + "base_release": "v4.0.0", + "base_release_commit": "79b8481639fb4187c41035de4e707545db93f59a", + "formalization_merge_commit": "124af8283dd69f78031d3a92249fdd7ea4a60508", + "tag_target_rule": "v4.1.0 must resolve to the merge commit containing this manifest after portable CI and the Lean theorem audit pass" + }, + "software_versions": { + "python_package": "4.1.0", + "rust_workspace": "4.1.0" + }, + "theorem_surfaces": { + "preserved": "RSH-FORMAL-V1", + "additive": "RSH-GLUBALL-FORMAL-V1" + }, + "preserved_contracts": { + "geometry_model": "2.0.0", + "tissue_contract": "1.0.0", + "epistemic_governance": "RSH-EPISTEMIC-V1", + "conformance_governance": "RSH-CONFORMANCE-V1", + "frenet_numerics": "RSH-FRENET-NUMERICS-V1", + "parallel_frenet": "RSH-FRENET-PARALLEL-V1" + }, + "gluball_source": { + "release": "v1.0.0", + "commit": "80941183d14531093117e122da0fc32c13d2464b", + "integration_mode": "additive-formal-theorem-surface", + "browser_renderer_is_mathematical_authority": false + }, + "formal_environment": { + "lean": "4.32.1", + "mathlib_commit": "520045ab14e26149ee970e2e617ca04b09bde5d6", + "proof_holes_allowed": false, + "project_defined_axioms_allowed": false + }, + "machine_checked_scope": [ + "exact GLUBALL parameter admissibility", + "componentwise derivative linkage for the declared centreline derivative", + "squared-speed identity and regularity", + "host-torus unit normal and tangent orthogonality", + "normalized tangent/binormal frame properties", + "exact squared tube-radius invariant", + "tube-angle periodicity", + "centreline closure", + "exact C3 rotational symmetry", + "uniform-floor sampling bounds and adjacent collision freedom", + "finite mesh-index wrap bounds" + ], + "claim_boundaries": { + "global_thick_tube_embeddedness_proved": false, + "ieee754_runtime_identity_proved": false, + "browser_render_identity_proved": false, + "gpu_wasm_android_correctness_proved": false, + "empirical_physics_validated": false, + "biological_interpretation_validated": false, + "consciousness_sentience_qualia_validated": false, + "ternary_triality_topology_proved": false + }, + "archive_metadata": { + "zenodo_file": ".zenodo.json", + "citation_file": "CITATION.cff", + "release_notes": "RELEASE_NOTES_v4.1.0.md" + } +} diff --git a/tests/test_release_v4_1_0.py b/tests/test_release_v4_1_0.py new file mode 100644 index 0000000..10cb6ba --- /dev/null +++ b/tests/test_release_v4_1_0.py @@ -0,0 +1,80 @@ +import json +import re +import unittest +from pathlib import Path + +ROOT = Path(__file__).resolve().parents[1] +VERSION = "4.1.0" +RSH_V4_COMMIT = "79b8481639fb4187c41035de4e707545db93f59a" +FORMALIZATION_MERGE_COMMIT = "124af8283dd69f78031d3a92249fdd7ea4a60508" +GLUBALL_V1_COMMIT = "80941183d14531093117e122da0fc32c13d2464b" + + +def _read(path: str) -> str: + return (ROOT / path).read_text(encoding="utf-8") + + +class ReleaseV410Test(unittest.TestCase): + def test_release_versions_are_synchronized(self): + self.assertIn('version = "4.1.0"', _read("pyproject.toml")) + self.assertIn('[workspace.package]\nversion = "4.1.0"', _read("Cargo.toml")) + self.assertIn("version: 4.1.0", _read("CITATION.cff")) + self.assertIn("**Release:** 4.1.0", _read("README.md")) + + lock = _read("Cargo.lock") + local_packages = re.findall( + r'\[\[package\]\]\nname = "(rsh-[^"]+)"\nversion = "([^"]+)"', + lock, + ) + self.assertTrue(local_packages) + self.assertEqual({version for _, version in local_packages}, {VERSION}) + + def test_archive_metadata_describes_gluball_formalization(self): + zenodo = json.loads(_read(".zenodo.json")) + self.assertEqual(zenodo["version"], VERSION) + self.assertIn("RSH-GLUBALL-FORMAL-V1", zenodo["description"]) + self.assertIn("RSH-GLUBALL-FORMAL-V1", zenodo["keywords"]) + + citation = _read("CITATION.cff") + self.assertIn("RSH-FORMAL-V1", citation) + self.assertIn("RSH-GLUBALL-FORMAL-V1", citation) + + def test_release_manifest_pins_frozen_boundaries(self): + manifest = json.loads(_read("release/manifest-v4.1.0.json")) + self.assertEqual(manifest["release"]["version"], VERSION) + self.assertEqual(manifest["release"]["tag"], "v4.1.0") + self.assertEqual(manifest["release"]["status"], "release-ready") + self.assertEqual(manifest["release"]["base_release_commit"], RSH_V4_COMMIT) + self.assertEqual( + manifest["release"]["formalization_merge_commit"], + FORMALIZATION_MERGE_COMMIT, + ) + self.assertEqual(manifest["gluball_source"]["commit"], GLUBALL_V1_COMMIT) + self.assertEqual( + manifest["theorem_surfaces"], + { + "preserved": "RSH-FORMAL-V1", + "additive": "RSH-GLUBALL-FORMAL-V1", + }, + ) + self.assertEqual(manifest["preserved_contracts"]["geometry_model"], "2.0.0") + self.assertEqual( + manifest["preserved_contracts"]["epistemic_governance"], + "RSH-EPISTEMIC-V1", + ) + self.assertEqual( + manifest["preserved_contracts"]["conformance_governance"], + "RSH-CONFORMANCE-V1", + ) + + def test_release_notes_and_readme_expose_additive_surface(self): + notes = _read("RELEASE_NOTES_v4.1.0.md") + readme = _read("README.md") + self.assertIn("RSH-GLUBALL-FORMAL-V1", notes) + self.assertIn(FORMALIZATION_MERGE_COMMIT, notes) + self.assertIn("RSH-GLUBALL-FORMAL-V1", readme) + self.assertIn("GLUBALL integration", readme) + + +if __name__ == "__main__": + unittest.main() diff --git a/tests/test_v4_release_contract.py b/tests/test_v4_release_contract.py index f628dd6..ff53bda 100644 --- a/tests/test_v4_release_contract.py +++ b/tests/test_v4_release_contract.py @@ -24,13 +24,12 @@ def test_machine_contracts_and_manifest_align(self) -> None: self.assertEqual(vector["contracts"]["epistemic"], epistemic["contract"]) self.assertEqual(vector["contracts"]["conformance"], conformance["contract"]) - def test_software_versions_are_v4_without_bumping_geometry_contract(self) -> None: - pyproject = (ROOT / "pyproject.toml").read_text() - cargo = (ROOT / "Cargo.toml").read_text() + def test_v4_manifest_preserves_software_and_geometry_boundary(self) -> None: + manifest = json.loads((ROOT / "release/manifest-v4.0.0.json").read_text()) constants = (ROOT / "src/rsh/constants.py").read_text() rust_core = (ROOT / "crates/rsh-core/src/lib.rs").read_text() - self.assertRegex(pyproject, r'(?m)^version = "4\.0\.0"$') - self.assertRegex(cargo, r'(?m)^version = "4\.0\.0"$') + self.assertEqual(manifest["implementation"]["python_package_version"], "4.0.0") + self.assertEqual(manifest["implementation"]["rust_workspace_version"], "4.0.0") self.assertIn('VERSION: str = "2.0.0"', constants) self.assertIn('MODEL_VERSION: &str = "2.0.0"', rust_core)