feat(proofs): witness-requiring attestations (A7, PROOF-NEEDS §P1.1)

Replaces every ceremonial nullary attestation in Proofs.idr with an
evidence-consuming variant.  The top-level certificate can no longer
be constructed from thin air — each level's attestation now requires
a matching witness from its level module:

  attestL1_InstructionValid  :: Schema                 -- Region.idr
  attestL2_RegionBound       :: FieldIn name schema    -- Region.idr
  attestL3_TypeCompat        :: WasmTypeCompat a b     -- MultiModule.idr
  attestL4_NullSafe          :: Pointer.Ptr k s l NonNull
  attestL5_BoundsProof       :: InBounds idx count     -- Region.idr
  attestL6_ResultType        :: AccessResult ty        -- TypedAccess.idr
  attestL7_AliasFree         :: ExclusiveWitness s     -- Pointer.idr
  attestL8_EffectSafe        :: EffectSubsumes d a     -- Effects.idr (pre-existing)
  attestL9_LifetimeSafe      :: Lifetime.Outlives rl sl
  attestL10_Linear           :: CompletedProtocol tok  -- Linear.idr

simpleReadCert, fullCert12, and fullCert15 now take every required
witness as an explicit argument and thread them through.  Witnesses
are compile-time-only (erased at runtime), so there is zero runtime
cost — but the certificate cannot be built without real proof
artefacts.

Qualification: `Lifetime` / `Outlives` resolve to Lifetime.idr's
propositional forms; Pointer.Ptr's lifetime parameter takes
Levels.Lifetime, since Pointer.idr imports from Levels.idr.  A short
comment in Proofs.idr explains the name clash.

Zero believe_me / assert_total / postulate / sorry; %default total
preserved; panic-attack clean.

PROOF-NEEDS.md §P1.1 marked DONE; LEVEL-STATUS.md Proofs.idr row
updated with the new witness-taking API.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Author: hyperpolymath

LEVEL-STATUS.md

@@ -96,7 +96,7 @@ toolchain remains future work.
 | SessionProtocol.idr | 0 | 0 | 0 | In package (v1.3 / L14) |
 | ResourceCapabilities.idr | 0 | 0 | 0 | In package (v1.4 / L15) |
 | Choreography.idr | 0 | 0 | 0 | In package (v1.5 / L16) |
-| Proofs.idr | 0 | 0 | 0 | In package |
+| Proofs.idr | 0 | 0 | 0 | In package.  Attestation API hardened A7 (2026-04-18): every L1-L10 attestation now requires a witness from its level module (Schema / FieldIn / WasmTypeCompat / Ptr-NonNull / InBounds / AccessResult / ExclusiveWitness / EffectSubsumes / Lifetime.Outlives / CompletedProtocol).  `simpleReadCert` / `fullCert12` / `fullCert15` thread witnesses per level; the certificate cannot be constructed without real proof artefacts. |
 | Tropical.idr | 0 | 0 | 0 | In package (A1, 2026-04-18) |
 | Epistemic.idr | 0 | 0 | 0 | In package (A1, 2026-04-18) |
 | Echo.idr | 0 | 0 | 0 | In package (A0, 2026-04-18) |

PROOF-NEEDS.md

@@ -233,7 +233,36 @@ to sanity-check the statement before proving it.
 ### P1 — Security (the parts where ceremony ≠ evidence)
 
 **P1.1. Replace every ceremonial attestation in `Proofs.idr` with
-evidence-consuming versions.** Current state:
+evidence-consuming versions. ✅ DONE 2026-04-18 (A7).**
+
+Every nullary attestation in `Proofs.idr` has been promoted to require
+a witness from its level's proof module:
+
+| Attestation | Witness type | Source module |
+|---|---|---|
+| `attestL1_InstructionValid` | `Schema` | Region.idr |
+| `attestL2_RegionBound` | `FieldIn name schema` | Region.idr |
+| `attestL3_TypeCompat` | `WasmTypeCompat a b` | MultiModule.idr |
+| `attestL4_NullSafe` | `Pointer.Ptr k s l NonNull` | Pointer.idr |
+| `attestL5_BoundsProof` | `InBounds idx count` | Region.idr |
+| `attestL6_ResultType` | `AccessResult ty` | TypedAccess.idr |
+| `attestL7_AliasFree` | `ExclusiveWitness s` | Pointer.idr |
+| `attestL8_EffectSafe` | `EffectSubsumes declared actual` | Effects.idr (pre-existing) |
+| `attestL9_LifetimeSafe` | `Lifetime.Outlives rl sl` | Lifetime.idr |
+| `attestL10_Linear` | `CompletedProtocol tok` | Linear.idr |
+
+`simpleReadCert`, `fullCert12`, and `fullCert15` now thread each of the
+required witnesses through their signatures.  The top-level certificate
+cannot be constructed without a proof term for every level it claims.
+
+Qualification note: `Lifetime` and `Outlives` are resolved as
+`Lifetime.Lifetime` / `Lifetime.Outlives` (from Lifetime.idr), while
+`Pointer.Ptr`'s lifetime parameter takes `Levels.Lifetime` (which is
+what Pointer.idr itself imports from Levels.idr).  A small comment in
+Proofs.idr explains the qualification; both `Lifetime` types remain
+in the codebase for now.
+
+**Original task description preserved for history:** Current state:
 
 ```
 attestL10_Linear : LevelAttestation