docs/semantic_contract.md

KAY Sentinel: Semantic Contract v1.0.0 (Normative)

Status: normative specification. This document supersedes the informal Σ/Δ notation in framework.md §1–§2 with precise, testable rules. It is still a design document — no reference extractor exists yet (see implementation_roadmap.md). Nothing in this file has been machine-checked; "SHALL"/"MUST" describe target invariants that an implementation is required to satisfy, not proofs that have been verified.

1. Structural Definitions & System Boundaries

1.1 The World State

The World State is the mapping from Ethereum accounts to their persistent consensus-defined state, as represented by the execution specification.

1.2 The State Transition Record (SSR)

The State Transition Record (SSR) is the net persistent consensus world-state mutation resulting from execution of a single Ethereum transaction. The SSR isolates state effects from execution paths.

• Persistent Consensus State (INCLUDED): account balance/nonce transitions, deployed bytecode hash updates, and persistent key-value storage slot mutations.
• Consensus Artifacts (EXCLUDED): transaction logs and receipts. These are part of blockchain history but are not part of the state trie, so they are out of scope for the SSR.
• Ephemeral / Execution Metadata (EXCLUDED): gas refunds, access lists, and transient storage exist only to govern execution mechanics and gas accounting. They do not persist in the world-state trie at the transaction boundary and SHALL NOT contribute to the canonical SSR.

2. Orthogonal Transaction Outcome Matrix

Extractors SHALL categorize every transaction along two independent axes.

2.1 Consensus Dimension

• Included: the transaction satisfied intrinsic consensus validity (valid signature, correct upfront gas payment, valid nonce) and was executed within a block. An SSR SHALL be generated for every Included transaction.
• Rejected: the transaction failed intrinsic consensus validation. No EVM execution occurred, no state mutation exists, and no SSR SHALL be generated.

2.2 Execution Dimension

• Success: execution terminated normally, with no halting exception and no explicit REVERT.
• Revert: execution hit an explicit REVERT. Speculative state changes are rolled back, but consensus-level billing (sender nonce increment, gas fee deduction) persists.
• Exceptional Halt: execution aborted on out-of-gas, invalid opcode, or stack under/overflow. All execution mutations roll back; only baseline consensus billing persists.

These two dimensions are orthogonal: a transaction is always exactly one of {Included, Rejected} and, if Included, exactly one of {Success, Revert, Exceptional Halt}.

3. Normative Normalization Rules

3.1 Identity Transition Pruning

Every state update is recorded as a delta Δ = (Value_original, Value_current). Implementations SHALL deep-copy mutable numeric values (e.g. balance integers) during collection to prevent reference aliasing.

If an account or storage slot is modified arbitrarily during execution but Value_original == Value_current at the transaction boundary, it is an identity transition and SHALL be omitted from the finalized SSR delta set.

3.2 Lifecycle Resolution

If an account is created within a transaction (via CREATE/CREATE2) and subsequently SELFDESTRUCTs within the same transaction, its account object SHALL NOT appear in the accounts update list — provided no persistent account remains at the transaction boundary. Structural side effects it caused (e.g. a value transfer to a beneficiary) SHALL still be captured under that beneficiary's own independent account delta.

Note: this rule governs the create-then-destroy case only. The resurrection case — an account that was previously destroyed and later becomes the beneficiary of a same-transaction transfer — is a distinct normative case; see the ssr_normalization/account_resurrection fixture for the worked example this rule does not yet cover explicitly.

3.3 Normalization Post-Condition

The normalization function 𝒩 acting on an unrefined SSR S SHALL be idempotent: 𝒩(𝒩(S)) = 𝒩(S).

4. Formal Compliance Invariants

A conforming extractor MUST satisfy:

• Determinism: identical pre-state + identical transaction input SHALL produce byte-identical SSR encodings across independent client implementations.
• Rollback Safety: mutations from an execution frame that was later rolled back by the client's journal SHALL NOT appear in the finalized SSR.
• Order Independence: internal data-structure ordering (e.g. language-specific hash map iteration order) SHALL NOT affect the structural alignment or serialization of the finalized SSR.
• Completeness: every persistent world-state mutation SHALL appear exactly once in the normalized SSR, unless removed by an explicit normalization rule (§3).
• Minimality: no identity transitions SHALL survive normalization.

5. Serialization Integration Constraints

The serialization layer is decoupled from the semantic layer above; width, byte-ordering, and structural grouping defer entirely to SSZ.

• Canonical sorting SHALL execute only after normalization has finalized the delta entries.
• Account delta sorting: ascending unsigned byte-wise comparison of 20-byte addresses.
• Storage delta sorting: for each mutated account, ascending unsigned byte-wise comparison of 32-byte storage slot keys.

6. Security Considerations

• Mutable Aliasing: extractors sharing memory with the host client MUST deep-copy value types (e.g. pointers to big-integer objects) so that ongoing block processing cannot mutate historical delta records.
• Rollback Desynchronization: if an implementation hooks speculative append points rather than transaction-finality hooks, misalignment between internal EVM call frames and client journal snapshots can leak rolled-back mutations into the "verified" state trie.
• State Bloat DoS: transactions performing deep A→B→A storage thrashing, or excessive transient-storage writes, can force an unoptimized extractor past memory/CPU limits during collection, before normalization trims the footprint. Extractors SHOULD bound per-transaction working-set memory independent of normalization.

7. Versioning Matrix

Field	Value
Semantic Contract Track Version	1.0.0
Serialization Schema Version	SSZ-v1
Target Ethereum Revision	Prague Execution Specification

---

Relationship to framework.md

This document is the normative source of truth for the extraction semantics described informally in framework.md §1 (Formal Semantic Foundation) and §2.3–2.4 (Determinism Rules / Canonical Constraint). Where the two disagree, this document governs until framework.md is updated to match.