chore(state): record Tier C vendoring + ACL2/MiniZinc boost

Tier C (6 provers) lifted from 0 records each — TLAPS 103, Alloy 136,
Boogie 1 319, Frama-C 1 317, Viper 3 541, Tamarin 4 595 = +11 011
records total. Extractors already existed; just needed upstream
corpora vendored at the expected paths.

Tier A boost: ACL2 277 → 170 455 (#2 corpus after Lean) from
acl2/acl2 books/; MiniZinc 29 → 327. Both committed in 618d6b9.

Note: training_data/*.jsonl outputs are large (some > 100 MB) and
cannot be pushed to GitHub with the current on-repo storage policy.
Extractors + cloned corpora are the reproducible source of truth —
regenerate with `just extract-<prover>` when needed.

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

Author: hyperpolymath

.machine_readable/6a2/STATE.a2ml

@@ -104,6 +104,36 @@ remaining-phase1-work = [
   "HP type-checker ecosystem (11 provers): synthetic type-derivation generator",
 ]
 
+[session-2026-04-18-tier-c-vendoring]
+summary = "Vendored 6 Tier C + 2 Tier A upstream corpora — unlocked 11 011 records and 170 178 ACL2 records"
+note = "Corpora cloned on local disk (each gitignored); training_data/*.jsonl outputs are too large (> 100 MB) for GitHub's per-file limit and are not committed. Extractors themselves unchanged — only corpus vendoring needed."
+tier-c-provers-unlocked = [
+  "TLAPS     0 → 103       (tlaplus/Examples)",
+  "Alloy     0 → 136       (AlloyTools/models)",
+  "Boogie    0 → 1 319     (boogie-org/boogie Test/)",
+  "Frama-C   0 → 1 317     (Frama-C/Frama-C-snapshot tests/)",
+  "Viper     0 → 3 541     (viperproject/silver src/test/)",
+  "Tamarin   0 → 4 595     (tamarin-prover/tamarin-prover examples/)",
+]
+tier-a-boost = [
+  "ACL2      277    → 170 455  (acl2/acl2 books/, ~ 13 478 .lisp files)  → #2 corpus overall",
+  "MiniZinc  29     →     327  (MiniZinc/minizinc-benchmarks)",
+]
+extractor-bugs-fixed = [
+  "extract_acl2.jl:    byte-index slice crash on multi-byte UTF-8 → first(s, n)",
+  "extract_minizinc.jl: 3 eachmatch calls wrapped in try/catch — PCRE match-limit on large data files",
+]
+new-corpora-on-disk = [
+  "external_corpora/acl2_full/           — acl2/acl2 books/ (1.5 GB)",
+  "external_corpora/minizinc_full/       — MiniZinc/minizinc-benchmarks (251 MB)",
+  "external_corpora/tlaplus_examples/    — tlaplus/Examples (34 MB)",
+  "external_corpora/alloy/               — AlloyTools/models (928 KB)",
+  "external_corpora/boogie/              — boogie-org/boogie Test/ (22 MB)",
+  "external_corpora/frama-c/             — Frama-C/Frama-C-snapshot tests/ (26 MB)",
+  "external_corpora/viper/               — viperproject/silver src/test/ (8 MB)",
+  "external_corpora/tamarin/             — tamarin-prover/tamarin-prover (360 MB)",
+]
+
 [session-2026-04-18-100k-campaign-continued]
 summary = "100 K campaign — 10 provers widened, +252 284 records"
 umbrella-issue = "https://github.com/hyperpolymath/echidna/issues/12"