Promotes gds-proof from a standalone package (Layer 0, protocol-only) to a
Layer 1 package that depends on gds-framework and integrates with the
existing verification infrastructure.
Breaking: ProofableBlock renamed to SymbolicBlock, ProofableModel
renamed to SymbolicModel. Deprecated aliases remain until v1.0.0.
Breaking: analyze_reachability() renamed to analyze_inductive_safety(),
ReachabilityAnalysisResult renamed to InductiveSafetyResult. Deprecated
aliases remain until v1.0.0. This resolves a naming collision with
gds_analysis.reachability (simulation-based forward/backward state sets).
New capabilities:
- gds-framework dependency -- gds-proof is now a Layer 1 package alongside gds-analysis, gds-domains, and gds-viz
GDSSymbolicBlock-- adapter wrappingAtomicBlock+GDSSpecwith user-supplied SymPy expressions. Auto-derivesprev_state_symbolsfromMechanism.updates+Entity.variables[var].symbolGDSSymbolicModel-- adapter wrappingGDSSpecwith symbolic enrichments and invariants. Auto-derives assumption context fromParameterDef.boundsfindings.py-- converts proof results toFinding/VerificationReportobjects. PopulatesFinding.exportable_predicatewith canonical SymPy form. Check ID:PROOF-001(invariant preservation)derive_state_symbols()-- utility to extract SymPy symbols from mechanism updates + entity variable symbolsderive_assumption_context()-- utility to build SymPy assumption dicts from parameter schema bounds
Documentation:
- Added
docs/proof/index.mdanddocs/proof/getting-started.md - Updated
CLAUDE.mdfor Layer 1 architecture - Added gds-proof to mkdocs.yml navigation and llmstxt sections
New package added via PR #193. Extracts the domain-agnostic proof engine from
crypto-econ-dynamics-skill into gds-core as the ninth workspace package.
Capabilities:
- Deterministic SHA-256 model identity (
hash_model,hash_proof) - 5-strategy symbolic implication prover (
analyze_invariants) - 3-layer predicate-guarded reachability (
analyze_reachability) - User-authored multi-lemma ProofScript with independent verification
- Canonical srepr serialization for third-party evidence exchange
112 tests, 95% coverage.
Implements the consolidation plan from issue #143. Reduces the monorepo from 14 independently published packages to 8, eliminating the N^2 integration problem and simplifying user installation.
-
gds-domains v0.1.0 — consolidates all 6 domain DSLs (stockflow, control, business, software, games, symbolic) into a single package with optional extras. Install what you need:
pip install gds-domains[games,symbolic]. Import paths:from gds_domains.stockflow import StockFlowModel, etc. -
gds-interchange v0.1.0 — replaces gds-owl as a broader interchange hub. OWL/RDF functionality lives at
gds_interchange.owl. Future bridges (SysML, FMI, SBML) will land as additional subpackages.
- gds-analysis v0.2.0 — absorbs gds-psuu. PSUU functionality is now at
gds_analysis.psuu. Install withpip install gds-analysis[psuu]for Optuna.
The following packages now re-export from their consolidated locations with a
DeprecationWarning. They will be removed in v0.3.0:
gds-owl→ usegds-interchange(from gds_interchange.owl import ...)gds-psuu→ usegds-analysis(from gds_analysis.psuu import ...)gds-stockflow→ usegds-domains(from gds_domains.stockflow import ...)gds-control→ usegds-domains(from gds_domains.control import ...)gds-business→ usegds-domains(from gds_domains.business import ...)gds-software→ usegds-domains(from gds_domains.software import ...)gds-games→ usegds-domains(from gds_domains.games import ...)gds-symbolic→ usegds-domains(from gds_domains.symbolic import ...)
gds-framework��� core engine (no changes)gds-sim— discrete-time simulation (standalone, no changes)gds-continuous— continuous-time ODE engine (standalone, no changes)gds-viz— visualization (no changes)gds-examples— updated imports to usegds_domains.*
Replace old imports with new paths:
# Before
from stockflow import StockFlowModel
from gds_control import ControlModel
from ogs import OpenGame
from gds_owl import spec_to_graph
# After
from gds_domains.stockflow import StockFlowModel
from gds_domains.control import ControlModel
from gds_domains.games import OpenGame
from gds_interchange.owl import spec_to_graphOld imports continue to work with a deprecation warning until v0.3.0.
Driven by external reviews from Zargham and Jamsheed (Shorish) against the GDS paper (Zargham & Shorish 2022). The reviews identified foundational gaps in notation alignment, formal property statements, ControlAction semantics, temporal agnosticism documentation, and execution contract formalization. This release closes all Tier 0 and Tier 1 roadmap items.
Breaking: CanonicalGDS.input_ports now contains only controlled inputs (U_c);
disturbance-tagged BoundaryAction ports are in the new disturbance_ports field.
New capabilities:
- ExecutionContract — DSL-layer time model declaration (
discrete,continuous,event,atemporal) with Moore/Mealy ordering. Attached as optional field on GDSSpec. A spec without a contract remains valid for structural verification. - ControlAction canonical projection —
CanonicalGDSnow extracts output ports (Y) and renders the output mapy = C(x, d)in the formula. - Disturbance input partition —
disturbance_portsonCanonicalGDSseparates policy-bypassing exogenous inputs (W) from controlled inputs (U_c) viatags={"role": "disturbance"}on BoundaryAction. - TypeDef.constraint_kind — optional named constraint pattern (
non_negative,positive,probability,bounded,enum) enabling round-trip export via SHACL.
New verification checks:
- SC-010 — ControlAction outputs must not feed the g pathway (Policy/BoundaryAction)
- SC-011 — ExecutionContract well-formedness
- DST-001 — Disturbance-tagged BoundaryAction must not wire to Policy
Documentation:
- Formal property statements for all 15 core checks (G-001..G-006, SC-001..SC-009)
- Requirement traceability markers on all verification tests
- Tests for SC-005..SC-009 (previously untested)
- Controller-plant duality design document
- Temporal agnosticism invariant with three-layer stack diagram
- Audit of 30+ docs replacing "timestep" with temporally neutral vocabulary
- Assurance claims document with verification passport template
- Execution semantics design document with DSL contract mapping
- Disturbance formalization design document
- Notation harmonized with Zargham & Shorish (2022)
- SHACL constraint promotion —
TypeDef.constraint_kindmetadata exports as SHACL property shapes (sh:minInclusive,sh:maxInclusive,sh:minExclusive,sh:in). Constraints with aconstraint_kindare now R2 round-trippable; those without remain R3 lossy. Import reconstructs Python callable constraints from SHACL metadata. - New ontology properties:
constraintKind,constraintLow,constraintHigh,constraintValue - New
build_constraint_shapes()public API
- Parameter schema validation —
ParameterSpace.from_parameter_schema()creates sweep dimensions from declared ParameterDef entries.validate_against_schema()catches missing params, type mismatches, and out-of-bounds sweeps. - PSUU-001 check following the GDS Finding pattern
- Sweep runner validates against schema when
parameter_schemais provided
- Emit
ExecutionContract(time_domain="discrete")fromcompile_model()
- Emit
ExecutionContract(time_domain="discrete")fromcompile_model()
- Emit
ExecutionContract(time_domain="atemporal")fromcompile_pattern_to_spec()
- Emit
ExecutionContractfrom all 6 compilers:atemporalfor DFD, C4, component, ERD, dependency;discretefor state machines
- Emit
ExecutionContractfrom all 3 compilers:discretefor CLD and supply chain,atemporalfor value stream maps
- Guard
gds-continuousimport inbackward_reachability.py(previously caused ImportError when gds-continuous wasn't installed)
- Add
StructuralWiringto public API (compiler intermediate for domain DSL wiring emitters) - Switch to dynamic versioning —
__version__in__init__.pyis the single source of truth - Tighten
gds-framework>=0.2.3lower bound across all dependent packages
- Add canonical bridge (
compile_pattern_to_spec) — projects OGS patterns toGDSSpec - Add view stratification architecture
- Require
gds-framework>=0.2.3
- Initial release — declarative stock-flow DSL over GDS semantics
- Initial release — state-space control DSL over GDS semantics
- Mermaid renderers for structural, canonical, architecture, parameter, and traceability views