docs/framework.md

Kaysentinel / PCAL + Sentinel — Formal + Engineering Framework

See also: semantic_contract.md is now the normative source of truth for the extraction semantics summarized informally in §1 and §2.3–2.4 below (identity pruning, lifecycle resolution, the Included/Rejected × Success/Revert/Halt outcome matrix, and the SSZ sorting rules). This file keeps the higher-level architecture and theorem statements; where the two disagree, semantic_contract.md governs. validation_vector_spec.md defines the frozen v1.0.0 test-vector schema and mutation-event vocabulary used by the conformance vectors in the fixtures repo's validation_vectors/. ssz_profile.md defines the Layer 2 serialization and merkleization rules, with a real, reproducible worked example and a runnable reference encoder (../scripts/ssz_reference.py). emes_profile.md defines the Layer 0.5 client telemetry format and a compiled, tested Geth tracer (../tracer/kaysentinel_tracer.go) targeting go-ethereum's current tracing.Hooks API, plus a real Gate 1 structural verifier (../validation/gate1.go) and fixture-writing harness (../harness/harness.go). Wire event types live in ../emes/, kept separate from the Geth-specific collector so a future Reth/Besu adapter can reuse them. raw/transcript/README.md documents a lower-level, in-process trace buffer (raw/transcript/), now on its second design (flat RawEvent, not the earlier tagged-union + hash version -- that tradeoff is recorded there), plus ../multiplexer/broadcast.go (panic-isolating fan-out to multiple hook sinks) and a differential validator (../validation/normalizer.go, ../validation/engine.go). All compiled, vetted, and exercised end-to-end -- see the README for what was actually tested versus what's still an open integration question.

0. System Overview

Kaysentinel defines a post-execution authorization architecture for state-machine systems (e.g., Ethereum-class runtimes) by lifting execution traces into a canonical Structural Sufficient Representation (SSR) and evaluating policies purely over that quotient space.

Core idea: instead of authorizing execution paths, the system authorizes equivalence classes of state-impacting traces.

1. Formal Semantic Foundation

1.1 Execution Model

• Σ = space of execution traces
• s ∈ S = pre-state
• t ∈ T = transaction
• Π(s,t) ∈ Σ = deterministic execution trace

1.2 Observation Model

Post(σ) := (State(σ), Receipt(σ), Context(σ))

• State(σ) = (balances, storage, transient, nonces, lifecycles)
• Receipt(σ) = (logs, status, gas)
• Context(σ) = (block, tx_index, basefee)

1.3 SSR Extraction Map

E: Σ → Δ, where Δ is the canonical SSR space.

1.4 Fundamental Equivalence Property

• Faithfulness: E(σ1) = E(σ2) ⇒ Post(σ1) = Post(σ2)
• Abstraction: Post(σ1) = Post(σ2) ⇒ E(σ1) = E(σ2)
• Result (quotient isomorphism): Σ / ~Post ≅ Δ

2. SSR Canonical Form

2.1 Canonical Type System (SSZ-based)

Primitive types: Address = Bytes20, Hash = Bytes32, Uint64 / Uint256.

2.2 SSR Structure

Δ := CanonicalSSR, containing account mutations, storage diffs, transient diffs, logs, tx metadata — all with bounded lists.

2.3 Determinism Rules

1. Accounts sorted by address
2. Storage sorted by slot
3. Logs preserve execution order
4. Serialization = SSZ canonical encoding

See semantic_contract.md §5 for the exact byte-wise sorting comparator.

2.4 Canonical Constraint

Ser(Δ1) = Ser(Δ2) ⟺ Δ1 = Δ2

3. Authorization Theory

3.1 Admissible Authorization Class

A ∈ 𝔄_obs iff Post(σ1) = Post(σ2) ⇒ A(σ1) = A(σ2)

3.2 Induced Policy (Factorization Core)

Theorem (Factorization): there exists a unique Ã: Δ → D such that A = Ã ∘ E.

All valid policies operate only over SSR space, never raw execution.

3.3 Policy Execution Pipeline

B(Δ, A_p ⋄ A_proto):

• FAIL if protocol rejects
• else policy evaluation on SSR

3.4 Null Policy Invariance

A_p^∅(Δ) = PASS, so valid execution ⇒ no behavioral divergence introduced.

4. Portability (Multi-Client Consensus Theorem)

Theorem (SSR Portability): let E1 = Geth extractor, E2 = Reth extractor. If both satisfy Faithfulness + Abstraction, then A = Ã∘E1 = Ã∘E2.

Corollary: all compliant clients compute identical policy outcomes — E1(Σ) ≡ E2(Σ) ⇒ no policy-induced forks.

5. Execution Model (Final Semantics)

5.1 Two-Phase Observation Model

• Phase 1 — TraceMid: captured during execution (transient storage snapshot, intermediate write-set)
• Phase 2 — Post(σ): captured after execution (state diff, receipt, logs)

5.2 Execution Identity

σ = Π(s,t); SSR extracted as E(σ).

6. Gating Semantics

6.1 Decision Output Space

{PASS, FAIL, QUARANTINE}

6.2 State Commitment Rules

Result	Effect
PASS	Commit state
FAIL	Revert execution
QUARANTINE	Commit state + isolate metadata

6.3 Non-Divergence Constraint

Policy layer must not alter consensus state root: StateRoot_native = StateRoot_sentinel.

7. Complexity Model

Let N = total state mutations.

• Extraction cost: T_extract = O(N)
• Canonicalization cost: worst-case O(N log N), bounded case O(N)
• Total cost: T_total = O(N log N), practical ≈ O(N)

8. Client Architecture Boundary Model

8.1 Geth Extraction Boundary

• Source: StateDB journal
• Hook: post-execution, pre-commit
• Extract: dirty accounts, storage diffs, logs, transient map snapshot

8.2 Reth Extraction Boundary

• Source: BundleState
• Hook: execution result stage
• Extract: state diffs, storage diffs, logs, transient snapshot

8.3 Canonicalization Layer

Both map into: φ_geth(E_geth) = φ_reth(E_reth)

9. Core Architectural Result

System Closure Theorem: the system defines a closed loop Σ →(E) Δ →(Ã) D satisfying determinism, client independence, post-execution isolation, and quotient-space completeness.

Summary: Kaysentinel is a client-agnostic post-execution authorization calculus over a canonical state quotient space.

10. Implementation Readiness

Specified across:

• Formal semantics (Σ → Δ quotient model)
• Canonical encoding (SSZ SSR)
• Multi-client extractors (Geth / Reth)
• Policy calculus (Ã factorization)
• Execution gating semantics (PASS/FAIL/QUARANTINE)
• Complexity guarantees (O(N) / O(N log N))
• Normative semantic contract with a validation-vector catalog (see semantic_contract.md and ../tests/ in the fixtures repo)

Not yet done: no reference implementation exists for the Geth/Reth extractors or the SSZ encoder. The theorems above are design invariants to build and test against, not proofs that have been mechanically verified.