-
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, and policy-added structural evidence obligations.
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.
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.
Planned: complete analysis graphs, waiver evaluation, in-session experiment controllers, planning, and the broader runtime. 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.
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, and verifier-added evidence are implemented through issues #29–#37; complete no-waiver conformance is the next boundary.
Decided, typed, and executable 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. The Phase 4 completion audit #49 is next.