Defines storage semantics, evidence/provenance, and orchestration surface.
Defines Core vs Packs, explicit loading, and deprecating “eval-only theory creep”.
Deterministic compilation to SMT-LIB2 (v0 fragment) as URC artifacts.
Capability registry + fragments + orchestration strategy across solver families.
| Step | Read | Why |
|---|---|---|
| 1 | DS03, DS26 | Current runtime boundaries (Session, universes, IoC) and where URC fits. |
| 2 | DS49 | Defines the semantics: dual-store, policy-driven current view, evidence hooks. |
| 3 | DS51 | Defines how configuration evolves (Core code vs explicit packs). |
| 4 | DS50 | First deterministic “externalizable” artifact path (compilation as evidence). |
| 5 | DS52 + DS53–DS72 | Roadmap for solver backends and orchestration tactics. |
| 6 | DS48 | Tooling surface: how developers inspect URC objects and evidence. |
This is an implementation-ordered walk through the DS documents. Each phase is intended to be independently testable and mergeable.
| Phase | DS scope | Implementation goal | Definition of done |
|---|---|---|---|
| 0 | DS03, DS26 | Establish the “runtime core” boundary and ensure Session isolation is stable. | Clear API boundaries; no implicit always-on semantic packs. |
| 1 | DS51 | Make pack loading explicit in all critical paths (runtime + evals + tooling). | Kernel/URC packs are loaded intentionally (no hidden dependencies). |
| 2 | DS49 | Introduce URC dual-store semantics: persisted facts vs derived indices. | Indices are rebuildable; persisted store is authoritative for proofs/queries. |
| 3 | DS49, DS34 | Add Evidence + Provenance objects and a minimal artifact lifecycle. | Every non-trivial result can attach a provenance chain and evidence links. |
| 4 | DS49, DS52 | Add a minimal capability registry + backend selection interface. | Backends declare supported fragments; orchestrator can route a request. |
| 5 | DS50 | Implement deterministic compilation for a small fragment (SMT-LIB2 v0). | Compilation output is stable-hashable and recorded as an artifact. |
| 6 | DS53–DS72 | Add one backend adapter at a time (SAT/SMT/CP/MC/…) | Each backend has a smoke test and produces evidence artifacts. |
| 7 | DS48 | Upgrade KBExplorer to inspect URC objects: Goals, Evidence, Policy views. | Developers can browse persisted facts vs indices and audit artifacts. |
Next: consider aligning evaluation harnesses to explicitly load packs and record artifacts as URC Evidence objects.