docs(spec): V4g — VCL-SPEC documents PROVEN + SANCTIFY proof types

Renames docs/VQL-SPEC.adoc → docs/VCL-SPEC.adoc (completes the VQL→VCL
filename migration; content was already renamed earlier).

Adds the two V4 proof types to §Proof Types:

  PROVEN    — (obligation_class, prover) pair certified via learning loop
              (success_rate ≥ τ_proven ∧ total_attempts ≥ N_proven)
  SANCTIFY  — class-level portfolio attestation (≥ k_sanctify PROVEN
              provers across ≥ N_sanctify combined attempts)

Both resolve at runtime via GET /api/v1/proof_attempts/certificates
and Hypatia.VCL.ProofResolver (committed in hypatia d142bb5).

Default thresholds: τ=0.80, N_proven=20, k_sanctify=2, N_sanctify=50.

Updates the keyword list to include PROVEN and SANCTIFY.
Updates all VQL-SPEC references in docs/code to VCL-SPEC.

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

Author: hyperpolymath

docs/VCL-SPEC.adoc

@@ -187,8 +187,8 @@ DESC      DOCUMENT  DOT_PRODUCT DRIFT   EUCLIDEAN EXISTENCE EXISTS
 FEDERATION FIELD    FROM      FULLTEXT  GRAPH     GROUP     HAS
 HAVING    HEXAD     INSERT    INTEGRITY JACCARD   LATEST    LIKE
 LIMIT     MATCHES   MAX       MIN       MODIFIED  NEAREST   NOT
-OF        OFFSET    OR        ORDER     PROOF     PROVENANCE RANK
-REPAIR    SELECT    SEMANTIC  SET       SHAPE     SIMILAR   STORE
+OF        OFFSET    OR        ORDER     PROOF     PROVEN    PROVENANCE RANK
+REPAIR    SANCTIFY  SELECT    SEMANTIC  SET       SHAPE     SIMILAR   STORE
 STRICT    SUM       TEMPORAL  TENSOR    TO        TOLERATE  UPDATE
 USING     VECTOR    VERIFIED  VERSION   WHERE     WITH      WITHIN
 false     true
@@ -559,7 +559,7 @@ The result is bundled with a proof that the result satisfies the stated property
 
 ==== Proof Types
 
-`Proof[φ]` — A type inhabited by evidence that proposition stem:[\phi] holds. There are six proof kinds:
+`Proof[φ]` — A type inhabited by evidence that proposition stem:[\phi] holds. There are eight proof kinds:
 
 [cols="1,3,1"]
 |===
@@ -588,9 +588,53 @@ The result is bundled with a proof that the result satisfies the stated property
 | `CUSTOM`
 | User-defined ZKP contract
 | Variable
+
+| `PROVEN`
+| *(V4)* A specific (obligation_class, prover) pair meets the
+  PROVEN-certificate threshold: aggregate success_rate ≥ τ_proven over
+  ≥ N_proven attempts in the `proof_attempts` learning loop. Resolved
+  against `mv_proven_certificates` via
+  `GET /api/v1/proof_attempts/certificates?class=X&prover=Y`.
+| Low (cached MV read)
+
+| `SANCTIFY`
+| *(V4)* A proof obligation class has at least `k_sanctify` distinct
+  PROVEN provers whose combined attempts meet `N_sanctify`. A
+  class-level portfolio attestation. Resolved against
+  `mv_sanctify_certificates`.
+| Low (cached MV read)
 |===
 
-`[.partial]` Parser recognises all six proof types. Type checker validates proof clause structure. Runtime proof generation is planned.
+`[.partial]` Parser recognises the six original proof types end-to-end.
+`PROVEN` and `SANCTIFY` are resolved at execution time via the V4 HTTP
+endpoint and `Hypatia.VCL.ProofResolver` in the Elixir execution layer
+(see `hypatia/lib/vcl/proof_resolver.ex`). Type-checker integration in
+the ReScript parser is planned but not yet wired — for now, PROVEN and
+SANCTIFY expressions pass through verbatim for runtime resolution.
+
+===== PROVEN / SANCTIFY usage examples
+
+[source]
+----
+-- Check whether z3 is certified on the safety class
+PROOF PROVEN(class='safety', prover='z3')
+  -> {proven, cert_id, success_rate, total_attempts}
+
+-- Class-level portfolio attestation
+PROOF SANCTIFY(class='equiv')
+  -> {sanctified, cert_id, proven_provers, combined_attempts}
+
+-- Embedded in a VCL statement
+INSPECT * FROM octads
+  WHERE modality = 'semantic'
+  PROOF PROVEN(class='correctness', prover='cvc5')
+  AND PROOF SANCTIFY(class='safety')
+----
+
+The thresholds (`τ_proven`, `N_proven`, `k_sanctify`, `N_sanctify`) live
+in the `proof_attempts_cert_policy` singleton table and propagate to the
+views immediately on update. Default policy: τ=0.80, N_proven=20,
+k_sanctify=2, N_sanctify=50.
 
 === Subtyping Rules