# Rustgen and Facet Artifact 2 integration plan For the complete repository architecture, current working/not-working status, file map, milestone history, and broader roadmap, start with [`SPECTRE_STATUS_AND_ROADMAP.md`](SPECTRE_STATUS_AND_ROADMAP.md). This document owns the detailed projected-backend exit gates. Status: authoritative projection, bounded archive validation, and the compatibility-tested projected-bundle/job v1 data contract are complete. Backend packaging and service operations remain unimplemented, and neither target is requestable from checker-service v1. **Transport is not an open design question in this plan.** The specification of record is [`Datum/PLDI27/TRANSPORT.md`](../../Datum/PLDI27/TRANSPORT.md), which derives the transport obligations T1–T10 from the individual rules of `Rmpst.Semantics` and states which assertion fails for each. The adopted model is a **peer-indexed connection map** — one framed, reliable, order-preserving channel per *ordered* participant pair, realized as one TCP connection per unordered pair — because that is the runtime image of the model's queue keys, not because of API ergonomics. Both backends below inherit those obligations; [`RUSTGEN_THREE_ROLE_TRANSPORT_DESIGN.md`](RUSTGEN_THREE_ROLE_TRANSPORT_DESIGN.md) is the Rust API that discharges them. ## Goal Add two honest participant-oriented bundles to the SPECTRE GUI: 1. a Rustgen Rust/Flux workspace with one crate per participant; and 2. a Facet Artifact 2 OCaml distributed protocol-enforcer bundle. Both require Tier 1P. They share projection/provenance infrastructure but make different runtime claims. ## Confirmed starting point - `.spe` projectable generation already produces a `complete_protocol_extraction` containing `local_projections`. - The current Rustgen backend consumes `local_protocol_graph` and generates crates for any number of roles. Canonical controllers now accept validated peer-indexed maps, and a refinement-safe three-role workspace passes offline `cargo check` and a genuine three-process direct-TCP session over separate Client↔Gateway and Gateway↔Server sockets. The website staged worker now validates exact agreement between projection-derived peers and generated `PeerStreams`; `unsupported-multiparty-transport` is removed. This does not make the hosted capability requestable. - The current Facet runtime can run Artifact 2 directly from specification local graphs over TCP. The same transport obligations apply to it — it is a second backend over the same semantics, not a different communication story — so F2 below must configure one channel per ordered pair and bind each socket to a participant ID, exactly as Rustgen must. - The website service accepts Tier-0 `fstar` source emission plus Tier-1G `graph`, `nuxmv`, and `platum` generation. It must continue rejecting projected backend targets until their backends are complete. ## Shared milestone 0: canonical projection bundle Implement this first because both targets depend on it. - Add canonical serialization for one participant local graph. - Add a Tier-1P generation operation that returns every participant exactly once. - Record participant numeric ID, source role name, local initial state, local graph hash, source SHA-256, compiler/core versions, and projectable profile. - Reject missing, duplicate, unknown, or hash-mismatched projections. - Define deterministic file ordering and canonical JSON formatting. - Add positive tests for two- and three-role protocols. - Add the globally-valid-but-non-projectable negative test. - Add stale revision/hash and partial-publication tests. `schemas/projected-bundle-v0.schema.json` is the website-side draft for this milestone. `scripts/projected-bundle.mjs` makes its cross-field rules executable. It validates complete/unique role coverage, target-specific configuration, safe relative paths, declared-file coverage, declared/actual byte sizes, and exact content and local-graph hashes. Its planning limits are 64 participants/graphs, 1,024 files, 8 MiB per file, and 64 MiB unpacked total; the size pass completes before hashing begins. The test suite contains valid hypothetical Rustgen and Facet Artifact 2 bundles, exact-limit cases, and one-over-limit mutations. Version zero is intentionally not accepted or produced by checker-service v1. Completed website-side prerequisites: - [x] Capability labels keep both targets planned and non-requestable. - [x] A shared manifest shape records source, Tier-1P assurance, immutable toolchain identity, participants, configuration, and files. - [x] Semantic contract tests reject duplicate/missing roles, target mismatch, unsafe paths, undeclared files, and hash mismatch. - [x] Manifest entries declare `sizeBytes`; schema and semantic checks bound participants, local graphs, file count, individual files, and total bytes. - [x] Canonical manifest encoding fixes normalized set-like arrays, recursively UTF-8-byte-sorted object keys, compact UTF-8 without a BOM, and exactly one trailing LF. - [x] Deterministic gzip/ustar output sorts entries by UTF-8 path bytes and fixes regular-file modes, timestamps, ownership, device metadata, gzip headers, and compression parameters. Repeated and reordered-input builds have identical bytes and hashes. - [x] Bounded archive consumption verifies strict ustar structure, checksums, canonical metadata and manifest bytes, resolves every path below an explicit bundle root, and rejects links, devices, non-regular types, duplicates, path escapes, malformed data, and decompression bombs before exposing files. - [x] Promote v0 losslessly into projected-bundle/job v1 after compatibility tests for both targets. Define job request/lifecycle/error/result shapes while keeping service capability `requestable: false`. Remaining authoritative prerequisites: - [x] Canonically serialize the real compiler `local_protocol_graph`. - [x] Return all participant projections atomically from the exact Tier-1P revision and source hash. - [x] Test two-role, three-role, non-projectable, stale, and partial-output cases against real compiler output. The upstream `Datum/guidsl` implementation now emits `local-projections-v1.schema.json` data directly from the verified `complete_protocol_extraction`. Its gated `spe/project` operation checks exact participant coverage before output, returns participant names and canonical local state/transition/refinement data, and adds per-graph and set SHA-256 values. `projection-response-v1.schema.json` binds success to document, revision, source SHA-256, generated compiler-source hash, ordered core hashes, and the actual F*/selected-Z3 versions and executable hashes. The real suite covers two- and three-role success, deterministic repetition, globally-valid/non-projectable rejection, stale revision, wrong source hash, participant-set mutations, and interrupted output with no partial publication. This is not yet promoted into the website checker-service or bundle v1. Exit gate: the same checked source deterministically produces a complete, hash-verified local-graph set, and no partial set can be published. Website handoff progress: - `scripts/projection-handoff.mjs` verifies the versioned upstream response, canonical graph hashes, projection-set hash, participant order/coverage, and structured compiler/core/F*/Z3 provenance. - It materializes one stable graph file per role and maps those files into projected-bundle v0 without inventing backend provenance. - A complete planning bundle still requires the caller to supply target configuration, an immutable backend identity, worker image digest, and any backend files. - Both target fixtures pass `scripts/projected-bundle.mjs`, and the optional live test has fed real OneShot `spe/project` output through the same path. - The handoff emits `sizeBytes` for every graph/backend file and passes the default resource policy; boundary tests prove exact limits pass and each over-limit category fails. This completes projection-to-bundle field reconciliation, reproducible producer encoding, bounded hostile archive validation, and compatibility-tested promotion into `projected-bundle-service-v1`. The v1 schema defines a complete manifest, create-job request, queued/running/terminal job states, safe errors, and a content-addressed expiring archive descriptor. Compatibility changes only the manifest `schemaVersion`; source, assurance, projection, toolchain, participants, configuration, file metadata, and bytes remain identical. This contract still does not implement either backend or add a service route. `planned-not-requestable` means capability discovery documents the target and its blockers, but clients cannot submit it and the service cannot generate it. `/v1/generate` continues to reject both projected targets. The next implementation boundary is Rustgen milestone R1. Canonical v0 representation: - `bundle-manifest.json` is recursively key-sorted by UTF-8 bytes; participants sort by role ID/name, files by path, and crates/endpoints by role ID; ordered core-module provenance is preserved. - JSON is compact UTF-8 with no BOM or CRLF and exactly one trailing LF. - The container is gzip-compressed POSIX ustar. All entries, including the manifest, sort lexically by UTF-8 path bytes. Every entry is a regular file with mode `0644`, UID/GID and mtime zero, empty owner/group names, and zero device fields. - Gzip uses level 9, memory level 9, a 15-bit window, the default strategy, mtime zero, and a fixed OS header byte. The archive SHA-256 covers the exact compressed bytes. - The reader allows at most 1 MiB of canonical manifest bytes and 70 MiB of compressed input. Its decompressed ceiling is calculated from 64 MiB file content, 1 MiB manifest content, the maximum 1,025 entry headers/padding, and the two-block terminator. It never constructs the returned file map until structural, type, duplicate, path-containment, and canonical-manifest checks pass; semantic sizes and hashes are checked immediately afterward. - Validation is in memory and does not extract files. A future worker must use the validated result in a fresh private job root and must not bypass this boundary with a general-purpose archive extractor. ## Rustgen milestones ### R1. Canonical backend installation - Move/install the supported Rustgen module beside canonical SPECTRE. - Remove the service dependency on the experimental PLDI27 checkout. - Pin the Rustgen, Rust, Cargo, Flux, and dependency versions. ⚠️ **Which artifact owns what — do not read "experimental PLDI27 checkout" as "disposable".** The *code generator* to depend on is canonical `Datum/SPECTRE/Rustgen.fst`; the two copies were checked equivalent on 2026-07-24 and F\* verified both. But the **asynchronous semantics and every theorem about it live only in `Datum/PLDI27`** — `Rmpst.Semantics.fst` plus the `Rmpst.Proofs.*` chain, which is what makes any statement about generated-code behaviour meaningful. So the service must not depend on PLDI27 at runtime, and the *specification* must continue to cite it: `TRANSPORT.md` for the transport obligations, `TCB.md` for the assumption ledger, `THEORY.md` for the theorem statements. ### R2. Eligibility Implemented at the compiler preflight boundary: `spe eligibility` with target `rust` returns a versioned result, exit code 3 for ineligible source, and source-located `backend_ineligible` issues plus the SHA-256 of the exact checked source. Generation must call this same core API once the backend driver exists. - Translate only the documented guard/refinement subset. - Return `backend_ineligible` with `.spe` source locations for an unsupported construct. - Never erase a guard, generate an unconstrained placeholder, or use `todo!()` to satisfy a refinement contract. ### R3. Atomic workspace generation The deterministic in-memory planning portion is implemented in `scripts/rustgen-workspace.mjs`: stable role-qualified crate names, optional workspace membership, generated-versus-user ownership, byte-preserving regeneration, and non-destructive obsolete-role reporting. `scripts/rustgen-output-handoff.mjs` validates the pure `generate_rust_project_files` manifest, role/crate identity, supported Flux pin, generator-owned completeness, and exact projection/eligibility source match, then builds the fresh projected-bundle representation. It performs no F*/OCaml invocation or filesystem publication. Canonical invocation is implemented as a narrow extension of the existing verified-artifact exporter in `guidsl/spe_core.ml`, not as a sibling verifier. The private API accepts the planner's role-ID/crate-name mapping, derives role names from the checked source, reads each graph from `complete_.local_projections`, invokes canonical `SPECTRE/Rustgen.fst`, and publishes only the pure JSON entry manifest after F*/extraction/OCaml success. This explicitly avoids hardcoded AuthLite names. The live website regression passes that output directly into `adaptRustgenManifestEntries`. The shared lockfile and poison worker gates are now implemented in `scripts/rustgen-staged-worker.mjs`. A job derives only its source-less workspace package entries around byte-preserved dependency blocks from an immutable pre-resolved lock seed. Registry dependencies require checksums and all git dependencies must be the exact supported Flux commit. The staged bundle carries this shared lock and canonical `rust-toolchain.toml`. Cargo runs locked and offline; Flux runs offline with fresh target roots, after which the worker verifies that Cargo.lock and every declared file remain byte-identical. The negative canary mutation occurs only in a copied staging tree. Manifest, hash, deterministic archive, and hostile-reader validation precede a single rename to a new publication path. Any failed gate publishes nothing. - Generate one stable crate name per role. - Optionally generate a workspace and shared lockfile. - Overwrite only generator-owned `Cargo.toml` and `src/prot.rs`. - Create `src/endpoint.rs` and `src/main.rs` only when absent. - Stage the entire workspace, validate it, hash it, then publish it atomically. ### R4. Validation - `cargo check` every crate. - Run Flux positive checks. - Run a negative mutation that removes a required application guard and confirm Flux rejects it. - Preserve the passing canonical two-role TCP session and add a genuine three-role session using the implemented peer-indexed API — with at least one role that receives from one peer and sends to another. - Test regeneration and preservation of user-owned files. The staged-worker AuthLite live fixture is stale against the current peer-indexed topology contract and fails before Flux because its terminal graphs omit required-peer metadata. It must be regenerated rather than used to weaken worker validation. The CLI Cargo/Flux gate passes locked/offline Cargo, normal Flux for every role, copied-canary rejection, the copied real protocol-guard mutation, and atomic publication. The canonical OneShot regression also passes an actual two-role generated TCP session. Canonical Rustgen now implements the peer-indexed API, and `tests/three_role_transport.spe` produces a complete three-role workspace that passes offline `cargo check` and a genuine live three-process session. The worker is adapted to validate the exact peer-indexed controller contract. Hidden-guard environment eligibility is also implemented: Authenticate is rejected with source-located `RUSTGEN011` issues for Server's unavailable `expected_code` references without weakening them. A Final projected-bundle provenance and the immutable production image remain exit gates; the validation-only real application-guard mutation is complete. ⚠️ **"A peer-indexed connection API *or* specified relay protocol" is no longer an either/or.** Peer-indexed is the adopted design (`TRANSPORT.md` §4). A relay is sound only if the receiving endpoint demultiplexes into per-`(from,to)` FIFO buffers — i.e. only if it reimplements the model's queues in user space — and it moves the router into the TCB for per-pair ordering, duplication and peer authenticity. It must never be presented as direct multiparty communication. One question this gate used to carry is **closed**: whether a receive state can offer branches from several peers, which would have required a multiplexing design. It cannot, for any protocol the metatheory covers (`Rmpst.Proofs.Choice.recv_peer_unique_at`, under (D1) `global_directed_choice` and `recv_reflects_at`), so a single blocking read on the peer named by `local_other_participant` is sufficient. Because sufficiency rests on two *decided* side conditions, the generator must run `global_directed_choice_b` and `recv_reflects_at_b` and refuse protocols failing them. The exact canonical change, peer-indexed API, migration boundary, assurance limits, and three-role exit tests are specified in [`RUSTGEN_THREE_ROLE_TRANSPORT_DESIGN.md`](RUSTGEN_THREE_ROLE_TRANSPORT_DESIGN.md); the obligations it discharges are in [`TRANSPORT.md`](../../Datum/PLDI27/TRANSPORT.md). Exit gate: a Tier-1P source produces an atomic, reproducible, hash-manifested workspace; ineligible protocols and failed validation publish nothing. ## Facet Artifact 2 milestones ### F1. Runtime packaging - Install the canonical OCaml runtime, serializers, and local-graph loader in a backend package. - Load the exact local graph selected by role ID. - Verify runtime/core/local-graph hashes at startup. ### F2. Configuration Define a versioned configuration with: - protocol/source hash; - every role ID and display name; - one local graph per role; - bind/connect host and port **per ordered peer pair the local graph uses**, not one address per role — the required peer set is read off the projection (`TRANSPORT.md` §6); - connection retry/startup policy; - optional logging destination without protocol-source telemetry. Reject incomplete, duplicate, unknown, or inconsistent assignments before starting any network process. The safety-relevant rejections are (`TRANSPORT.md` T6b, T7): an unknown participant; **the local role's own ID** (no self-channel is ever needed — `Position.typed_self_queues_empty`); a duplicate connection for one peer; a missing required peer; and a connection claimed for a peer absent from the projected local graph. A socket bound to the wrong participant injects messages the model has no run for, which puts the system outside the theorems rather than merely misconfiguring it. ### F3. Bundle Package: - participant local graphs; - OCaml sources or pinned runtime executable/package; - configuration template; - build and run instructions; - source/profile/core/tool/file manifest; - no user-authored F* process. ### F4. End-to-end tests - Launch every participant on unprivileged loopback ports, with one channel per ordered pair the projection requires. - Confirm an allowed trace completes. - Confirm an unexpected label is rejected. - Confirm an out-of-order message is rejected. - Confirm a refinement-violating payload is rejected. - Confirm a malformed, truncated, or over-long frame fails closed rather than decoding to a default value (`TRANSPORT.md` T4/T5). - Confirm a connection bound to the wrong participant is rejected before any protocol step, and that a configuration naming the local role as its own peer is rejected (T6b/T7). - Confirm incomplete and duplicate role configurations fail before launch. - Confirm a newer revision supersedes an older bundle job. Exit gate: the bundle launches a complete local topology and produces the expected decisions for allowed and violating traces, with hashes tied to the Tier-1P source. ## Service and GUI sequence 1. Keep `/v1/generate` restricted to the explicit Tier-0 F* source target and current Tier-1G targets; do not expose projected backend generation. 2. Publish `/v1/capabilities` so the GUI and tests can distinguish available, planned, and out-of-scope targets. 3. Complete shared milestone 0 in the authoritative compiler/bridge. 4. Add a new versioned bundle/job contract rather than overloading the current single-inline-artifact response. 5. Enable Rustgen only after R1–R4. 6. Enable Facet Artifact 2 only after F1–F4. 7. Add GUI configuration/download controls only when the corresponding capability is reported `available`. Facet Artifact 1 remains out of scope for this sequence because it requires a separate user-authored F* process workflow. `../TODO_STEPS.md` is the concise ordered checklist for executing this plan.