tb-encode: admission codec + strength-attenuation lemma (self-modification gate, Kani-proven)#91
Open
bahadirarda wants to merge 3 commits into
Open
tb-encode: admission codec + strength-attenuation lemma (self-modification gate, Kani-proven)#91bahadirarda wants to merge 3 commits into
bahadirarda wants to merge 3 commits into
Conversation
…ation gate)
The pure, host-verifiable value layer of the capability-gated self-modification
protocol (docs/cogi-cognitive-architecture.md): an untrusted proposer submits an
AdmissionRequest (organ + witness + spec digests, claimed strength, effect mask,
budget); the trusted verifier plane answers with an AdmissionVerdict (admit XOR
reject + the GRANTED, attenuated strength & rights). Two fixed-layout LE codecs
(ADMIT_REQ_LEN=117, ADMIT_VERDICT_LEN=86), total decoders, no unsafe, zero dep.
strength_attenuate() is the trust-lattice analogue of Rights::intersect: the
granted strength is the WEAKER of claimed vs warranted (PROVEN=1 .. EMPIRICAL=4),
out-of-range clamps fail-closed to EMPIRICAL. So EMPIRICAL evidence can never be
laundered into a PROVEN grant.
Kani (cargo kani -p tb-encode), all SUCCESSFUL:
* kani_admit_req_roundtrip - decode(encode(r)) == r, full symbolic input
* kani_admit_verdict_roundtrip - decode(encode(v)) == v
* kani_strength_attenuate_never_inflates - forall c,w in u8xu8: result is a valid
level AND >= both clamped inputs (the monotone never-inflate lemma)
Not yet wired into the kernel boot path; this is the Phase-0 value foundation.
Yuva is agent-agnostic (docs/spec/yuva-abi-v1.md §8); the module doc must not name a specific resident agent. Describe the admission gate generically instead.
…35 -> 138) The prove-encode shards fail closed unless the four pinned lists sum to EXPECTED_HARNESSES_TOTAL == the proofs.rs '#[kani::proof]' count. Adding the admission codec harnesses without this lockstep edit left the count at 135 vs 138 in source, so every shard reported the guard failure. Route the three cheap value-layer harnesses (kani_admit_req_roundtrip / kani_admit_verdict_roundtrip / kani_strength_attenuate_never_inflates, all <2.5s local) into shard A next to the thematically-adjacent attest codec, and bump the pin + shard-A count. SHARD GUARD: OK -- A=58 + B=36 + C=9 + D=35 == 138 == proofs.rs count.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
What
The pure, host-verifiable value layer of the capability-gated self-modification protocol (
docs/cogi-cognitive-architecture.md/cogi-substrate-architecture.md) — the Phase-0 foundation for admitting a proposed organ/skill into a running Yuva.AdmissionRequest(untrusted proposer's ask): organ/witness/spec content digests, claimed strength, proposer id, effect mask, budget.ADMIT_REQ_LEN=117, total LE codec.AdmissionVerdict(trusted verifier plane's decision): admit XOR reject + the granted, attenuated strength & rights, folded into provenance.ADMIT_VERDICT_LEN=86, total LE codec.strength_attenuate— the trust-lattice analogue oftb_caps_core::Rights::intersect: the granted strength is the weaker of claimed vs warranted (PROVEN=1 .. EMPIRICAL=4); out-of-range clamps fail-closed toEMPIRICAL.EMPIRICALevidence can never be laundered into aPROVENgrant.#![no_std]+forbid(unsafe_code)+ zero-dep, socargo kani -p tb-encodemodel-checks the exact bytes the kernel would admit.Proofs (all
VERIFICATION: SUCCESSFUL, localcargo kani -p tb-encode)kani_admit_req_roundtripdecode(encode(r)) == rover the full symbolic requestkani_admit_verdict_roundtripdecode(encode(v)) == vover the full symbolic verdictkani_strength_attenuate_never_inflatesc,w ∈ u8×u8: result is a valid level and>=both clamped inputs (the monotone never-inflate lemma)Each harness carries a negative-control note (the concrete code break that turns it
FAILED).Honesty / scope
The four strengths are not interchangeable and are documented as such: only
PROVEN(Kani/CBMC) is actually sound;CONFORMANCEis a single test vector;EFFECT_BOUNDEDis as strong as its spec;EMPIRICALis evidence for a human. The codec also notes the standing caveat that a sound proof of a proposer-authored spec still admits an unsafe organ — the spec must originate in / be countersigned by the trusted ring.Not yet wired into the kernel boot path — this is the value foundation only; the in-kernel admit-dispatch + witness marker land in a follow-up.
No behavioural change to any existing organ; net-new module, additive only.