KERN v2.2.0 - Independent Z3 Proof Checker (Farkas/Resolution) & 8-Way SIMD BLAKE3 (3.42x)

KERN v2.2.0 introduces two major engine upgrades: an independent mathematical verifier for native Z3 proof DAGs and an 8-lane SIMD multi-buffer BLAKE3 engine for small-object verification.

1. Independent Z3 Proof DAG Checker (src/verifier/proof_check.zig)

Instead of trusting solver unsat output as an opaque string, KERN parses and mathematically audits native Z3 S-expression proof DAGs across 6 invariants:

• No proof holes: immediate rejection on hole, trust, or sorry steps.
• Premise binding: every nested (asserted ...) node is recursively matched against the normalized clauses of the input contract (premises_unbound == 0).
• Modus Ponens structure: verifies implication/equivalence matching between premises.
• Unit resolution: verifies that every resolved literal is refuted by its premise literals.
• Farkas' Lemma arithmetic: normalizes linear integer inequalities (negation of l <= r is r - l + 1 <= 0 over Z), applies Farkas weights, and verifies that all variable coefficients cancel to 0 while yielding a strictly contradictory positive constant.
• Root contradiction: the DAG must conclude false.

Scope note: internal Z3 rewrite steps are tracked separately in trusted_steps and are not claimed as independently re-derived. Alethe is not used: this Z3 build does not emit it (strings z3 | grep -ic alethe -> 0; no proof.format option). See docs/METRICS.md section 48.

2. 8-Way SIMD BLAKE3 Batch Engine (src/core/blake3_simd8.zig)

Single-chunk objects (<= 1024 B) cannot saturate 8-lane AVX2 chunk parallelism when hashed one by one. The engine hashes 8 objects of arbitrary individual lengths simultaneously across @Vector(8, u32) lanes using per-lane @select masking, without altering a single byte of the .kimg format. Each of the 8 results is still compared against its own 32-byte entry.digest.

Workload (10,000 objects, Intel i7-7700 AVX2)	Scalar	8-Way SIMD	Speedup
Isolated primitive - 96 B	352 MB/s	1,939 MB/s	5.51x
Isolated primitive - 200 B	369 MB/s	1,834 MB/s	4.97x
Isolated primitive - 512 B	537 MB/s	2,395 MB/s	4.46x
Isolated primitive - 1024 B	550 MB/s	2,728 MB/s	4.96x
End-to-end .kimg safe read (200 B)	356 MB/s	1,219 MB/s	3.42x
Single-read loop via cluster cache	387 MB/s	1,699 MB/s	4.39x

Raw unverified zero-copy slice addressing runs at ~102 GB/s; the end-to-end gap drops from 287x to 84x.

3. Cluster Cache for Per-Object Reads (KernFS.objectPayloadCached)

A 1-bit-per-object bitset (1250 bytes for 10,000 objects): the first access to any object verifies the whole cluster of 8 neighbours in one vector pass, and bits are set only after all eight match their own digests. Precondition, stated plainly: the cache is valid only for an immutable image (mmap of a sealed file); for mutable buffers objectPayload / verifyAllBatch / payloadSlice remain the honest paths.

Verification Baseline

• Core tests: 220 / 220 passed (+12 proof checker, +3 SIMD-8, +2 cluster cache, +1 linear rewrite verification, +2 boolean rules).
• Proof checker visible in the CLI: kernc prove formal/example.smt2 prints
  [PROOF VERIFIED] steps: 16 | premises bound: 1/1 | mp: 2 | rewrite (linear): 5 | farkas: 0 | trusted: 0 | holes: 0 - all 16 steps of that DAG are re-checked
  independently, with trusted_steps down to 0 (comparisons, linear arithmetic, mp, unit-resolution, Farkas, refl/symm/trans, and-elim, monotonicity).
• Static binary in Assets: kernc-x86_64-linux-musl (5,689,232 bytes, sha256 7f29d979...) - no toolchain needed, verify with SHA256SUMS.
• Non-vacuous canfail checks: 71 fault-injection cases registered; tools/registry.py reports 64/64 build targets covered with a proven-can-fail check (added proof-hole, proof-binding, simd8-masking).
• Evidence gate: all verification logs clean (RC=0).