# Developer Guide This guide describes how to inspect, build, test, and change the current Sovereign Event Bus repository. It documents the repository as it exists, including known failures. It does not treat historical completion reports as a substitute for a clean build. ## Start here SEB is a collection of component projects, not a root workspace or a single server. Choose the boundary you are changing before installing toolchains. ```text contracts/codegen -> candidate language contracts kernel -> Ada state and append interfaces, C Erlang NIF surface runtime -> Erlang/OTP coordination reasoning -> Rust A2A events and in-memory traces universe -> Rust artifact manifests and gate model human_touch -> Rust review workflow prototype verification -> Lean models and proof sources adapters -> IBM i and z/OS integration assets ``` There is no JavaScript application, Node build, root `package.json`, or root `Cargo.toml` in this repository. ## Clean checkout ```bash git clone https://github.com/SNAPKITTYWEST/Sovereign-Event-Bus.git cd Sovereign-Event-Bus git status --short ``` The last command should print nothing. Build in the repository only when local artifacts are acceptable; Cargo creates nested `target/` directories and can create a crate-level `Cargo.lock` when one is absent. Before committing: ```bash git status --short git diff --check git diff --stat ``` Inspect every untracked file. Do not commit `target/`, `.lake/`, native binaries, reports containing local paths, credentials, or generated deployment archives. ## Toolchains ### Rust components Install Rust and Cargo through a controlled toolchain appropriate to your environment. The repository does not currently pin a Rust version. Crates: - `seb/reasoning` - `seb/universe` - `seb/human_touch` Each crate is independent. Run commands with `--manifest-path` from the root or change into that crate. ### Erlang runtime Install Erlang/OTP and `rebar3`. Dependency resolution needs registry/network access unless dependencies are already cached. The current runtime has source issues that must be fixed before a release build can pass. ### Lean verification Install `elan`, which provides Lean and `lake`. The project pins Lean 4.7.0 in `seb/verification/lean4/lean-toolchain` and mathlib 4.7.0 in its Lake configuration. The first build may need to download dependencies. ### Kernel The intended native boundary needs: - GNAT/SPARK and GNATprove for Ada; - a C compiler; - Erlang NIF headers matching the deployment OTP version; - selected BLAKE3 and Ed25519 libraries; and - a supported persistence API for the target operating system. No GNAT project, native dependency manifest, or portable kernel build target is currently checked in. Establish those before publishing a build command. ### Contracts and adapters Contract generation assumes Bash, GNU Make, and common GNU command-line utilities. Python 3 is used by the kernel vector script. TypeScript and YAML tools are optional checks in the current Makefile. The RPG source requires an IBM i environment with the external objects described in `seb/adapters/L4_ADAPTER_BUILD_GUIDE.md`. The PL/I asset is a set of declarations, not a complete executable adapter. ## Verified baseline The following results were observed on 2026-07-25. Re-run them after any source or dependency change. | Component | Command | Current result | | --- | --- | --- | | Reasoning library | `cargo test --manifest-path seb/reasoning/Cargo.toml --lib` | Passes 18 tests | | Reasoning build | `cargo build --manifest-path seb/reasoning/Cargo.toml` | Passes | | Reasoning all targets | `cargo test --manifest-path seb/reasoning/Cargo.toml --all-targets --all-features` | Fails to compile the example | | Universe library | `cargo test --manifest-path seb/universe/Cargo.toml --lib` | Passes 15 tests | | Universe build | `cargo build --manifest-path seb/universe/Cargo.toml` | Passes | | Universe all targets | `cargo test --manifest-path seb/universe/Cargo.toml --all-targets` | Fails to compile the example | | Human review | `cargo test --manifest-path seb/human_touch/Cargo.toml` | Fails to compile | | Erlang runtime | `rebar3 compile` | Not established as a passing build | | Lean | `lake build` in `seb/verification/lean4` | Fails; admitted terms also remain | | Ada/C kernel | No portable command | Build is not established | | IBM adapters | Platform-specific | Not validated on target systems | All three Rust crates currently report formatting drift under `cargo fmt --all -- --check`, and the all-target Clippy commands are not clean. Formatting and linting are therefore repair gates, not passing evidence. ### Reproduce the passing Rust suites ```bash cargo test --manifest-path seb/reasoning/Cargo.toml --lib cargo test --manifest-path seb/universe/Cargo.toml --lib ``` Library-only testing is intentionally explicit. Plain `cargo test` also builds examples in these crates and currently fails. ## Known build failures These are starting points for repair, not an exhaustive defect list. ### Reasoning example `seb/reasoning/examples/demo.rs` accesses the private `protocol_handler` field and passes `Option` where the current `set_query` API accepts a different value. Reconcile the example with the public library API, then make the all-targets command a required test. ### Universe example `seb/universe/examples/universe_demo.rs` imports `Invariant`, `ProofMetadata`, and `TestMetadata` from the crate root, but `seb/universe/src/lib.rs` does not re-export those names. Decide whether they belong in the public API or update the example to import their defining module. ### Human review crate `seb/human_touch/src/main.rs` passes `Arc>` into a function that expects `Arc`. Fix the ownership contract rather than adding an unsafe or duplicate synchronization layer. After it compiles, connect a real submission source and prove that an approval reaches the commit gateway exactly once. ### Erlang runtime Current issues include: - `void()` is used as an undefined type in `seb_agent_fsm.erl`; - a deprecated `catch` form conflicts with warnings-as-errors; - test function names are not discoverable by EUnit; - integration fixtures return `{ok, Pid}` but later treat the tuple as a PID; - the release configuration lists modules where relx expects applications; - `runtime/config/sys.config` contains a checked-in distributed Erlang cookie that must be removed from source, externally provisioned, and rotated; - the Datalog bridge can have no live port; and - the Erlang kernel facade neither loads nor matches the C NIF interface. A successful runtime repair must show nonzero discovered-test counts, not only a zero exit code. ### Lean project The default Lake library does not type-check, multiple sources contain `sorry`, and the checked-in `Tests.lean` is not wired as a Lake test target. Some cryptographic functions are deliberately trivial models. Repair the build before deciding which theorem closure is eligible for release evidence. ### Kernel The Ada kernel and C NIF do not currently form one implementation: - the C NIF duplicates state instead of calling Ada; - the NIF has a duplicate local declaration; - signature/hash validation and key registry paths include placeholders; - WAL source exists but is not connected to append; - the Ada source has unresolved type/build issues; and - the runtime facade uses a different handle and arity contract. Start by writing a versioned ABI document and a minimal native build that treats warnings as errors. Do not repair each side independently without conformance tests. ## Component workflows ### Reasoning Primary files: - `seb/reasoning/src/a2a_protocol.rs` - `seb/reasoning/src/trace.rs` - `seb/reasoning/src/streaming.rs` - `seb/reasoning/src/integration.rs` - `seb/reasoning/src/lib.rs` Suggested local loop: ```bash cargo fmt --manifest-path seb/reasoning/Cargo.toml -- --check cargo test --manifest-path seb/reasoning/Cargo.toml --lib cargo test --manifest-path seb/reasoning/Cargo.toml --all-targets --all-features ``` The first two commands should remain fast. The final command is the integration gate to restore. Add boundary tests for empty, short, long, and multibyte IDs: some current diagnostics slice strings by fixed byte offsets. The current trace signature is a placeholder digest/length check. Name any replacement type after its actual security property and add negative tests before describing it as a signature. ### Universe Primary files: - `seb/universe/src/manifest.rs` - `seb/universe/src/search_substrate.rs` - `seb/universe/src/compile_verify_merge.rs` - `seb/universe/src/lib.rs` Suggested local loop: ```bash cargo fmt --manifest-path seb/universe/Cargo.toml -- --check cargo test --manifest-path seb/universe/Cargo.toml --lib cargo test --manifest-path seb/universe/Cargo.toml --all-targets ``` Current gate stages model metadata transitions; they do not invoke a compiler, test runner, proof checker, reviewer, merge service, or deployment target. Keep simulation types separate from production execution types. A caller can also mutate or mark gate state directly, so no authorization decision should depend on this object yet. `seb/universe/repository.json` is development data, not a trusted manifest. It contains structural and value issues; validate it against a schema before using it in tests or tooling. ### Runtime Intended commands: ```bash cd seb/runtime rebar3 format --verify rebar3 compile rebar3 eunit rebar3 dialyzer rebar3 release ``` Some plugins or targets may need to be added or pinned before every command is available. The eventual CI job must report the number of EUnit tests executed. Runtime changes should cover: - supervisor restart and shutdown behavior; - correct `gen_statem` call/reply actions; - policy timeout and deny-on-error behavior; - idempotent partition assignment and real reassignment; - drain behavior with queued and in-flight events; - NIF load/version errors; and - crash containment for native work. ### Verification ```bash cd seb/verification/lean4 lake build ``` Before a proof artifact is release eligible: 1. Define the exact imported theorem closure. 2. Reject `sorry`, `admit`, and unreviewed axioms in that closure. 3. Record Lean, Lake, mathlib, and source digests. 4. Connect the model to a canonical protocol or implementation conformance artifact. 5. Preserve full command output and exit status. `lake test` is not currently declared. Add an explicit executable/test target or use buildable example/theorem modules with a documented command. ### Contracts and code generation The five templates in `seb/contracts` are independent hand-maintained shapes. The scripts under `seb/scripts/codegen` mainly copy them to expected locations. Some output directories referenced by the scripts are absent in this repository. Before running a generator: ```bash git status --short sed -n '1,220p' seb/scripts/codegen/generate_all.sh ``` After running one: ```bash git status --short git diff --check git diff ``` Do not accept generated parity based on filenames. Add golden byte vectors and round-trip tests for every language. The protocol source of truth must define canonical bytes, not only language-level field names. The root `seb/Makefile` still validates scaffold paths that are not present and can downgrade tool failures to warnings. Treat its targets as development helpers until they fail reliably on missing required work. The manifest-hash target also depends on GNU traversal tools. Its current output does not match the value recorded in `seb/GenesisConfig.toml`, and the existing verification target checks for the configuration key rather than proving the value is current. Rebuild this as a canonical, cross-platform manifest format before treating the hash as integrity evidence. ### Legacy adapters Use the platform guide in `seb/adapters` to inventory external programs, files, queues, DB2 tables, authorities, and transaction boundaries. Before enabling a real effect: - escape and validate every value embedded in JSON or command text; - reconcile RPG, copybook, PL/I, and canonical protocol layouts; - define idempotency and outcome reconciliation; - test commit, rollback, timeout, and connection loss on the actual platform; - restrict program/library authority to the required operation; and - capture platform compiler, linker, object, and deployment versions. PL/I declarations should remain labeled declarations until a callable implementation and platform test evidence exist. ## BOB shell workflow The six scripts in `bob-shell` are development wrappers. Read a script before using it in a protected checkout: ```bash sed -n '1,260p' bob-shell/bob-build.sh sed -n '1,300p' bob-shell/bob-test.sh sed -n '1,320p' bob-shell/bob-audit.sh sed -n '1,320p' bob-shell/bob-policy.sh sed -n '1,320p' bob-shell/bob-proof.sh sed -n '1,360p' bob-shell/bob-deploy.sh ``` Current behavior to account for: - missing tools can be skipped by build logic; - deterministic test mode sets environment variables but does not control all sources of nondeterminism; - audit output depends on traversal order, timestamps, GNU utilities, and working-tree contents; - policy and proof commands can create root-level scaffold files; - a caller-supplied Prolog query is executable input; - proof certificates can describe placeholder output; - deploy validation and sealing can be disabled; and - packaging success does not prove runtime, policy, evidence, or adapter health. For evaluation, use a disposable branch or worktree and compare status before and after: ```bash git status --short bash bob-shell/bob-audit.sh git status --short ``` For CI, replace silent skips with an explicit required/optional component manifest. Emit structured results containing command, tool version, exit code, duration, test count, skipped reason, and artifact digest. ## Contract change procedure Any envelope, receipt, offset, signature, policy-decision, or evidence change is a cross-component change. 1. Write the byte-level compatibility rule and migration behavior. 2. Add positive and negative vectors before updating implementations. 3. Update every supported decoder and encoder. 4. Run cross-language round-trip and byte-equality tests. 5. Update proof models and state whether the theorem set changed. 6. Exercise mixed-version producer, runtime, adapter, and verifier pairs. 7. Record the oldest readable and writable protocol versions. 8. Update operational rollback constraints. A source-compatible struct change can still be wire-incompatible. ## Testing expectations Choose tests according to the boundary: | Change | Required evidence | | --- | --- | | Pure Rust logic | Unit tests plus all-target compilation | | Parser or serializer | Golden vectors, negative cases, property tests, and fuzz seed | | Signature or hash input | Known-answer and mutation tests across languages | | Runtime state machine | EUnit/property tests for every transition and timeout | | Native boundary | ABI tests, sanitizers, leak checks, malformed input, and crash isolation | | Persistence | Kill-point, partial-write, corruption, restore, and concurrent-writer tests | | Human approval | RBAC, expiry, replay, race, restart, and idempotent commit tests | | Adapter | Target-platform integration plus unknown-outcome reconciliation | | Lean model | Clean build, admitted-term gate, assumptions review, and implementation traceability | | Release tooling | Clean-checkout run with required-tool and zero-test failure cases | Tests that depend on time, random input, filesystem order, locale, or network must either control those inputs or record them in reproducible evidence. ## Security-sensitive review Require at least one reviewer who understands the affected trust boundary for: - canonical parsing and serialization; - authentication, authorization, keys, signatures, or hashes; - policy evaluation; - offsets, ordering, idempotency, or replay; - WAL, evidence, backup, restore, or retention; - NIF/native memory and scheduler behavior; - human approval and separation of duties; - release signing, provenance, or dependency changes; and - theorem assumptions or model-to-code claims. Reviewers should ask what happens on timeout, retry, restart, duplicate input, partial completion, stale authorization, malformed data, and rollback. ## Pull request evidence A focused change should state: ```text Boundary changed: Behavior before: Behavior after: Failure behavior: Compatibility impact: Commands executed: Tests discovered/passed/failed/skipped: Generated artifacts: Security assumptions: Operational or rollback impact: Known residual risk: ``` Attach logs or machine-readable reports for release gates, but keep transient build output out of Git. Claims in README files, reports, certificates, and release notes must match the commands executed in the same revision. ## Documentation rules - Describe implemented behavior in the present tense. - Describe intended design with words such as "intended," "planned," or "modeled." - Name the command and test count behind a passing claim. - Call a cryptographic primitive by name only when that primitive is actually used and verified. - Do not call ordinary files WORM storage. - Do not call metadata checks compilation, proof, review, merge, or deployment. - Do not label a proof zero-placeholder until CI scans the release theorem closure. - Keep performance values labeled as targets until a reproducible benchmark produces them. The release-readiness criteria live in [`PRODUCTION_HARDENING.md`](PRODUCTION_HARDENING.md).