# proposal/13-package-system.md · versecafe/strata [View on GitCafe](https://git.cafe/versecafe/strata/blob/767e62307e55eabc137ef32eacc8018b03dda842/proposal/13-package-system.md) Repository: [versecafe/strata](https://git.cafe/versecafe/strata) Visibility: public Requested revision: 767e62307e55eabc137ef32eacc8018b03dda842 Requested commit: 767e62307e55eabc137ef32eacc8018b03dda842 Commit: 767e62307e55eabc137ef32eacc8018b03dda842 Blob: e66af619808972b9756710fe37ce7727c7014f75 Size: 10884 bytes [Immutable source](https://git.cafe/versecafe/strata/blob/767e62307e55eabc137ef32eacc8018b03dda842/proposal/13-package-system.md?format=markdown) ```` # Package and Module System (working name: forge) How Strata code is organized, named, versioned, exchanged, and trusted. Principles in force: P-6 (reproducibility extends to resolution), P-7 (imported claims carry evidence), P-1 (imported risk is explicit). Builds directly on component summaries ([07 §6](07-compiler-architecture.md)), the evidence lattice ([06 §3](06-refinements-and-evidence.md), D-017), editions and config coverage (D-042, D-043). ## Why this is load-bearing, not plumbing SystemVerilog has no module system in any modern sense: textual `include`, a global namespace, preprocessor macros as the composition mechanism, and IP exchange conducted as zip files plus integration guides plus a filelist in a tool-specific order. It is markup pretending to be a language — structure without names, reuse without contracts. The practical consequence is that hardware reuse today is _social_: you trust a vendor's testbench claims and wire it up by hand. A language whose components carry machine-checked summaries can replace that with _mechanical_ exchange — and if Strata is ever to take off, frictionless, trustworthy reuse is as decisive as any type-system feature. Cargo is the existence proof that a package system can be a language's primary adoption engine. ## Committed design ### 1. What we take from Cargo, and what changes (D-047) Cargo's success came from five decisions: one canonical manifest, lockfile-pinned reproducible builds, semver as the compatibility contract, a single shared registry with immutable versions, and features composing additively. Strata inherits all five — but hardware lets us make three of them stronger than software can, because the unit of exchange is a component summary, not an API surface. ### 2. Manifest ```toml [package] name = "riscv-base-core" version = "2.3.1" edition = "2027" # per-component edition pinning (D-043) license = "SHL-2.1" [dependencies] axi-fabric = "1.4" # semver over summaries, not source branch-tage = { version = "3", contract = "Predictor" } vendor-fifo = { version = "2.1", unsafe-surface = ["clock_crossing"] } # must acknowledge [proofs] lsq-ordering = { artifact = "sha256:...", evidence = "InductivelyProved" } [targets] vu19p = { evidence-required = "Measured" } ``` Key departures from Cargo: - **Declared unsafe surfaces.** A dependency whose summary exports unsafe categories (`clock_crossing`, `primitive`, ...) must be acknowledged in the manifest — importing risk is explicit, and the aggregate unsafe report (P-1) rolls up transitively. An unacknowledged unsafe surface is a resolution error, not a warning. - **Proof artifacts are first-class dependencies.** Content-addressed, evidence-tagged, checkable by the small trusted checker ([06 north star](06-refinements-and-evidence.md)) — a formally verified arbiter ships its invariants as an importable object, not a paper citation. Proof artifacts version and pin like code. - **Contract-typed dependency slots.** `contract = "Predictor"` means the slot accepts any package whose summary _refines_ that contract — this is what makes "pop in a base core, swap the predictor" a manifest edit, with substitution legality checked at resolution time (refinement, not equality — [06 §4](06-refinements-and-evidence.md)). ### 3. Versioning: semver made mechanical and timing-inclusive This is the headline upgrade (D-043). Cargo's semver is convention plus `cargo-semver-checks` over API surface only. Strata summaries capture interface types, protocol, effect rows, timing contract, active optional contract families, guarantees, owned assumptions, validity/invalidation rules, relation-completeness declarations, authority/unsafe surface, evidence axes, expiry, and residue — so compatibility over the closed summary schema is decidable and total: - **Major** (mechanically forced): any summary change a dependent could observe as a regression — weakened guarantee, strengthened or newly unowned assumption, changed/narrowed protocol, slower schedule/lower throughput, widened authority or unsafe surface, weakened containment/progress/memory completeness, shorter validity, raised resource requirement, new residue, or removed export. - **Minor** (mechanically permitted): **strictly** refining changes — new exports, strengthened guarantees, weakened assumptions, faster timing within contract, stronger containment, wider config/fault coverage, longer validity, removed residue, or upgraded evidence on the same comparable axis. ("Strictly" is load-bearing: a lateral equal-strength change is minor in both directions, the one deliberate antisymmetry exception — probe finding, `probes/summary-semver/`.) - **Patch**: the summary is _bit-identical_ and the implementation change ships equivalence evidence — a translation-validation or LEC certificate against the previous version at the declared equivalence class ([07 §4](07-compiler-architecture.md)). A patch release is not a promise; it is a checked artifact. Bit-identity presupposes a **specified canonical summary encoding** (canonical collections, normalized rationals — `1/2` vs `2/4` throughput must not fake a diff); the canonical encoding is part of the summary spec, not an implementation detail. The version bump is computed by diffing summaries, not chosen by the author; `forge publish` refuses a version number the diff contradicts. No software ecosystem can offer this because no software summary contains timing. Three probe-established rules travel with the mechanism: **evidence comparison respects the lattice's partial order** — `Measured → InductivelyProved` is _not_ an upgrade (a consumer requiring `>= Measured` regresses), so incomparable evidence moves force MAJOR with a human-review flag in both directions; the schema is **closed with a per-field polarity table** (In-port widening is minor, Out-port widening is major; a new input is major, a new output is minor — polarity ships as a table, not prose, and every new summary field must declare its polarity before landing); and an unclassifiable difference hits the **totality backstop**: forced MAJOR plus flag, never silence. ### 4. Registry Immutable versions; summaries (not just tarballs) indexed and queryable — so **search is by contract**: "components refining `Predictor` with `latency ≤ 2 @ ≥800MHz(Measured, vu19p)` and empty unsafe surface" is a registry query, and it is exactly the query the [architecture agent](09-agent-system.md) runs when proposing alternatives. Published packages must satisfy the eager-library-boundary rule (D-042): definition-checked bounds plus a declared config coverage set, recorded as `Tested` evidence. Two further publish gates come from the [toolchain](14-toolchain.md): fmt-clean (hard gate, D-049) and lint-adjudicated — zero unaddressed `suspicious`/`design` findings, with the suppression surface published beside the unsafe surface (D-060). Yanking requires a stated reason and never deletes (dependents keep building against the lockfile); security/soundness advisories attach to versions and surface at resolution. ### 5. Features are configuration, not conditional compilation Cargo features compose additively because adding code is cheap; hardware "features" add _silicon_. Strata features are comptime config surfaces: a feature flag is a `comptime fixed` parameter (or a `param` range the optimizer owns, D-035) whose contract impact is declared — either contract-invariant (a true feature, additively composable) or contract-changing (a _variant_, which is a different summary and therefore a different resolvable artifact). Feature unification across a dependency graph is then a typed operation: two dependents demanding incompatible variants of one instance is a resolution error with both demand chains named (P-9), not a silent union. ### 6. The language module system Distinct from hardware components: language modules organize _names_; components are units of _hardware and summary_. Rules, each the negation of a SystemVerilog failure: - **Namespaces, not a global scope.** Every item has one canonical path (`core::lsu::StoreBuffer`); imports are explicit; no name enters scope by file order. - **No textual inclusion, no preprocessor.** There is no `include` and no token-level macro layer — comptime is the only metaprogram, and it computes over typed structures (D-022). Conditional hardware is comptime config (§5), never `ifdef`. - **Visibility is declared.** `pub` / `pub(package)` on items; a component's _implementation_ namespace is private by default — the summary is the public surface, which is what makes summary-level semver (§3) total rather than aspirational. - **One definition rule, enforced by resolution.** Two packages exporting the same canonical path is a resolution conflict, not an elaboration-order surprise. - **Workspaces** group co-versioned packages (a core and its verification package) with one lockfile and shared config, Cargo-style. ### 7. Reproducibility to the bitstream The lockfile pins package versions, summary hashes, proof-artifact hashes, toolchain and firtool versions, and target evidence requirements. P-6 determinism composes through resolution: same lockfile + same source = same architectural IR, and — given pinned vendor tools — the same bitstream hash, which the [experiment database](09-agent-system.md) records. `forge build --locked` is the only mode CI and agents use. ## North star - Federated/private registries with the same summary index (hardware IP is often contractually private; the mechanism must not assume one public registry). - License and export-control metadata as first-class, resolution-checked fields (hardware IP reality; a design that can't prove its license composition is unshippable). - Registry-wide contract search as an agent tool: the [architecture agent](09-agent-system.md) proposing "replace your hand-rolled arbiter with `fair-arbiter@2.x`, which refines your contract with stronger evidence" directly from the index. - Vendored proof-artifact mirrors and reproducible proof re-checking as a registry service. - Cross-package ledger queries ("which packages in my tree contain `Assumed`-only CDC contracts?") as standard tooling. - Release-assurance export compatible with structured assurance-case tooling such as OMG SACM, while preserving the rule that exported argument graphs summarize rather than create evidence. ## Open problems touching this doc Consumes [OP-3](open-problems.md) directly: contract-slot resolution is summary subtyping at ecosystem scale, so obligation stability and decidable catalog compatibility are load-bearing here too — if Tier-2 outcomes drift across solver versions, _dependency resolution itself_ becomes flaky. That coupling raises OP-3's stakes and should be named in its probe. ````