-
Notifications
You must be signed in to change notification settings - Fork 0
Architecture and Approaches
flowchart LR
A["Profile-selected source"] --> B["Canonical tokens"]
B --> C["Canonical AST"]
C --> D["Type, effect, and policy elaboration"]
D --> E["Semantic IR"]
E --> F["Obligation and capability analysis"]
F --> G["Planning and execution"]
G --> H["Evidence and result artifacts"]
Implemented today: canonical source through semantic IR, deterministic artifact encoding and identity, a focused kernel/prelude path, registered verifier dispatch, deterministic evidence bundles, a capability-bounded local verifier process runner, targeted process-result mapping with retained declaration/executable provenance, policy-added structural evidence obligations, and the bhcp verify project-registry path used by controlled agent sessions.
Implemented definition front end: #100 parses complete v0 type definitions, general function signatures and bodies within the current expression slice, predicates with optional source definitions and canonical verifier arguments, and standalone refinement edges. The canonical AST retains source order and exact spans plus bounded generics, structural/algebraic/collection types, nominal identity, handles and lifetimes, refinement binders, effect rows, and verifier argument modes. Duplicate, malformed, unsupported, or reserved-capture forms fail before an artifact. Checked type definitions now enter semantic IR.
Implemented value/type checker: #103 and PR #139 normalize and validate every v0 wire type, enforce generic arity/bounds, nominal and structural subtyping, goal variance, relational union/intersection canonicality, exact machine bounds, closed resource/handle references, and recursive checked Dynamic transitions. Refinement evidence is produced only by evaluating the supported total comparison/Boolean predicate and is bound to both its normalized predicate and exact candidate. Refinement binder presentation names do not affect semantic identity. The shared integer representation covers both deterministic-CBOR integer major types and rejects diagnostic values outside that wire domain before IR or serialization.
Implemented expression and pattern calculus: #104 and PR #140 validate the complete S5 wire expression tree before evaluation and deterministically evaluate every v0 expression and pattern form. The closed evaluator covers immutable records, tuples, lists, sets, Text-key maps and canonically ordered generic-key map pairs; exact Integer, Rational, and Decimal operations; checked machine integers; exhaustive guarded matching; casts; and static or accepted-evidence-bound finite quantification. Rational intermediates use exact unbounded arithmetic, nonzero Decimal exponent magnitude is bounded to prevent resource exhaustion, and verifier witnesses bind the exact expression, verifier, evidence, trust domain, and finite domain.
Implemented function and predicate elaboration: #105 and PR #141 resolve parsed definitions independent of registration order, infer bounded generic arguments, emit deterministic concrete specializations, alpha-normalize local bindings, and retain canonical predicate verifier inputs and configuration. Specialization identity is bound to its originating template and canonical type arguments; source/generated symbol collisions fail closed. Verifier-only predicates remain declarative evidence boundaries: source calls, verifier configuration calls, retained ordinary expressions, and reducer selection all require the appropriate retained pure body rather than becoming an implicit callback.
Implemented goal front end: #101 parses complete v0 goal headers, facts and initializers, contracts and authority, preferences and verifier arguments, cases and calls, quantified goals, and nested compositions. Structured payloads preserve source order and exact spans; duplicate, malformed, reserved-capture, unknown nested, and mismatched-delimiter forms fail before an artifact. Goal syntax still stops before checked semantic IR until type checking, ownership/effects, recursion, and elaboration land.
Implemented governance front end: #102 parses closed §syntax, §profile, §waiver, and derived/native §extension definitions alongside the typed policy path. All six waiver weakening shapes, scopes, target order, timestamps, authorization and delegation topology, byte-bound references, and extension content-reference rules fail closed through the existing typed models and wire validators. Fully materialized waivers and descriptors round-trip deterministically; exact-symbol references in the frozen source remain explicitly deferred until registry resolution. Arbitrary policy parameters values remain unrestricted and do not inherit closed governance-record ordering.
Implemented foundation: source and effective policy documents now cross a strongly typed Rust boundary covering all four layers and all six rule categories. Canonical §policy source lowers through that same boundary with explicit layer and inheritance syntax, typed meta-values, waivability and issuers, and retained definition/rule spans. Comments, layout, and optional human labels remain AST presentation rather than policy meaning. The boundary normalizes deterministic CBOR, rejects unknown fields and invalid category/operation/value combinations, and checks effective semantic and artifact identity. Generic document provenance and per-rule policy provenance are distinct fields (provenance and rule_provenance) so both can coexist without an ambiguous CDDL map key. Strongly typed waiver documents use that provenance to name exact source rules and one of six closed weakening shapes.
Implemented policy composition: validated source documents compose in fixed organization → team → repository → user order. The composer validates inheritance and source uniqueness before joining; rejects capability, limit, and type-mode weakening; intersects scoped capabilities; takes exact limit minima and the strongest mode; retains deny rules; merges waiver governance restrictively; and emits content-addressed source layers, rule provenance, semantic identity, and artifact identity. Equivalent decompositions have identical effective meaning while retaining distinct audit artifacts.
Implemented policy conflict boundary: #33 makes failure atomic and auditable. Distinct codes cover capability widening (BHCP8101), limit loosening (BHCP8102), type-mode weakening (BHCP8103), requirement/evidence removal (BHCP8104/BHCP8105), allow-over-deny (BHCP8106), incompatible limit units (BHCP8107), and invalid source topology (BHCP8110). A conflict names the attempted source rule, the governing earlier contributor after composition, the precise change, and the waiver requirement; no partial effective policy escapes an invalid layer.
Implemented layered-policy identity: #34 exposes and validates one semantic projection over normalized effective restrictions and one artifact projection over the complete effective-policy document minus artifact_id. Observable requirements, evidence, effects, limits, type mode, waivability, and issuers change semantic identity. Presentation and source enumeration normalize away; retained source layers, rule provenance, and authoring decomposition distinguish audit artifacts only. Materialization and external validation use the same algorithm-tagged recomputation boundary.
Implemented semantic policy enforcement: #36 applies a validated effective policy during elaboration. Type-mode floors, prohibited effects, scoped capability grants, and exact dimensioned maxima fail closed before valid semantic IR can escape. Every policy-aware IR retains the effective semantic/artifact reference plus normalized per-goal decision indices; semantic identity commits to effective policy meaning while source-layer decomposition remains audit-only. Applicability is proven from the goal/effect coordinates, deny wins conservatively, and scoped maxima also constrain matching global goal limits.
Implemented policy-added evidence: #37 turns every applicable effective evidence rule into a deterministic structural obligation. Hosts explicitly bind its semantic obligation symbol to sorted registered producers; accepted classes and positive minima govern discharge while missing mappings remain unresolved and rejection/fault semantics stay unchanged. Evidence bundles expose the effective rule and every originating layer/policy/rule. Duplicate restrictions collapse with unioned provenance, distinct later demands remain independent, and retained policy authority is revalidated before dispatch.
Implemented waiver application: one injected decision time validates [not_before, expires_at), complete exact provenance targets, non-waivability, authorized issuers, and finite connected delegation before any mutation. All six weakening categories apply atomically and deterministically, with waiver audit references retained in artifact identity and post-waiver restrictions determining semantic identity. Scope subtraction that the current product-scope rule model cannot represent exactly fails closed.
Implemented experiment boundary: #25 adds a reproducible fail-closed controller for frozen coding-agent plans, isolated candidate workspaces, withheld oracles, ordered judge-specific views, bounded process execution, and auditable Markdown reports. #26 adds the repository-owned Codex driver and versioned runner: macOS applies an operating-system read boundary, denies agent-command network access, withholds the original oracle, isolates credentials, and freezes exact Codex, BHCP, Rustup, and Rust-toolchain identities; unsupported platforms fail closed. The hosted model service remains outside the repository boundary.
Implemented in-session evidence boundary: #27 discovers the nearest manifest, compiles the contract, validates the typed candidate, registers only contract-bounded adapters, binds the exact supplied subject reference and bytes, and emits canonical evidence through bhcp verify. Exit states preserve accepted, rejected, unresolved, and faulted outcomes. Forward 001 is retained as a valid 0/1 negative: the model made no edit, invoked no adapter, and claimed no success. #28 pins and classifies the complete Phase 2 evidence ledger.
Planned outside the completed four-phase roadmap: complete analysis graphs, add planning, build the broader runtime, and run the separately preregistered evidence-generalization studies. The diagram is the v0 architecture, not a claim that every box ships.
A lowered kernel-network carries a structural ID, output type, finite typed children, and a reducer symbol. The Rust kernel supplies only behavior-neutral operations: inspect sealed child observations, construct checked results, resolve stable child tags, and seal derivations. #15 generalizes the retained evaluator with whole-tree validation, typed literals and Boolean/equality operations, total conditionals, stable choice/sequential observation selectors, immediate primitive-result type checks, and final network-output checks. Unsupported calls fail even in an unselected branch and never become host callbacks.
Scheduling order, parallelism, budgets, guards, quantifier families, and behavior kinds do not belong in that network. The checked-in all, any, none, chain, and gate prelude definitions determine their own precedence and aggregation. any uses a stable homogeneous tagged winner; none exposes true Unit and requires every counter-example; chain retains source order and represents each immediate predecessor dependency as a typed observed-output child argument with its ownership mode. Its reducer requests one child at a time, stops on the first non-satisfaction, returns the last output, and includes predecessor satisfaction evidence in later-step refutation proofs. gate specializes a total pure parent-input condition into its retained reducer, binds its unary child's inputs through typed parent-field edges, returns Excluded | Included<T>, and rejects any observation for a closed branch. The generic IR/runtime boundary rejects forward, mistyped, forged, prematurely observed, or closed-gate data edges without adding a behavior tag or guard field. #20 binds the complete five-form algebra to deterministic AST/IR regeneration, schema round trips, feature negotiation, edge cases, and per-form generic proof-check tamper evidence.
This design pays an up-front metamodel/evaluator cost. Its benefit is a smaller trusted runtime and the ability to evolve standard behavior through the language’s own type, purity, totality, policy, and derivation checks.
Goal verdicts are Satisfied, Refuted, or Unresolved. Execution is factored as Completed(verdict) or Faulted(fault), so operational failure cannot masquerade as a semantic answer. Reducers themselves are in the adjectival states Pending or Concluded; those are not verdicts.
Canonical wire artifacts use RFC 8949 deterministic CBOR. The current identity algorithm is the versioned bhcp.hash/sha3-512@0; algorithm choice is explicit in bhcp-project.toml.
- A semantic ID covers normalized meaning and excludes presentation and provenance.
- An artifact ID covers the retained artifact, including provenance-sensitive material where specified.
Observable outputs, obligations, effects, preferences, policies, and authorized evidence change semantic identity. Formatting, comments, diagnostic labels, and presentation-only profile data do not.
The v0 CDDL bundle is the machine-readable artifact contract. The repository uses the Rust cddl crate to parse RFC 8610 and validates all 17 root diagnostic fixtures through the Rust test harness. The compiler, deterministic CBOR codec, and fixture policy remain repository-owned safe Rust.
Policy composes organization → team → repository → user as a restriction lattice, not a last-writer-wins override stack. Typed value/order, composition, identity, CLI, semantic enforcement, verifier-added evidence, and complete no-waiver conformance are implemented through issue #38. Issue #39 fixes exact typed waiver targets, scope, authority chains, injected half-open time validity, atomic rejection, audit retention, and semantic/artifact identity effects; #40 applies that contract across every weakening category with deterministic identity and inspection evidence.
Decided, typed, executable, and audited profile boundary: #41 permits only one-token registered keyword, punctuation, and alias mappings plus bounded whitespace formatting. Exact single-parent syntax/profile chains resolve before tokenization; effective spellings are globally unambiguous and prefix-safe; aliases cannot chain or rebind core symbols. A child profile must retain or descend from inherited syntax, keep or strengthen type mode, and append unique overlays root to leaf before the ordinary restrictive policy composer. Presentation stays in AST artifact identity while normalized tokens and resolved policy meaning determine semantic identity. #42 scans the fixed ASCII preamble from raw bytes before lexing, preserves original hashes and source points, defaults omission to bhcp/canonical@0, and rejects malformed selection before profile rules can run. #43 implements deterministic typed Rust/CBOR syntax and profile artifacts. #44 validates explicitly registered effective maps, lowers NFC keyword/sigil/delimiter/terminator/alias surfaces before the canonical parser, retains original diagnostic spans, and proves canonical/custom semantic identity. #45 resolves profile and syntax chains, accumulates inherited mappings and features, composes attached policy closures through the restrictive engine, and exposes deterministic resolution inspection. #46 formats canonical and custom source through the resolved bounded layout, inverts every effective mapping category, retains presentation data, and proves exact-token and AST-shape idempotence before returning output. #47 pins fail-closed vectors for ambiguous aliases, recursive aliases, token capture, core rebinding, canonical spelling reuse, mapped-away syntax, parser callbacks, unrestricted macros, and semantic overrides; diagnostics identify the exact profile, syntax, mapping, rule, and registry or source span before any artifact can escape. #48 proves the identity split across checked-in symbolic and narrative roots, deterministic formatter snapshots, one policy-governed goal, CBOR root round trips, presentation-only relabeling, a semantic policy-change control, and stable diagnostics. #49 audits all 27 Phase 4 acceptance claims against named executable evidence and keeps arbitrary executable syntax extensions outside the boundary.