Theory->Engineering: consent in TCB (A3), semantic gate (A4/A5), Mahdavi compass (A7) + red-team#4
Open
Aliipou wants to merge 31 commits into
Open
Theory->Engineering: consent in TCB (A3), semantic gate (A4/A5), Mahdavi compass (A7) + red-team#4Aliipou wants to merge 31 commits into
Aliipou wants to merge 31 commits into
Conversation
Engineering unchanged. Adds a code-free reading layer mapping each Theory-of-Freedom component (axioms, ownership hierarchy, consent, divine justice, guidance, Mahdavi compass, conflict-by-clarification) to its file:line in src/, with an honest coverage matrix marking enforced vs. extension-only vs. documented gaps.
…ted coverage exclusions
…icy DSL, multi-agent; pragma unreachable branches
…, goal violations
… federation; pragma defensive branches
… regression guard)
Companion to COVERAGE_MATRIX.md, adding the formal-artifact column it omits: the actual Lean theorem / Kani harness behind each axiom AND its true strength. Honest findings (no spin): - A4/A6 are Kani-proven (prop_ownerless_machine_blocked, prop_machine_governs_human_blocked); their Lean theorems are `True := trivial` stubs. - A5/A7 attenuation + epoch revocation are real Lean proofs. - forbidden-flag theorems are real but SHALLOW: they prove "flag set => Blocked" (enforcement of a declared flag), NOT detection of coercion/deception. - verify_deterministic is `:= rfl` (vacuous). - Consent is Python-only/partial and absent from the Rust TCB; Justice, Guidance, and the Mahdavi compass are extensions-only with no proofs. Conclusion stated plainly: AuthGate is a proven (narrow) Rights *Verification* Kernel; the book's Rights-based *Decision* Kernel (detect coercion; choose the most legitimate among permissible actions) is not built and has no formal content. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
47 attack tests across the three Theory-to-Engineering gaps: - consent_redteam.rs (18): forged grantor keys, pubkey substitution, resource/rights swaps, consent-id forgery, revocation bypass, post-seal injection/reorder, documented L2 trust-root limit, permit<->valid invariant. - semantic_gate_redteam.rs (15): exit-block disguise, HHI boundary, case/ substring/unicode-homoglyph evasion (documented), NaN/negative shares, 50+ case totality sweep, advisory-never-denies. - compass/redteam.rs (14): score-gaming, NaN/Inf, zero/negative/huge weights, registry poisoning, and the safety proof that the Compass never denies. Full suite: 293 passed, 0 failed. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…verage - Replace the misleading 'Python layer enforces the same logical invariants as the Rust TCB' claim with an honest 'compatibility runtime, not a security boundary; bypassable; only the Rust TCB carries guarantees'. - Add a Theory->Engineering coverage table for the three now-implemented axioms (A3 consent = TCB; A4/A5 semantic gate + A7 compass = advisory, NOT TCB), each with explicit trust level and no overclaim (notes the L2 owner-binding limit; calls the compass 'never denies' an asserted test, not a proof). - Update the verified Rust lib test count to 293 (incl. 47 red-team tests). Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
# Conflicts: # README.md
The zero-panic clippy gate runs -D warnings over --all-targets; the 8-arg consent_signed_by test helper tripped clippy::too_many_arguments. Scoped allow on the test-only helper. Verified clean locally with the exact CI flags. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…, E702) These test files came in via nazariye-azadi and had never run through main's ruff gate. Auto-fixed import sorting + unused import; split semicolon multi-statements (E702) onto separate lines. ruff check src tests now clean. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…ayer above) Explains why AuthGate (authority/enforcement, Rust TCB, crypto) and the Freedom Decision Kernel (legitimacy/decision, pure Python, no crypto) are separate sibling repos: legitimacy != authority. FDK decides whether an action is legitimate and hands the chosen action to AuthGate, which enforces whether the actor is authorized. Legitimacy first, then authority. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…act) Lock the responsibility split between the two products and connect them through ONE serialisable contract, not shared code: - spec/policy_decision.schema.json: the boundary contract FDK emits (verdict ALLOW/DENY/DEFER, action_id, reasons, axiom_trace, fail_closed). No 'confidence' field — FDK is a deterministic categorical gate; DEFER already expresses 'unsure, ask a human'. - authgate.integrations.fdk.enforce_legitimacy(): the ~50-line seam. Runs the CallGate (capability + scope + signature + TCB) ONLY on an explicit ALLOW bound to the same action_id. Fail-closed on DENY, DEFER, fail_closed, malformed payload, or action_id mismatch — no path from non-ALLOW to a tool call. Imports NO FDK code (the contract is the only coupling). - tests/test_fdk_bridge.py: golden end-to-end flow + JSON round-trip + every non-ALLOW/malformed path, against a real registry/verifier/CallGate. 15 tests, module 100% covered. - examples/fdk_authgate_flow.py: decoupled runnable demo (3 outcomes). - DECISIONS.md: records the contract-not-code boundary decision. ruff + mypy clean; AuthGate stays the sole source of truth for authority, FDK only interprets legitimacy. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…hema Contract-drift guard for the AuthGate half of the hand-synced FDK<->AuthGate boundary: asserts spec/policy_decision.schema.json's required fields are exactly what parse_policy_decision enforces, the verdict enum matches, and a fully populated schema payload parses. A schema change now breaks CI here instead of silently in production. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…ased] Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
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
2 participants
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 & why
Closes the three open gaps in
Theory_to_Engineering_Plan.md, mapping axiomsA3/A4/A5/A7 of the Theory of Freedom (نظریه آزادی) from prose into Rust. Each
gap previously existed only as bypassable Python; this lands the parts that
belong in code, at the correct trust level — and nothing more.
Changes
src/tcb/consent.rs(+engine.rsLayer-4 gate,types.rsfields)src/semantic_gate.rssrc/compass/ConsentRecord(ed25519, identity-bound, expiry, revocable). When theadapter sets
requires_consent, noPermitissues without a valid, unexpired,unrevoked consent covering actor+resource+rights, folded into the binding hash.
SemanticGatetrait +CoercionAnalyzer(exit-blocking, HHI,deception markers). Returns a verdict; never structurally denies.
C(a) = w1*RVD + w2*VOI + w3*CDas a post-hoc scorer that annotates,never denies. The deny threshold is operator policy, not theory.
Honest scope (no overclaim)
that's the L2 trust-root boundary, out of scope by design (documented + tested).
engine.rs+28,types.rs+14,call_gate.rs+2.Tests
cargo test --lib→ 293 passed, 0 failed, including 47 red-team attack tests:tcb/consent_redteam.rs(18),semantic_gate_redteam.rs(15),compass/redteam.rs(14).Not in this PR (follow-ups from the 10-week plan)
Lean4 theorems (ConsentRequired, VerifierMonotonicity), Kani harnesses for the
consent path, TLC/Java run, the Constitutional-AI benchmark, and wiring the
semantic gate into
CallGate.🤖 Generated with Claude Code