-
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 ownership and resource analysis: #106 and PR #142 run a closed pass before semantic IR emission. Owned/shared/borrowed handles retain access, usage, lifetime, and nominal resource identity; value/move/borrow/share crossings, use-after-move, affine/linear joins, and persistent capture are checked through nested goal topology. Concurrent sibling branches reject incompatible access while explicit chain steps remain ordered. Persistent initializers are inspected recursively, shared retention requires an exact external approval, and executable handle values use the canonical exact {ref: nonempty Text} envelope.
Implemented effect and authority analysis: #107 and PR #143 materialize canonical possible-effect rows before semantic hashing. Atomic goals conservatively expose authored allowed atoms; composite goals preserve actual child effects, project exact parent resource coordinates when available, and retain typed child coordinates otherwise. Deny wins across authored prohibitions, explicit parent ceilings, and effective-policy scopes. Unsafe/foreign effects add unresolved evidence, direct dimensioned limits reject negative or inexact bounds, and same-priority preference objectives require compatible types. Retained semantic IR rederives the row closure and rejects hidden effects, untyped resources, or malformed evidence without panic. Budget allocation, retries, graph construction, and runtime enforcement remain separate stages; obligation and capability construction have since landed as the independently validated artifacts below.
Implemented shared typed graph model: #113 and PR #144 add one safe-Rust wire boundary for obligation, capability, state, execution, and evidence graph roots. It normalizes semantic-set ordering, validates closed shapes and duplicate/dangling/cyclic-forbidden references, recomputes semantic and provenance-sensitive artifact identities from distinct schema-coordinate-aware projections, and renders graph structure without a JSON canonical intermediate. Obligation and capability builders now use this infrastructure; state/execution builders, planning, runtime enforcement, and final evidence-graph assembly remain roadmap work.
Implemented structural obligation graph: #114 and PR #147 deterministically construct the complete v0 obligation graph for every retained semantic-IR goal. Structural nodes cover requirements, guarantees, retained invariants and cases, verifier bindings, typed parent-child discharge dependencies, and every applicable effective-policy requirement, evidence, and limit. IDs derive from stable structural meaning rather than source ordinals; source clauses and policy provenance remain artifact-only. Retained policy applicability and its type-mode floor are recomputed before construction, so deletion, substitution, scope drift, or weakening cannot silently erase governed obligations. All nodes begin open; discharge remains owned by later proof-checking and execution stages.
Implemented capability decision graph: #115 and PR #149 lower each fully revalidated possible effect into one deterministic request and final allow decision, with exact structural resource coordinates, authored or propagated ceilings, matching effective-policy grants, denial context, parent propagation, applied-waiver audit material, and required unsafe/foreign/unsupported gaps. Policy grant and denial records preserve their exact normalized goal/resource/operation scopes; source clauses, policy decomposition, positional indices, and waiver artifacts remain audit identity rather than structural authority identity. Obligation and capability builders now reject stale IR bytes, semantic identity, artifact identity, policy applicability, or fabricated graph decisions before planning. Planning still cannot grant authority, and runtime enforcement remains separate.
Implemented graph-builder feature negotiation: #148 and PR #152 advertise the exact bhcp/feature.obligation-graph-builder@0 and bhcp/feature.capability-graph-builder@0 identifiers emitted by real graph artifacts. The executable manifest check derives coverage from both builders instead of trusting a parallel hard-coded claim. State/execution graph construction, planning, runtime enforcement, and final evidence assembly remain outside those feature declarations.
Implemented complete-obligation-graph proof checker: #117, PR #150, and the follow-up #151 / PR #153 revalidate the exact compilation and obligation closure, re-evaluate the retained behavior-neutral reducer, bind every premise to its structural child dependency and exact execution instance, and check candidate, payload, producer, verifier, policy-minimum, expression-context, gap-reason, and derivation identities. The exact reducer remains authoritative for child composition; parent-local dispositions combine under Refuted > Faulted > Unresolved > Satisfied, rejecting a weaker reducer result without treating discharge labels as parent proof rules. The checker preserves satisfied, refuted, unresolved, and faulted outcomes across zero, one, or many discharges and repeated invocations of the same goal. It does not construct the state, execution, or final evidence graphs and does not grant planning or runtime authority.
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. Supported goal slices now cross type checking, definition elaboration, ownership/resource analysis, and effect/authority analysis; complete case execution, recursion, and retention lowering remain explicit later boundaries.
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 extension resolution and lowering: #110 and PR #145 execute derived descriptors through a restricted total-pure BHCP meta evaluator, check and monomorphize reducer declarations including generic bounds, assign structural IDs only after lowering, and retain only checked core kernel IR. Explicitly registered native extensions retain their exact validated descriptor and deterministic payload as sorted unique must-understand semantic nodes. Unsupported, schema-mismatched, malformed, policy/core-overriding, or tampered source and retained forms fail before planning; derived lowerer presentation does not survive runtime semantic identity.
Implemented inline policy and waiver lowering: #108 and PR #146 compose materialized source policies and apply fully materialized source waivers through the canonical policy engines before governed semantic IR emission. One caller-injected decision time governs every waiver; all six typed changes, exact scope, delegated authority, interval, audit, and partial-scope rejection semantics match the canonical document path. Inline and external effective policy cannot be mixed. Governance remains active for supported native-extension-only IR, so retained policy cannot disappear and missing-time or unresolved-waiver inputs fail closed at that boundary.
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: construct the remaining state and execution graphs, add the cross-graph audit and planning, and build the broader runtime and final evidence assembly. Generic complete-obligation-graph proof checking is already implemented by #117, PR #150, and its precedence correction #151 / PR #153. 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.