docs: clarify Layer 1 vs contract spec proofs

Th0rgal · Th0rgal · commit 5ec6593c62ef · 2026-03-10T12:17:31.000+01:00
diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md
@@ -283,7 +283,7 @@ See [AXIOMS.md](AXIOMS.md) for current axioms and detailed guidelines.
 
 ## Key Files
 
-- `Verity/` - EDSL, specs, Layer 1 proofs
+- `Verity/` - EDSL, user-facing specs, and contract-specific specification proofs
 - `Compiler/` - IR, Yul, codegen
 - `Compiler/Proofs/` - Layer 2 & 3 proofs
 - `docs/ROADMAP.md` - Progress tracking
diff --git a/Compiler/Proofs/README.md b/Compiler/Proofs/README.md
@@ -7,9 +7,10 @@ See `TRUST_ASSUMPTIONS.md` for the full trust boundary.
 
 ## Verification Layers
 
-- **Layer 1: EDSL ≡ CompilationModel**. Contract-specific proofs live in
-  `Contracts/<Name>/Proofs/`, with generic typed-IR compilation correctness in
-  `Compiler/TypedIRCompilerCorrectness.lean`.
+- **Layer 1: EDSL ≡ CompilationModel**. This is the frontend semantic bridge.
+  Contract-specific specification proofs live separately in
+  `Contracts/<Name>/Proofs/`, while generic typed-IR compilation correctness
+  lives in `Compiler/TypedIRCompilerCorrectness.lean`.
 - **Layer 2: CompilationModel -> IR**. The current proof surface is split:
   a generic supported-statement-fragment theorem lives in
   `Compiler/TypedIRCompilerCorrectness.lean` and
diff --git a/README.md b/README.md
@@ -95,7 +95,7 @@ EVM Bytecode
 | 2 | Supported-statement CompilationModel → IR fragment is generic; full-contract bridges remain contract-specific | [SupportedFragment.lean](Compiler/Proofs/IRGeneration/SupportedFragment.lean) |
 | 3 | IR → Yul codegen preserves behavior | [Preservation.lean](Compiler/Proofs/YulGeneration/Preservation.lean) |
 
-Layer 3 is generically verified with 1 documented axiom (the selector axiom). Layer 2 currently combines a generic supported-statement theorem with contract-specific full-contract bridges. See [docs/VERIFICATION_STATUS.md](docs/VERIFICATION_STATUS.md) and [AXIOMS.md](AXIOMS.md).
+Layer 1 is the frontend EDSL-to-`CompilationModel` bridge. The per-contract files in `Contracts/<Name>/Proofs/` prove human-readable contract specifications; they are not what “Layer 1” means in the compiler stack. Layer 3 is generically verified with 1 documented axiom (the selector axiom). Layer 2 currently combines a generic supported-statement theorem with contract-specific full-contract bridges. See [docs/VERIFICATION_STATUS.md](docs/VERIFICATION_STATUS.md) and [AXIOMS.md](AXIOMS.md).
 
 ### 5. Test the compiled output (belt and suspenders)
 
diff --git a/TRUST_ASSUMPTIONS.md b/TRUST_ASSUMPTIONS.md
@@ -20,8 +20,8 @@ Layer 1 and Layer 3 have generic proof surfaces in Lean. Layer 2 currently combi
 
 ## What's Verified
 
-- **Layer 1**: EDSL behavior matches its CompilationModel. For supported contracts, a generic typed-IR compilation-correctness theorem eliminates per-contract manual proofs.
-- **Layer 2**: a supported statement-list CompilationModel → IR theorem exists, but whole-contract Layer 2 preservation still relies on contract-specific bridge theorems.
+- **Layer 1**: EDSL behavior matches its `CompilationModel`. This names the frontend semantic bridge only; it does not refer to the contract-specific specification theorems in `Contracts/<Name>/Proofs/`. For supported contracts, macro-generated bridge theorems and the typed-IR correctness path discharge this boundary.
+- **Layer 2**: a supported statement-list `CompilationModel → IR` theorem exists, but whole-contract Layer 2 preservation still relies on contract-specific bridge theorems.
 - **Layer 3**: IR → Yul preserves behavior, with 1 documented axiom (keccak256 selector).
 - **Cross-layer**: `Contracts/Proofs/SemanticBridge.lean` provides the active contract-specific Layer 2 bridge surface; `Compiler/Proofs/EndToEnd.lean` composes that current Layer 2 boundary with Layer 3.
 
diff --git a/docs-site/content/add-contract.mdx b/docs-site/content/add-contract.mdx
@@ -44,7 +44,7 @@ This creates 7 scaffold files (EDSL, Spec, Invariants, Proofs re-export shim, Ba
    - Implement contract logic in `Verity/Examples/<Name>.lean`
    - Reuse helper lemmas for storage updates and mapping reads
 
-3. **Layer 1 Proofs**
+3. **Contract Specification Proofs**
    - Prove correctness in `Verity/Proofs/<Name>/Basic.lean` and `Correctness.lean`
    - Each theorem states observable behavior (return values + storage deltas)
 
@@ -74,7 +74,7 @@ Verity/Specs/<Name>/
 
 Verity/Examples/<Name>.lean     # EDSL implementation
 Verity/Proofs/<Name>/
-  ├── Basic.lean       # Basic correctness proofs (Layer 1)
+  ├── Basic.lean       # Basic contract-spec correctness proofs
   └── Correctness.lean # Advanced correctness proofs
 Compiler/TypedIRCompilerCorrectness.lean  # Generic compilation correctness (shared)
 test/Differential<Name>.t.sol          # Differential tests
diff --git a/docs-site/content/compiler.mdx b/docs-site/content/compiler.mdx
@@ -29,12 +29,14 @@ Important: Verity has two different "spec" concepts.
 ## Trust Model
 
 ### What's Verified (Zero Trust Required)
-- **Layer 1 per contract**: EDSL behavior is proven equivalent to its `CompilationModel`.
+- **Layer 1 frontend bridge**: EDSL behavior is proven equivalent to its `CompilationModel`.
 - **Layer 2 boundary today**: a supported-statement `CompilationModel -> IR` theorem exists, but full-contract Layer 2 preservation still relies on contract-specific bridge theorems.
 - **Layer 3 framework proof**: `IR -> Yul` preserves semantics.
 - **Machine-checked proofs**: see [VERIFICATION_STATUS.md](https://github.com/Th0rgal/verity/blob/main/docs/VERIFICATION_STATUS.md) for the current proof-status snapshot and [AXIOMS.md](https://github.com/Th0rgal/verity/blob/main/AXIOMS.md) for documented axioms.
 - **Interpreter semantics**: Spec, IR, and Yul semantics defined and linked in Lean
 
+The per-contract files in `Contracts/<Name>/Proofs/` are separate contract-specification proofs. They show that a given contract satisfies its human-readable spec; they are not the definition of Layer 1 in the compiler stack.
+
 ### What's Tested (High Confidence)
 - **Compilation correctness**: Foundry unit and differential tests cover compiled contracts
 - **Output validation**: Generated Yul is exercised against expected runtime behavior
diff --git a/docs-site/content/guides/first-contract.mdx b/docs-site/content/guides/first-contract.mdx
@@ -250,7 +250,7 @@ If successful, the `#eval` block evaluates and prints `some 100`.
 
 This is where formal verification happens. We prove that our implementation matches our specification.
 
-### 4.1 Write Layer 1 Proofs
+### 4.1 Write Contract Specification Proofs
 
 Open `Verity/Proofs/TipJar/Basic.lean`:
 
diff --git a/docs-site/content/index.mdx b/docs-site/content/index.mdx
@@ -80,7 +80,7 @@ The Lean compiler verifies every proof. If a proof is wrong, compilation fails.
 
 - **User-facing specs**: `Verity/Specs/<Name>/Spec.lean` (+ `Invariants.lean`)
 - **Implementations (EDSL)**: `Verity/Examples/<Name>.lean`
-- **Layer 1 proofs (EDSL correctness)**: `Verity/Proofs/<Name>/Basic.lean` + `Correctness.lean`
+- **Contract-specific specification proofs**: `Verity/Proofs/<Name>/Basic.lean` + `Correctness.lean`
 - **Compilation correctness**: `Compiler/TypedIRCompilerCorrectness.lean` (generic typed-IR theorem) + `Contracts/Proofs/SemanticBridge.lean` (current contract bridge layer)
 - **Reusable proof infrastructure**: `Verity/Proofs/Stdlib/` (spec interpreter + automation)
 - **Compiler specs (for codegen)**: `Compiler/Specs.lean` (separate from user specs)
@@ -99,6 +99,8 @@ Use `python3 scripts/generate_contract.py <Name>` to scaffold all boilerplate fi
 
 See [Add a Contract](/add-contract) for the full guide.
 
+In this repo, “Layer 1” refers specifically to the EDSL-to-`CompilationModel` semantic bridge in the compiler pipeline. The files under `Verity/Proofs/<Name>/` are contract-level specification proofs.
+
 ## Example Contracts
 
 Eight contracts are formally verified (plus one unverified linker demo):
diff --git a/docs-site/content/research.mdx b/docs-site/content/research.mdx
@@ -19,7 +19,7 @@ The project evolved in two phases:
 
 This is the single source of truth for progress, roadmap, and milestone updates.
 
-- **Layer 1 (Spec Correctness)**: Complete for all 8 verified contracts (7 compiler-spec contracts + ReentrancyExample).
+- **Contract-specific specification proofs**: Complete for all 8 verified contracts (7 compiler-spec contracts + ReentrancyExample).
 - **Layer 2 (CompilationModel → IR)**: Partial generic coverage only. A supported-statement theorem exists, while whole-contract preservation still relies on contract-specific bridges and the generic `CompilationModel.compile` theorem is tracked in [#1510](https://github.com/Th0rgal/verity/issues/1510).
 - **Layer 3 (IR → Yul)**: Complete — all 8 statement equivalence proofs + universal dispatcher proven (PR #42).
 
@@ -102,8 +102,8 @@ Each contract has:
 - `Verity/Examples/X.lean` — Implementation (EDSL)
 - `Verity/Specs/X/Spec.lean` — Pre/postconditions for each operation
 - `Verity/Specs/X/Invariants.lean` — State properties that should hold
-- `Verity/Proofs/X/Basic.lean` — Layer 1: Spec conformance, basic properties
-- `Verity/Proofs/X/Correctness.lean` — Layer 1: Revert proofs, composition, end-to-end
+- `Verity/Proofs/X/Basic.lean` — Contract-specific spec conformance and basic properties
+- `Verity/Proofs/X/Correctness.lean` — Contract-specific revert proofs, composition, and end-to-end properties
 - `Compiler/TypedIRCompilerCorrectness.lean` — Compilation correctness (generic theorem, 36 supported fragments)
 
 Some contracts have additional proof files:
diff --git a/docs-site/content/verification.mdx b/docs-site/content/verification.mdx
@@ -45,11 +45,11 @@ Verity/
 ├── Specs/{Contract}/
 │   ├── Spec.lean                 # What each operation should do
 │   └── Invariants.lean           # Properties that should always hold
-│   └── Proofs.lean               # User-facing proofs (spec → impl)
+│   └── Proofs.lean               # User-facing spec statements and re-exports
 ├── Proofs/Stdlib/                # Reusable proof infrastructure
 └── Proofs/{Contract}/            # Deeper contract proof suites
-    ├── Basic.lean                # Core properties and lemmas
-    ├── Correctness.lean          # Composition and revert behavior
+    ├── Basic.lean                # Contract-specific spec conformance and lemmas
+    ├── Correctness.lean          # Contract-specific composition and revert behavior
     ├── Conservation.lean         # Sum conservation laws (Ledger)
     ├── Supply.lean               # Supply conservation (SimpleToken)
     └── Isolation.lean            # Storage isolation (SimpleToken)
diff --git a/docs-site/public/llms.txt b/docs-site/public/llms.txt
@@ -26,7 +26,8 @@ Lean 4 EDSL for writing smart contracts with machine-checked proofs. Three-layer
 ## Architecture
 
 ```
-Layer 1: EDSL Proofs      — Lean theorems about contract behavior
+Layer 1: EDSL -> CompilationModel bridge
+Contract proofs: human-readable spec theorems for each contract
 Layer 2: Compiler Proofs  — partial generic CompilationModel -> IR boundary
 Layer 3: IR -> Yul        — Statement/expression equivalence proofs
 Trust:   Yul -> Bytecode  — Via solc (validated by differential testing)
diff --git a/docs/VERIFICATION_STATUS.md b/docs/VERIFICATION_STATUS.md
@@ -18,7 +18,7 @@ EVM Bytecode
 
 ## Layer 1: EDSL ≡ CompilationModel — COMPLETE
 
-**What it proves**: The EDSL `Contract` monad execution is equivalent to `CompilationModel` interpretation for all supported contracts. Per-contract proofs under `Contracts/<Name>/Proofs/` then show these contracts satisfy their human-readable specifications.
+**What it proves**: The EDSL `Contract` monad execution is equivalent to `CompilationModel` interpretation for all supported contracts. This is the frontend semantic bridge. Separate per-contract proofs under `Contracts/<Name>/Proofs/` show that each contract satisfies its human-readable specifications; those specification theorems are downstream contract proofs, not the definition of Layer 1 itself.
 
 ### Verified Contracts
 
@@ -38,11 +38,11 @@ EVM Bytecode
 | CryptoHash | 0 | No specs | `Contracts/CryptoHash/Contract.lean` |
 | **Total** | **277** | **✅ 100%** | — |
 
-> **Note**: Stdlib (0 internal proof-automation properties) is excluded from the Layer 1 contracts table above but included in overall coverage statistics (277 total properties).
+> **Note**: Stdlib (0 internal proof-automation properties) is excluded from the contract-spec theorem table above but included in overall coverage statistics (277 total properties).
 
-Layer 1 uses macro-generated bridge theorems backed by a generic typed-IR compilation-correctness theorem ([`TypedIRCompilerCorrectness.lean`](../Compiler/TypedIRCompilerCorrectness.lean)). Tuple/bytes/fixed-array/dynamic-array/string parameters now stay inside that proof path when they are carried as ABI head words/offsets. Advanced constructs beyond that typed-IR head-word surface (linked libraries, ECMs, fully custom ABI behavior) are still expressed directly in `CompilationModel` and trusted at that boundary.
+Layer 1 uses macro-generated EDSL-to-`CompilationModel` bridge theorems backed by a generic typed-IR compilation-correctness theorem ([`TypedIRCompilerCorrectness.lean`](../Compiler/TypedIRCompilerCorrectness.lean)). Tuple/bytes/fixed-array/dynamic-array/string parameters now stay inside that proof path when they are carried as ABI head words/offsets. Advanced constructs beyond that typed-IR head-word surface (linked libraries, ECMs, fully custom ABI behavior) are still expressed directly in `CompilationModel` and trusted at that boundary.
 
-Internal helper calls are supported operationally in `CompilationModel` and the fuel-based interpreter path, but helper-level compositional proof reuse across callers is not yet a first-class verified interface. Current Layer 1 bridges remain contract-specific; the reusable internal-helper proof boundary is tracked in [#1335](https://github.com/Th0rgal/verity/issues/1335).
+Internal helper calls are supported operationally in `CompilationModel` and the fuel-based interpreter path, but helper-level compositional proof reuse across callers is not yet a first-class verified interface. Current EDSL-to-`CompilationModel` bridge instantiations remain contract-specific; the reusable internal-helper proof boundary is tracked in [#1335](https://github.com/Th0rgal/verity/issues/1335).
 
 ### Lowering Bridge
 
diff --git a/scripts/test_check_verification_status_doc.py b/scripts/test_check_verification_status_doc.py
@@ -91,7 +91,7 @@ def test_matching_doc_passes(self) -> None:
             | CryptoHash | 0 | No specs | `Contracts/CryptoHash/Contract.lean` |
             | **Total** | **7** | **✅ 100%** | — |
 
-            > **Note**: Stdlib (0 internal proof-automation properties) is excluded from the Layer 1 contracts table above but included in overall coverage statistics (7 total properties).
+            > **Note**: Stdlib (0 internal proof-automation properties) is excluded from the contract-spec theorem table above but included in overall coverage statistics (7 total properties).
 
             | Contract | Coverage | Exclusions |
             |----------|----------|------------|
@@ -146,7 +146,7 @@ def test_stale_covered_bullet_fails(self) -> None:
             | CryptoHash | 0 | No specs | `Contracts/CryptoHash/Contract.lean` |
             | **Total** | **7** | **✅ 100%** | — |
 
-            > **Note**: Stdlib (0 internal proof-automation properties) is excluded from the Layer 1 contracts table above but included in overall coverage statistics (7 total properties).
+            > **Note**: Stdlib (0 internal proof-automation properties) is excluded from the contract-spec theorem table above but included in overall coverage statistics (7 total properties).
 
             | Contract | Coverage | Exclusions |
             |----------|----------|------------|
