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), the evidence lattice (06 §3, 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

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) — 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).

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). 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 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: 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 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 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 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.