# Using the interactive SPECTRE page For repository architecture, implementation status, file ownership, completed milestones, and the full roadmap, start with [`SPECTRE_STATUS_AND_ROADMAP.md`](SPECTRE_STATUS_AND_ROADMAP.md). This guide is focused on operating and interpreting the interactive page. This guide explains what the page does, how to connect the authoritative checker, what Tier 0 and Tier 1 mean, what each current download contains, and what is planned for Rustgen and Facet Artifact 2. The short version is: ```text draw or edit locally → authoritative Tier 0 language check → explicit Tier 1G or Tier 1P F*/Z3 verification → capability-appropriate artifact generation ``` The browser is an editor and viewer. It is not the checker. ## 1. The three states you will see ### Local draft The service is offline, but visual controls still work. The browser checks only basic editor invariants, such as: - participant references exist; - sender and receiver differ; - editor IDs are not duplicated; - a structural block does not contain statements after a terminal; - loop and choice frames are internally consistent. This is useful drafting feedback. It does not mean the `.spe` language accepts the source, and it is never a verification result. The status says `Local draft updated. Checker offline`. Free-form source import does not work in this mode. Import needs the real parser, so **Apply to diagram** preserves the existing diagram and explains that a checker is required. ### Tier-0 well-formed The connected service sent the exact source to `spe_core`, the authoritative `.spe` frontend. Tier 0 runs: - lexing and parsing; - name and participant checks; - payload, loop-state, guard, and update kind checks; - scope and shadowing checks; - choice-label and continuation checks; - `continue` resolution to an enclosing loop; - reachability checks after terminal constructs; - guard classification as payload-local or history-dependent. Tier 0 is fast and launches neither F* nor Z3. It answers: > “Is this a well-formed `.spe` protocol that the compiler understands?” It does **not** answer: - whether refinements are satisfiable; - whether the global protocol passes the Facet extraction obligations; - whether every participant can receive a safe local projection; - whether a generated endpoint, monitor, or model satisfies its own backend conditions. ### Tier-1 verified Tier 1 runs the generated F* through the SPECTRE/Facet core and Z3. It is explicit because it is substantially more expensive than Tier 0. A Tier 1 result is accepted by the page only when its document revision, compiler source hash, and SHA-256 still match the source displayed in the editor. Editing after verification makes the result stale. Tier 1 has two capability profiles: | Profile | Meaning | Required by | |---|---|---| | Tier 1G, `global` | F*/Z3 accepted global extraction and validation. | Verified global graph, nuXmv generation, Platum. | | Tier 1P, `projectable` | Tier 1G plus mergeability and a valid local projection for every participant. | The page’s Verify action, future Rustgen, future Facet Artifact 2. | A protocol can pass Tier 1G and fail Tier 1P. That is expected: a centralized consumer can sometimes use a valid global graph even when one participant cannot determine which local branch it should follow. ## 2. What “Connect a checker and run Tier-0 first” means There is no separate Tier 0 button. When the service is connected, Tier 0 runs automatically for the current visual document: 1. Open the **Editor** view. 2. Look at the service card. 3. `Authoritative checker available` means the browser can reach the local checker-service contract and that service can reach `spe_core`. 4. The current diagram is serialized to complete `.spe` source. 5. The browser computes its SHA-256 and sends source, revision, and hash to `POST /v1/check`. 6. The service recomputes the hash, rejects stale revisions, and calls the authoritative compiler. 7. If accepted, the editor status becomes `Tier-0 well-formed`. Every committed visual edit repeats this process. **Apply to diagram** also runs Tier 0, requests the compiler surface AST, imports only the exactly supported visual subset, and checks the editor’s serialization again. If the Verify button says that Tier 0 must run first, one of these is true: - the checker service is offline; - the service endpoint is wrong; - the current source has a Tier 0 diagnostic; - the source changed after the last accepted result; - a newer revision superseded the request. Fix the diagnostic or reconnect the service. Tier 0 will rerun automatically. ## 3. Starting the local checker The public static page cannot start native tools on your computer. For local development, run three processes. ### Terminal 1: authoritative bridge Tier 0 only: ```sh cd /Users/arthuramorim/Documents/code/Datum/guidsl make spe-bridge ./spe-bridge ``` Tier 0 plus local F*/Z3 verification and generation: ```sh cd /Users/arthuramorim/Documents/code/Datum/guidsl make spe-bridge SPE_BRIDGE_VERIFY=1 \ SPE_CORE_DIR=../SPECTRE \ PATH="$HOME/nuXmv/bin:$HOME/.opam/tools/bin:$PATH" \ SPE_FSTAR_FLAGS="--z3version 4.16.0" \ ./spe-bridge ``` This trusted bridge binds to `127.0.0.1:8137`. Do not expose it to the internet. ### Terminal 2: versioned browser adapter ```sh cd /Users/arthuramorim/Documents/code/website npm run checker:service ``` The adapter binds to `127.0.0.1:8138`. It presents health, version, capability, Tier 0, scope, verification, and generation endpoints. It is local development infrastructure, not a public sandbox. ### Terminal 3: static preview ```sh cd /Users/arthuramorim/Documents/code/website npm run build npm run preview ``` Open `http://127.0.0.1:8080/protocol-editor.html`, choose **Editor**, and press **Retry** in the service card if the page was already open. The Developer disclosure lets you change the service URL. Normally leave it at `http://127.0.0.1:8138`. ## 4. A normal editing and verification session 1. Start with the default two-participant draft. 2. Add or rename participants. 3. Add messages by using the structural controls or dragging between participant handles. 4. Select a message to edit its label, direction, payload type, payload name, and refinement. 5. Add choice or loop frames to the selected structural block. 6. Watch **Diagnostics** and the Tier 0 status after every committed edit. 7. Use the source pane when text is clearer. **Apply to diagram** uses the authoritative parser and preserves the last valid diagram on failure. 8. Once the exact revision is Tier-0 well-formed, press **Verify Tier 1P (F*/Z3)**. 9. Do not edit while interpreting the result. Any edit makes the verification stale and requires a new run. 10. Request an artifact. The F* module is emitted from the exact Tier-0 revision; graph, nuXmv, and Platum independently verify the exact revision under Tier 1G. ## 5. What the current downloads mean ### F* module This is generated F* source for the exact Tier-0-accepted revision. It is the browser counterpart to `spe generate --target fstar`; it does not run F*, Z3, or establish a proof verdict. Use the CLI when the retained `.spemap` and artifact manifest are needed alongside the `.fst`. ### Global graph JSON This is a machine-readable serialization of the **verified global protocol graph** produced from the canonical Facet extraction context after Tier 1G. It contains the protocol-wide state machine: - participants; - state identifiers; - directed transitions; - sender, receiver, and message label; - structured guards and variables; - loop/recursion metadata; - initial and terminal structure. It is useful for: - inspecting the verified state machine; - building visualizers or analysis tools; - feeding backend adapters from a stable structured representation; - recording an exact source/profile/toolchain artifact. It is not: - a participant implementation; - a participant-local graph; - an executable network monitor; - proof that every participant projection exists; - a nuXmv property result. The website’s `Global graph JSON` is different from the compiler’s advisory Tier-0 graph dump. The download is generated from the Tier-1G-verified extraction. ### nuXmv model This is an `.smv` finite-state model generated by Fact from the verified global extraction. Generation requires Tier 1G. Downloading the model does not mean nuXmv has run. A future bundle can include both the model and a separate nuXmv log/property verdict. F*/Z3 verification and nuXmv model checking answer different questions and must remain separate. ### Platum C monitor This is a centralized C runtime monitor generated from the Tier-1G global extraction. It checks protocol order and guards at a monitoring boundary. The current generator uses Platum’s default MAVLink-oriented conventions. Deployment still needs matching message headers, payload/schema mappings, and C validation for the chosen environment. A generated file is not automatically a deployable monitor for an arbitrary wire protocol. ## 6. How to read failures The UI distinguishes protocol results from infrastructure failures: - **Tier 0 rejected**: the authoritative `.spe` frontend found a language or structural error. - **F* rejected this revision**: F*/Z3 produced a negative verification verdict for the exact source/profile. - **Toolchain error**: missing tools, timeout, configuration, or another environmental failure prevented a verdict. This is not protocol rejection. - **Stale**: a newer revision or different source hash exists. The result is intentionally discarded. - **Verified artifact generation disabled**: the local bridge was started without `SPE_BRIDGE_VERIFY=1`. F* source emission remains available through a connected Tier-0 bridge because it makes no verification claim. - **Offline**: the browser cannot reach the service or the service cannot reach the authoritative bridge. ## 7. Future participant-oriented outputs Both planned GUI targets begin from the same new prerequisite: ```text Tier 1P verified complete projection → one canonical local graph per participant → versioned, hash-scoped projection bundle ├─→ Rustgen workspace └─→ Facet Artifact 2 OCaml enforcer bundle ``` The repository retains a legacy v0 manifest as compatibility input and now has a promoted v1 bundle/job data contract plus executable semantic validator. Tests prove that the contract can represent both targets and reject incomplete role coverage, unsafe paths, target mismatch, undeclared files, changed file contents, manifest-size mismatches, and participant/graph/file/byte-limit violations. The envelope is 64 participants/graphs, 1,024 files, 8 MiB per file, and 64 MiB unpacked file content, checked before hashing. This does **not** mean either backend exists in the browser or service: no current operation produces or accepts a projected backend job, and capability discovery still reports both targets as `planned-not-requestable`. In plain language, `planned-not-requestable` means “documented, but impossible to ask this service to run.” The service knows the future target and its requirements, but there is no generation route or working backend behind it. The browser must keep the control disabled or absent, and direct attempts are rejected as unsupported. It does not mean queued, partially available, or available only to developers. The planning bundle now has deterministic bytes. Its compact UTF-8 manifest uses normalized participant/file/configuration arrays, recursively UTF-8-byte-sorted object keys, no BOM, and exactly one final LF. The manifest and declared files are placed in bytewise-path order in a gzip-compressed POSIX ustar archive with fixed regular-file modes, zero timestamps and ownership, and fixed gzip settings. Repeated builds and builds from differently ordered input produce the same bytes and SHA-256. The matching archive reader validates untrusted bytes in memory without extracting them. It bounds both compressed and decompressed size, verifies ustar structure and normalized metadata, accepts regular files only, detects duplicate entries, keeps every resolved path below an explicit intended root, requires canonical manifest bytes, and verifies declared file sizes and hashes. Hard/symbolic links, character/block devices, other entry types, relative or absolute escapes, malformed archives, and decompression bombs are rejected. The planning shape has now been compatibility-promoted to `projected-bundle-service-v1`. The contract defines the v1 manifest, create-job request, lifecycle states, safe failures, and content-addressed expiring download result. Both target fixtures retain every v0 field except the promoted schema version, and tampered input cannot promote. This defines future messages; it does not add the route or backend. Rustgen and Facet Artifact 2 remain unavailable in both the browser and service. ### Rustgen Rustgen produces one Rust/Flux endpoint crate per participant from that participant’s local graph. The generated controller owns protocol order, receive validation, environment threading, and calls into user-owned endpoint hooks. Before the GUI can offer it, the canonical backend must: - live beside the canonical SPECTRE core rather than depend on an experimental Facet fork; - consume Tier-1P `local_projections`; - make unsupported refinement translations hard eligibility errors; - stage and validate all role crates atomically; - distinguish generator-owned files from user-owned hook files; - support stable role-to-crate and TCP endpoint configuration; - run Cargo and Flux positive/negative checks in the isolated worker; - return a multi-file manifest with source, profile, tool, and file hashes. ### Facet Artifact 2: Distributed Protocol Enforcer Artifact 2 deploys each specification local graph at that participant’s network boundary. It does not inspect or certify the endpoint application behind the boundary. The OCaml runtime validates live sends/receives against the projected specification graph over TCP/IP. Before the GUI can offer it, the canonical backend must: - export one exact local graph for every participant after Tier 1P; - package the OCaml runtime and the selected local graphs; - define role identities and a role-to-host/port configuration file; - validate missing, duplicate, and inconsistent role assignments; - specify connection establishment and startup ordering; - build without privileged networking; - launch a complete local topology in tests; - accept an allowed trace; - reject an order, label, or refinement violation; - record runtime/core/configuration/file hashes in the bundle manifest. ### Why Facet Artifact 1 is not in this GUI Artifact 1 verifies a **user-authored F* process** against a participant local type. The current GUI authors only the global `.spe` protocol. It has no F* process language, process editor, build inputs, or process-to-role mapping. Offering Artifact 1 from the global protocol alone would omit its defining input and overstate what was checked. Artifact 1 could become a separate expert workflow later, but it is not part of the Rustgen/Artifact 2 plan. The implementation order and exact remaining gates are in [`PROJECTED_BACKENDS_PLAN.md`](PROJECTED_BACKENDS_PLAN.md) and [`../TODO_STEPS.md`](../TODO_STEPS.md). ## 8. Provenance and privacy Every authoritative request carries a client ID, document ID, monotonically increasing revision, full source, and source SHA-256. Results echo the revision and hashes. The browser refuses stale results. The current adapter is loopback-only. A public service must add actual short-lived worker isolation, hard CPU/memory/process/filesystem limits, disabled outbound networking, immutable toolchain images, production queue and rate limits, expiring content-addressed artifacts, and source-minimizing retention. See `CHECKER_SERVICE.md`.