Document
Proof Obligations
**Verifiable Semantic Execution Layer (VSEL)**
Verifiable Semantic Execution Layer (VSEL)
PROOF OBLIGATIONS
1. Purpose
This document enumerates the complete set of propositions that must be demonstrably true for VSEL to be considered semantically sound.
This is not a checklist of runtime validations. This is not a list of "things we test."
This is the set of theorems that must hold.
If any obligation listed here cannot be discharged — by model checking, theorem proving, or formal argument — the system contains an unresolved semantic gap.
An unresolved proof obligation is not technical debt. It is an active vulnerability.
2. Structural Classification
Proof obligations are classified into the following categories:
- Axioms — Foundational assumptions accepted without proof within the model
- Definitions — Derived constructs whose well-formedness must be verified
- Semantic Lemas — Intermediate propositions required by higher-level proofs
- Safety Properties — Propositions asserting absence of bad states/traces
- Liveness Properties — Propositions asserting eventual progress
- External Hypotheses — Assumptions about the environment that the model does not prove but depends on
Each obligation must be tagged with:
- Category (axiom / definition / lemma / safety / liveness / external)
- Layer (FSL / SIR / EL / CDL / PL / VL / CL)
- Dependency set (which other obligations it depends on)
- Falsification target (what counterexample would destroy it)
- Discharge method (model checking / theorem proving / testing / argument)
3. Axioms
Axioms are accepted as ground truth within the model. They are not proven; they are assumed. Every axiom must be explicitly listed because an incorrect axiom silently corrupts everything built on top of it.
AX-1: Determinism of Apply
∀ s ∈ S, σ ∈ Σ: ∃! s' such that Apply(s, σ) = s'
Category: Axiom Layer: FSL Dependency: None Falsification: Find (s, σ) producing two distinct s' Discharge: Structural analysis of Apply definition
AX-2: Closure of State Space
∀ s ∈ S, σ ∈ Σ: Apply(s, σ) ∈ S
Category: Axiom Layer: FSL Dependency: AX-1 Falsification: Find transition producing s' ∉ S Discharge: Type-level enforcement + model checking
AX-3: Well-Foundedness of Initial States
∀ s₀ ∈ I: ValidState(s₀) ∧ D(s₀) = Derive(C(s₀)) ∧ τ(s₀) = 0
Category: Axiom Layer: FSL Dependency: None Falsification: Construct s₀ ∈ I violating any conjunct Discharge: Explicit enumeration of genesis constraints
AX-4: Cryptographic Soundness
Pr[adversary forges proof π for invalid τ] ≤ ε (negligible)
Category: External Hypothesis Layer: PL Dependency: None (external to model) Falsification: Cryptographic break of underlying primitives Discharge: Reduction to standard cryptographic assumptions
AX-5: Hash Collision Resistance
Pr[H(x) = H(y) ∧ x ≠ y] ≤ ε (negligible)
Category: External Hypothesis Layer: All Dependency: None Falsification: Collision found in chosen hash function Discharge: Cryptographic assumption
AX-6: Environment Faithfulness
E represents actual external conditions at time of execution
Category: External Hypothesis Layer: EL Dependency: None Falsification: E diverges from reality (oracle failure, timestamp manipulation) Discharge: Cannot be formally proven; must be bounded by threat model
4. Definitional Obligations
These verify that derived constructs are well-formed.
DEF-1: Derived State Functional Dependence
∀ s = (C, D, E, τ): D = Derive(C)
Prove: Derive is a total, deterministic function over valid C. Falsification: Find C where Derive is undefined or non-unique. Discharge: Structural proof over Derive definition.
DEF-2: Canonical Encoding Injectivity
∀ s₁, s₂ ∈ S: Encode(s₁) = Encode(s₂) ⟹ s₁ = s₂
Prove: Encoding does not collapse distinct states. Falsification: Two semantically distinct states with identical encoding. Discharge: Proof over encoding scheme structure.
DEF-3: Commitment Binding
∀ s₁, s₂: Commit(s₁) = Commit(s₂) ⟹ s₁ = s₂ (with overwhelming probability)
Depends on: AX-5 Falsification: Commitment collision for distinct states. Discharge: Reduction to hash collision resistance.
DEF-4: Observable Determinism
∀ (s, σ, s') ∈ T: Obs(s, σ, s') is uniquely determined
Falsification: Same transition producing different observables. Discharge: Structural analysis of Obs definition.
DEF-5: Input Canonicalization Idempotence
∀ σ: Canonical(Canonical(σ)) = Canonical(σ)
Falsification: Double canonicalization changes result. Discharge: Proof over canonicalization function.
DEF-6: Input Canonicalization Semantic Preservation
∀ σ₁, σ₂: SemanticEquiv(σ₁, σ₂) ⟹ Canonical(σ₁) = Canonical(σ₂)
Falsification: Semantically equivalent inputs with different canonical forms. Discharge: Proof over equivalence relation and canonicalization.
5. Semantic Lemmas
LEM-1: Invariant Preservation Under Transition
∀ (s, σ, s') ∈ T, ∀ G ∈ GlobalInvariants:
G(s) ⟹ G(s')
This is the single most important lemma in the system. Falsification: Find transition preserving local invariants but breaking a global one. Discharge: Per-invariant proof for each transition class.
LEM-2: Trace Inductive Invariance
∀ τ = (s₀, ..., sₙ):
s₀ ∈ I ∧ (∀ i: G(sᵢ) ⟹ G(sᵢ₊₁)) ⟹ ∀ i: G(sᵢ)
Discharge: Induction over trace length. Requires LEM-1 as inductive step.
LEM-3: Semantic Mapping Commutativity
∀ (s_c, σ_c):
μ_S(Apply_c(s_c, σ_c)) = Apply_f(μ_S(s_c), μ_Σ(σ_c))
This is the fundamental semantic binding condition. Falsification: Concrete execution followed by mapping ≠ mapping followed by formal transition. Discharge: Per-transition-class proof. This is where most real systems fail.
LEM-4: Constraint Soundness
∀ τ: SatisfiesConstraints(τ) ⟹ ValidTrace(τ)
Falsification: Invalid trace that satisfies all constraints. Discharge: Structural proof over constraint derivation pipeline.
LEM-5: Constraint Completeness
∀ τ: ValidTrace(τ) ⟹ SatisfiesConstraints(τ)
Falsification: Valid trace that cannot be represented in constraint system. Discharge: Coverage analysis of constraint templates.
LEM-6: Witness Semantic Uniqueness
∀ π, W₁, W₂:
Verify(π) ∧ WitnessOf(π) ∈ {W₁, W₂} ⟹ Semantics(W₁) = Semantics(W₂)
Multiple witnesses may exist, but they must map to the same semantic execution. Falsification: Two witnesses for same proof with divergent semantic meaning. Discharge: Analysis of constraint system + observable binding.
LEM-7: Error State Invariant Preservation
∀ (s, σ_invalid):
Apply(s, σ_invalid) = s_error ⟹ G(s_error) ∧ s_error ∈ S
Falsification: Error transition producing state that violates global invariant. Discharge: Per-error-class proof.
LEM-8: No-Op Semantic Neutrality
∀ (s, σ_noop):
Apply(s, σ_noop) = s ⟹ Obs(s, σ_noop, s) = ⊥_observable
No-op must not produce semantically meaningful observables. Falsification: No-op that emits observable indistinguishable from real transition. Discharge: Analysis of observable function over no-op class.
LEM-9: Batch Decomposition Equivalence
∀ s, [σ₁, ..., σₙ]:
Apply(s, [σ₁, ..., σₙ]) = Apply(Apply(...Apply(s, σ₁)..., σₙ₋₁), σₙ)
Batching must be semantically equivalent to sequential application. Falsification: Batch result differs from sequential application. Discharge: Structural proof. WARNING: This fails when intermediate states violate preconditions that the batch skips.
LEM-10: Trace Reconstruction Fidelity
∀ τ = (s₀, σ₀, s₁, ...):
Reconstruct(s₀, [σ₀, ..., σₙ₋₁]) = τ
Falsification: Reconstruction from initial state + inputs produces different trace. Discharge: Follows from AX-1 (determinism).
6. Safety Properties
SAFE-1: Unreachability of Invalid States
∀ τ starting from I: ∀ sᵢ ∈ τ: ValidState(sᵢ)
Discharge: Model checking over reachable state space + LEM-2.
SAFE-2: Resource Conservation
∀ (s, σ, s') ∈ T: Total(C_s) = Total(C_s') + Δ_fees(σ)
Falsification: Transition that creates or destroys resources outside fee model. Discharge: Per-transition arithmetic proof.
SAFE-3: No Hidden State Mutation
∀ (s, σ, s') ∈ T:
Diff(s, s') ⊆ AllowedMutations(σ)
Falsification: Field changes outside the allowed mutation set for given input class. Discharge: Per-transition-class field analysis.
SAFE-4: Temporal Monotonicity
∀ τ = (s₀, ..., sₙ): ∀ i < j: τ(sᵢ) < τ(sⱼ)
Falsification: Trace metadata regression. Discharge: Inductive proof over trace construction.
SAFE-5: No Rollback
∀ τ: ¬∃ i < j: sᵢ = sⱼ ∧ IsRollback(i, j)
Falsification: State revisitation that constitutes semantic rollback. Discharge: Model checking + temporal invariant enforcement.
SAFE-6: Domain Isolation
∀ π₁ from Domain_A, π₂ from Domain_B:
¬Compatible(π₁, π₂) unless explicitly composed
Falsification: Proof from one domain accepted in another. Discharge: Domain separation tag verification.
7. Liveness Properties
LIVE-1: No Deadlock
∀ s ∈ S: ∃ σ ∈ Σ: Apply(s, σ) ≠ ⊥
Every valid state has at least one valid transition (even if it's a no-op). Falsification: State with no applicable input. Discharge: Model checking.
LIVE-2: Provability of Valid Traces
∀ τ: ValidTrace(τ) ⟹ ∃ π: Verify(π) = true ∧ π attests τ
Every valid execution can be proven. Falsification: Valid trace that cannot produce a valid proof. Discharge: Completeness of proof system + constraint completeness (LEM-5).
8. Composition Obligations
COMP-1: Cross-System Resource Conservation
∀ composed (A, B):
Total_A(s_A) + Total_B(s_B) = constant
Falsification: Cross-system transition that creates resources. Discharge: Proof over cross-transition definitions.
COMP-2: Shared State Consistency
∀ composed (A, B):
C_shared^A = C_shared^B at every synchronization point
Falsification: Divergent shared state after cross-transition. Discharge: Synchronization protocol proof.
COMP-3: Compositional Invariant Preservation
∀ G_cross ∈ CrossInvariants:
Valid(A) ∧ Valid(B) ∧ Compatible(A, B) ⟹ G_cross holds
Falsification: Locally valid systems violating cross-invariant. Discharge: Per-cross-invariant proof under composition rules.
8.1 Economic Obligations
ECON-1: Economic Invariant Preservation Under Transition
∀ (s, σ, s') ∈ T:
EconomicallyValid(s) ⟹ EconomicallyValid(s')
Category: Safety Layer: FSL / EL Dependency: LEM-1 (structural invariant preservation) Falsification: Find transition preserving structural invariants but breaking economic invariant. Discharge: Per-economic-invariant, per-transition-class proof.
ECON-2: Initial State Economic Validity
∀ s₀ ∈ I: EconomicallyValid(s₀)
Category: Axiom Layer: FSL Dependency: AX-3 (initial state well-foundedness) Falsification: Construct initial state violating economic predicates. Discharge: Explicit verification of genesis economic parameters.
ECON-3: Temporal Economic Invariant Enforcement
∀ τ: AdmissibleTrace(τ) ⟹ ∀ TE_econ: TE_econ(τ)
Category: Safety Layer: FSL Dependency: LEM-2 (trace inductive invariance), ECON-1 Falsification: Find trace satisfying all per-step economic invariants but violating temporal economic invariant. Discharge: Induction over trace length + temporal invariant analysis.
ECON-4: Economic Context Determinism
∀ s = (C, D, E, Ω, τ): Ω = DeriveEconomic(C, E)
Category: Definition Layer: FSL / EL Dependency: DEF-1 (derived state determinism) Falsification: Find (C, E) where DeriveEconomic is undefined or non-unique. Discharge: Structural proof over DeriveEconomic definition.
ECON-5: Economic Admissibility Completeness
¬∃ τ: ValidTrace(τ) ∧ (∀ G_econ: G_econ holds) ∧ (∀ TE_econ: TE_econ holds) ∧ EconomicallyExploitable(τ)
Category: Completeness Layer: FSL Dependency: All ECON obligations Falsification: Find trace satisfying all economic invariants but still economically exploitable. Discharge: Adversarial economic analysis + domain expert review. This is the hardest obligation.
9. Constraint-Layer Obligations
CONST-1: No Unconstrained Variables
∀ v ∈ WitnessVariables: ∃ constraint C referencing v
Falsification: Free variable in witness. Discharge: Static analysis of constraint system.
CONST-2: No Unused Witness Inputs
∀ w ∈ WitnessInputs: w influences at least one constraint output
Falsification: Witness input that can be changed without affecting constraint satisfaction. Discharge: Dependency analysis.
CONST-3: Branch Completeness
∀ conditional in SIR: both branches are constrained
Falsification: Unconstrained branch path. Discharge: SIR → constraint template coverage analysis.
CONST-4: Constraint Derivation Determinism
∀ SIR_program P: D(P) produces unique constraint system C
Falsification: Same SIR producing different constraints. Discharge: Determinism proof of derivation function D.
10. Proof-Layer Obligations
PROOF-1: Full Trace Binding
∀ π: π binds to complete trace τ, not partial
Falsification: Proof that validates without committing to intermediate states. Discharge: Public input analysis + commitment structure.
PROOF-2: Observable Binding
∀ π: Obs(τ) ⊆ PublicInputs(π)
Falsification: Observable not represented in proof public inputs. Discharge: Public input completeness analysis.
PROOF-3: Domain Separation
∀ π: Domain(π) is unique and non-reusable across contexts
Falsification: Proof accepted in unintended domain. Discharge: Domain tag construction analysis.
PROOF-4: Knowledge Soundness
∀ π: ∃ extractor E: E(π) = valid witness W
Falsification: Proof generated without knowledge of valid execution. Discharge: Reduction to proof system knowledge soundness.
11. Obligation Dependency Graph
AX-1 ──→ DEF-1, DEF-4, LEM-9, LEM-10
AX-2 ──→ LEM-7, SAFE-1
AX-3 ──→ LEM-2
AX-4 ──→ PROOF-4
AX-5 ──→ DEF-3
LEM-1 ──→ LEM-2, SAFE-1
LEM-3 ──→ LEM-4, LEM-5
LEM-4 ──→ SAFE-1 (via constraints)
LEM-5 ──→ LIVE-2
LEM-6 ──→ PROOF-1
DEF-2 ──→ DEF-3
CONST-1..4 ──→ LEM-4, LEM-5
If any node in this graph is unresolved, everything downstream is suspect.
12. Discharge Status Template
Each obligation must be tracked:
Obligation: [ID]
Status: [unresolved / in-progress / discharged / failed]
Method: [model-check / theorem-prove / test / argument]
Tool: [TLA+ / Coq / Lean / manual]
Evidence: [artifact reference]
Last verified: [date]
Reviewer: [identity]
13. Closing Statement
This document is the contract between VSEL's ambition and its reality.
Every obligation listed here is a claim the system makes about itself.
If the claim cannot be backed by evidence, it is not a feature. It is a liability.