Skip to content

Development and Operations

Sasha Lopashev edited this page Jul 21, 2026 · 34 revisions

Development and Operations

Stack

BHCP is a Rust-only repository-owned implementation. Rust 1.97.1 is pinned in .mise.toml and in the crate manifest. Runtime dependencies are pinned Rust crates: cddl for RFC 8610 parsing/validation support and RustCrypto sha3 for SHA3-512. The repository has no project-owned Ruby, Python, Node.js, or C toolchain.

Install the pinned toolchain:

mise install

Local quality gate

Run the same four checks before delivery:

cargo fmt --check
cargo clippy --all-targets -- -D warnings
cargo test --all-targets
cargo build --release

The 17-root CDDL fixture gate is part of the Rust test suite and can be run directly with:

cargo test --test schema_fixtures

Use cargo run --bin generate-fixtures only when intentionally regenerating checked-in AST/IR fixtures, then review deterministic byte changes.

CLI smoke path

cargo run -- parse conformance/v0/fixtures/canonical-simple.bhcp > /tmp/canonical-simple.ast.cbor
cargo run -- lower conformance/v0/fixtures/canonical-simple.bhcp > /tmp/canonical-simple.ir.cbor
cargo run -- inspect conformance/v0/fixtures/canonical-simple.bhcp
cargo run -- inspect /tmp/canonical-simple.ir.cbor
cargo run -- hash conformance/v0/fixtures/canonical-simple.bhcp
cargo run -- policy inspect conformance/v0/fixtures/canonical-policy.bhcp
cargo run -- policy compose conformance/v0/fixtures/canonical-policy.bhcp > /tmp/effective-policy.cbor
cargo run -- policy inspect /tmp/effective-policy.cbor
cargo run -- verify <contract.bhcp> <goal-symbol> <candidate.cbor> <subject-file> <produced-at>

parse and lower emit CBOR, inspect emits a human-readable outline, and hash emits the algorithm-tagged semantic ID. JSON is not a BHCP repository artifact format.

policy compose consumes explicitly ordered canonical source or source-policy CBOR inputs and emits deterministic validated effective-policy CBOR only after every input, layer transition, feature, and monotonicity check succeeds. policy inspect renders source values or effective layers, rule values, waiver governance, semantic/artifact identities, and exact source-rule provenance. It never uses JSON as an intermediate artifact format.

Delivery status

  • Implemented and measured: the Rust quality GitHub Actions workflow runs formatting, warnings-as-errors Clippy, a release build, and the exact 17-root CDDL fixture invariant independently. A plan validator requires every root integration target exactly once plus library/binary coverage; six concurrent partitions feed the stable fail-closed Rust quality / Tests aggregate. Test-only SHA3/Keccak optimization leaves release semantics unchanged. #97 reduced exact-head protected feedback from 38:01 to about 5:06 (86.6%, 7.5× faster). PR #142 retained the 64 MiB adapter executable ceiling while removing platform debug payloads from test binaries; its complete hosted matrix finished in about three minutes and the formerly failing adapter shards completed in 52–83 seconds. Actions are commit-pinned and Cargo dependency caches are keyed by .mise.toml and Cargo.lock.
  • Required on main: strict branch protection, including for administrators, requires Rust quality / Format, Rust quality / Clippy, Rust quality / Tests, Rust quality / Release build, and Rust quality / 17-root CDDL fixtures; force pushes and deletion are disabled and review conversations must be resolved.
  • Implemented: the goal-algebra conformance harness regenerates and root-validates exact AST/IR bytes for all, any, none, chain, and gate; resolves named empty/adversarial and generic proof-check evidence; pins the six generator inputs and 17 schema roots; and requires the feature manifest to distinguish the implemented algebra from deferred complete obligation graphs.
  • Implemented: the repository-local AGENTS.md operating contract and project-loop profile define authority, issue selection, atomic remote-ref claims, TDD, protected review/merge, fenced release, and completion reconciliation.
  • Implemented: the safe-Rust bhcp::experiment controller freezes model/reasoning/sandbox/toolchain pins, exact executables, inputs, run order, limits, and canonical tree identities before launch. It exclusively owns scratch/target trees, clears process environments, enforces combined output/time ceilings and process-group cleanup, withholds oracles until agent completion, gives every judge an ephemeral isolated view, and emits bounded Markdown evidence rather than repository JSON event logs. The focused controller suite includes adversarial tree framing, symlink escape, hidden target content, output flooding, orphaned descendants, ambient judge variables, judge mutation, and both oracle-order cases.
  • Implemented: bhcp verify discovers the nearest bhcp-project.toml, compiles and validates the exact contract/candidate boundary, rejects unregistered or contract-extraneous bindings, dispatches only capability-bounded adapters, binds the exact supplied subject reference and bytes, and emits deterministic evidence with distinct accepted, rejected, unresolved, and faulted results.
  • Implemented: bhcp::proof independently revalidates complete obligation closures against sealed child observations and evidence, including exact execution-instance binding for claims, items, gaps, expression contexts, and reducer premises. Its protected integration suite covers four-state outcomes, behavior-neutral none, zero/one/many discharges, repeated-goal substitution, registry and adapter authority, policy minima, and deterministic derivation identity.
  • Audited: cargo test --test phase_two_evidence_audit hashes every recorded Phase 2 input, result, and executable evidence source, requires the named Rust test declaration, checks semantic identities, and enforces the exact experiment-to-issue/PR/squash-merge map. The linked replay suites remain the executable outcome evidence.
  • Registered: cargo test --test evidence_generalization_preregistration checks the closed future-study manifest, every Git-blob and semantic-ID pin, the four-task registered-use and three-task comparative populations, exact 36-session schedule, six/six order balance, analysis/non-claims, billing preflight, and enforceable resource boundary before any model turn.
  • Measured and replayable: cargo test --test evidence_generalization_positive_runner checks every preserved positive-use session and its 0/12 result. cargo test --test evidence_generalization_comparative_results recomputes the 12 paired outcomes, 0/12 acceptance per arm, zero paired risk difference, exact McNemar p=1, and 12/12 calibrated claims per arm from the checked-in comparative record.
  • Implemented: squash-only auto-merge is matched to the reviewed head SHA, merged topic branches are deleted automatically, and PR bodies use issue-closing links. Disposable probe PR #56 proved that a mismatched expected head and author approval are rejected and that one failed required check keeps queued auto-merge blocked.

Remote CI and branch protection are now authoritative. A local green run remains the required fast feedback loop, but is not a substitute for the protected hosted checks or review.

Troubleshooting principles

  • Unsupported canonical syntax must return a stable diagnostic; do not silently ignore it.
  • Source files are scanned as raw bytes before lexing. Invalid UTF-8, CRLF or non-ASCII preamble whitespace, aliases, duplicate or misplaced directives, and a BOM outside byte zero fail as BHCP0003 without artifact output. Omission and an optional leading BOM select bhcp/canonical@0; an exact custom profile that has no registered normalizer fails closed as BHCP0004. The scanner retains original byte offsets while treating a leading BOM as logical column 1.
  • Typed syntax/profile artifact failures use stable BHCP9001 diagnostics. Check unknown fields, malformed or self-referential parents, illegal type modes, invalid formatting records, duplicate local overlays, and mapping coordinates that are duplicated or not in category/canonical order. Mapping entries serialize in deterministic coordinate order, while valid policy overlays retain declared order. The generic 17-root validator deliberately maps these typed failures to its root-level BHCP5002 boundary.
  • Effective syntax registration fails as BHCP9002 before reading program tokens when inheritance is unresolved or a map has an unknown coordinate, non-NFC/invalid surface, ambiguous spelling, punctuation prefix, alias recursion, core rebinding, or capture of fixed operators and contextual words. The diagnostic names the selected profile, syntax, offending category:canonical=>surface mapping, stable mapping-list entry, and rule. An unregistered selected profile remains BHCP0004; using a canonical spelling that the selected map replaced is BHCP0005 at the actual program-source point with the same structured context. Unsupported parser callbacks, unrestricted macros, and semantic overrides fail typed artifact decoding as BHCP9001. Every failure is atomic: no artifact or stdout is emitted. Registered custom source lowers through the ordinary parser while diagnostics retain original byte, line, and column points; comments and string contents are never remapped.
  • Resolved profile topology failures use BHCP9003: inspect missing or cyclic profile/syntax parents, unrelated child syntax, weakened child type modes, duplicate root-to-leaf overlays, and missing overlay policy parents. Successful inspection prints deterministic profile and syntax chains, overlay order, effective type mode, and effective-policy identity. Overlay weakening still uses the policy composer's category-specific BHCP8101BHCP8107 diagnostics.
  • bhcp format accepts canonical source directly or custom source plus explicit syntax/profile/source-policy CBOR registry artifacts. It retains comments, mapped Unicode spellings, an explicit preamble or BOM, wraps only between tokens, and honors the resolved indentation, width, and final-newline record. A reparse that changes the canonical token stream or AST shape fails atomically as BHCP9004; never redirect a failed invocation into a source replacement.
  • The checked-in conformance/v0/profile-layout manifest indexes two syntax roots, two profile roots, a shared policy overlay, compact symbolic and spaced narrative sources, and their exact formatter snapshots. The harness validates deterministic syntax/profile/AST/IR CBOR roots, equal semantic IDs with different presentation artifacts, label/comment sensitivity only in artifact identity, a semantic policy-change control, and stable diagnostic code/message with layout-sensitive source points.
  • The Phase 4 completion audit contains exactly three acceptance claims for every issue #41–#49, binds each claim to a named checked-in test on the correct issue row, resolves every local evidence link, and pins the reviewed #41–#48 delivery ledger. It closes the bounded presentation milestone while retaining the incomplete-v0 and arbitrary executable syntax non-goals.
  • Process-backed verifiers run only through the packaged bhcp-adapter-sandbox helper. macOS uses /usr/bin/sandbox-exec; Linux requires Landlock ABI 4 with full requested enforcement plus seccomp network denial. A missing helper or unavailable enforcement fails closed before the verifier starts (BHCP7001).
  • Adapter execution uses the registered project-relative executable and exact argv without a shell or PATH, clears ambient environment, closes inherited file descriptors above stderr, and enforces declared project read/write scopes. Timeouts and cancellation remain unresolved outcomes; malformed output, nonzero exit, limit violations, and sandbox or launch failures remain operational faults rather than semantic verdicts.
  • Registered verifier executables must not be mutated concurrently. The runner revalidates stable executable identity through the final pre-launch boundary, but native launch still reopens the canonical path; deployment permissions must prevent replacement during that residual path-open window.
  • For policy failures, use the category-specific BHCP8101BHCP8107 code or BHCP8110 for source topology. If a weakening message names the wrong earlier rule after several rules compose, inspect the governing contributor rather than provenance order. An invalid layer must return no effective policy; a partial result is always a composer bug.
  • If a policy identity mismatch appears, recompute semantic ID from effective only and artifact ID from the complete document with only artifact_id removed. Source layers or provenance changing semantic ID is a projection bug; observable effective rules changing only artifact ID is also a bug.
  • If policy compose emits bytes on a failing invocation, treat it as an atomicity bug. Wrong layer order must be BHCP8110; unsupported policy features or malformed policy forms must remain BHCP8001; category weakening keeps its BHCP8101BHCP8107 diagnostic. Source and equivalent source-policy CBOR inputs must produce identical effective bytes.
  • Policy-aware elaboration fails before valid semantic IR with BHCP8200 for an invalid policy boundary, BHCP8201 for a type-mode floor violation, BHCP8202 for a prohibited effect, BHCP8203 for missing or non-provable capability authority, and BHCP8204 for an exact dimensioned limit above an applicable maximum. Check goal/effect scope applicability as well as the rule value; deny wins, and a scoped maximum can constrain a matching global goal limit.
  • If two policies with equal effective restrictions produce different program semantic IDs, inspect the IR policy projection: it must retain the effective semantic ID only. Artifact identity and serialized IR bytes may still differ because source layers, rule provenance, and policy artifact identity are audit material.
  • Reducer failures in an unselected branch are still definition failures: the whole expression tree must validate before execution. An unknown call must remain a stable kernel diagnostic, and any primitive value or satisfied conclusion that disagrees with its declared type must be rejected before generic derivation verification.
  • If any chooses a different winner across equivalent source or observation arrival orders, inspect canonical child-tag ordering. Multiple sealed satisfactions must choose the lexicographically least normalized tag; explicit composition must pass the same winner type boundary as the convenience form.
  • If none emits an empty record, accepts a declared output field, or drops counter-evidence from a mixed unresolved result, inspect its inferred goal signature and sealed partial-evidence aggregation. Its output is canonical Unit; satisfaction requires every child's counter-evidence.
  • If chain requests or accepts a later child before its predecessor is sealed satisfied, inspect both the observed-output edge and runtime readiness validation. A later-step refutation must retain prior satisfaction evidence as derivation premises; terminal counter-evidence alone does not prove causal reachability.
  • If gate observes a child while its condition is false, inspect the excluded primitive and sealed observation record: a closed gate must reject the execution claim. If two same-signature gates share a reducer despite different conditions, inspect the condition component of reducer specialization identity. Parent-to-child argument tampering must fail at the typed parent-field edge, and claimed derivation tampering must still fail through the generic checker.
  • Unknown hash algorithms fail before parsing; the project manifest is an agility boundary, not arbitrary dynamic loading.
  • Missing verifier registrations remain unresolved evidence gaps; contract strings are never executed as shell commands.
  • A policy evidence obligation runs only producers explicitly bound by its semantic symbol through the verifier registry. Missing mappings or registrations use bhcp.reason/policy-verifier-unregistered@0; too few accepted policy-class items use bhcp.reason/policy-evidence-minimum@0. Check the inspected structural target, accepted classes, minimum, and layer/policy/rule provenance. Reordering registrations must not change bytes, and removing the retained effective policy must fail closed before dispatch.
  • When schema tests fail, compare Rust model encoding, CDDL, examples, and SEMANTICS in the same change.
  • Preserve unrelated worktree changes and never regenerate fixtures incidentally.

Clone this wiki locally