5G4CaN…NrdQaV

//! Two-pass parse priced by the encoder's own blocks.
//!
//! * First pass: cost-aware lazy matching refined by a block-wise optimal parse (a 4-byte
//!   hash chain, a single-entry 3-byte table, a backward dynamic program per 32 KB under
//!   costs learned from the previous block). Its tokens go to the output buffer.
//! * Those tokens are cut the way the encoder cuts them, 16384 per block; each block's
//!   symbol counts become that block's literal, length and distance costs.
//! * Second pass: every position is searched and keeps its two longest matches; a backward
//!   dynamic program over segments that end where a first-pass block ends finds the
//!   cheapest path under that block's costs, trying every length of both matches.
//! * The emission re-verifies every chosen match with `match_len` before writing it, so
//!   neither pass nor the costs are trusted.
//!
//! On corpus-stage1, gated two-pass parse: first pass of the 1.60× constants (SPAN1=28,
//! MISS_COST=150, TRY_ALL=56), then an adaptive-depth binary-tree second pass (48 probes
//! below 800 KB, else 32) on files that are neither incompressible nor long repeats.
//!
//! Tokens: `t < 256` literal, else `2^24 + (dist-1)*256 + (len-3)`.

pub const DEPTH: usize = 160;
pub const LDEPTH: usize = 80;
pub const MDEPTH: usize = 16;
pub const MISS_D: usize = 2;
pub const NICE: usize = 258;
pub const BLOCK: usize = 32768;
pub const NEAR3: usize = 32768;
pub const TRY_ALL: usize = 64;
pub const MISS_COST: u32 = 150;
pub const BIAS: u32 = 8;
pub const INNER_MAXL: usize = 64;
pub const LAZY_LIMIT: usize = 258;
pub const BK: usize = 128;
pub const LONG_BELOW: u32 = 44;
pub const SKIP_AFTER: usize = 256;
pub const SKIPN: usize = 1;
pub const RUN_D: usize = 16;
pub const RUN_L: usize = 64;
pub const RUN_KEEP: usize = 16;
pub const SPAN1: usize = 28;
pub const SPAN2: usize = 8;
pub const INNER_L: usize = 40;
pub const INNER_D: usize = 16;

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

/// How many bytes agree at `a < b` and `b`, up to `cap`, for the search: 0 unless
/// `b + cap` is within the input.
pub fn ext_len(input: &[u8], a: usize, b: usize, cap: usize) -> usize {
    let n = input.len();
    let mut l = 0usize;
    if a < b && b <= n && cap <= n - b {
        let mut go = 1usize;
        while go == 1 && l < cap && cap - l >= 8 {
            let x = load64(input, a + l) ^ load64(input, b + l);
            if x != 0 {
                l += (x.leading_zeros() / 8) as usize;
                go = 0;
            } else {
                l += 8;
            }
        }
        while go == 1 && l < cap && input[b + l] == input[a + l] {
            l += 1;
        }
    }
    l
}

/// `ext_len` when the first `l0` bytes are already known to agree: 0 unless
/// `b + cap` is within the input and `l0 <= cap`.
pub fn ext_from(input: &[u8], a: usize, b: usize, cap: usize, l0: usize) -> usize {
    let n = input.len();
    let mut l = 0usize;
    if a < b && b <= n && cap <= n - b && l0 <= cap {
        l = l0;
        let mut go = 1usize;
        while go == 1 && l < cap && cap - l >= 8 {
            let x = load64(input, a + l) ^ load64(input, b + l);
            if x != 0 {
                l += (x.leading_zeros() / 8) as usize;
                go = 0;
            } else {
                l += 8;
            }
        }
        while go == 1 && l < cap && input[b + l] == input[a + l] {
            l += 1;
        }
    }
    l
}

/// Eight bytes from `p`, the first one most significant. Needs `p + 8 <= input.len()`.
#[inline(always)]
pub fn load64(input: &[u8], p: usize) -> u64 {
    let n = input.len();
    if p < n && n - p >= 8 {
        let b7 = input[p + 7] as u64;
        let b6 = input[p + 6] as u64;
        let b5 = input[p + 5] as u64;
        let b4 = input[p + 4] as u64;
        let b3 = input[p + 3] as u64;
        let b2 = input[p + 2] as u64;
        let b1 = input[p + 1] as u64;
        let b0 = input[p] as u64;
        b7 + 256 * (b6 + 256 * (b5 + 256 * (b4 + 256 * (b3 + 256 * (b2 + 256 * (b1 + 256 * b0))))))
    } else {
        0
    }
}

/// `16 * log2(total / freq)`, rounded down to 1/16 bit; `MISS_COST` for an unseen symbol.
pub fn cost16(freq: u32, total: u32) -> u32 {
    if freq == 0 {
        return MISS_COST;
    }
    let t = total as u64;
    let mut f = freq as u64;
    let mut c = 0u32;
    let lzf = f.leading_zeros();
    let lzt = t.leading_zeros();
    if lzf > lzt {
        let s0 = lzf - lzt;
        let s = if f.wrapping_shl(s0) > t { s0 - 1 } else { s0 };
        f = f.wrapping_shl(s);
        c = 16 * s;
    }
    let mut k = 0usize;
    while k < 16 && f.wrapping_mul(1069) / 1024 <= t {
        f = f.wrapping_mul(1069) / 1024;
        c += 1;
        k += 1;
    }
    if c < 16 {
        16
    } else {
        c
    }
}

/// Distance code of `d` in 1..=32768.
pub fn dcode(dlo: &[u8; 256], dhi: &[u8; 256], d: usize) -> usize {
    if d <= 256 {
        let k = if d >= 1 { d - 1 } else { 0 };
        dlo[k % 256] as usize
    } else {
        dhi[((d - 1) / 128) % 256] as usize
    }
}

/// Bits saved by the match `(l, d)` at block index `i`: literal cost of the covered bytes
/// minus the match cost, or 0 when the match costs more.
pub fn gain(
    pref: &[u32; 65536],
    lenc: &[u32; 512],
    dcost: &[u32; 32],
    dlo: &[u8; 256],
    dhi: &[u8; 256],
    i: usize,
    l: usize,
    d: usize,
) -> u32 {
    let lit = pref[(i + l) % 65536].wrapping_sub(pref[i % 65536]);
    let mc = lenc[l % 512].saturating_add(dcost[dcode(dlo, dhi, d) % 32]);
    if lit > mc {
        lit - mc
    } else {
        0
    }
}

/// The match at `p` (block index `i`) saving the most bits among the near 3-byte candidate
/// `c3` and `pcap` entries of the chain from `start`, looking only at matches longer than
/// `floor`: `(len, dist, gain)`.
pub fn find(
    input: &[u8],
    prev: &[u32; 32768],
    pref: &[u32; 65536],
    lenc: &[u32; 512],
    dcost: &[u32; 32],
    dlo: &[u8; 256],
    dhi: &[u8; 256],
    p: usize,
    i: usize,
    cap: usize,
    start: usize,
    c3: usize,
    floor: usize,
    pcap: usize,
) -> (usize, usize, u32, usize, usize) {
    let mut bl = 0usize;
    let mut bd = 0usize;
    let mut bg = 0u32;
    let mut sl = 0usize;
    let mut sd = 0usize;
    let mut need = floor;
    let n = input.len();
    let ok = if p <= n && cap <= n - p { 1usize } else { 0usize };
    if ok == 1 && c3 > 0 && c3 <= p && p - (c3 - 1) <= NEAR3 && need < cap {
        let c = c3 - 1;
        if input[c + need] == input[p + need] {
            let l = ext_len(input, c, p, cap);
            if l >= 3 && l > need {
                let g = gain(pref, lenc, dcost, dlo, dhi, i, l, p - c);
                if g > 0 {
                    bl = l;
                    bd = p - c;
                    bg = g;
                    need = l;
                }
            }
        }
    }
    let mut cur = start;
    let mut probes = 0usize;
    while ok == 1 && probes < pcap && cur > 0 && cur <= p {
        let c = cur - 1;
        if p - c <= 32768 && need < cap {
            if input[c + need] == input[p + need] {
                let l = ext_len(input, c, p, cap);
                if l > need && l >= 3 {
                    let g = gain(pref, lenc, dcost, dlo, dhi, i, l, p - c);
                    sl = if g > bg { bl } else { l };
                    sd = if g > bg { bd } else { p - c };
                    if g > bg {
                        bl = l;
                    }
                    if g > bg {
                        bd = p - c;
                    }
                    if g > bg {
                        bg = g;
                    }
                    need = l;
                }
            }
            if need >= NICE {
                cur = 0;
            } else {
                cur = prev[c % 32768] as usize;
            }
        } else {
            cur = 0;
        }
        probes += 1;
    }
    (bl, bd, bg, sl, sd)
}

/// `find` with `INNER_D` chain entries, for the inner positions of a committed match.
pub fn find_in(
    input: &[u8],
    prev: &[u32; 32768],
    pref: &[u32; 65536],
    lenc: &[u32; 512],
    dcost: &[u32; 32],
    dlo: &[u8; 256],
    dhi: &[u8; 256],
    p: usize,
    i: usize,
    cap: usize,
    start: usize,
    c3: usize,
    floor: usize,
) -> (usize, usize, u32, usize, usize) {
    let mut bl = 0usize;
    let mut bd = 0usize;
    let mut bg = 0u32;
    let mut sl = 0usize;
    let mut sd = 0usize;
    let mut need = floor;
    let n = input.len();
    let ok = if p <= n && cap <= n - p { 1usize } else { 0usize };
    if ok == 1 && c3 > 0 && c3 <= p && p - (c3 - 1) <= NEAR3 && need < cap {
        let c = c3 - 1;
        if input[c + need] == input[p + need] {
            let l = ext_len(input, c, p, cap);
            if l >= 3 && l > need {
                let g = gain(pref, lenc, dcost, dlo, dhi, i, l, p - c);
                if g > 0 {
                    bl = l;
                    bd = p - c;
                    bg = g;
                    need = l;
                }
            }
        }
    }
    let mut cur = start;
    let mut probes = 0usize;
    while ok == 1 && probes < INNER_D && cur > 0 && cur <= p {
        let c = cur - 1;
        if p - c <= 32768 && need < cap {
            if input[c + need] == input[p + need] {
                let l = ext_len(input, c, p, cap);
                if l > need && l >= 3 {
                    let g = gain(pref, lenc, dcost, dlo, dhi, i, l, p - c);
                    sl = if g > bg { bl } else { l };
                    sd = if g > bg { bd } else { p - c };
                    if g > bg {
                        bl = l;
                    }
                    if g > bg {
                        bd = p - c;
                    }
                    if g > bg {
                        bg = g;
                    }
                    need = l;
                }
            }
            if need >= NICE {
                cur = 0;
            } else {
                cur = prev[c % 32768] as usize;
            }
        } else {
            cur = 0;
        }
        probes += 1;
    }
    (bl, bd, bg, sl, sd)
}

/// Enters position `p` into the tables; returns the previous heads `(chain start, near)`.
/// Needs `p + 4 <= input.len()`.
pub fn insert(
    input: &[u8],
    head4: &mut [u32; 65536],
    prev: &mut [u32; 32768],
    near: &mut [u32; 65536],
    p: usize,
) -> (usize, usize) {
    let x3 = (input[p] as u32)
        .wrapping_add((input[p + 1] as u32).wrapping_mul(256))
        .wrapping_add((input[p + 2] as u32).wrapping_mul(65536));
    let x4 = x3.wrapping_add((input[p + 3] as u32).wrapping_mul(16777216));
    let h = ((x4.wrapping_mul(2654435761) / 65536) % 65536) as usize;
    let start = head4[h] as usize;
    prev[p % 32768] = head4[h];
    head4[h] = (p + 1) as u32;
    let h3 = ((x3.wrapping_mul(2654435761) / 65536) % 65536) as usize;
    let c3 = near[h3] as usize;
    near[h3] = (p + 1) as u32;
    (start, c3)
}

/// Prefix sums of the literal costs over the block.
pub fn prefix(input: &[u8], litc: &[u32; 256], pref: &mut [u32; 65536], p0: usize, blen: usize) {
    let n = input.len();
    pref[0] = 0;
    let mut k = 0usize;
    let mut acc = 0u32;
    while k < blen && blen <= 32768 && p0 <= n && blen <= n - p0 {
        acc = acc.wrapping_add(litc[input[p0 + k] as usize]);
        pref[(k + 1) % 65536] = acc;
        k += 1;
    }
}

/// Commits the match `(l, d)` at block index `q` as the first candidate of its first
/// position and enters positions `q+2..q+l`; for a match of at most `INNER_MAXL` bytes each
/// of those is offered, as its second candidate, a near match that runs past the end.
pub fn commit(
    input: &[u8],
    head4: &mut [u32; 65536],
    prev: &mut [u32; 32768],
    near: &mut [u32; 65536],
    c1l: &mut [u16; 32768],
    c1d: &mut [u16; 32768],
    c2l: &mut [u16; 32768],
    c2d: &mut [u16; 32768],
    pref: &[u32; 65536],
    lenc: &[u32; 512],
    dcost: &[u32; 32],
    dlo: &[u8; 256],
    dhi: &[u8; 256],
    p0: usize,
    q: usize,
    l: usize,
    d: usize,
    blen: usize,
) {
    let n = input.len();
    let has4 = n >= 4;
    let lim4 = if has4 { n - 4 } else { 0 };
    c1l[q % 32768] = l as u16;
    c1d[q % 32768] = d as u16;
    let mut k = 1usize;
    while k < l && l <= 258 {
        let j = q + k;
        c1l[j % 32768] = 0;
        if k >= 2 {
            c2l[j % 32768] = 0;
            let p = p0 + j;
            let keep = if has4 && p <= lim4 && (d > RUN_D || l < RUN_L || k < RUN_KEEP || k + RUN_KEEP >= l) {
                1usize
            } else {
                0usize
            };
            if keep == 1 {
                let r = insert(input, head4, prev, near, p);
                if j < blen && l <= INNER_L {
                    let rem = l - k;
                    let rest = blen - j;
                    let cap = if rest < 258 { rest } else { 258 };
                    let f = find_in(input, prev, pref, lenc, dcost, dlo, dhi, p, j, cap, r.0, r.1, rem);
                    if f.0 >= 3 && f.0 > rem && f.0 <= 258 {
                        c2l[j % 32768] = f.0 as u16;
                        c2d[j % 32768] = f.1 as u16;
                        if f.3 >= 3 && f.3 > rem && f.3 <= 258 && f.4 != f.1 {
                            c1l[j % 32768] = f.3 as u16;
                            c1d[j % 32768] = f.4 as u16;
                        }
                    }
                } else if j < blen && l <= INNER_MAXL {
                    let c3 = r.1;
                    let rem = l - k;
                    let rest = blen - j;
                    let cap = if rest < 258 { rest } else { 258 };
                    if c3 > 0 && c3 <= p && p - (c3 - 1) <= NEAR3 && p - (c3 - 1) != d && rem < cap && cap <= n - p {
                        let c = c3 - 1;
                        if input[c + rem] == input[p + rem] {
                            let e = ext_len(input, c, p, cap);
                            if e > rem && e >= 3 {
                                c2l[j % 32768] = e as u16;
                                c2d[j % 32768] = (p - c) as u16;
                            }
                        }
                    }
                }
            }
        }
        k += 1;
    }
}

/// Extends the match `(l, d)` at `p = p0 + q` backward, offering each earlier position of
/// the block the longer match as its second candidate.
pub fn extend_back(
    input: &[u8],
    c2l: &mut [u16; 32768],
    c2d: &mut [u16; 32768],
    p0: usize,
    q: usize,
    l: usize,
    d: usize,
) {
    let n = input.len();
    let p = p0 + q;
    let mut j = 1usize;
    let mut go = 1usize;
    while go == 1 && j <= BK && j <= q && l + j <= 258 && p >= j + d && d >= 1 && p < n {
        if input[p - j] == input[p - j - d] {
            let k = q - j;
            let el = l + j;
            if el > c2l[k % 32768] as usize {
                c2l[k % 32768] = el as u16;
                c2d[k % 32768] = d as u16;
            }
            j += 1;
        } else {
            go = 0;
        }
    }
}

/// Takes up to `SKIPN` positions from block index `i` as literals, unsearched.
pub fn skip(c1l: &mut [u16; 32768], c2l: &mut [u16; 32768], i0: usize, blen: usize) -> usize {
    let mut i = i0;
    let mut s = 0usize;
    while s < SKIPN && i < blen {
        c1l[i % 32768] = 0;
        c2l[i % 32768] = 0;
        i += 1;
        s += 1;
    }
    i
}

/// Lazy pass over the block `[p0, p0 + blen)`: enters the positions into the tables and
/// leaves the candidates of the dynamic program in `c1*` (the chosen matches) and `c2*`
/// (backward extensions, the second-best match of each chosen one, the lazy step's loser).
pub fn lazy(
    input: &[u8],
    head4: &mut [u32; 65536],
    prev: &mut [u32; 32768],
    near: &mut [u32; 65536],
    pref: &[u32; 65536],
    lenc: &[u32; 512],
    dcost: &[u32; 32],
    dlo: &[u8; 256],
    dhi: &[u8; 256],
    c1l: &mut [u16; 32768],
    c1d: &mut [u16; 32768],
    c2l: &mut [u16; 32768],
    c2d: &mut [u16; 32768],
    p0: usize,
    blen: usize,
    long: usize,
) {
    let n = input.len();
    let has4 = n >= 4;
    let lim4 = if has4 { n - 4 } else { 0 };
    let mut pl = 0usize;
    let mut pd = 0usize;
    let mut pg = 0u32;
    let mut psl = 0usize;
    let mut psd = 0usize;
    let mut miss = 0usize;
    let mut i = 0usize;
    let mut steps = 0usize;
    while i < blen && steps < 32768 && blen <= 32768 && p0 <= n && blen <= n - p0 {
        let p = p0 + i;
        let rest = blen - i;
        let cap = if rest < 258 { rest } else { 258 };
        c1l[i % 32768] = 0;
        c2l[i % 32768] = 0;
        let mut cl = 0usize;
        let mut cd = 0usize;
        let mut cg = 0u32;
        let mut csl = 0usize;
        let mut csd = 0usize;
        if has4 && p <= lim4 {
            let r = insert(input, head4, prev, near, p);
            if pl < LAZY_LIMIT {
                let floor = if pl >= 3 { pl - 1 } else { 0 };
                let pcap = if pl >= 3 { LDEPTH } else if miss >= MISS_D { MDEPTH } else { DEPTH };
                let f = find(input, prev, pref, lenc, dcost, dlo, dhi, p, i, cap, r.0, r.1, floor, pcap);
                cl = f.0;
                cd = f.1;
                cg = f.2;
                csl = f.3;
                csd = f.4;
            }
        }
        if pl >= 3 && i >= 1 {
            if cl >= 3 && cg > pg {
                if pl <= 258 {
                    c2l[(i - 1) % 32768] = pl as u16;
                    c2d[(i - 1) % 32768] = pd as u16;
                }
                pl = cl;
                pd = cd;
                pg = cg;
                psl = csl;
                psd = csd;
                i += 1;
            } else {
                let q = i - 1;
                if cl >= 3 && cl <= 258 {
                    c2l[i % 32768] = cl as u16;
                    c2d[i % 32768] = cd as u16;
                }
                if psl >= 3 && psl <= 258 && psl < pl {
                    c2l[q % 32768] = psl as u16;
                    c2d[q % 32768] = psd as u16;
                }
                if pl <= 258 && pd >= 1 {
                    commit(input, head4, prev, near, c1l, c1d, c2l, c2d, pref, lenc, dcost, dlo, dhi, p0, q, pl, pd, blen);
                    extend_back(input, c2l, c2d, p0, q, pl, pd);
                }
                i = q + pl;
                pl = 0;
                pd = 0;
                pg = 0;
            }
        } else if cl >= 3 {
            pl = cl;
            pd = cd;
            pg = cg;
            psl = csl;
            psd = csd;
            miss = 0;
            i += 1;
        } else {
            i += 1;
            if miss < SKIP_AFTER {
                miss += 1;
            }
            if miss >= SKIP_AFTER && long == 0 {
                i = skip(c1l, c2l, i, blen);
            }
        }
        steps += 1;
    }
}

/// The cheapest way to cover `[j, j + l)` for `l` in `lo..=hi` at one distance cost:
/// every length below `tall`, then one per length code.
pub fn relax_run(
    cost: &[u32; 65536],
    lenc: &[u32; 512],
    bend: &[u16; 512],
    j: usize,
    lo: usize,
    hi: usize,
    dcs: u32,
    best0: u32,
    bl0: usize,
    tall: usize,
) -> (u32, usize) {
    let mut best = best0;
    let mut bl = bl0;
    let mut l = lo;
    while l <= hi && l < tall && hi <= 258 {
        let c = cost[(j + l) % 65536].wrapping_add(lenc[l % 512]).wrapping_add(dcs);
        if c < best {
            best = c;
            bl = l;
        }
        l += 1;
    }
    let mut steps = 0usize;
    while l <= hi && hi <= 258 && steps < 300 {
        let c = cost[(j + l) % 65536].wrapping_add(lenc[l % 512]).wrapping_add(dcs);
        if c < best {
            bl = l;
        }
        if c < best {
            best = c;
        }
        if l >= hi {
            l += 1;
        } else {
            let e = bend[l % 512] as usize;
            let nx = if e <= l { bend[(l + 1) % 512] as usize } else { e };
            l = if nx > hi { hi } else if nx <= l { l + 1 } else { nx };
        }
        steps += 1;
    }
    (best, bl)
}

/// Backward pass: `cost[j]` is the cheapest cost from `j` to the block end, `chl`/`chd` the choice.
pub fn backward(
    input: &[u8],
    c1l: &mut [u16; 32768],
    c1d: &mut [u16; 32768],
    c2l: &[u16; 32768],
    c2d: &[u16; 32768],
    cost: &mut [u32; 65536],
    litc: &[u32; 256],
    lenc: &[u32; 512],
    dcost: &[u32; 32],
    bend: &[u16; 512],
    dlo: &[u8; 256],
    dhi: &[u8; 256],
    p0: usize,
    blen: usize,
) {
    let n = input.len();
    if blen <= 32768 && p0 <= n && blen <= n - p0 {
        cost[blen % 65536] = 0;
        let mut cn = 0u32;
        let mut j = blen;
        while j > 0 {
            j -= 1;
            let lit = cn.wrapping_add(litc[input[p0 + j] as usize]);
            let l2 = c2l[j % 32768] as usize;
            let l1 = c1l[j % 32768] as usize;
            if l1 < 3 && l2 < 3 {
                cost[j % 65536] = lit;
                cn = lit;
                c1l[j % 32768] = 0;
            } else {
                let rest = blen - j;
                let mut best = 4294967295u32;
                let mut bl = 0usize;
                let mut bdd = 0usize;
                let d2 = c2d[j % 32768] as usize;
                if l2 >= 3 && l2 <= rest && d2 >= 1 && d2 <= 32768 {
                    let dcs = dcost[dcode(dlo, dhi, d2) % 32];
                    let from2 = if l2 > SPAN2 + 3 { l2 - SPAN2 } else { 3 };
                    let r = relax_run(cost, lenc, bend, j, from2, l2, dcs, best, bl, TRY_ALL);
                    if r.0 < best {
                        bdd = d2;
                    }
                    best = r.0;
                    bl = r.1;
                }
                let d1 = c1d[j % 32768] as usize;
                if l1 >= 3 && l1 <= rest && d1 >= 1 && d1 <= 32768 {
                    let dcs = dcost[dcode(dlo, dhi, d1) % 32];
                    let from = if l1 > SPAN1 + 3 { l1 - SPAN1 } else { 3 };
                    let r = relax_run(cost, lenc, bend, j, from, l1, dcs, best, bl, TRY_ALL);
                    if r.0 < best {
                        bdd = d1;
                    }
                    best = r.0;
                    bl = r.1;
                }
                if lit <= best {
                    best = lit;
                    bl = 0;
                    bdd = 0;
                }
                cost[j % 65536] = best;
                cn = best;
                c1l[j % 32768] = bl as u16;
                c1d[j % 32768] = bdd as u16;
            }
        }
    }
}

/// Symbol counts of the chosen path through the block.
pub fn count(
    input: &[u8],
    chl: &[u16; 32768],
    chd: &[u16; 32768],
    lf: &mut [u32; 512],
    df: &mut [u32; 32],
    lcode: &[u8; 512],
    dlo: &[u8; 256],
    dhi: &[u8; 256],
    olf: &[u32; 512],
    odf: &[u32; 32],
    half: usize,
    p0: usize,
    blen: usize,
) {
    let n = input.len();
    let mut s = 0usize;
    while s < 512 {
        lf[s] = if half == 1 { olf[s] / 2 } else { olf[s] };
        s += 1;
    }
    s = 0;
    while s < 32 {
        df[s] = if half == 1 { odf[s] / 2 } else { odf[s] };
        s += 1;
    }
    let mut k = 0usize;
    while k < blen && p0 <= n && blen <= n - p0 {
        let l = chl[k % 32768] as usize;
        let d = chd[k % 32768] as usize;
        if l >= 3 && l <= 258 && d >= 1 && d <= 32768 {
            let li = (257 + lcode[l % 512] as usize) % 512;
            lf[li] = lf[li].saturating_add(1);
            let di = dcode(dlo, dhi, d) % 32;
            df[di] = df[di].saturating_add(1);
            k += l;
        } else {
            let b = input[p0 + k] as usize;
            lf[b] = lf[b].saturating_add(1);
            k += 1;
        }
    }
    lf[256] = lf[256].saturating_add(1);
}

/// Copies the counts `lf`/`df` into `olf`/`odf`.
pub fn keep(lf: &[u32; 512], df: &[u32; 32], olf: &mut [u32; 512], odf: &mut [u32; 32]) {
    let mut s = 0usize;
    while s < 512 {
        olf[s] = lf[s];
        s += 1;
    }
    s = 0;
    while s < 32 {
        odf[s] = df[s];
        s += 1;
    }
}

/// Literal, length and distance costs from the symbol counts.
pub fn learn(
    lf: &[u32; 512],
    df: &[u32; 32],
    litc: &mut [u32; 256],
    lenc: &mut [u32; 512],
    dcost: &mut [u32; 32],
    lcode: &[u8; 512],
    lextra: &[u8; 512],
    dext: &[u8; 32],
    bias: u32,
) {
    let mut tot = 1u32;
    let mut s = 0usize;
    while s < 286 {
        tot = tot.saturating_add(lf[s]);
        s += 1;
    }
    s = 0;
    while s < 256 {
        litc[s] = cost16(lf[s], tot).saturating_add(bias);
        s += 1;
    }
    let mut cc = [0u32; 32];
    let mut c = 0usize;
    while c < 29 {
        cc[c] = cost16(lf[(257 + c) % 512], tot).saturating_add(bias);
        c += 1;
    }
    let mut l = 3usize;
    while l <= 258 {
        lenc[l] = cc[(lcode[l] as usize) % 32].saturating_add((lextra[l] as u32) * 16);
        l += 1;
    }
    let mut dt = 1u32;
    c = 0;
    while c < 30 {
        dt = dt.saturating_add(df[c]);
        c += 1;
    }
    c = 0;
    while c < 30 {
        dcost[c] = cost16(df[c], dt).saturating_add((dext[c] as u32) * 16);
        c += 1;
    }
}

/// True iff the match `(ch, d)` at `pos` is in range and its bytes agree.
pub fn verified(input: &[u8], pos: usize, d: usize, ch: usize, k: usize, blen: usize) -> bool {
    if ch < 3 || ch > 258 || d < 1 || d > 32768 || d > pos || k + ch > blen {
        return false;
    }
    let v = match_len(input, pos - d, pos, ch);
    v >= ch
}

/// Writes the chosen path of the block; a match is written only once `verified`.
pub fn emit(
    input: &[u8],
    out: &mut [u32],
    chl: &[u16; 32768],
    chd: &[u16; 32768],
    ntok0: usize,
    p0: usize,
    blen: usize,
) -> usize {
    let mut ntok = ntok0;
    let mut k = 0usize;
    while k < blen {
        let pos = p0 + k;
        let ch = chl[k % 32768] as usize;
        let d = chd[k % 32768] as usize;
        if verified(input, pos, d, ch, k, blen) {
            out[ntok] = 16777216u32 + ((d - 1) as u32) * 256 + ((ch - 3) as u32);
            ntok += 1;
            k += ch;
        } else {
            out[ntok] = input[pos] as u32;
            ntok += 1;
            k += 1;
        }
    }
    ntok
}

/// Length codes and their extra bits for lengths 3..=258.
pub fn len_tables(
    lbase: &[u16; 32],
    lext: &[u8; 32],
    lcode: &mut [u8; 512],
    lextra: &mut [u8; 512],
    bend: &mut [u16; 512],
) {
    let mut c = 0usize;
    let mut l = 3usize;
    while l <= 258 {
        if c < 28 && lbase[(c + 1) % 32] as usize <= l {
            c += 1;
        }
        lcode[l] = c as u8;
        lextra[l] = lext[c % 32];
        let top = lbase[(c + 1) % 32];
        bend[l] = if top >= 1 { top - 1 } else { 0 };
        l += 1;
    }
}

/// The code of distance `d`, continuing the scan from code `c0`.
pub fn code_from(dbase: &[u16; 32], d: usize, c0: usize) -> usize {
    let mut c = c0;
    while c < 29 && dbase[(c + 1) % 32] as usize <= d {
        c += 1;
    }
    c
}

/// Distance codes: `dlo` for distances 1..=256, `dhi` by `(d - 1) / 128` above.
pub fn dist_tables(dbase: &[u16; 32], dlo: &mut [u8; 256], dhi: &mut [u8; 256]) {
    let mut c = 0usize;
    let mut d = 1usize;
    while d <= 256 {
        c = code_from(dbase, d, c);
        dlo[(d - 1) % 256] = c as u8;
        d += 1;
    }
    let mut k = 0usize;
    c = 0;
    while k < 256 {
        c = code_from(dbase, k * 128 + 1, c);
        dhi[k] = c as u8;
        k += 1;
    }
}

/// Length and distance code tables.
pub fn tables(
    lcode: &mut [u8; 512],
    lextra: &mut [u8; 512],
    bend: &mut [u16; 512],
    dlo: &mut [u8; 256],
    dhi: &mut [u8; 256],
    dext: &mut [u8; 32],
) {
    let lbase: [u16; 32] = [
        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, 259, 259, 259,
    ];
    let lext: [u8; 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,
    ];
    let dbase: [u16; 32] = [
        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, 32769, 32769,
    ];
    let dx: [u8; 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,
    ];
    len_tables(&lbase, &lext, lcode, lextra, bend);
    dist_tables(&dbase, dlo, dhi);
    *dext = dx;
}

/// Starting costs: literals from a byte histogram of the first 32 KB, static match costs.
pub fn seed(
    input: &[u8],
    litc: &mut [u32; 256],
    lenc: &mut [u32; 512],
    dcost: &mut [u32; 32],
    lextra: &[u8; 512],
    dext: &[u8; 32],
) {
    let n = input.len();
    let lim = if n < 32768 { n } else { 32768 };
    let mut hist = [1u32; 256];
    let mut i = 0usize;
    while i < lim {
        let b = input[i] as usize;
        hist[b] = hist[b].saturating_add(1);
        i += 1;
    }
    let tot = (lim as u32).saturating_add(256);
    let mut s = 0usize;
    while s < 256 {
        litc[s] = cost16(hist[s], tot);
        s += 1;
    }
    let mut l = 3usize;
    while l <= 258 {
        lenc[l] = 112u32.saturating_add((lextra[l] as u32) * 16);
        l += 1;
    }
    let mut c = 0usize;
    while c < 30 {
        dcost[c] = 80u32.saturating_add((dext[c] as u32) * 16);
        c += 1;
    }
}

/// Adds the per-token cost `bias` to every literal and every length.
pub fn add_bias(litc: &mut [u32; 256], lenc: &mut [u32; 512], bias: u32) {
    let mut s = 0usize;
    while s < 256 {
        litc[s] = litc[s].saturating_add(bias);
        s += 1;
    }
    let mut l = 3usize;
    while l <= 258 {
        lenc[l] = lenc[l].saturating_add(bias);
        l += 1;
    }
}

/// 1 when the average literal cost over the first 32 KB is below `LONG_BELOW`, so only long
/// matches pay: no per-token bias and no skipping in literal runs.
pub fn avg_lit(input: &[u8], litc: &[u32; 256]) -> usize {
    let n = input.len();
    let lim = if n < 32768 { n } else { 32768 };
    let mut s = 0u64;
    let mut i = 0usize;
    while i < lim {
        s = s.wrapping_add(litc[input[i] as usize] as u64);
        i += 1;
    }
    if lim >= 8 && s < (LONG_BELOW as u64) * (lim as u64) {
        1
    } else {
        0
    }
}

/// First pass: the lazy-then-optimal block parse; every written match is re-verified.
pub fn first_pass(input: &[u8], out: &mut [u32]) -> usize {
    let n = input.len();
    let mut lcode = [0u8; 512];
    let mut lextra = [0u8; 512];
    let mut bend = [0u16; 512];
    let mut dlo = [0u8; 256];
    let mut dhi = [0u8; 256];
    let mut dext = [0u8; 32];
    tables(&mut lcode, &mut lextra, &mut bend, &mut dlo, &mut dhi, &mut dext);
    let mut litc = [0u32; 256];
    let mut lenc = [0u32; 512];
    let mut dcost = [0u32; 32];
    seed(input, &mut litc, &mut lenc, &mut dcost, &lextra, &dext);
    let long = avg_lit(input, &litc);
    let bias = if long == 1 { 0 } else { BIAS };
    add_bias(&mut litc, &mut lenc, bias);
    let mut head4 = [0u32; 65536];
    let mut prev = [0u32; 32768];
    let mut near = [0u32; 65536];
    let mut c1l = [0u16; 32768];
    let mut c1d = [0u16; 32768];
    let mut c2l = [0u16; 32768];
    let mut c2d = [0u16; 32768];
    let mut cost = [0u32; 65536];
    let mut lf = [0u32; 512];
    let mut df = [0u32; 32];
    let mut olf = [0u32; 512];
    let mut odf = [0u32; 32];
    let mut ntok = 0usize;
    let mut p0 = 0usize;
    while p0 < n {
        let rest = n - p0;
        let blen = if rest > BLOCK { BLOCK } else { rest };
        prefix(input, &litc, &mut cost, p0, blen);
        lazy(
            input, &mut head4, &mut prev, &mut near, &cost, &lenc, &dcost, &dlo, &dhi, &mut c1l, &mut c1d,
            &mut c2l, &mut c2d, p0, blen, long,
        );
        count(input, &c1l, &c1d, &mut lf, &mut df, &lcode, &dlo, &dhi, &olf, &odf, 0, p0, blen);
        learn(&lf, &df, &mut litc, &mut lenc, &mut dcost, &lcode, &lextra, &dext, 0);
        backward(
            input, &mut c1l, &mut c1d, &c2l, &c2d, &mut cost, &litc, &lenc, &dcost, &bend, &dlo,
            &dhi, p0, blen,
        );
        if blen < rest {
            count(input, &c1l, &c1d, &mut lf, &mut df, &lcode, &dlo, &dhi, &olf, &odf, 1, p0, blen);
            learn(&lf, &df, &mut litc, &mut lenc, &mut dcost, &lcode, &lextra, &dext, bias);
            keep(&lf, &df, &mut olf, &mut odf);
        }
        ntok = emit(input, out, &c1l, &c1d, ntok, p0, blen);
        p0 += blen;
    }
    ntok
}

/// Chain entries searched at every position of the second pass.
pub const DEPTH2: usize = 84;
pub const DEPTH2L: usize = 64;
pub const ADAPTN: usize = 200000;
/// Once the second-pass search holds a match this long, each chain step counts four.
pub const GOOD2: usize = 32;
/// The second-pass search stops at a match this long.
pub const NICE2: usize = 258;
/// The second pass tries every match length below this, then one per length code.
pub const TRY2: usize = 60;
/// For a longest match of at least `LONGM` bytes the second pass tries every length only
/// below `LTALL`.
pub const LONGM: usize = 64;
pub const LTALL: usize = 16;
/// Longest second-pass segment; a segment also ends where a first-pass block ends.
pub const SEG2: usize = 32768;
/// Per-token cost added in the second pass, in 1/16 bits.
pub const BIAS2: u32 = 0;
/// Tokens per block of the encoder: the unit the second pass prices by.
pub const BTOK: usize = 16384;
/// Most blocks priced separately; later tokens share the last table.
pub const MAXB: usize = 64;
/// Longest input whose second-pass candidates are kept for a repricing pass; a longer
/// input gets one second pass.
pub const KEEPN: usize = 2097152;
/// 1 for one more repricing of the stored candidates before the output is written.
pub const REPRICE: usize = 1;
/// Shortest input repriced.
pub const RP_MIN: usize = 0;
/// Inputs are repriced when the first pass writes between `RP_LO` and `RP_HI` tokens per
/// thousand bytes: denser inputs barely compress, sparser ones are long repeats.
pub const RP_LO: usize = 135;
pub const RP_HI: usize = 950;

/// Enters `p` as the root of its binary tree: returns `(old root, near)`. Needs
/// `p + 4 <= input.len()`.
pub fn root_bt(input: &[u8], head4: &mut [u32; 65536], near: &mut [u32; 65536], p: usize) -> (usize, usize) {
    let x3 = (input[p] as u32)
        .wrapping_add((input[p + 1] as u32).wrapping_mul(256))
        .wrapping_add((input[p + 2] as u32).wrapping_mul(65536));
    let x4 = x3.wrapping_add((input[p + 3] as u32).wrapping_mul(16777216));
    let h = ((x4.wrapping_mul(2654435761) / 65536) % 65536) as usize;
    let start = head4[h] as usize;
    head4[h] = (p + 1) as u32;
    let h3 = ((x3.wrapping_mul(2654435761) / 65536) % 65536) as usize;
    let c3 = near[h3] as usize;
    near[h3] = (p + 1) as u32;
    (start, c3)
}

/// The binary-tree search at `p` from the old root `start`, re-rooting the tree at `p`:
/// the two longest matches `(l1, d1, l2, d2)` among the near candidate `c3` and up to
/// `DEPTH2` tree nodes, each longer than the one before. Search only.
pub fn find_bt(
    input: &[u8],
    child: &mut [u32; 65536],
    p: usize,
    cap: usize,
    start: usize,
    c3: usize,
    hl: usize,
    hd: usize,
    depth: usize,
) -> (usize, usize, usize, usize) {
    let n = input.len();
    let mut l1 = 0usize;
    let mut d1 = 0usize;
    let mut l2 = 0usize;
    let mut d2 = 0usize;
    let ok = if p <= n && cap <= n - p { 1usize } else { 0usize };
    if ok == 1 && c3 > 0 && c3 <= p && p - (c3 - 1) <= NEAR3 && cap >= 3 {
        let c = c3 - 1;
        let l = if p - c == hd && hl > 1 && hl - 1 <= cap { ext_from(input, c, p, cap, hl - 1) } else { ext_len(input, c, p, cap) };
        if l >= 3 {
            l1 = l;
            d1 = p - c;
        }
    }
    let slot = (p % 32768).wrapping_mul(2);
    let mut plt = slot;
    let mut pgt = slot.wrapping_add(1);
    let mut llt = 0usize;
    let mut lgt = 0usize;
    let mut len = 0usize;
    let mut cur = start;
    let mut probes = 0usize;
    let mut open = 1usize;
    while ok == 1 && open == 1 && probes < depth && cur > 0 && cur <= p && p - (cur - 1) <= 32767 && len < cap {
        let c = cur - 1;
        if p - c == hd && hl > len + 1 && hl - 1 <= cap {
            len = ext_from(input, c, p, cap, hl - 1);
        } else if input[c + len] == input[p + len] {
            len = ext_from(input, c, p, cap, len + 1);
        }
        if len > l1 && len >= 3 {
            l2 = l1;
            d2 = d1;
            l1 = len;
            d1 = p - c;
        }
        let cs = (c % 32768) * 2;
        if len >= cap || len >= NICE2 {
            child[plt % 65536] = child[cs % 65536];
            child[pgt % 65536] = child[(cs + 1) % 65536];
            open = 0;
        } else if input[c + len] < input[p + len] {
            child[plt % 65536] = cur as u32;
            plt = cs + 1;
            cur = child[plt % 65536] as usize;
            llt = len;
        } else {
            child[pgt % 65536] = cur as u32;
            pgt = cs;
            cur = child[pgt % 65536] as usize;
            lgt = len;
        }
        len = if llt < lgt { llt } else { lgt };
        probes += 1;
    }
    if open == 1 {
        child[plt % 65536] = 0;
        child[pgt % 65536] = 0;
    }
    (l1, d1, l2, d2)
}

/// Second-pass candidates of every position of `[p0, p0 + blen)`: the longest match in `c1`,
/// the one before it in `c2`, cut at the segment end.
pub fn search2(
    input: &[u8],
    head4: &mut [u32; 65536],
    child: &mut [u32; 65536],
    near: &mut [u32; 65536],
    c1l: &mut [u16; 32768],
    c1d: &mut [u16; 32768],
    c2l: &mut [u16; 32768],
    c2d: &mut [u16; 32768],
    p0: usize,
    blen: usize,
) {
    let n = input.len();
    let has4 = n >= 4;
    let lim4 = if has4 { n - 4 } else { 0 };
    let mut i = 0usize;
    let mut run = 0usize;
    let mut rd = 0usize;
    while i < blen && blen <= 32768 && p0 <= n && blen <= n - p0 {
        let p = p0 + i;
        let rest = n - p;
        let cap = if rest < 258 { rest } else { 258 };
        let seg = blen - i;
        c1l[i % 32768] = 0;
        c2l[i % 32768] = 0;
        if has4 && p <= lim4 {
            let r = root_bt(input, head4, near, p);
            let depth = if n > ADAPTN { DEPTH2L } else { DEPTH2 };
            let f = find_bt(input, child, p, cap, r.0, r.1, run, rd, depth);
            run = f.0;
            rd = f.1;
            let a = if f.0 > seg { seg } else { f.0 };
            let b = if f.2 > seg { seg } else { f.2 };
            if a >= 3 && a <= 258 && f.1 <= 32768 {
                c1l[i % 32768] = a as u16;
                c1d[i % 32768] = f.1 as u16;
            }
            if b >= 3 && b < a && f.3 <= 32768 {
                c2l[i % 32768] = b as u16;
                c2d[i % 32768] = f.3 as u16;
            }
        }
        i += 1;
    }
}

/// Backward pass of the second pass: `c2` is tried at every length up to its own, `c1` at
/// every length above that. The choice is left in `c1l`/`c1d`.
pub fn backward2(
    input: &[u8],
    c1l: &mut [u16; 32768],
    c1d: &mut [u16; 32768],
    c2l: &[u16; 32768],
    c2d: &[u16; 32768],
    cost: &mut [u32; 65536],
    litc: &[u32; 256],
    lenc: &[u32; 512],
    dcost: &[u32; 32],
    bend: &[u16; 512],
    dlo: &[u8; 256],
    dhi: &[u8; 256],
    p0: usize,
    blen: usize,
) {
    let n = input.len();
    if blen <= 32768 && p0 <= n && blen <= n - p0 {
        cost[blen % 65536] = 0;
        let mut cn = 0u32;
        let mut j = blen;
        while j > 0 {
            j -= 1;
            let lit = cn.wrapping_add(litc[input[p0 + j] as usize]);
            let rest = blen - j;
            let l2r = c2l[j % 32768] as usize;
            let l1r = c1l[j % 32768] as usize;
            let l2 = if l2r > rest { rest } else { l2r };
            let l1 = if l1r > rest { rest } else { l1r };
            let mut best = lit;
            let mut bl = 0usize;
            let mut bdd = 0usize;
            let tall = if l1 >= LONGM { LTALL } else { TRY2 };
            let d2 = c2d[j % 32768] as usize;
            if l2 >= 3 && l2 <= rest && d2 >= 1 && d2 <= 32768 {
                let dcs = dcost[dcode(dlo, dhi, d2) % 32];
                let r = relax_run(cost, lenc, bend, j, 3, l2, dcs, best, bl, tall);
                if r.0 < best {
                    bdd = d2;
                }
                best = r.0;
                bl = r.1;
            }
            let d1 = c1d[j % 32768] as usize;
            if l1 >= 3 && l1 <= rest && d1 >= 1 && d1 <= 32768 {
                let dcs = dcost[dcode(dlo, dhi, d1) % 32];
                let from = if l2 >= 3 && l2 < l1 { l2 + 1 } else { 3 };
                let r = relax_run(cost, lenc, bend, j, from, l1, dcs, best, bl, tall);
                if r.0 < best {
                    bdd = d1;
                }
                best = r.0;
                bl = r.1;
            }
            if bl < 3 {
                bl = 0;
                bdd = 0;
            }
            cost[j % 65536] = best;
            cn = best;
            c1l[j % 32768] = bl as u16;
            c1d[j % 32768] = bdd as u16;
        }
    }
}


/// Clears `lf` and `df`.
pub fn clear_counts(lf: &mut [u32; 512], df: &mut [u32; 32]) {
    let mut s = 0usize;
    while s < 512 {
        lf[s] = 0;
        s += 1;
    }
    s = 0;
    while s < 32 {
        df[s] = 0;
        s += 1;
    }
}

/// Stores the costs learned from `lf`/`df` as the tables of block `b`.
pub fn store_block(
    lf: &mut [u32; 512],
    df: &[u32; 32],
    lcode: &[u8; 512],
    lextra: &[u8; 512],
    dext: &[u8; 32],
    blitc: &mut [u32; 16384],
    blenc: &mut [u32; 32768],
    bdcost: &mut [u32; 2048],
    b: usize,
) {
    let mut litc = [0u32; 256];
    let mut lenc = [0u32; 512];
    let mut dcost = [0u32; 32];
    lf[256] = lf[256].saturating_add(1);
    learn(lf, df, &mut litc, &mut lenc, &mut dcost, lcode, lextra, dext, BIAS2);
    let base = b % MAXB;
    let mut s = 0usize;
    while s < 256 {
        blitc[(base * 256 + s) % 16384] = litc[s];
        s += 1;
    }
    s = 0;
    while s < 512 {
        blenc[(base * 512 + s) % 32768] = lenc[s];
        s += 1;
    }
    s = 0;
    while s < 32 {
        bdcost[(base * 32 + s) % 2048] = dcost[s];
        s += 1;
    }
}

/// Encoder blocks of the first-pass tokens `out[..ntok]`: where each starts in the input
/// (`bstart`) and the costs its symbol counts give (`blitc`, `blenc`, `bdcost`). Returns
/// how many blocks. Search only: the tokens are not trusted here.
pub fn block_costs(
    out: &[u32],
    ntok: usize,
    lcode: &[u8; 512],
    lextra: &[u8; 512],
    dext: &[u8; 32],
    dlo: &[u8; 256],
    dhi: &[u8; 256],
    bstart: &mut [u32; 65],
    blitc: &mut [u32; 16384],
    blenc: &mut [u32; 32768],
    bdcost: &mut [u32; 2048],
) -> usize {
    let mut lf = [0u32; 512];
    let mut df = [0u32; 32];
    let mut nb = 0usize;
    let mut pos = 0usize;
    let mut k = 0usize;
    while k < ntok && k < out.len() {
        if k % BTOK == 0 && nb < MAXB {
            if nb > 0 {
                store_block(&mut lf, &df, lcode, lextra, dext, blitc, blenc, bdcost, nb - 1);
                clear_counts(&mut lf, &mut df);
            }
            bstart[nb % 65] = pos as u32;
            nb += 1;
        }
        let t = out[k];
        if t < 256 {
            lf[t as usize] = lf[t as usize].saturating_add(1);
            pos = pos.saturating_add(1);
        } else {
            let r = t.wrapping_sub(16777216);
            let l = (r % 256) as usize + 3;
            let d = (r / 256) as usize % 32768 + 1;
            let li = (257 + lcode[l % 512] as usize) % 512;
            lf[li] = lf[li].saturating_add(1);
            let di = dcode(dlo, dhi, d) % 32;
            df[di] = df[di].saturating_add(1);
            pos = pos.saturating_add(l);
        }
        k += 1;
    }
    if nb > 0 {
        store_block(&mut lf, &df, lcode, lextra, dext, blitc, blenc, bdcost, nb - 1);
    }
    nb
}

/// Copies the tables of block `b` into `litc`, `lenc` and `dcost`.
pub fn load_block(
    blitc: &[u32; 16384],
    blenc: &[u32; 32768],
    bdcost: &[u32; 2048],
    litc: &mut [u32; 256],
    lenc: &mut [u32; 512],
    dcost: &mut [u32; 32],
    b: usize,
) {
    let base = b % MAXB;
    let mut s = 0usize;
    while s < 256 {
        litc[s] = blitc[(base * 256 + s) % 16384];
        s += 1;
    }
    s = 0;
    while s < 512 {
        lenc[s] = blenc[(base * 512 + s) % 32768];
        s += 1;
    }
    s = 0;
    while s < 32 {
        dcost[s] = bdcost[(base * 32 + s) % 2048];
        s += 1;
    }
}

/// The block holding `p0` (searching on from `bi`) and the length of the segment starting
/// at `p0`: at most `SEG2`, the input end, and the start of the next block.
pub fn segment(bstart: &[u32; 65], nb: usize, p0: usize, n: usize, bi0: usize) -> (usize, usize) {
    let mut bi = bi0;
    while bi + 1 < nb && bi + 1 < 65 && (bstart[(bi + 1) % 65] as usize) <= p0 {
        bi += 1;
    }
    let rest = if p0 < n { n - p0 } else { 1 };
    let mut blen = if rest > SEG2 { SEG2 } else { rest };
    if bi + 1 < nb && bi + 1 < 65 {
        let e = bstart[(bi + 1) % 65] as usize;
        if e > p0 && e - p0 < blen {
            blen = e - p0;
        }
    }
    (blen, bi)
}

/// Stores the candidates of `[p0, p0 + blen)` for the repricing pass: `out` packs the
/// first candidate and the second one's length, `d2s` the second one's distance.
pub fn stash(
    c1l: &[u16; 32768],
    c1d: &[u16; 32768],
    c2l: &[u16; 32768],
    c2d: &[u16; 32768],
    out: &mut [u32],
    d2s: &mut [u16; 2097152],
    p0: usize,
    blen: usize,
) {
    let mut i = 0usize;
    while i < blen && blen <= 32768 && p0 <= out.len() && blen <= out.len() - p0 {
        let l1 = c1l[i % 32768] as u32;
        let d1 = c1d[i % 32768] as u32;
        let l2 = c2l[i % 32768] as u32;
        let d2 = c2d[i % 32768] as u32;
        let a = pack1(l1, d1);
        let b = pack2(l2, d2);
        out[p0 + i] = a.wrapping_add(16777216u32.wrapping_mul(b % 256));
        d2s[(p0 + i) % 2097152] = if b > 0 { d2.wrapping_sub(1) as u16 } else { 0 };
        i += 1;
    }
}

/// The first candidate for `stash`: bit 23 set, then the distance less one and the
/// length less three; 0 when there is none.
pub fn pack1(l1: u32, d1: u32) -> u32 {
    if l1 >= 3 && l1 <= 258 && d1 >= 1 && d1 <= 32768 {
        (l1 - 3).wrapping_add(256u32.wrapping_mul(d1 - 1)).wrapping_add(8388608)
    } else {
        0
    }
}

/// The second candidate's length for `stash`, less two; 0 when there is none.
pub fn pack2(l2: u32, d2: u32) -> u32 {
    if l2 >= 3 && l2 <= 258 && d2 >= 1 && d2 <= 32768 {
        l2 - 2
    } else {
        0
    }
}

/// The stored candidates of `[p0, p0 + blen)` back into `c1`/`c2`.
pub fn unstash(
    out: &[u32],
    d2s: &[u16; 2097152],
    c1l: &mut [u16; 32768],
    c1d: &mut [u16; 32768],
    c2l: &mut [u16; 32768],
    c2d: &mut [u16; 32768],
    p0: usize,
    blen: usize,
) {
    let mut i = 0usize;
    while i < blen && blen <= 32768 && p0 <= out.len() && blen <= out.len() - p0 {
        let a = out[p0 + i];
        let has1 = (a / 8388608) % 2;
        let l1 = if has1 == 1 { a % 256 + 3 } else { 0 };
        let d1 = (a / 256) % 32768 + 1;
        let b = a / 16777216;
        c1l[i % 32768] = l1 as u16;
        c1d[i % 32768] = d1 as u16;
        c2l[i % 32768] = if b > 0 { (b + 2) as u16 } else { 0 };
        c2d[i % 32768] = (d2s[(p0 + i) % 2097152] as u32 + 1) as u16;
        i += 1;
    }
}

/// Counts the chosen path of `[p0, p0 + blen)` into the encoder blocks it will fall in,
/// storing each finished block's costs; `st` is (tokens so far, blocks so far, position).
pub fn tally(
    input: &[u8],
    chl: &[u16; 32768],
    chd: &[u16; 32768],
    lcode: &[u8; 512],
    lextra: &[u8; 512],
    dext: &[u8; 32],
    dlo: &[u8; 256],
    dhi: &[u8; 256],
    lf: &mut [u32; 512],
    df: &mut [u32; 32],
    bstart: &mut [u32; 65],
    blitc: &mut [u32; 16384],
    blenc: &mut [u32; 32768],
    bdcost: &mut [u32; 2048],
    ntok0: usize,
    nb0: usize,
    pos0: usize,
    p0: usize,
    blen: usize,
) -> (usize, usize, usize) {
    let n = input.len();
    let mut ntok = ntok0;
    let mut nb = nb0;
    let mut pos = pos0;
    let mut k = 0usize;
    while k < blen && blen <= 32768 && p0 <= n && blen <= n - p0 {
        if ntok % BTOK == 0 && nb < MAXB {
            if nb > 0 {
                store_block(lf, df, lcode, lextra, dext, blitc, blenc, bdcost, nb - 1);
                clear_counts(lf, df);
            }
            bstart[nb % 65] = pos as u32;
            nb += 1;
        }
        let ch = chl[k % 32768] as usize;
        let d = chd[k % 32768] as usize;
        if ch >= 3 && ch <= 258 && d >= 1 && d <= 32768 && ch <= blen - k {
            let li = (257 + lcode[ch % 512] as usize) % 512;
            lf[li] = lf[li].saturating_add(1);
            let di = dcode(dlo, dhi, d) % 32;
            df[di] = df[di].saturating_add(1);
            k += ch;
            pos = pos.saturating_add(ch);
        } else {
            let b = input[p0 + k] as usize;
            lf[b] = lf[b].saturating_add(1);
            k += 1;
            pos = pos.saturating_add(1);
        }
        ntok = ntok.saturating_add(1);
    }
    (ntok, nb, pos)
}

/// The searching second pass: every position is searched, the cheapest path under the
/// costs of the first pass's blocks is counted into new block costs (`nbstart` ...), and
/// the candidates are stored in `out` and `d2s`. Returns how many new blocks.
pub fn search_pass(
    input: &[u8],
    out: &mut [u32],
    d2s: &mut [u16; 2097152],
    lcode: &[u8; 512],
    lextra: &[u8; 512],
    bend: &[u16; 512],
    dlo: &[u8; 256],
    dhi: &[u8; 256],
    dext: &[u8; 32],
    bstart: &[u32; 65],
    blitc: &[u32; 16384],
    blenc: &[u32; 32768],
    bdcost: &[u32; 2048],
    nb: usize,
    nbstart: &mut [u32; 65],
    nblitc: &mut [u32; 16384],
    nblenc: &mut [u32; 32768],
    nbdcost: &mut [u32; 2048],
) -> usize {
    let n = input.len();
    let mut head4 = [0u32; 65536];
    let mut prev = [0u32; 65536];
    let mut near = [0u32; 65536];
    let mut c1l = [0u16; 32768];
    let mut c1d = [0u16; 32768];
    let mut c2l = [0u16; 32768];
    let mut c2d = [0u16; 32768];
    let mut cost = [0u32; 65536];
    let mut litc = [0u32; 256];
    let mut lenc = [0u32; 512];
    let mut dcost = [0u32; 32];
    let mut lf = [0u32; 512];
    let mut df = [0u32; 32];
    let mut tk = 0usize;
    let mut tb = 0usize;
    let mut tp = 0usize;
    let mut p0 = 0usize;
    let mut bi = 0usize;
    while p0 < n {
        let sg = segment(bstart, nb, p0, n, bi);
        let blen = sg.0;
        bi = sg.1;
        load_block(blitc, blenc, bdcost, &mut litc, &mut lenc, &mut dcost, bi);
        search2(input, &mut head4, &mut prev, &mut near, &mut c1l, &mut c1d, &mut c2l, &mut c2d, p0, blen);
        stash(&c1l, &c1d, &c2l, &c2d, out, d2s, p0, blen);
        backward2(input, &mut c1l, &mut c1d, &c2l, &c2d, &mut cost, &litc, &lenc, &dcost, bend, dlo, dhi, p0, blen);
        let t = tally(input, &c1l, &c1d, lcode, lextra, dext, dlo, dhi, &mut lf, &mut df, nbstart, nblitc, nblenc, nbdcost, tk, tb, tp, p0, blen);
        tk = t.0;
        tb = t.1;
        tp = t.2;
        p0 += blen;
    }
    if tb > 0 {
        store_block(&mut lf, &df, lcode, lextra, dext, nblitc, nblenc, nbdcost, tb - 1);
    }
    tb
}

/// A repricing pass that writes nothing: the cheapest path of every segment from the stored
/// candidates, under the costs of the blocks of the pass before, counted into new block costs.
/// Returns how many new blocks.
pub fn reprice(
    input: &[u8],
    out: &[u32],
    d2s: &[u16; 2097152],
    lcode: &[u8; 512],
    lextra: &[u8; 512],
    bend: &[u16; 512],
    dlo: &[u8; 256],
    dhi: &[u8; 256],
    dext: &[u8; 32],
    bstart: &[u32; 65],
    blitc: &[u32; 16384],
    blenc: &[u32; 32768],
    bdcost: &[u32; 2048],
    nb: usize,
    nbstart: &mut [u32; 65],
    nblitc: &mut [u32; 16384],
    nblenc: &mut [u32; 32768],
    nbdcost: &mut [u32; 2048],
) -> usize {
    let n = input.len();
    let mut c1l = [0u16; 32768];
    let mut c1d = [0u16; 32768];
    let mut c2l = [0u16; 32768];
    let mut c2d = [0u16; 32768];
    let mut cost = [0u32; 65536];
    let mut litc = [0u32; 256];
    let mut lenc = [0u32; 512];
    let mut dcost = [0u32; 32];
    let mut lf = [0u32; 512];
    let mut df = [0u32; 32];
    let mut tk = 0usize;
    let mut tb = 0usize;
    let mut tp = 0usize;
    let mut p0 = 0usize;
    let mut bi = 0usize;
    while p0 < n {
        let sg = segment(bstart, nb, p0, n, bi);
        let blen = sg.0;
        bi = sg.1;
        load_block(blitc, blenc, bdcost, &mut litc, &mut lenc, &mut dcost, bi);
        unstash(out, d2s, &mut c1l, &mut c1d, &mut c2l, &mut c2d, p0, blen);
        backward2(input, &mut c1l, &mut c1d, &c2l, &c2d, &mut cost, &litc, &lenc, &dcost, bend, dlo, dhi, p0, blen);
        let t = tally(input, &c1l, &c1d, lcode, lextra, dext, dlo, dhi, &mut lf, &mut df, nbstart, nblitc, nblenc, nbdcost, tk, tb, tp, p0, blen);
        tk = t.0;
        tb = t.1;
        tp = t.2;
        p0 += blen;
    }
    if tb > 0 {
        store_block(&mut lf, &df, lcode, lextra, dext, nblitc, nblenc, nbdcost, tb - 1);
    }
    tb
}

/// The writing second pass from the stored candidates: the cheapest path of every segment
/// under the costs of its block; every written match is re-verified.
pub fn final_stored(
    input: &[u8],
    out: &mut [u32],
    d2s: &[u16; 2097152],
    bend: &[u16; 512],
    dlo: &[u8; 256],
    dhi: &[u8; 256],
    bstart: &[u32; 65],
    blitc: &[u32; 16384],
    blenc: &[u32; 32768],
    bdcost: &[u32; 2048],
    nb: usize,
) -> usize {
    let n = input.len();
    let mut c1l = [0u16; 32768];
    let mut c1d = [0u16; 32768];
    let mut c2l = [0u16; 32768];
    let mut c2d = [0u16; 32768];
    let mut cost = [0u32; 65536];
    let mut litc = [0u32; 256];
    let mut lenc = [0u32; 512];
    let mut dcost = [0u32; 32];
    let mut ntok = 0usize;
    let mut p0 = 0usize;
    let mut bi = 0usize;
    while p0 < n {
        let sg = segment(bstart, nb, p0, n, bi);
        let blen = sg.0;
        bi = sg.1;
        load_block(blitc, blenc, bdcost, &mut litc, &mut lenc, &mut dcost, bi);
        unstash(out, d2s, &mut c1l, &mut c1d, &mut c2l, &mut c2d, p0, blen);
        backward2(input, &mut c1l, &mut c1d, &c2l, &c2d, &mut cost, &litc, &lenc, &dcost, bend, dlo, dhi, p0, blen);
        ntok = emit(input, out, &c1l, &c1d, ntok, p0, blen);
        p0 += blen;
    }
    ntok
}

/// The writing second pass with a fresh search: the cheapest path of every segment under
/// the costs of its block; every written match is re-verified.
pub fn final_search(
    input: &[u8],
    out: &mut [u32],
    bend: &[u16; 512],
    dlo: &[u8; 256],
    dhi: &[u8; 256],
    bstart: &[u32; 65],
    blitc: &[u32; 16384],
    blenc: &[u32; 32768],
    bdcost: &[u32; 2048],
    nb: usize,
) -> usize {
    let n = input.len();
    let mut head4 = [0u32; 65536];
    let mut prev = [0u32; 65536];
    let mut near = [0u32; 65536];
    let mut c1l = [0u16; 32768];
    let mut c1d = [0u16; 32768];
    let mut c2l = [0u16; 32768];
    let mut c2d = [0u16; 32768];
    let mut cost = [0u32; 65536];
    let mut litc = [0u32; 256];
    let mut lenc = [0u32; 512];
    let mut dcost = [0u32; 32];
    let mut ntok = 0usize;
    let mut p0 = 0usize;
    let mut bi = 0usize;
    while p0 < n {
        let sg = segment(bstart, nb, p0, n, bi);
        let blen = sg.0;
        bi = sg.1;
        load_block(blitc, blenc, bdcost, &mut litc, &mut lenc, &mut dcost, bi);
        search2(input, &mut head4, &mut prev, &mut near, &mut c1l, &mut c1d, &mut c2l, &mut c2d, p0, blen);
        backward2(input, &mut c1l, &mut c1d, &c2l, &c2d, &mut cost, &litc, &lenc, &dcost, bend, dlo, dhi, p0, blen);
        ntok = emit(input, out, &c1l, &c1d, ntok, p0, blen);
        p0 += blen;
    }
    ntok
}

/// Inputs whose first-pass matches weigh more than `WMAX` per byte (see `weight`) are left
/// as the first pass wrote them: long repeats, where the second pass is slow.
pub const WMAX: usize = 18;
/// Inputs whose first pass writes more tokens than all but one in `DSKIP` of their bytes are
/// left as the first pass wrote them: they barely compress.
pub const DSKIP: usize = 24;

/// The first-pass tokens `out[..ntok]` weighed by what they cost the second pass: half of
/// `min(l, 48) * l` for each match of length `l`. Search only.
pub fn weight(out: &[u32], ntok: usize) -> usize {
    let mut w = 0usize;
    let mut k = 0usize;
    while k < ntok && k < out.len() {
        let t = out[k];
        if t >= 16777216 {
            let l = ((t - 16777216) % 256) as usize + 3;
            let m = if l > 48 { 48 } else { l };
            w = w.saturating_add(m * l / 2);
        }
        k += 1;
    }
    w
}

/// Two passes. The first (the lazy-then-optimal block parse) writes a token stream whose
/// encoder blocks give per-block costs; a searching second pass finds the cheapest path
/// under them and counts it into new block costs; a final pass reprices the stored
/// candidates under those and writes the output. Every written match is re-verified.
pub fn parse(input: &[u8], out: &mut [u32]) -> usize {
    let n1 = first_pass(input, out);
    let mut lcode = [0u8; 512];
    let mut lextra = [0u8; 512];
    let mut bend = [0u16; 512];
    let mut dlo = [0u8; 256];
    let mut dhi = [0u8; 256];
    let mut dext = [0u8; 32];
    tables(&mut lcode, &mut lextra, &mut bend, &mut dlo, &mut dhi, &mut dext);
    let mut bstart = [0u32; 65];
    let mut blitc = [0u32; 16384];
    let mut blenc = [0u32; 32768];
    let mut bdcost = [0u32; 2048];
    let nb = block_costs(out, n1, &lcode, &lextra, &dext, &dlo, &dhi, &mut bstart, &mut blitc, &mut blenc, &mut bdcost);
    let n = input.len();
    // Direct if (no bool let) — matches admitted 3x / Parse.lean; avoids Decidable heavy.
    if n1 > n || n - n1 < n / DSKIP || weight(out, n1) / WMAX > n {
        return n1;
    }
    let dense = if n <= KEEPN && n >= RP_MIN && n1 <= n {
        n1 * 1000 >= RP_LO * n && n1 * 1000 <= RP_HI * n
    } else {
        false
    };
    if dense && n <= out.len() {
        let mut d2s = [0u16; 2097152];
        let mut nbstart = [0u32; 65];
        let mut nblitc = [0u32; 16384];
        let mut nblenc = [0u32; 32768];
        let mut nbdcost = [0u32; 2048];
        let nb2 = search_pass(input, out, &mut d2s, &lcode, &lextra, &bend, &dlo, &dhi, &dext, &bstart, &blitc, &blenc, &bdcost, nb, &mut nbstart, &mut nblitc, &mut nblenc, &mut nbdcost);
        if REPRICE == 1 {
            let nb3 = reprice(input, out, &d2s, &lcode, &lextra, &bend, &dlo, &dhi, &dext, &nbstart, &nblitc, &nblenc, &nbdcost, nb2, &mut bstart, &mut blitc, &mut blenc, &mut bdcost);
            final_stored(input, out, &d2s, &bend, &dlo, &dhi, &bstart, &blitc, &blenc, &bdcost, nb3)
        } else {
            final_stored(input, out, &d2s, &bend, &dlo, &dhi, &nbstart, &nblitc, &nblenc, &nbdcost, nb2)
        }
    } else {
        final_search(input, out, &bend, &dlo, &dhi, &bstart, &blitc, &blenc, &bdcost, nb)
    }
}

import Lz77
import Slot

/-!
The two-pass parse. The first pass is the lazy-then-optimal block parse. The lazy pass, the candidate search, the cost model,
the backward dynamic program and the symbol counts are search: postcondition `True` (or a
bound), only termination and indices in range. The bounds the lazy pass carries are the
ones its callees rely on: a pending match fits in the block and its distance is in range.
The emission re-verifies every chosen match with `match_len`, so its invariant is the
template's: the tokens written so far decode to the input consumed so far.
-/

namespace Submission
open Aeneas Aeneas.Std Result ControlFlow

set_option maxRecDepth 8192
set_option maxHeartbeats 12000000

open LZ77 (toks bytes bytes_length bytes_getElem! toks_update bytes_congr Matches ite_ok)

/-! ## The match-length loop: the one load-bearing function -/

theorem match_len_loop_spec (input : Slice Std.U8) (a b cap l0 : Std.Usize)
    (ha : a.val + cap.val ≤ input.length) (hb : b.val + cap.val ≤ input.length)
    (hl0 : l0.val ≤ cap.val) (h0 : Matches input a.val b.val l0.val) :
    slot.match_len_loop input a b cap l0 ⦃ fun l =>
      l.val ≤ cap.val ∧ Matches input a.val b.val l.val ⦄ := by
  prove_match_len_loop

@[local step]
theorem match_len_spec (input : Slice Std.U8) (a b cap : Std.Usize)
    (ha : a.val + cap.val ≤ input.length) (hb : b.val + cap.val ≤ input.length) :
    slot.match_len input a b cap ⦃ fun l =>
      l.val ≤ cap.val ∧ Matches input a.val b.val l.val ⦄ := by
  prove_match_len

/-! ## The guarded match length of the search: a bound only -/

theorem lz64_le (x : Std.U64) : (core.num.U64.leading_zeros x).val ≤ 64 := by
  rw [core.num.U64.leading_zeros]
  simp only [UScalar.val, BitVec.leadingZeros]
  refine le_trans (Nat.mod_le _ _) ?_
  split <;> omega

theorem lz_div8_le (x : Std.U64) (i6 : Std.U32) (i7 : Std.Usize)
    (h6 : i6.val = (core.num.U64.leading_zeros x).val / 8)
    (h7 : i7 = UScalar.cast .Usize i6) : i7.val ≤ 8 := by
  have := lz64_le x
  subst h7
  simp only [U32.cast_Usize_val_eq]
  omega

@[local step]
theorem load64_spec (input : Slice Std.U8) (p : Std.Usize) :
    slot.load64 input p ⦃ fun _ => True ⦄ := by
  rw [slot.load64]
  have hmax : input.length ≤ Std.Usize.max := Std.Slice.length_ineq input
  simp only [lift]
  split
  · step*
  · simp

theorem ext_len_loop0_spec (input : Slice Std.U8) (a b cap l0 go0 : Std.Usize)
    (ha : a.val < b.val) (hb : b.val + cap.val ≤ input.length) (hl0 : l0.val ≤ cap.val) :
    slot.ext_len_loop0 input a b cap l0 go0 ⦃ fun r => r.1.val ≤ cap.val ⦄ := by
  rw [slot.ext_len_loop0]
  apply Std.loop.spec_decr_nat
    (measure := fun s => cap.val - s.1.val + s.2.val)
    (inv := fun s => s.1.val ≤ cap.val)
  · rintro ⟨l, go⟩ hle
    simp only at hle
    have hmax : input.length ≤ Std.Usize.max := Std.Slice.length_ineq input
    simp only [slot.ext_len_loop0.body]
    by_cases hg : go = 1#usize
    · rw [if_pos hg]
      by_cases hlc : l < cap
      · rw [if_pos hlc]
        step*
        all_goals first
          | scalar_tac
          | (have h7 := lz_div8_le x i6 i7 (by rw [i6_post, i5_post]) i7_post
             scalar_tac)
      · rw [if_neg hlc]
        simp
        exact hle
    · rw [if_neg hg]
      simp
      exact hle
  · exact hl0

theorem ext_len_loop1_spec (input : Slice Std.U8) (a b cap l0 go : Std.Usize)
    (ha : a.val < b.val) (hb : b.val + cap.val ≤ input.length) (hl0 : l0.val ≤ cap.val) :
    slot.ext_len_loop1 input a b cap l0 go ⦃ fun l => l.val ≤ cap.val ⦄ := by
  rw [slot.ext_len_loop1]
  apply Std.loop.spec_decr_nat
    (measure := fun l => cap.val - l.val)
    (inv := fun l => l.val ≤ cap.val)
  · intro l hle
    have hmax : input.length ≤ Std.Usize.max := Std.Slice.length_ineq input
    simp only [slot.ext_len_loop1.body]
    split
    · split
      · step*
      · exact hle
    · exact hle
  · exact hl0

@[local step]
theorem ext_len_spec (input : Slice Std.U8) (a b cap : Std.Usize) :
    slot.ext_len input a b cap ⦃ fun l => l.val ≤ cap.val ⦄ := by
  rw [slot.ext_len]
  have hmax : input.length ≤ Std.Usize.max := Std.Slice.length_ineq input
  split
  · split
    · step*
      apply Std.WP.spec_bind (ext_len_loop0_spec input a b cap 0#usize 1#usize
        (by scalar_tac) (by scalar_tac) (by simp))
      rintro ⟨l, go⟩ hl
      exact ext_len_loop1_spec input a b cap l go (by scalar_tac) (by scalar_tac) hl
    · simp
  · simp

theorem ext_from_loop0_spec (input : Slice Std.U8) (a b cap l0 go0 : Std.Usize)
    (ha : a.val < b.val) (hb : b.val + cap.val ≤ input.length) (hl0 : l0.val ≤ cap.val) :
    slot.ext_from_loop0 input a b cap l0 go0 ⦃ fun r => r.1.val ≤ cap.val ⦄ := by
  rw [slot.ext_from_loop0]
  apply Std.loop.spec_decr_nat
    (measure := fun s => cap.val - s.1.val + s.2.val)
    (inv := fun s => s.1.val ≤ cap.val)
  · rintro ⟨l, go⟩ hle
    simp only at hle
    have hmax : input.length ≤ Std.Usize.max := Std.Slice.length_ineq input
    simp only [slot.ext_from_loop0.body]
    by_cases hg : go = 1#usize
    · rw [if_pos hg]
      by_cases hlc : l < cap
      · rw [if_pos hlc]
        step*
        all_goals first
          | scalar_tac
          | (have h7 := lz_div8_le x i6 i7 (by rw [i6_post, i5_post]) i7_post
             scalar_tac)
      · rw [if_neg hlc]
        simp
        exact hle
    · rw [if_neg hg]
      simp
      exact hle
  · exact hl0

theorem ext_from_loop1_spec (input : Slice Std.U8) (a b cap l0 go : Std.Usize)
    (ha : a.val < b.val) (hb : b.val + cap.val ≤ input.length) (hl0 : l0.val ≤ cap.val) :
    slot.ext_from_loop1 input a b cap l0 go ⦃ fun l => l.val ≤ cap.val ⦄ := by
  rw [slot.ext_from_loop1]
  apply Std.loop.spec_decr_nat
    (measure := fun l => cap.val - l.val)
    (inv := fun l => l.val ≤ cap.val)
  · intro l hle
    have hmax : input.length ≤ Std.Usize.max := Std.Slice.length_ineq input
    simp only [slot.ext_from_loop1.body]
    split
    · split
      · step*
      · exact hle
    · exact hle
  · exact hl0

@[local step]
theorem ext_from_spec (input : Slice Std.U8) (a b cap l0 : Std.Usize) :
    slot.ext_from input a b cap l0 ⦃ fun l => l.val ≤ cap.val ⦄ := by
  rw [slot.ext_from]
  have hmax : input.length ≤ Std.Usize.max := Std.Slice.length_ineq input
  split
  · split
    · step*
      all_goals first
        | simp
        | (apply Std.WP.spec_bind (ext_from_loop0_spec input a b cap l0 1#usize
            (by scalar_tac) (by scalar_tac) (by scalar_tac))
           rintro ⟨l, go⟩ hl
           exact ext_from_loop1_spec input a b cap l go (by scalar_tac) (by scalar_tac) hl)
    · simp
  · simp

/-! ## Bit costs -/

theorem cost16_loop_spec (t f : Std.U64) (c : Std.U32) (k : Std.Usize)
    (hc : c.val ≤ 1024 + k.val) (hk : k.val ≤ 16) :
    slot.cost16_loop t f c k ⦃ fun _ => True ⦄ := by
  rw [slot.cost16_loop]
  apply Std.loop.spec_decr_nat
    (measure := fun s => 16 - s.2.2.val)
    (inv := fun s => s.2.1.val ≤ 1024 + s.2.2.val ∧ s.2.2.val ≤ 16)
  · rintro ⟨f1, c1, k1⟩ ⟨hc1, hk1⟩
    simp only at hc1 hk1
    simp only [slot.cost16_loop.body, lift]
    step*
  · exact ⟨hc, hk⟩

@[local step]
theorem cost16_spec (freq total : Std.U32) : slot.cost16 freq total ⦃ fun _ => True ⦄ := by
  rw [slot.cost16]
  split
  · step*
  · step*
    have hlz := lz64_le f
    rw [← lzf_post] at hlz
    apply Std.WP.spec_bind (Pₘ := fun (x : Std.U64 × Std.U32) => x.2.val ≤ 1024)
    · split
      · step*
        apply Std.WP.spec_bind (Pₘ := fun (s : Std.U32) => s.val ≤ s0.val)
        · split <;> step*
        · intro s hs
          step*
      · simp
    · rintro ⟨f1, c⟩ hc
      simp only at hc
      apply Std.WP.spec_bind (cost16_loop_spec _ f1 c 0#usize (by simp; omega) (by simp))
      intro c1 _
      split <;> step*

@[local step]
theorem dcode_spec (dlo dhi : Array Std.U8 256#usize) (d : Std.Usize) :
    slot.dcode dlo dhi d ⦃ fun _ => True ⦄ := by
  rw [slot.dcode]
  split
  · apply Std.WP.spec_bind (Pₘ := fun (_ : Std.Usize) => True)
    · split <;> step*
    · intro k _
      step*
  · step*


/-! ## Candidate search: search only, with the bounds the lazy pass carries -/

@[local step]
theorem gain_spec (pref : Array Std.U32 65536#usize) (lenc : Array Std.U32 512#usize)
    (dcost : Array Std.U32 32#usize) (dlo dhi : Array Std.U8 256#usize) (i l d : Std.Usize)
    (hil : i.val + l.val ≤ Std.Usize.max) :
    slot.gain pref lenc dcost dlo dhi i l d ⦃ fun _ => True ⦄ := by
  rw [slot.gain]
  simp only [lift]
  step*

theorem find_loop_spec (input : Slice Std.U8) (prev : Array Std.U32 32768#usize)
    (pref : Array Std.U32 65536#usize) (lenc : Array Std.U32 512#usize)
    (dcost : Array Std.U32 32#usize) (dlo dhi : Array Std.U8 256#usize)
    (p i cap pcap bl0 bd0 : Std.Usize) (bg0 : Std.U32) (sl0 sd0 need0 ok1 cur0 probes0 : Std.Usize)
    (hok : ok1 = 1#usize → p.val + cap.val ≤ input.length) (hip : i.val ≤ p.val)
    (hbl : bl0.val ≤ cap.val) (hbd : bd0.val ≤ 32768) :
    slot.find_loop input prev pref lenc dcost dlo dhi p i cap pcap bl0 bd0 bg0 sl0 sd0 need0
      ok1 cur0 probes0 ⦃ fun r => r.1.val ≤ cap.val ∧ r.2.1.val ≤ 32768 ⦄ := by
  rw [slot.find_loop]
  apply Std.loop.spec_decr_nat
    (measure := fun s => pcap.val - s.2.2.2.2.2.2.2.val)
    (inv := fun s => s.1.val ≤ cap.val ∧ s.2.1.val ≤ 32768)
  · rintro ⟨bl, bd, bg, sl, sd, need, cur, probes⟩ ⟨hb1, hb2⟩
    simp only at hb1 hb2
    have hmax : input.length ≤ Std.Usize.max := Std.Slice.length_ineq input
    simp only [slot.find_loop.body]
    by_cases hok1 : ok1 = 1#usize
    · rw [if_pos hok1]
      have hpc := hok hok1
      by_cases hpr : probes < pcap
      · rw [if_pos hpr]
        by_cases hc0 : cur > 0#usize
        · rw [if_pos hc0]
          by_cases hcp : cur ≤ p
          · rw [if_pos hcp]
            step*
            apply Std.WP.spec_bind
              (Pₘ := fun (x : Std.Usize × Std.Usize × Std.U32 × Std.Usize × Std.Usize ×
                Std.Usize × Std.Usize) => x.1.val ≤ cap.val ∧ x.2.1.val ≤ 32768)
            · split
              case isTrue hw =>
                split
                case isTrue hlt =>
                  step*
                  apply Std.WP.spec_bind
                    (Pₘ := fun (x : Std.Usize × Std.Usize × Std.U32 × Std.Usize × Std.Usize ×
                      Std.Usize) => x.1.val ≤ cap.val ∧ x.2.1.val ≤ 32768)
                  · split
                    case isTrue =>
                      step*
                      simp only [ite_ok]
                      step*
                      refine ⟨?_, ?_⟩ <;> split <;> scalar_tac
                    case isFalse => exact ⟨hb1, hb2⟩
                  · rintro ⟨b2, d2, g2, s2, e2, n2⟩ ⟨h1, h2⟩
                    simp only at h1 h2
                    step*
                    split <;> step*
                case isFalse => simp; exact ⟨hb1, hb2⟩
              case isFalse => simp; exact ⟨hb1, hb2⟩
            · rintro ⟨b1, d1, g1, s1, e1, n1, c1⟩ ⟨h1, h2⟩
              simp only at h1 h2
              step*
          · rw [if_neg hcp]; simp; exact ⟨hb1, hb2⟩
        · rw [if_neg hc0]; simp; exact ⟨hb1, hb2⟩
      · rw [if_neg hpr]; simp; exact ⟨hb1, hb2⟩
    · rw [if_neg hok1]; simp; exact ⟨hb1, hb2⟩
  · exact ⟨hbl, hbd⟩

@[local step]
theorem find_spec (input : Slice Std.U8) (prev : Array Std.U32 32768#usize)
    (pref : Array Std.U32 65536#usize) (lenc : Array Std.U32 512#usize)
    (dcost : Array Std.U32 32#usize) (dlo dhi : Array Std.U8 256#usize)
    (p i cap start c3 floor pcap : Std.Usize) (hip : i.val ≤ p.val) :
    slot.find input prev pref lenc dcost dlo dhi p i cap start c3 floor pcap
      ⦃ fun r => r.1.val ≤ cap.val ∧ r.2.1.val ≤ 32768 ⦄ := by
  rw [slot.find]
  have hmax : input.length ≤ Std.Usize.max := Std.Slice.length_ineq input
  apply Std.WP.spec_bind
    (Pₘ := fun (o : Std.Usize) => o = 1#usize → p.val + cap.val ≤ input.length)
  · split
    · step*
    · intro h; simp at h
  · intro ok1 hok
    apply Std.WP.spec_bind
      (Pₘ := fun (x : Std.Usize × Std.Usize × Std.U32 × Std.Usize) =>
        x.1.val ≤ cap.val ∧ x.2.1.val ≤ 32768)
    · split
      case isTrue hok1 =>
        have hpc := hok hok1
        split
        · split
          · step*
          · simp
        · simp
      case isFalse => simp
    · rintro ⟨bl, bd, bg, need⟩ ⟨h1, h2⟩
      exact find_loop_spec input prev pref lenc dcost dlo dhi p i cap pcap bl bd bg 0#usize
        0#usize need ok1 start 0#usize hok hip h1 h2

theorem find_in_loop_spec (input : Slice Std.U8) (prev : Array Std.U32 32768#usize)
    (pref : Array Std.U32 65536#usize) (lenc : Array Std.U32 512#usize)
    (dcost : Array Std.U32 32#usize) (dlo dhi : Array Std.U8 256#usize)
    (p i cap bl0 bd0 : Std.Usize) (bg0 : Std.U32) (sl0 sd0 need0 ok1 cur0 probes0 : Std.Usize)
    (hok : ok1 = 1#usize → p.val + cap.val ≤ input.length) (hip : i.val ≤ p.val)
    (hbl : bl0.val ≤ cap.val) (hbd : bd0.val ≤ 32768) :
    slot.find_in_loop input prev pref lenc dcost dlo dhi p i cap bl0 bd0 bg0 sl0 sd0 need0
      ok1 cur0 probes0 ⦃ fun r => r.1.val ≤ cap.val ∧ r.2.1.val ≤ 32768 ⦄ := by
  rw [slot.find_in_loop]
  apply Std.loop.spec_decr_nat
    (measure := fun s => slot.INNER_D.val - s.2.2.2.2.2.2.2.val)
    (inv := fun s => s.1.val ≤ cap.val ∧ s.2.1.val ≤ 32768)
  · rintro ⟨bl, bd, bg, sl, sd, need, cur, probes⟩ ⟨hb1, hb2⟩
    simp only at hb1 hb2
    have hmax : input.length ≤ Std.Usize.max := Std.Slice.length_ineq input
    simp only [slot.find_in_loop.body]
    by_cases hok1 : ok1 = 1#usize
    · rw [if_pos hok1]
      have hpc := hok hok1
      by_cases hpr : probes < slot.INNER_D
      · rw [if_pos hpr]
        by_cases hc0 : cur > 0#usize
        · rw [if_pos hc0]
          by_cases hcp : cur ≤ p
          · rw [if_pos hcp]
            step*
            apply Std.WP.spec_bind
              (Pₘ := fun (x : Std.Usize × Std.Usize × Std.U32 × Std.Usize × Std.Usize ×
                Std.Usize × Std.Usize) => x.1.val ≤ cap.val ∧ x.2.1.val ≤ 32768)
            · split
              case isTrue hw =>
                split
                case isTrue hlt =>
                  step*
                  apply Std.WP.spec_bind
                    (Pₘ := fun (x : Std.Usize × Std.Usize × Std.U32 × Std.Usize × Std.Usize ×
                      Std.Usize) => x.1.val ≤ cap.val ∧ x.2.1.val ≤ 32768)
                  · split
                    case isTrue =>
                      step*
                      simp only [ite_ok]
                      step*
                      refine ⟨?_, ?_⟩ <;> split <;> scalar_tac
                    case isFalse => exact ⟨hb1, hb2⟩
                  · rintro ⟨b2, d2, g2, s2, e2, n2⟩ ⟨h1, h2⟩
                    simp only at h1 h2
                    step*
                    split <;> step*
                case isFalse => simp; exact ⟨hb1, hb2⟩
              case isFalse => simp; exact ⟨hb1, hb2⟩
            · rintro ⟨b1, d1, g1, s1, e1, n1, c1⟩ ⟨h1, h2⟩
              simp only at h1 h2
              step*
          · rw [if_neg hcp]; simp; exact ⟨hb1, hb2⟩
        · rw [if_neg hc0]; simp; exact ⟨hb1, hb2⟩
      · rw [if_neg hpr]; simp; exact ⟨hb1, hb2⟩
    · rw [if_neg hok1]; simp; exact ⟨hb1, hb2⟩
  · exact ⟨hbl, hbd⟩

@[local step]
theorem find_in_spec (input : Slice Std.U8) (prev : Array Std.U32 32768#usize)
    (pref : Array Std.U32 65536#usize) (lenc : Array Std.U32 512#usize)
    (dcost : Array Std.U32 32#usize) (dlo dhi : Array Std.U8 256#usize)
    (p i cap start c3 floor : Std.Usize) (hip : i.val ≤ p.val) :
    slot.find_in input prev pref lenc dcost dlo dhi p i cap start c3 floor
      ⦃ fun r => r.1.val ≤ cap.val ∧ r.2.1.val ≤ 32768 ⦄ := by
  rw [slot.find_in]
  have hmax : input.length ≤ Std.Usize.max := Std.Slice.length_ineq input
  apply Std.WP.spec_bind
    (Pₘ := fun (o : Std.Usize) => o = 1#usize → p.val + cap.val ≤ input.length)
  · split
    · step*
    · intro h; simp at h
  · intro ok1 hok
    apply Std.WP.spec_bind
      (Pₘ := fun (x : Std.Usize × Std.Usize × Std.U32 × Std.Usize) =>
        x.1.val ≤ cap.val ∧ x.2.1.val ≤ 32768)
    · split
      case isTrue hok1 =>
        have hpc := hok hok1
        split
        · split
          · step*
          · simp
        · simp
      case isFalse => simp
    · rintro ⟨bl, bd, bg, need⟩ ⟨h1, h2⟩
      exact find_in_loop_spec input prev pref lenc dcost dlo dhi p i cap bl bd bg 0#usize
        0#usize need ok1 start 0#usize hok hip h1 h2

@[local step]
theorem insert_spec (input : Slice Std.U8) (head4 : Array Std.U32 65536#usize)
    (prev : Array Std.U32 32768#usize) (near : Array Std.U32 65536#usize) (p : Std.Usize)
    (hp : p.val + 4 ≤ input.length) :
    slot.insert input head4 prev near p ⦃ fun _ => True ⦄ := by
  rw [slot.insert]
  have hmax : input.length ≤ Std.Usize.max := Std.Slice.length_ineq input
  simp only [lift]
  step*

/-! ## Block bookkeeping of the lazy pass: search only -/

theorem prefix_loop_spec (input : Slice Std.U8) (litc : Array Std.U32 256#usize)
    (pref : Array Std.U32 65536#usize) (p0 blen n k : Std.Usize) (acc : Std.U32)
    (hn : n.val = input.length) :
    slot.prefix_loop input litc pref p0 blen n k acc ⦃ fun _ => True ⦄ := by
  rw [slot.prefix_loop]
  apply Std.loop.spec_decr_nat
    (measure := fun s => blen.val - s.2.1.val)
    (inv := fun _ => True)
  · rintro ⟨pf, kk, ac⟩ _
    have hmax : input.length ≤ Std.Usize.max := Std.Slice.length_ineq input
    simp only [slot.prefix_loop.body, lift]
    step*
  · trivial

@[local step]
theorem prefix_spec (input : Slice Std.U8) (litc : Array Std.U32 256#usize)
    (pref : Array Std.U32 65536#usize) (p0 blen : Std.Usize) :
    slot.«prefix» input litc pref p0 blen ⦃ fun _ => True ⦄ := by
  rw [slot.«prefix»]
  step*
  exact prefix_loop_spec input litc _ p0 blen _ 0#usize 0#u32 (by simp)

theorem commit_loop_spec (input : Slice Std.U8) (head4 : Array Std.U32 65536#usize)
    (prev : Array Std.U32 32768#usize) (near : Array Std.U32 65536#usize)
    (c1l c1d c2l c2d : Array Std.U16 32768#usize) (pref : Array Std.U32 65536#usize)
    (lenc : Array Std.U32 512#usize) (dcost : Array Std.U32 32#usize)
    (dlo dhi : Array Std.U8 256#usize) (p0 q l d blen n : Std.Usize) (has4 : Bool)
    (lim4 k : Std.Usize) (hn : n.val = input.length)
    (hq : p0.val + q.val + l.val ≤ input.length)
    (hlim : has4 = true → lim4.val + 4 ≤ input.length) :
    slot.commit_loop input head4 prev near c1l c1d c2l c2d pref lenc dcost dlo dhi p0 q l d
      blen n has4 lim4 k ⦃ fun _ => True ⦄ := by
  rw [slot.commit_loop]
  apply Std.loop.spec_decr_nat
    (measure := fun s => l.val - s.2.2.2.2.2.2.2.2.val)
    (inv := fun s => s.2.2.2.2.2.2.2.1 = true → lim4.val + 4 ≤ input.length)
  · rintro ⟨hd, pv, nr, a1, a2, a3, a4, h4, kk⟩ hinv
    simp only at hinv
    have hmax : input.length ≤ Std.Usize.max := Std.Slice.length_ineq input
    simp only [slot.commit_loop.body]
    by_cases hkl : kk < l
    · rw [if_pos hkl]
      by_cases hl : l ≤ 258#usize
      · rw [if_pos hl]
        step*
        apply Std.WP.spec_bind (Pₘ := fun (x : (Array Std.U32 65536#usize) ×
          (Array Std.U32 32768#usize) × (Array Std.U32 65536#usize) ×
          (Array Std.U16 32768#usize) × (Array Std.U16 32768#usize) ×
          (Array Std.U16 32768#usize) × (Array Std.U16 32768#usize) × Bool) =>
            x.2.2.2.2.2.2.2 = h4)
        · by_cases hk2 : kk ≥ 2#usize
          · rw [if_pos hk2]
            step*
            apply Std.WP.spec_bind (Pₘ := fun (kp : Std.Usize) =>
              kp = 1#usize → p.val + 4 ≤ input.length)
            · split
              · have h4l := hinv (by assumption)
                split
                · step*
                · simp
              · simp
            · intro keep hkp
              apply Std.WP.spec_bind (Pₘ := fun (_ : (Array Std.U32 65536#usize) ×
                (Array Std.U32 32768#usize) × (Array Std.U32 65536#usize) ×