Document
Proof Layer
**Verifiable Semantic Execution Layer (VSEL)**
Verifiable Semantic Execution Layer (VSEL)
1. Purpose
This document defines the structure, semantics, and guarantees of the proof system used in VSEL.
It specifies:
- what statements are proven
- how proofs relate to execution traces
- how proofs bind to formal semantics
- what guarantees verifiers can rely on
The core requirement is:
A valid proof must certify that an execution trace is semantically valid under the formal specification.
Not that it satisfies a circuit. That part is just an implementation detail.
2. Proof Statement
Given:
- a formal execution trace ( \tau )
- a constraint system ( C ) derived from semantics
A proof ( \pi ) must attest:
[ \pi = Proof(\tau, C) ]
Such that:
[ Verify(\pi) \Rightarrow ValidTrace(\tau) ]
This is the only statement that matters.
Anything weaker is insufficient.
3. Proof Object Structure
A proof object consists of:
[ \pi = (Com, W, Aux, Meta) ]
Where:
- ( Com ): commitments to trace/state
- ( W ): witness data (possibly implicit in ZK systems)
- ( Aux ): auxiliary proof artifacts (queries, openings, etc.)
- ( Meta ): metadata (domain separation, versioning, parameters)
4. Public Inputs
The proof must expose a well-defined set of public inputs:
[ Pub = (root_{init}, root_{final}, inputs, outputs, domain) ]
These include:
- initial state commitment
- final state commitment
- observable outputs
- execution domain parameters
Everything else must be either:
- derived deterministically, or
- part of the private witness
5. Witness Definition
The witness encodes:
- intermediate states
- transition values
- auxiliary variables required for constraint satisfaction
Constraint:
[ Witness \rightarrow \tau ]
The witness must correspond to a single valid execution trace.
Multiple valid interpretations of the same witness are not allowed.
6. Proof Semantics
A proof is valid if and only if:
[ Verify(\pi, Pub) = true ]
Which implies:
[ \exists \tau \text{ such that:} ]
- ( \tau ) matches commitments
- ( \tau ) satisfies constraints
- ( \tau ) is a valid formal trace
7. Binding Requirements
7.1 State Binding
Proof must bind:
[ root_{init} = Commitment(s_0) ]
[ root_{final} = Commitment(s_n) ]
7.2 Trace Binding
The proof must bind to the entire execution trace, not only endpoints.
Partial proofs are not sufficient.
7.3 Observable Binding
All observables must be:
[ o = Obs(\tau) ]
and included in the proof statement.
8. Proof System Choices
VSEL supports:
- STARKs (transparent, scalable)
- SNARKs (succinct, trusted setup optional)
- hybrid systems
Choice depends on:
- trust assumptions
- performance requirements
- recursion needs
But regardless of system:
The semantics of what is proven must remain identical.
9. Zero-Knowledge Considerations
Zero-knowledge is optional from a correctness standpoint.
If used, it must guarantee:
[ Leak(\pi) \subseteq Pub ]
No additional information about:
- state
- inputs
- intermediate transitions
10. Proof Composition
Proofs may be composed:
[ \pi_{combined} = Compose(\pi_1, \pi_2, ..., \pi_n) ]
Requirements:
- compositional correctness
- preservation of invariants
- consistent state chaining
11. Recursive Proofs
Recursive proofs must ensure:
[ Verify(\pi_{inner}) \subseteq Constraints(\pi_{outer}) ]
Ensuring:
- proof validity is embedded
- no external trust required
12. Soundness
Soundness guarantees:
[ Pr[\text{invalid } \tau \text{ accepted}] \leq \epsilon ]
Where ( \epsilon ) is negligible.
This depends on:
- cryptographic assumptions
- constraint correctness
13. Completeness
Completeness guarantees:
[ ValidTrace(\tau) \Rightarrow \exists \pi ]
All valid executions must be provable.
14. Knowledge Soundness
The prover must “know” a valid witness:
[ \exists W \Rightarrow Proof(\tau) ]
Prevents:
- proof forgery without execution
15. Domain Separation
Proofs must include domain identifiers:
[ Domain = Hash(context) ]
Prevents:
- replay across systems
- cross-protocol confusion
16. Proof Verification
Verification checks:
- commitment consistency
- constraint satisfaction
- trace validity (via constraints)
- domain correctness
[ Verify(\pi, Pub) \Rightarrow ValidTrace(\tau) ]
17. Failure Modes
17.1 Weak Binding
Proof does not bind to full trace.
17.2 Constraint Drift
Proof verifies constraints that no longer match semantics.
17.3 Witness Ambiguity
Multiple traces satisfy same proof.
17.4 Partial Proof Acceptance
Verifier accepts incomplete proof.
17.5 Domain Collision
Proof reused in unintended context.
18. Minimal Proof Validity Conditions
A valid proof must ensure:
- full trace binding
- invariant enforcement
- semantic correctness
- deterministic interpretation
19. Separation of Concerns
The proof layer guarantees:
- correctness of execution
It does not guarantee:
- completeness of specification
- correctness of semantics
If the spec is wrong, the proof is perfectly wrong.
20. Closing Statement
A proof is not truth.
It is a statement about a model.
VSEL ensures that:
the model being proven is the actual system, not a convenient approximation.