5EZAwz…FwdTaA

//! The slot: a portfolio of proven LZ77 parsers behind a content router.
//!
//! `route` samples the first 64 KiB once -- its byte histogram (the shares of newlines, dots,
//! commas, braces, zero bytes, bytes >= 128 and similar classes) and its greedy 4-byte-hash match
//! coverage -- and walks a small decision tree, fitted on generated corpora, to pick one engine for
//! the whole input. Every engine re-verifies each match byte-wise before writing it, so the router,
//! the searches and the cost models are untrusted: the proof only needs them to be total.
//! Engines (see the section comments): `a_` = parse.rs, `b_` = parse.rs, `c_` = parse.rs, `d_` = parse.rs.
//!
//! Tokens: `t < 256` literal, else `2^24 + (dist-1)*256 + (len-3)`.

/// Bytes the router samples.
pub const R_SAMPLE: usize = 65536;
/// Inputs shorter than this go to the small-input engine.
pub const R_TINY: usize = 20000;

/// How many bytes agree at `a < b` and `b`, up to `cap`; needs `b + cap <= input.len()`.
pub fn r_len(input: &[u8], a: usize, b: usize, cap: usize) -> usize {
    let mut l = 0usize;
    while l < cap && input[a + l] == input[b + l] {
        l += 1;
    }
    l
}

/// The 4-byte hash at `p`; needs `p + 4 <= input.len()`.
pub fn r_hash(input: &[u8], p: usize) -> usize {
    let x = (input[p] as u32)
        .wrapping_add((input[p + 1] as u32).wrapping_mul(256))
        .wrapping_add((input[p + 2] as u32).wrapping_mul(65536))
        .wrapping_add((input[p + 3] as u32).wrapping_mul(16777216));
    ((x.wrapping_mul(2654435761) / 65536) % 65536) as usize
}

/// Greedy coverage of `input[start..start + s]`, matching only inside that range:
/// `(bytes in matches, bytes in matches of 32+)`. Needs `4 <= s` and `start + s <= input.len()`.
pub fn r_cover(input: &[u8], start: usize, s: usize) -> (usize, usize) {
    let mut head = [0u32; 65536];
    let mut cov = 0usize;
    let mut long = 0usize;
    let mut i = 0usize;
    let lim = s - 4;
    while i <= lim {
        let h = r_hash(input, start + i);
        let c = head[h] as usize;
        head[h] = (i + 1) as u32;
        let mut l = 0usize;
        if c > 0 && c - 1 < i {
            let rest = s - i;
            let cap = if rest < 258 { rest } else { 258 };
            l = r_len(input, start + (c - 1), start + i, cap);
        }
        if l >= 4 {
            cov = cov.wrapping_add(l);
            if l >= 32 {
                long = long.wrapping_add(l);
            }
            let mut q = i + 1;
            let e = i + l;
            while q < e && q <= lim {
                let hq = r_hash(input, start + q);
                head[hq] = (q + 1) as u32;
                q += 1;
            }
            i = e;
        } else {
            i += 1;
        }
    }
    (cov, long)
}

/// Byte histogram of the first `s` bytes; needs `s <= input.len()`.
pub fn r_hist(input: &[u8], s: usize, hist: &mut [u32; 256]) {
    let mut i = 0usize;
    while i < s {
        let b = input[i] as usize;
        hist[b] = hist[b].wrapping_add(1);
        i += 1;
    }
}

/// Sum of `hist[a..b]`; needs `b <= 256`.
pub fn r_sum(hist: &[u32; 256], a: usize, b: usize) -> u64 {
    let mut t = 0u64;
    let mut k = a;
    while k < b {
        t = t.wrapping_add(hist[k] as u64);
        k += 1;
    }
    t
}

/// Number of distinct byte values in the histogram.
pub fn r_alpha(hist: &[u32; 256]) -> usize {
    let mut c = 0usize;
    let mut k = 0usize;
    while k < 256 {
        if hist[k] > 0 {
            c += 1;
        }
        k += 1;
    }
    c
}

/// The engine for this input: its index in `parse`. Shares are compared per 100000 sampled bytes.
pub fn route(input: &[u8]) -> usize {
    let n = input.len();
    if n < R_TINY {
        return 3;
    }
    if n < R_SAMPLE {
        return 0;
    }
    let s = R_SAMPLE;
    let s64 = s as u64;
    let mut hist = [0u32; 256];
    r_hist(input, s, &mut hist);
    let f_colon = hist[58] as u64;
    let f_ctrl = r_sum(&hist, 1, 9).wrapping_add(r_sum(&hist, 11, 13)).wrapping_add(r_sum(&hist, 14, 32));
    let f_dot = hist[46] as u64;
    let f_hash = hist[35] as u64;
    let f_letter = r_sum(&hist, 65, 91).wrapping_add(r_sum(&hist, 97, 123));
    let f_lt = hist[60] as u64;
    let f_nl = hist[10] as u64;
    let f_paren = hist[40] as u64;
    let f_quote = hist[34] as u64;
    let f_semi = hist[59] as u64;
    let f_slash = hist[47] as u64;
    let f_space = hist[32] as u64;
    let f_zero = hist[0] as u64;
    if f_colon.wrapping_mul(100000) <= 522u64.wrapping_mul(s64) {
        if f_space.wrapping_mul(100000) <= 735u64.wrapping_mul(s64) {
            if f_nl.wrapping_mul(100000) <= 234u64.wrapping_mul(s64) {
                if f_ctrl.wrapping_mul(100000) <= 7470u64.wrapping_mul(s64) {
                    0
                } else {
                    1
                }
            } else {
                if f_letter.wrapping_mul(100000) <= 4478u64.wrapping_mul(s64) {
                    1
                } else {
                    if f_zero.wrapping_mul(100000) <= 1395u64.wrapping_mul(s64) {
                        2
                    } else {
                        1
                    }
                }
            }
        } else {
            if f_slash.wrapping_mul(100000) <= 1248u64.wrapping_mul(s64) {
                if f_colon.wrapping_mul(100000) <= 492u64.wrapping_mul(s64) {
                    if f_letter.wrapping_mul(100000) <= 75239u64.wrapping_mul(s64) {
                        1
                    } else {
                        2
                    }
                } else {
                    0
                }
            } else {
                3
            }
        }
    } else {
        if f_paren.wrapping_mul(100000) <= 750u64.wrapping_mul(s64) {
            if f_nl.wrapping_mul(100000) <= 3337u64.wrapping_mul(s64) {
                if f_hash.wrapping_mul(100000) <= 286u64.wrapping_mul(s64) {
                    if f_semi.wrapping_mul(100000) <= 1384u64.wrapping_mul(s64) {
                        3
                    } else {
                        0
                    }
                } else {
                    if f_colon.wrapping_mul(100000) <= 1535u64.wrapping_mul(s64) {
                        1
                    } else {
                        0
                    }
                }
            } else {
                if f_semi.wrapping_mul(100000) <= 26u64.wrapping_mul(s64) {
                    0
                } else {
                    2
                }
            }
        } else {
            if f_dot.wrapping_mul(100000) <= 1272u64.wrapping_mul(s64) {
                if f_quote.wrapping_mul(100000) <= 83u64.wrapping_mul(s64) {
                    1
                } else {
                    if f_lt.wrapping_mul(100000) <= 405u64.wrapping_mul(s64) {
                        0
                    } else {
                        3
                    }
                }
            } else {
                if f_colon.wrapping_mul(100000) <= 2368u64.wrapping_mul(s64) {
                    if f_space.wrapping_mul(100000) <= 23028u64.wrapping_mul(s64) {
                        1
                    } else {
                        0
                    }
                } else {
                    2
                }
            }
        }
    }
}

pub fn parse(input: &[u8], out: &mut [u32]) -> usize {
    let r = route(input);
    if r == 0 {
        a_parse(input, out)
    } else if r == 1 {
        b_parse(input, out)
    } else if r == 2 {
        c_parse(input, out)
    } else {
        d_parse(input, out)
    }
}


// ===== engine a: parse.rs =====

pub const A_H3B: u32 = 14;
pub const A_H3N: usize = 16384;
pub const A_H4B: u32 = 16;
pub const A_H4N: usize = 65536;
pub const A_H7B: u32 = 16;
pub const A_H7N: usize = 65536;
pub const A_WN: usize = 32768;
/// Price ring and backtracking chunk (positions).
pub const A_RING: usize = 8192;
pub const A_CHUNK: usize = 4096;
/// Long chain key length in bytes (5..8).
pub const A_KB7: u32 = 7;
/// Every length up to A_FULL_LEN is tried; above it, the last length of each length code.
pub const A_FULL_LEN: usize = 258;
/// The nearest 3-byte match is a candidate up to this distance.
pub const A_H3DIST: usize = 32768;
pub const A_H3DIST_STRUCT: usize = 32768;
pub const A_H3DIST_BIN: usize = 32768;
pub const A_H3DIST_PROSE: usize = 32768;
/// DNA-like inputs: the nearest 3-byte match is not worth its cost there.
pub const A_H3DIST_DNA: usize = 0;
/// DNA-like inputs price symbols by Huffman code lengths (1) instead of entropy (0).
pub const A_HUFF_DNA: usize = 1;
pub const A_HUFF_TEXT: usize = 0;
pub const A_HUFF_STRUCT: usize = 0;
pub const A_HUFF_BIN: usize = 0;
pub const A_HUFF_PROSE: usize = 0;
/// Symbol costs are rebuilt every A_UPD positions; counts are halved above A_HALF_AT symbols.
pub const A_UPD: usize = 2048;
pub const A_HALF_AT: u32 = 6000;
pub const A_INF: u32 = 0x3FFF_FFFF;
pub const A_UNREACHED: u64 = 0x3FFF_FFFF_0000_0000;
/// Backward extension: at most A_TMAX bytes, for the A_BEXT_TOP longest candidates of a position.
pub const A_TMAX: usize = 128;
pub const A_BEXT_TOP: usize = 3;
pub const A_BTRUNC: usize = 1;
/// Lazy positions beyond the first are searched only after an anchor match of at most A_LZ2MAX bytes.
pub const A_LZ2MAX: usize = 258;
/// Inputs below A_SMALL bytes take the lazy engine (see the module comment).
pub const A_SMALL: usize = 65536;
/// Long-match share (per 1024, `sample_long`) from which text / structured text / other binary
/// inputs take the lazy engine; samples of A_SBLOCKS x A_SBS bytes.
pub const A_LONG_T: usize = 400;
pub const A_LONG_S: usize = 512;
pub const A_LONG_B: usize = 1000000;
/// Any input with a long-repeat share of at least A_LONG_X/1024 takes route A_R_XLONG.
pub const A_LONG_X: usize = 800;
/// Text with at least A_HIGH_MB/1024 bytes >= 128 (multi-byte UTF-8 text) is its own route.
pub const A_HIGH_MB: usize = 154;
/// Engine per route: 3 lazy engine (full settings), 4 lazy engine (lighter text settings), 10..14 dynamic
/// program (10 text, 11 structured text, 12 other binary, 13 DNA-like, 14 prose).
pub const A_R_SMALL: usize = 3;
pub const A_R_FLAT: usize = 3;
pub const A_R_HIGH: usize = 3;
pub const A_R_DNA: usize = 13;
pub const A_R_PROSE: usize = 14;
pub const A_R_MB: usize = 10;
pub const A_R_TEXT: usize = 10;
pub const A_R_TLONG: usize = 3;
pub const A_R_STRUCT: usize = 11;
pub const A_R_SLONG: usize = 11;
pub const A_R_BIN: usize = 12;
pub const A_R_XLONG: usize = 3;
pub const A_R_BLONG: usize = 3;
pub const A_SBLOCKS: usize = 16;
pub const A_SBS: usize = 4096;
/// Dynamic-program settings per route: text, structured text, other binary, DNA-like, prose.
/// A_CT: continuation threshold, A_LZ: lazy positions searched, A_D4/A_D7: chain depths, A_SKIP: take-as-is length.
pub const A_CT: usize = 3;
pub const A_LZ: usize = 3;
pub const A_D4: usize = 4;
pub const A_D7: usize = 48;
pub const A_SKIP: usize = 64;
pub const A_CT_STRUCT: usize = 6;
pub const A_LZ_STRUCT: usize = 2;
pub const A_D4_STRUCT: usize = 2;
pub const A_D7_STRUCT: usize = 16;
pub const A_SKIP_STRUCT: usize = 64;
pub const A_CT_BIN: usize = 4;
pub const A_LZ_BIN: usize = 3;
pub const A_D4_BIN: usize = 4;
pub const A_D7_BIN: usize = 32;
pub const A_SKIP_BIN: usize = 64;
pub const A_CT_DNA: usize = 8;
pub const A_LZ_DNA: usize = 2;
pub const A_D4_DNA: usize = 8;
pub const A_D7_DNA: usize = 8;
pub const A_SKIP_DNA: usize = 32;
pub const A_CT_PROSE: usize = 6;
pub const A_LZ_PROSE: usize = 3;
pub const A_D4_PROSE: usize = 8;
pub const A_D7_PROSE: usize = 8;
pub const A_SKIP_PROSE: usize = 32;

/// DEFLATE length-code base lengths (codes 257..285) and extra bits.
pub const A_LBASE: [u32; 29] = [
    3, 4, 5, 6, 7, 8, 9, 10, 11, 13, 15, 17, 19, 23, 27, 31, 35, 43, 51, 59, 67, 83, 99, 115,
    131, 163, 195, 227, 258,
];
pub const A_LEXTRA: [u32; 32] = [
    0, 0, 0, 0, 0, 0, 0, 0, 1, 1, 1, 1, 2, 2, 2, 2, 3, 3, 3, 3, 4, 4, 4, 4, 5, 5, 5, 5, 0, 0, 0, 0,
];
/// DEFLATE distance-code base distances and extra bits.
pub const A_DBASE: [u32; 30] = [
    1, 2, 3, 4, 5, 7, 9, 13, 17, 25, 33, 49, 65, 97, 129, 193, 257, 385, 513, 769, 1025, 1537,
    2049, 3073, 4097, 6145, 8193, 12289, 16385, 24577,
];
pub const A_DEXTRA: [u32; 32] = [
    0, 0, 0, 0, 1, 1, 2, 2, 3, 3, 4, 4, 5, 5, 6, 6, 7, 7, 8, 8, 9, 9, 10, 10, 11, 11, 12, 12, 13,
    13, 0, 0,
];
/// round(16 * log2(1 + m/32)) for m < 32.
pub const A_FRAC: [u32; 32] = [
    0, 1, 1, 2, 3, 3, 4, 5, 5, 6, 6, 7, 7, 8, 9, 9, 9, 10, 10, 11, 11, 12, 12, 13, 13, 14, 14, 14,
    15, 15, 15, 16,
];

// ───────────────────────────── the load-bearing part ─────────────────────────────

/// The eight bytes at `p` as one big-endian number (byte `p` most significant), or 0 when
/// fewer than eight bytes remain (Horner form; one load plus `bswap` once inlined).
#[inline(always)]
pub fn a_load8(input: &[u8], p: usize) -> u64 {
    let n = input.len();
    if n >= 8 && p <= n - 8 {
        let mut v = input[p] as u64;
        v = v * 256 + input[p + 1] as u64;
        v = v * 256 + input[p + 2] as u64;
        v = v * 256 + input[p + 3] as u64;
        v = v * 256 + input[p + 4] as u64;
        v = v * 256 + input[p + 5] as u64;
        v = v * 256 + input[p + 6] as u64;
        v * 256 + input[p + 7] as u64
    } else {
        0
    }
}

/// How many leading (most significant) bytes the words `x` and `y` share: 8 when equal.
#[inline(always)]
pub fn a_first_diff(x: u64, y: u64) -> usize {
    let z = x ^ y;
    let lz = z.leading_zeros();
    let bytes = lz / 8;
    bytes as usize
}

/// How many bytes agree at `a` and `b`, up to `cap`: eight at a time, the first mismatching
/// word resolved by `first_diff`, the last `cap % 8` bytes one at a time.
#[inline(always)]
pub fn a_mlen(input: &[u8], a: usize, b: usize, cap: usize) -> usize {
    let mut l = 0usize;
    while cap - l >= 8 {
        let x = a_load8(input, a + l);
        let y = a_load8(input, b + l);
        if x != y {
            return l + a_first_diff(x, y);
        }
        l += 8;
    }
    while l < cap && input[a + l] == input[b + l] {
        l += 1;
    }
    l
}

/// True only if `(len, dist)` is a legal match at `p` whose bytes all agree.
pub fn a_check(input: &[u8], p: usize, len: usize, dist: usize) -> bool {
    let n = input.len();
    if p > n || len < 3 || len > 258 || dist < 1 || dist > 32768 || dist > p || len > n - p {
        return false;
    }
    let src = p - dist;
    let l = a_mlen(input, src, p, len);
    l == len
}

/// `v[i]`, or 0 when `i` is out of range.
pub fn a_get0(v: &[u32], i: usize) -> u32 {
    if i < v.len() {
        v[i]
    } else {
        0
    }
}


/// Phase 2: walk the plan from 0 (entry `k` for the `k`-th planned token); a planned match is
/// written only if `check` accepts it, else its bytes become literals (so the plan stays aligned).
pub fn a_emit(input: &[u8], plan: &[u32], out: &mut [u32]) -> usize {
    let n = input.len();
    let mut ntok = 0usize;
    let mut k = 0usize;
    let mut owed = 0usize;
    let mut p = 0usize;
    while p < n {
        if owed > 0 {
            out[ntok] = input[p] as u32;
            ntok += 1;
            p += 1;
            owed -= 1;
        } else {
            let v = a_get0(plan, k);
            k += 1;
            let len = (v % 512) as usize;
            let dist = (v / 512) as usize;
            let valid = a_check(input, p, len, dist);
            if valid {
                let tok = 16777216u32 + ((dist - 1) as u32) * 256 + ((len - 3) as u32);
                out[ntok] = tok;
                ntok += 1;
                p += len;
            } else {
                out[ntok] = input[p] as u32;
                ntok += 1;
                p += 1;
                if len >= 2 {
                    owed = len - 1;
                }
            }
        }
    }
    ntok
}

/// The whole parser: one sniff, then the route's engine (the dynamic program's plan is re-checked
/// by `emit`).
pub fn a_parse(input: &[u8], out: &mut [u32]) -> usize {
    let cls = a_a_sniff(input);
    let r = a_route(input, cls);
    if r == 3 {
        a_a_parse_cls(input, out, cls, 1)
    } else if r == 4 {
        a_a_parse_cls(input, out, cls, 0)
    } else {
        let plan = a_make_plan(input, r);
        a_emit(input, &plan, out)
    }
}

// ─────────────────────────── phase 1: search, totality only ───────────────────────────



/// Eight bytes at `i`, first byte most significant (0 when out of range).
#[inline(always)]
pub fn a_be8(s: &[u8], i: usize) -> u64 {
    if i + 8 <= s.len() {
        ((s[i] as u64) << 56)
            | ((s[i + 1] as u64) << 48)
            | ((s[i + 2] as u64) << 40)
            | ((s[i + 3] as u64) << 32)
            | ((s[i + 4] as u64) << 24)
            | ((s[i + 5] as u64) << 16)
            | ((s[i + 6] as u64) << 8)
            | (s[i + 7] as u64)
    } else {
        0
    }
}

/// Length of the common prefix of s[a..] and s[b..], at most `cap`.
#[inline(always)]
pub fn a_common(s: &[u8], a: usize, b: usize, cap: usize) -> usize {
    let mut k = 0usize;
    let mut run = 1u32;
    while run == 1 && k + 8 <= cap {
        let x = a_be8(s, a + k) ^ a_be8(s, b + k);
        if x == 0 {

import Lz77
import Slot

/-!
Proof for the portfolio slot. Each engine's proof is its own published proof with the engine's
functions and constants renamed, in its own namespace; the router is only proven total, and
`parse_spec` takes each branch from the engine it dispatches to.
-/

namespace Submission
open Aeneas Aeneas.Std Result ControlFlow
open LZ77 (toks bytes)

set_option maxRecDepth 8192
set_option maxHeartbeats 4000000



/-!
# mB hybrid: router + lazy engine (tokens proved) + DP engine (plan re-verified), the proof

Sections, in this order, form this file (see /root/66/work/pk/mb/CONTRACT.md):
`sec_head` (this part: header, generic step rules, bound lemmas), `sec_dp` (the dynamic
program: totality only, `make_plan_spec`), `sec_lazy` (the lazy engine: tokens decode to the
input, `a_sniff_spec`, `a_parse_cls_spec`), `sec_spine` (match check, plan emission, router,
`parse_spec`), then the closing `end Submission`.
-/

namespace EA
open Aeneas Aeneas.Std Result ControlFlow

set_option maxRecDepth 8192
set_option maxHeartbeats 1000000
-- The search recipe is uniform on purpose; where a step of it has nothing to do, say nothing.
set_option linter.unusedTactic false
set_option linter.unreachableTactic false
set_option linter.unusedSimpArgs false
set_option linter.unusedVariables false

open LZ77 (toks bytes bytes_getElem! Matches emit_lit emit_match)

/-! ## Step rules shared by every section -/

/-- Any pure operation in bind position (`lift (saturating_add ..)`, `lift (deref_mut ..)`,
    casts, `leading_zeros`): `step*` names its result instead of stopping. -/
@[local step]
theorem lift_spec {α : Type} (x : α) : lift x ⦃ fun y => y = x ⦄ := by
  simp [lift, WP.spec_ok]

/-- The guarded read: total, and nothing is known about the value. -/
@[local step]
theorem get0_spec (v : Slice Std.U32) (i : Std.Usize) : slot.a_get0 v i ⦃ fun _ => True ⦄ := by
  rw [slot.a_get0]; split <;> step*

/-! ## Facts `scalar_tac` instantiates by itself

`x &&& mask ≤ mask`, `x >>> k ≤ x` (after `scalar_tac_simps` turns `(a &&& b).val` into
`a.val &&& b.val`), and `usize` has at least 32 bits (a `usize` shift by a constant `k < 32`
needs `k < System.Platform.numBits`, which is otherwise unknown: the platform may be 32-bit). -/

@[local scalar_tac x &&& y]
theorem nat_and_le_right (x y : Nat) : x &&& y ≤ y := Nat.and_le_right

@[local scalar_tac x >>> y]
theorem nat_shiftRight_le (x y : Nat) : x >>> y ≤ x := Nat.shiftRight_le x y

theorem numBits_ge : 32 ≤ System.Platform.numBits := by
  cases System.Platform.numBits_eq <;> simp [*]

@[local scalar_tac System.Platform.numBits]
theorem numBits_ge' : 32 ≤ System.Platform.numBits := numBits_ge

/-! ## `leading_zeros`

`core.num.U32.leading_zeros x` is `⟨BitVec.leadingZeros x.bv⟩`; `step*` passes over it with
`lift_spec` and then knows nothing about the value. Use these before `scalar_tac`:
`have := lz32_le_of_pow_le x 3 (by scalar_tac)` gives `lz + 3 ≤ 31` when `8 ≤ x`. -/

theorem lz_le_w {w : Nat} (x : BitVec w) : BitVec.leadingZeros x ≤ w := by
  unfold BitVec.leadingZeros; split <;> omega

theorem lz32_val (x : Std.U32) :
    (core.num.U32.leading_zeros x).val = BitVec.leadingZeros x.bv := by
  simp only [core.num.U32.leading_zeros, UScalar.val]
  have := lz_le_w x.bv
  apply Nat.mod_eq_of_lt
  simp at this ⊢
  omega

theorem lz32_eq (x : Std.U32) (h : x.val ≠ 0) :
    (core.num.U32.leading_zeros x).val = 31 - Nat.log 2 x.val := by
  rw [lz32_val]
  unfold BitVec.leadingZeros
  have hx : x.bv ≠ 0 := by
    intro h0; apply h; show x.bv.toNat = 0; rw [h0]; rfl
  rw [if_neg hx, UScalar.bv_toNat]
  omega

theorem lz32_le (x : Std.U32) : (core.num.U32.leading_zeros x).val ≤ 32 := by
  rw [lz32_val]; exact lz_le_w x.bv

/-- `2^k ≤ x` (so `x ≠ 0`): at most `31 - k` leading zeros. -/
theorem lz32_le_of_pow_le (x : Std.U32) (k : Nat) (h : 2 ^ k ≤ x.val) :
    (core.num.U32.leading_zeros x).val + k ≤ 31 := by
  have hx : x.val ≠ 0 := by have := Nat.one_le_two_pow (n := k); omega
  rw [lz32_eq x hx]
  have hk : k ≤ Nat.log 2 x.val := Nat.le_log_of_pow_le (by norm_num) h
  have : x.val < 2 ^ 32 := by scalar_tac
  have hl : Nat.log 2 x.val < 32 := Nat.log_lt_of_lt_pow (by omega) this
  omega

/-- `x < 2^k`: at least `32 - k` leading zeros. -/
theorem lz32_ge_of_lt_pow (x : Std.U32) (k : Nat) (h : x.val < 2 ^ k) :
    32 - k ≤ (core.num.U32.leading_zeros x).val := by
  by_cases hx : x.val = 0
  · rw [lz32_val]; unfold BitVec.leadingZeros
    have : x.bv = 0 := by
      apply BitVec.eq_of_toNat_eq; rw [UScalar.bv_toNat]; simpa using hx
    rw [if_pos this]; omega
  · rw [lz32_eq x hx]
    have hl : Nat.log 2 x.val < k := Nat.log_lt_of_lt_pow hx h
    omega

theorem lz64_val (x : Std.U64) :
    (core.num.U64.leading_zeros x).val = BitVec.leadingZeros x.bv := by
  simp only [core.num.U64.leading_zeros, UScalar.val]
  have := lz_le_w x.bv
  apply Nat.mod_eq_of_lt
  simp at this ⊢
  omega

theorem lz64_le (x : Std.U64) : (core.num.U64.leading_zeros x).val ≤ 64 := by
  rw [lz64_val]; exact lz_le_w x.bv

/-- Registered for `scalar_tac`: `31 - lz` cannot underflow once `x ≠ 0` is known. -/
@[local scalar_tac core.num.U32.leading_zeros x]
theorem lz32_bound (x : Std.U32) :
    (core.num.U32.leading_zeros x).val ≤ 32 ∧
      (x.val = 0 ∨ (core.num.U32.leading_zeros x).val ≤ 31) := by
  refine ⟨lz32_le x, ?_⟩
  by_cases h : x.val = 0
  · exact Or.inl h
  · right; rw [lz32_eq x h]; omega

@[local scalar_tac core.num.U64.leading_zeros x]
theorem lz64_bound (x : Std.U64) : (core.num.U64.leading_zeros x).val ≤ 64 := lz64_le x

/-! ## Bounded tables

`LeAll l B`: every entry of the list `l` (an `Array`'s or a `Vec`'s `.val`) is at most `B`.
The invariant for tables whose entries are only ever written with bounded values (Huffman
lengths `≤ 15`) or that count loop iterations (`LeAll lf.val t`, then `lf[j] + 1` cannot
overflow while `t < 2^32 - 1`). After `step*`, a read `x = a.val[i]` plus
`have := LeAll_get hinv i.val (by scalar_tac)` gives `scalar_tac` the bound. -/

def LeAll {ty : UScalarTy} (l : List (UScalar ty)) (B : Nat) : Prop :=
  ∀ j (h : j < l.length), (l[j]).val ≤ B

theorem LeAll_get {ty : UScalarTy} {l : List (UScalar ty)} {B : Nat} (hl : LeAll l B)
    (j : Nat) (hj : j < l.length) : (l[j]).val ≤ B := hl j hj

theorem LeAll_get! {ty : UScalarTy} {l : List (UScalar ty)} {B : Nat} (hl : LeAll l B)
    (j : Nat) (hj : j < l.length) : (l[j]!).val ≤ B := by
  rw [List.getElem!_eq_getElem?_getD, List.getElem?_eq_getElem hj]; exact hl j hj

theorem LeAll_mono {ty : UScalarTy} {l : List (UScalar ty)} {B B' : Nat} (hl : LeAll l B)
    (h : B ≤ B') : LeAll l B' := fun j hj => Nat.le_trans (hl j hj) h

theorem LeAll_replicate {ty : UScalarTy} (n : Nat) (x : UScalar ty) (B : Nat) (h : x.val ≤ B) :
    LeAll (List.replicate n x) B := by
  intro j hj; simp [List.getElem_replicate]; exact h

theorem LeAll_set {ty : UScalarTy} {l : List (UScalar ty)} {B : Nat} (hl : LeAll l B)
    (i : Nat) (x : UScalar ty) (hx : x.val ≤ B) : LeAll (l.set i x) B := by
  intro j hj
  rw [List.getElem_set]
  split
  · exact hx
  · exact hl j (by simpa using hj)

theorem LeAll_append {ty : UScalarTy} {l : List (UScalar ty)} {B : Nat} (hl : LeAll l B)
    (x : UScalar ty) (hx : x.val ≤ B) : LeAll (l ++ [x]) B := by
  intro j hj
  rw [List.getElem_append]
  split
  · exact hl j (by assumption)
  · simp; exact hx

/-- The counter step: `l[i] ≤ t` everywhere, one entry goes up by one. -/
theorem LeAll_set_succ {ty : UScalarTy} {l : List (UScalar ty)} {t : Nat} (hl : LeAll l t)
    (i : Nat) (x : UScalar ty) (hx : x.val ≤ t + 1) : LeAll (l.set i x) (t + 1) :=
  LeAll_set (LeAll_mono hl (Nat.le_succ t)) i x hx

/-! # sec_dp (owner: dp) -- the dynamic program: candidate collection, cost models, DP passes,
plan writing. Totality only (the plan is re-verified by `emit`): every post is `True` except the few
bounds the callers inside this section need. Statements = CONTRACT.md section 7.2 (Rust edits G, E1-E4). -/

/-! ## dp facts: constants (bounds only, except the array sizes) and small lemmas -/

/-- The nextl table after `fill_nextl` (edit E3): every length below 512 has a larger successor. -/
def DpNextl (nextl : Array Std.U16 512#usize) : Prop := ∀ j, j < 512 → j < (nextl.val[j]!).val

theorem dp_size {n : Nat} (h : n + n ≤ Std.Usize.max) : n + 2147483648 ≤ Std.Usize.max := by
  have : Std.Usize.max = 2 ^ System.Platform.numBits - 1 := by
    simp [Std.Usize.max, Std.Usize.numBits]
  rcases System.Platform.numBits_eq with h32 | h64
  · rw [this, h32] at h ⊢; omega
  · rw [this, h64] at h ⊢; omega

theorem dp_RING_val : slot.A_RING.val = 8192 := by simp [slot.A_RING]
theorem dp_WN_val : slot.A_WN.val = 32768 := by simp [slot.A_WN]
theorem dp_H3N_val : slot.A_H3N.val = 16384 := by simp [slot.A_H3N]
theorem dp_H4N_val : slot.A_H4N.val = 65536 := by simp [slot.A_H4N]
theorem dp_H7N_val : slot.A_H7N.val = 65536 := by simp [slot.A_H7N]
theorem dp_H3B_bound : 1 ≤ slot.A_H3B.val ∧ slot.A_H3B.val ≤ 32 := by simp [slot.A_H3B]
theorem dp_H4B_bound : 1 ≤ slot.A_H4B.val ∧ slot.A_H4B.val ≤ 32 := by simp [slot.A_H4B]
theorem dp_H7B_bound : 1 ≤ slot.A_H7B.val ∧ slot.A_H7B.val ≤ 64 := by simp [slot.A_H7B]
theorem dp_KB7_bound : slot.A_KB7.val ≤ 8 := by simp [slot.A_KB7]
theorem dp_UPD_bound : slot.A_UPD.val ≤ 1048576 := by simp [slot.A_UPD]
theorem dp_TMAX_bound : slot.A_TMAX.val ≤ 1048576 := by simp [slot.A_TMAX]
theorem dp_BEXT_TOP_bound : slot.A_BEXT_TOP.val ≤ 1048576 := by simp [slot.A_BEXT_TOP]

/-- `FRAC` (16 log2(1 + m/32)): every entry is at most 16. -/
theorem dp_FRAC_le : LeAll slot.A_FRAC.val 16 := by
  unfold slot.A_FRAC LeAll; simp only [Array.make]; decide

/-- A `u32` shifted right by 9 (a candidate's distance) is below `2^23`. -/
theorem dp_shr9 (c : Std.U32) : c.val >>> 9 < 8388608 := by
  rw [Nat.shiftRight_eq_div_pow]
  have : c.val < 2 ^ 32 := by scalar_tac
  omega

/-- `n + n` does not wrap iff it is above `n` (for `n ≥ 1`); edit G tests it. -/
theorem dp_wadd_self (n : Std.Usize) (h : n.val < (core.num.Usize.wrapping_add n n).val) :
    n.val + n.val ≤ Std.Usize.max := by
  rw [core.num.Usize.wrapping_add_val_eq] at h
  have hs : Std.Usize.max = UScalar.size .Usize - 1 := by
    simp [Std.Usize.max, Std.Usize.size, Std.Usize.numBits]
  have hn : n.val < UScalar.size .Usize := by
    have := n.hBounds; simp only [UScalar.size]; exact this
  by_contra hc
  have h2 : UScalar.size .Usize ≤ n.val + n.val := by omega
  rw [Nat.mod_eq_sub_mod h2, Nat.mod_eq_of_lt (by omega)] at h
  omega

theorem dp_or_one_le (x : Nat) : x ||| 1 ≤ x + 1 := by
  have h := Nat.two_pow_add_eq_or_of_lt (i := 1) (b := 1) (by omega) (x / 2)
  have hx : x ||| 1 = 2 ^ 1 * (x / 2) ||| 1 := by
    rcases Nat.mod_two_eq_zero_or_one x with h0 | h1
    · have : x = 2 ^ 1 * (x / 2) := by omega
      conv_lhs => rw [this]
    · have e := Nat.two_pow_add_eq_or_of_lt (i := 1) (b := 1) (by omega) (x / 2)
      have : x = 2 ^ 1 * (x / 2) ||| 1 := by omega
      conv_lhs => rw [this]
      rw [Nat.or_assoc, Nat.or_self]
  rw [hx, ← h]
  omega

/-- A fresh table `[x; n]` is bounded by any bound of `x`. -/
theorem dp_LeAll_repeat {ty : UScalarTy} (n : Std.Usize) (x : UScalar ty) (B : Nat) (h : x.val ≤ B) :
    LeAll (Array.repeat n x).val B := by
  rw [Array.repeat_val]; exact LeAll_replicate _ _ _ h

/-- `r = a.set i v` with `a` and `v` bounded: `r` is bounded. -/
theorem dp_LeAll_set_of_eq {ty : UScalarTy} {n : Std.Usize} {a r : Array (UScalar ty) n} {i : Std.Usize}
    {v : UScalar ty} {B : Nat} (hr : r = a.set i v) (ha : LeAll a.val B) (hv : v.val ≤ B) : LeAll r.val B := by
  rw [hr, Array.set_val_eq]; exact LeAll_set ha _ _ hv

theorem dp_getElem!_set {ty : UScalarTy} (l : List (UScalar ty)) (i j : Nat) (x : UScalar ty)
    (hi : i < l.length) : (l.set i x)[j]! = if i = j then x else l[j]! := by
  simp only [List.getElem!_eq_getElem?_getD, List.getElem?_set]
  split
  · simp [*]
  · rfl

/-! ## words and match lengths (`be8`, `common` are shared with the router) -/

@[local step] theorem be8_spec (s : Slice Std.U8) (i : Std.Usize) (h : i.val + 8 ≤ Std.Usize.max) :
    slot.a_be8 s i ⦃ fun _ => True ⦄ := by
  rw [slot.a_be8]
  step*

@[local step]
theorem common_loop0_spec (s : Slice Std.U8) (a b cap k : Std.Usize) (run : Std.U32)
    (ha : a.val + cap.val + 8 ≤ Std.Usize.max) (hb : b.val + cap.val + 8 ≤ Std.Usize.max) (hk : k.val ≤ cap.val) :
    slot.a_common_loop0 s a b cap k run ⦃ fun r => r.1.val ≤ cap.val ⦄ := by
  rw [slot.a_common_loop0]
  apply Std.loop.spec_decr_nat
    (measure := fun (k', run') => cap.val + 9 - k'.val + run'.val)
    (inv := fun (k', _) => k'.val ≤ cap.val)
  · rintro ⟨k', run'⟩ hk'
    simp only [slot.a_common_loop0.body]
    step*
    repeat' (split <;> step*)
    all_goals try (have := lz64_bound x)
    all_goals scalar_tac
  · exact hk

@[local step]
theorem common_loop1_spec (s : Slice Std.U8) (a b cap k : Std.Usize) (run : Std.U32)
    (ha : a.val + cap.val + 8 ≤ Std.Usize.max) (hb : b.val + cap.val + 8 ≤ Std.Usize.max) (hk : k.val ≤ cap.val) :
    slot.a_common_loop1 s a b cap k run ⦃ fun r => r.val ≤ cap.val ⦄ := by
  rw [slot.a_common_loop1]
  apply Std.loop.spec_decr_nat
    (measure := fun (k', run') => cap.val + 1 - k'.val + run'.val)
    (inv := fun (k', _) => k'.val ≤ cap.val)
  · rintro ⟨k', run'⟩ hk'
    simp only [slot.a_common_loop1.body]
    step*
    repeat' (split <;> step*)
    all_goals scalar_tac
  · exact hk

@[local step] theorem common_spec (s : Slice Std.U8) (a b cap : Std.Usize)
    (ha : a.val + cap.val + 8 ≤ Std.Usize.max) (hb : b.val + cap.val + 8 ≤ Std.Usize.max) :
    slot.a_common s a b cap ⦃ fun r => r.val ≤ cap.val ⦄ := by
  rw [slot.a_common]
  step*

@[local step] theorem hash3_spec (x : Std.U32) : slot.a_hash3 x ⦃ fun r => r.val < 16384 ⦄ := by
  have := dp_H3B_bound
  have := dp_H3N_val
  rw [slot.a_hash3]
  step*

@[local step] theorem hash4_spec (x : Std.U32) : slot.a_hash4 x ⦃ fun r => r.val < 65536 ⦄ := by
  have := dp_H4B_bound
  have := dp_H4N_val
  rw [slot.a_hash4]
  step*

@[local step] theorem hash7_spec (x : Std.U64) : slot.a_hash7 x ⦃ fun r => r.val < 65536 ⦄ := by
  have := dp_H7B_bound
  have := dp_H7N_val
  rw [slot.a_hash7]
  step*

@[local step] theorem probe_spec (s : Slice Std.U8) (c i : Std.Usize) (b8 : Std.U64) (cap best : Std.Usize)
    (hc : c.val ≤ i.val) (hcap : 9 ≤ cap.val) (hic : i.val + cap.val ≤ s.length)
    (hs8 : s.length + 8 ≤ Std.Usize.max) :
    slot.a_probe s c i b8 cap best ⦃ fun r => r.val ≤ cap.val ∧ (r.val = 0 ∨ best.val < r.val) ⦄ := by
  rw [slot.a_probe]
  step*
  repeat' (split <;> step*)
  all_goals try (have := lz64_bound x)
  all_goals scalar_tac

@[local step]
theorem walk_loop_spec (s : Slice Std.U8) (prev) (i : Std.Usize) (b8 : Std.U64) (cap : Std.Usize)
    (cands) (nc best c k : Std.Usize)
    (hc : c.val ≤ i.val) (hcap : 9 ≤ cap.val) (hic : i.val + cap.val ≤ s.length)
    (hs8 : s.length + 8 ≤ Std.Usize.max) (hb : best.val ≤ cap.val) :
    slot.a_walk_loop s prev i b8 cap cands nc best c k ⦃ fun r => best.val ≤ r.2.2.val ∧ r.2.2.val ≤ cap.val ⦄ := by
  have hwn := dp_WN_val
  rw [slot.a_walk_loop]
  apply Std.loop.spec_decr_nat
    (measure := fun (_, _, _, _, k') => k'.val)
    (inv := fun (_, _, best', c', _) => c'.val ≤ i.val ∧ best.val ≤ best'.val ∧ best'.val ≤ cap.val)
  · rintro ⟨cands', nc', best', c', k'⟩ ⟨h1, h2, h3⟩
    simp only [slot.a_walk_loop.body]
    step*
    repeat' (split <;> step*)
    all_goals scalar_tac
  · exact ⟨hc, le_refl _, hb⟩

@[local step] theorem walk_spec (s : Slice Std.U8) (prev) (i start depth : Std.Usize) (b8 : Std.U64)
    (cap : Std.Usize) (cands) (nc0 best0 : Std.Usize)
    (hst : start.val ≤ i.val) (hcap : 9 ≤ cap.val) (hic : i.val + cap.val ≤ s.length)
    (hs8 : s.length + 8 ≤ Std.Usize.max) (hb : best0.val ≤ cap.val) :
    slot.a_walk s prev i start depth b8 cap cands nc0 best0 ⦃ fun r => best0.val ≤ r.1.2.val ∧ r.1.2.val ≤ cap.val ⦄ := by
  rw [slot.a_walk]
  step*

@[local step] theorem skip_same_spec (prev) (start depth : Std.Usize) (same : Bool) :
    slot.a_skip_same prev start depth same ⦃ fun r => r.1.val ≤ start.val ⦄ := by
  have hwn := dp_WN_val
  rw [slot.a_skip_same]
  step*
  repeat' (split <;> step*)
  all_goals scalar_tac

/-! ## the three position tables (heads stay below the current position) -/

@[local step] theorem insert_pos_spec (head3 : Array Std.U32 16384#usize) (head4 : Array Std.U32 65536#usize)
    (prev4) (head7 : Array Std.U32 65536#usize) (prev7) (q : Std.Usize) (b8 : Std.U64) (sh7 : Std.U32) (B : Nat)
    (h3 : LeAll head3.val B) (h4 : LeAll head4.val B) (h7 : LeAll head7.val B) (hq : q.val ≤ B) :
    slot.a_insert_pos head3 head4 prev4 head7 prev7 q b8 sh7 ⦃ fun r =>
      r.1.1.val ≤ B ∧ r.1.2.1.val ≤ B ∧ r.1.2.2.val ≤ B ∧
      LeAll r.2.1.val B ∧ LeAll r.2.2.1.val B ∧ LeAll r.2.2.2.2.1.val B ⦄ := by
  have hwn := dp_WN_val
  have H3 := h3
  have H4 := h4
  have H7 := h7
  rw [slot.a_insert_pos]
  step*
  have e3 := LeAll_get H3 h3.val (by scalar_tac)
  have e4 := LeAll_get H4 h4.val (by scalar_tac)
  have e7 := LeAll_get H7 h7.val (by scalar_tac)
  refine ⟨by scalar_tac, by scalar_tac, by scalar_tac, ?_, ?_, ?_⟩
  · exact dp_LeAll_set_of_eq head31_post H3 (by scalar_tac)
  · exact dp_LeAll_set_of_eq head41_post H4 (by scalar_tac)
  · exact dp_LeAll_set_of_eq head71_post H7 (by scalar_tac)

@[local step]
theorem insert_range_loop_spec (input : Slice Std.U8) (head3 : Array Std.U32 16384#usize)
    (head4 : Array Std.U32 65536#usize) (prev4) (head7 : Array Std.U32 65536#usize) (prev7)
    (e : Std.Usize) (sh7 : Std.U32) (q : Std.Usize) (B : Nat)
    (h3 : LeAll head3.val B) (h4 : LeAll head4.val B) (h7 : LeAll head7.val B)
    (he : e.val ≤ B + 1) (he8 : e.val + 8 ≤ Std.Usize.max) :
    slot.a_insert_range_loop input head3 head4 prev4 head7 prev7 e sh7 q ⦃ fun r =>
      LeAll r.1.val B ∧ LeAll r.2.1.val B ∧ LeAll r.2.2.2.1.val B ⦄ := by
  rw [slot.a_insert_range_loop]
  apply Std.loop.spec_decr_nat
    (measure := fun (_, _, _, _, _, q') => e.val - q'.val)
    (inv := fun (h3', h4', _, h7', _, _) => LeAll h3'.val B ∧ LeAll h4'.val B ∧ LeAll h7'.val B)
  · rintro ⟨h3', h4', p4', h7', p7', q'⟩ ⟨i3, i4, i7⟩
    simp only [slot.a_insert_range_loop.body]
    split
    · step*
      all_goals scalar_tac
    · step*
  · exact ⟨h3, h4, h7⟩

@[local step] theorem insert_range_spec (input : Slice Std.U8) (head3 : Array Std.U32 16384#usize)
    (head4 : Array Std.U32 65536#usize) (prev4) (head7 : Array Std.U32 65536#usize) (prev7)
    (f e : Std.Usize) (sh7 : Std.U32) (B : Nat)
    (h3 : LeAll head3.val B) (h4 : LeAll head4.val B) (h7 : LeAll head7.val B)
    (he : e.val ≤ B + 1) (he8 : e.val + 8 ≤ Std.Usize.max) :
    slot.a_insert_range input head3 head4 prev4 head7 prev7 f e sh7 ⦃ fun r =>
      LeAll r.1.val B ∧ LeAll r.2.1.val B ∧ LeAll r.2.2.2.1.val B ⦄ := by
  rw [slot.a_insert_range]
  exact insert_range_loop_spec input head3 head4 prev4 head7 prev7 e sh7 f B h3 h4 h7 he he8
/-! ## the price ring (`pa`, slots `% RING`) -/

theorem dp_nextl_lt {nextl : Array Std.U16 512#usize} (hnx : DpNextl nextl) (j : Nat)
    (hj : j < nextl.val.length) : j < (nextl.val[j]).val := by
  have hl : nextl.val.length = 512 := by simp
  have := hnx j (by omega)
  rwa [List.getElem!_eq_getElem?_getD, List.getElem?_eq_getElem hj, Option.getD_some] at this

@[local step] theorem relax_one_spec (pa) (slt : Std.Usize) (cost choice : Std.U32) :
    slot.a_relax_one pa slt cost choice ⦃ fun _ => True ⦄ := by
  have := dp_RING_val
  rw [slot.a_relax_one]
  step*
  repeat' (split <;> step*)

@[local step]
theorem relax_run_loop_spec (pa lc) (nextl : Array Std.U16 512#usize) (i hi : Std.Usize) (base dpack : Std.U32)
    (l : Std.Usize) (hnx : DpNextl nextl) (hhi : hi.val ≤ 512) (hih : i.val + hi.val ≤ Std.Usize.max) :
    slot.a_relax_run_loop pa lc nextl i hi base dpack l ⦃ fun _ => True ⦄ := by
  have := dp_RING_val
  rw [slot.a_relax_run_loop]
  apply Std.loop.spec_decr_nat
    (measure := fun (_, l') => hi.val - l'.val)
    (inv := fun _ => True)
  · rintro ⟨pa', l'⟩ _
    simp only [slot.a_relax_run_loop.body]
    split
    · step*
      repeat' (split <;> step*)
      all_goals
        have hx := dp_nextl_lt hnx i1.val (by scalar_tac)
        scalar_tac
    · step*
  · trivial

@[local step] theorem relax_run_spec (pa lc) (nextl : Array Std.U16 512#usize) (i lo hi : Std.Usize)
    (base dpack : Std.U32) (hnx : DpNextl nextl) (hhi : hi.val < 512) (hih : i.val + hi.val ≤ Std.Usize.max) :
    slot.a_relax_run pa lc nextl i lo hi base dpack ⦃ fun _ => True ⦄ := by
  have := dp_RING_val
  rw [slot.a_relax_run]
  step*
  repeat' (split <;> step*)

@[local step]
theorem back_best_loop_spec (input : Slice Std.U8) (pa lc) (i s len dd t bt : Std.Usize) (bv : Std.U32)
    (hi : i.val < input.length) (hlen : len.val < 512) (hdd : dd.val < 8388608)
    (hN : input.length + 2147483648 ≤ Std.Usize.max)
    (ht : t.val ≤ i.val) (hbt : bt.val ≤ t.val) (ht258 : t.val = 0 ∨ len.val + t.val ≤ 258) :
    slot.a_back_best_loop input pa lc i s len dd t bt bv ⦃ fun r =>
      r.1.val ≤ i.val ∧ (r.1.val = 0 ∨ len.val + r.1.val ≤ 258) ⦄ := by
  have := dp_RING_val
  rw [slot.a_back_best_loop]
  apply Std.loop.spec_decr_nat
    (measure := fun (t', _, _) => slot.A_TMAX.val - t'.val)
    (inv := fun (t', bt', _) => t'.val ≤ i.val ∧ bt'.val ≤ t'.val ∧ (t'.val = 0 ∨ len.val + t'.val ≤ 258))
  · rintro ⟨t', bt', bv'⟩ ⟨h1, h2, h3⟩
    simp only [slot.a_back_best_loop.body]
    step*
    repeat' (split <;> step*)
    all_goals scalar_tac
  · exact ⟨ht, hbt, ht258⟩

@[local step] theorem back_best_spec (input : Slice Std.U8) (pa lc) (i s len dd : Std.Usize)
    (hi : i.val < input.length) (hlen : len.val < 512) (hdd : dd.val < 8388608)
    (hN : input.length + 2147483648 ≤ Std.Usize.max) :
    slot.a_back_best input pa lc i s len dd ⦃ fun r => r.1.val ≤ i.val ∧ (r.1.val = 0 ∨ len.val + r.1.val ≤ 258) ⦄ := by
  rw [slot.a_back_best]
  step*