mo-lazy

//! # The slot: LZ77 parsing -- a faithful reproduction of `miniz_oxide`'s own
//! level-9 strategy (`miniz_oxide::deflate::core`, as vendored at 0.8.9),
//! reimplemented in this repo's provable subset.
//!
//! This whole file is what a miner replaces. It must be compilable as its own
//! crate root (`charon rustc … src/parse.rs`), so it may not `use crate::…`.
//!
//! ## The contract
//!
//! `parse` reads `input` and writes a token stream into `out`, returning how many
//! tokens it wrote. A token is a `u32`:
//!
//! * `t < 256`                           — emit the literal byte `t`
//! * `t = 2^24 + (dist-1)*256 + (len-3)` — copy `len` bytes from `dist` back
//!
//! with `1 ≤ dist ≤ 32768` and `3 ≤ len ≤ 258`.
//!
//! ## What this reproduces, and why
//!
//! `miniz_oxide`'s reference bars (`mo1`, `mo9`) are the harness's own points
//! of comparison, but neither `template` (miniz_oxide level 1's shape: a
//! single hash-head candidate, greedy) nor `lazy` (lazy matching over hash
//! chains, but tuned far shallower than miniz_oxide ever runs) actually *is*
//! what miniz_oxide's better levels do. This is an attempt at the real thing,
//! ported line-for-line from `deflate/core.rs`'s `find_match` and its lazy
//! decision loop, level 9's parameters:
//!
//! * The exact hash: `(a << 10) ^ (b << 5) ^ c`, masked to 15 bits. Their
//!   code masks with `& 0x7FFF`; this uses `% 32768` instead, which is the
//!   same operation (32768 is a power of two) done in the form `omega` can
//!   reason about arithmetically rather than as a bitvector fact.
//! * The **split probe budget** real miniz_oxide uses and none of this
//!   repo's other examples do: up to 257 probes while the best match found
//!   so far is under 32 bytes, dropping to 65 once it reaches 32 -- spend
//!   less further effort once a match is already decent.
//! * Lazy matching (defer one byte, take the better of the two), *except*
//!   accept immediately without deferring when a match reaches 128 bytes --
//!   already excellent, not worth the lookahead.
//! * The "far and small" rule: a length-3 match at distance ≥ 8192 is
//!   discarded (falls back to a literal) -- not worth the distance code for
//!   that little payoff.
//!
//! What is *not* reproduced: `miniz_oxide`'s low-level match-length shortcut
//! (comparing two bytes at a time via a `u16`/`u64` read rather than one at a
//! time) and its RLE/filtered-match modes (level 9 default uses neither).
//! These are speed micro-optimizations and encoder strategy switches, not
//! part of *this* strategy, and the byte-at-a-time `match_len` below is the
//! same one every other example in this repo uses, so its cost is already
//! accounted for identically across candidates.
//!
//! ## Prover-friendly Rust — the rules
//!
//! Same four rules as every other slot in this repo: guarded subtraction,
//! `%`-bounded indices, no labelled control flow, a decreasing loop counter
//! independent of the data. `find_match` takes its probe budget as a
//! parameter (`probe_cap`) rather than a fixed constant, since miniz_oxide's
//! own budget varies call to call -- the loop still terminates on `probes`,
//! whatever `probe_cap` happens to be.

pub const MIN_MATCH: usize = 3;
pub const MAX_MATCH: usize = 258;
pub const WINDOW: usize = 32768;
pub const HASH_SIZE: usize = 32768;

/// `miniz_oxide`'s own split: many probes while the match is still short,
/// fewer once it is already long. Level 9's numbers (`NUM_PROBES[9] = 768`
/// fed through `probes_from_flags`).
pub const PROBES_SHORT: usize = 257;
pub const PROBES_LONG: usize = 65;
pub const LONG_THRESHOLD: usize = 32;
/// Accept a match immediately, without checking the next position, once it
/// reaches this length.
pub const IMMEDIATE_ACCEPT: usize = 128;
/// A length-3 match this far away or farther is not worth its distance code.
pub const FAR_DIST: usize = 8192;

/// `miniz_oxide`'s own hash: `(a << 10) ^ (b << 5) ^ c`, 15 bits. `% 32768`
/// here is the arithmetic form of their `& 0x7FFF`; same value either way.
pub fn hash3(a: u8, b: u8, c: u8) -> usize {
    let x = ((a as u32) << 10) ^ ((b as u32) << 5) ^ (c as u32);
    (x % 32768) as usize
}

/// How many bytes match at `a` and `b`, up to `cap`. This is the *only* function
/// whose result the correctness proof depends on.
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
}

/// Walk a hash chain and return the best `(length, distance)` it finds,
/// spending at most `probe_cap` probes.
pub fn find_match(
    input: &[u8],
    prev: &[u32],
    pos: usize,
    cap: usize,
    start: usize,
    probe_cap: usize,
) -> (usize, usize) {
    let mut best_len = 0usize;
    let mut best_dist = 0usize;
    let mut cur = start;
    let mut probes = 0usize;
    while probes < probe_cap && cur > 0 && cur <= pos && best_len < cap {
        let cpos = cur - 1;
        if pos - cpos <= 32768 {
            let l = match_len(input, cpos, pos, cap);
            if l > best_len {
                best_len = l;
                best_dist = pos - cpos;
            }
            cur = prev[cpos % 32768] as usize;
        } else {
            cur = 0;
        }
        probes += 1;
    }
    (best_len, best_dist)
}

/// The probe budget for a search that already knows about a match of length
/// `hint` (0 if none yet) -- `miniz_oxide`'s own dial: ease off once a match
/// is already decent.
pub fn probe_budget(hint: usize) -> usize {
    if hint >= LONG_THRESHOLD {
        PROBES_LONG
    } else {
        PROBES_SHORT
    }
}

/// Reject a match not worth its own encoding: a minimum-length match at a
/// large distance costs more in the distance code than the three literal
/// bytes it would otherwise be.
pub fn far_and_small(len: usize, dist: usize) -> bool {
    len == MIN_MATCH && dist >= FAR_DIST
}

/// Lazy matching over hash chains, `miniz_oxide` level 9's own dials.
pub fn parse(input: &[u8], out: &mut [u32]) -> usize {
    let n = input.len();
    let mut head = [0u32; 32768];
    let mut prev = [0u32; 32768];
    let mut ntok = 0usize;
    let mut pos = 0usize;
    let has3 = n >= 3;
    let lim = if has3 { n - 3 } else { 0 };
    let mut pend_len = 0usize;
    let mut pend_dist = 0usize;
    while pos < n {
        let mut cur_len = 0usize;
        let mut cur_dist = 0usize;
        if has3 && pos <= lim {
            let h = hash3(input[pos], input[pos + 1], input[pos + 2]);
            let start = head[h] as usize;
            prev[pos % 32768] = head[h];
            head[h] = (pos + 1) as u32;

            let mut cap = n - pos;
            if cap > 258 {
                cap = 258;
            }
            let budget = probe_budget(pend_len);
            let found = find_match(input, &prev, pos, cap, start, budget);
            cur_len = found.0;
            cur_dist = found.1;
            if cur_len < 3 || far_and_small(cur_len, cur_dist) {
                cur_len = 0;
                cur_dist = 0;
            }
        }

        if pend_len >= 3 {
            if cur_len > pend_len {
                // The lookahead beat the pending match: `pos - 1` is a
                // literal, and this new match either replaces it as pending
                // (still worth a further look) or, if already excellent, is
                // taken immediately.
                out[ntok] = input[pos - 1] as u32;
                ntok += 1;
                if cur_len >= IMMEDIATE_ACCEPT {
                    out[ntok] =
                        16777216u32 + ((cur_dist - 1) as u32) * 256 + ((cur_len - 3) as u32);
                    ntok += 1;
                    let end = pos + cur_len;
                    let mut k = pos + 1;
                    while k < end && has3 && k <= lim {
                        let h2 = hash3(input[k], input[k + 1], input[k + 2]);
                        prev[k % 32768] = head[h2];
                        head[h2] = (k + 1) as u32;
                        k += 1;
                    }
                    pos = end;
                    pend_len = 0;
                    pend_dist = 0;
                } else {
                    pend_len = cur_len;
                    pend_dist = cur_dist;
                    pos += 1;
                }
            } else {
                // The pending match still wins: emit it, insert the
                // positions it covers, continue after it.
                out[ntok] = 16777216u32 + ((pend_dist - 1) as u32) * 256 + ((pend_len - 3) as u32);
                ntok += 1;
                let end = pos - 1 + pend_len;
                let mut k = pos + 1;
                while k < end && has3 && k <= lim {
                    let h2 = hash3(input[k], input[k + 1], input[k + 2]);
                    prev[k % 32768] = head[h2];
                    head[h2] = (k + 1) as u32;
                    k += 1;
                }
                pos = end;
                pend_len = 0;
                pend_dist = 0;
            }
        } else if cur_len >= IMMEDIATE_ACCEPT {
            // No pending match, and this one is already excellent: take it
            // without spending a lookahead on it.
            out[ntok] = 16777216u32 + ((cur_dist - 1) as u32) * 256 + ((cur_len - 3) as u32);
            ntok += 1;
            let end = pos + cur_len;
            let mut k = pos + 1;
            while k < end && has3 && k <= lim {
                let h2 = hash3(input[k], input[k + 1], input[k + 2]);
                prev[k % 32768] = head[h2];
                head[h2] = (k + 1) as u32;
                k += 1;
            }
            pos = end;
        } else if cur_len >= 3 {
            pend_len = cur_len;
            pend_dist = cur_dist;
            pos += 1;
        } else {
            out[ntok] = input[pos] as u32;
            ntok += 1;
            pos += 1;
        }
    }
    // Provably unreachable (see Parse.lean): the loop above never leaves
    // `pos == n` with a pending match still unemitted, since the last
    // position that could start a match has `pos <= lim < n`.
    if pend_len >= 3 {
        out[ntok] = 16777216u32 + ((pend_dist - 1) as u32) * 256 + ((pend_len - 3) as u32);
        ntok += 1;
    }
    ntok
}

import Lz77
import Slot

/-!
Lazy matching over hash chains, `miniz_oxide` level 9's own dials: a split
probe budget, a `far_and_small` filter on freshly found matches, and an
immediate-accept shortcut once a match reaches `IMMEDIATE_ACCEPT`. The search
side (`find_match`) is the `lazy` proof's, generalized to a variable probe
budget. The emission side adds two new leaves beyond `lazy`'s three: taking a
match immediately (no pending) and taking a lookahead match immediately after
flushing the previously-pending byte as a literal (two tokens in one step).
-/

namespace Submission
open Aeneas Aeneas.Std Result ControlFlow

set_option maxRecDepth 8192
set_option maxHeartbeats 4000000

open LZ77 (toks bytes bytes_length bytes_getElem! toks_update bytes_congr
  Matches Found Pending emitted emitted_ge emitted_lt pending_of_found emit_lit emit_match)

/-! ## The hash: in range, and nothing else -/

@[local step]
theorem hash3_spec (a b c : Std.U8) :
    slot.hash3 a b c ⦃ fun h => h.val < 32768 ⦄ := by
  prove_hash3

/-! ## Two arithmetic helpers: only need to terminate, values are irrelevant -/

@[local step]
theorem probe_budget_spec (hint : Std.Usize) :
    slot.probe_budget hint ⦃ fun _ => True ⦄ := by
  rw [slot.probe_budget]
  split <;> simp

@[local step]
theorem far_and_small_spec (len dist : Std.Usize) :
    slot.far_and_small len dist ⦃ fun _ => True ⦄ := by
  rw [slot.far_and_small]
  split <;> simp

/-! ## 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 three hash-insert loops (one per emission site): terminate, prove nothing else -/

@[local step]
theorem parse_loop0_loop0_spec (input : Slice Std.U8)
    (head0 prev0 : Array Std.U32 32768#usize)
    (has30 : Bool) (lim «end» k0 : Std.Usize)
    (hlim : has30 = true → lim.val + 3 ≤ input.length) :
    slot.parse_loop0_loop0 input head0 prev0 has30 lim «end» k0
      ⦃ fun r => r.2.2 = true → lim.val + 3 ≤ input.length ⦄ := by
  rw [slot.parse_loop0_loop0]
  apply Std.loop.spec_decr_nat
    (measure := fun s => «end».val - s.2.2.2.val)
    (inv := fun s => s.2.2.1 = true → lim.val + 3 ≤ input.length)
  · rintro ⟨hd, pv, h3, k⟩ hinv
    have hmax : input.length ≤ Std.Usize.max := Std.Slice.length_ineq input
    simp only [slot.parse_loop0_loop0.body]
    step*
  · exact hlim

@[local step]
theorem parse_loop0_loop1_spec (input : Slice Std.U8)
    (head0 prev0 : Array Std.U32 32768#usize)
    (has30 : Bool) (lim «end» k0 : Std.Usize)
    (hlim : has30 = true → lim.val + 3 ≤ input.length) :
    slot.parse_loop0_loop1 input head0 prev0 has30 lim «end» k0
      ⦃ fun r => r.2.2 = true → lim.val + 3 ≤ input.length ⦄ := by
  rw [slot.parse_loop0_loop1]
  apply Std.loop.spec_decr_nat
    (measure := fun s => «end».val - s.2.2.2.val)
    (inv := fun s => s.2.2.1 = true → lim.val + 3 ≤ input.length)
  · rintro ⟨hd, pv, h3, k⟩ hinv
    have hmax : input.length ≤ Std.Usize.max := Std.Slice.length_ineq input
    simp only [slot.parse_loop0_loop1.body]
    step*
  · exact hlim

@[local step]
theorem parse_loop0_loop2_spec (input : Slice Std.U8)
    (head0 prev0 : Array Std.U32 32768#usize)
    (has30 : Bool) (lim «end» k0 : Std.Usize)
    (hlim : has30 = true → lim.val + 3 ≤ input.length) :
    slot.parse_loop0_loop2 input head0 prev0 has30 lim «end» k0
      ⦃ fun r => r.2.2 = true → lim.val + 3 ≤ input.length ⦄ := by
  rw [slot.parse_loop0_loop2]
  apply Std.loop.spec_decr_nat
    (measure := fun s => «end».val - s.2.2.2.val)
    (inv := fun s => s.2.2.1 = true → lim.val + 3 ≤ input.length)
  · rintro ⟨hd, pv, h3, k⟩ hinv
    have hmax : input.length ≤ Std.Usize.max := Std.Slice.length_ineq input
    simp only [slot.parse_loop0_loop2.body]
    step*
  · exact hlim

/-! ## The search: `Found` is the postcondition and the invariant; `cur` is never mentioned.
    Unlike `lazy`, the probe budget is a parameter, not a fixed constant, and there is no
    "nice length" early cutoff, so the loop body is a straight line once the chain step
    is reached -- simpler than `lazy`'s, not harder. -/

theorem find_match_loop_spec (input : Slice Std.U8) (prev : Slice Std.U32)
    (n pos cap probe_cap bl0 bd0 cur0 probes0 : Std.Usize)
    (hn : n.val = input.length) (hprev : prev.length = 32768)
    (hcap : pos.val + cap.val ≤ n.val) (hcap258 : cap.val ≤ 258)
    (h0 : Found input n pos bl0 bd0) :
    slot.find_match_loop input prev pos cap probe_cap bl0 bd0 cur0 probes0
      ⦃ fun r => Found input n pos r.1 r.2 ⦄ := by
  rw [slot.find_match_loop]
  apply Std.loop.spec_decr_nat
    (measure := fun s => probe_cap.val - s.2.2.2.val)
    (inv := fun s => Found input n pos s.1 s.2.1)
  · rintro ⟨bl, bd, cur, probes⟩ hinv
    simp only at hinv
    have hmax : input.length ≤ Std.Usize.max := Std.Slice.length_ineq input
    simp only [slot.find_match_loop.body]
    step*
    apply Std.WP.spec_bind (Pₘ := fun r => Found input n pos r.1 r.2.1)
    · split
      case isTrue hw =>
        step*
        rw [show ((if l > bl then ok (l, i) else ok (bl, bd))
              : Result (Std.Usize × Std.Usize))
            = ok (if l > bl then (l, i) else (bl, bd)) from by split <;> rfl]
        step*
        split
        case isTrue hbetter =>
          step*
          rcases Nat.lt_or_ge l.val 3 with h | h
          · exact Or.inl h
          · exact Or.inr ⟨h, by scalar_tac, by scalar_tac, by scalar_tac,
              by scalar_tac, by scalar_tac,
              by rw [show pos.val - i.val = cpos.val by scalar_tac]; exact l_post2⟩
        case isFalse =>
          step*
      case isFalse => exact hinv
    · rintro ⟨bl1, bd1, cur1⟩ hf
      step*
  · exact h0

@[local step]
theorem find_match_spec (input : Slice Std.U8) (prev : Slice Std.U32)
    (n pos cap start probe_cap : Std.Usize)
    (hn : n.val = input.length) (hprev : prev.length = 32768)
    (hcap : pos.val + cap.val ≤ n.val) (hcap258 : cap.val ≤ 258) :
    slot.find_match input prev pos cap start probe_cap
      ⦃ fun r => Found input n pos r.1 r.2 ⦄ :=
  find_match_loop_spec input prev n pos cap probe_cap 0#usize 0#usize start 0#usize
    hn hprev hcap hcap258 (Or.inl (by scalar_tac))

/-! ## The parse loop: tokens so far decode to `emitted`, and a pending match is `Pending` -/

theorem parse_loop0_spec (input : Slice Std.U8) (out0 : Slice Std.U32)
    (n lim : Std.Usize) (head0 prev0 : Array Std.U32 32768#usize)
    (ntok0 pos0 pl0 pd0 : Std.Usize) (has30 : Bool)
    (hn : n.val = input.length)
    (hout : input.length ≤ out0.length)
    (hlim : has30 = true → lim.val + 3 ≤ input.length)
    (hpos : pos0.val ≤ n.val) (hntok : ntok0.val ≤ emitted pos0.val pl0.val)
    (hpend : Pending input n pos0 pl0 pd0)
    (hdec : LZ77.decode (toks out0 ntok0.val) =
      some ((bytes input).take (emitted pos0.val pl0.val))) :
    slot.parse_loop0 input out0 n head0 prev0 ntok0 pos0 has30 lim pl0 pd0 ⦃ fun r =>
      r.2.2.1.val < 3 ∧ r.2.1.val ≤ input.length ∧ r.1.length = out0.length ∧
      LZ77.decode (toks r.1 r.2.1.val) = some (bytes input) ⦄ := by
  rw [slot.parse_loop0]
  apply Std.loop.spec_decr_nat
    (measure := fun s => n.val - s.2.2.2.2.1.val)
    (inv := fun s =>
      s.2.2.2.2.1.val ≤ n.val ∧
      s.2.2.2.1.val ≤ emitted s.2.2.2.2.1.val s.2.2.2.2.2.2.1.val ∧
      s.1.length = out0.length ∧
      (s.2.2.2.2.2.1 = true → lim.val + 3 ≤ input.length) ∧
      Pending input n s.2.2.2.2.1 s.2.2.2.2.2.2.1 s.2.2.2.2.2.2.2 ∧
      LZ77.decode (toks s.1 s.2.2.2.1.val) =
        some ((bytes input).take (emitted s.2.2.2.2.1.val s.2.2.2.2.2.2.1.val)))
  · rintro ⟨out, hd, pv, ntok, pos, h3, pl, pd⟩ ⟨hp, hnt, hlen, hh3, hpd, hde⟩
    simp only at hp hnt hlen hh3 hpd hde
    have hmax : input.length ≤ Std.Usize.max := Std.Slice.length_ineq input
    have hmaxout : out.length ≤ Std.Usize.max := Std.Slice.length_ineq out
    simp only [slot.parse_loop0.body]
    split
    case isTrue hposlt =>
      apply Std.WP.spec_bind (Pₘ := fun (r : (Array Std.U32 32768#usize) ×
          (Array Std.U32 32768#usize) × Std.Usize × Std.Usize) =>
        Found input n pos r.2.2.1 r.2.2.2)
      · split
        case isTrue hb3 =>
          split
          case isTrue hpl =>
            have hlim3 : lim.val + 3 ≤ input.length := hh3 hb3
            have hposl : pos.val ≤ lim.val := by scalar_tac
            step*
            rw [show ((if cap > 258#usize then ok 258#usize else ok cap)
                  : Result Std.Usize)
                = ok (if cap > 258#usize then 258#usize else cap) from by
                  split <;> rfl]
            step*
            case hcap => split <;> scalar_tac
            case hcap258 => split <;> scalar_tac
            split
            case isTrue hlt3 => exact Or.inl (by scalar_tac)
            case isFalse hge3 =>
              step*
              split
              case isTrue hfar => exact Or.inl (by scalar_tac)
              case isFalse hnfar => exact cur_len1_post
          case isFalse => exact Or.inl (by scalar_tac)
        case isFalse => exact Or.inl (by scalar_tac)
      · rintro ⟨head1, prev1, cur_len, cur_dist⟩ hfound
        replace hfound : Found input n pos cur_len cur_dist := hfound
        have hlim3 : h3 = true → lim.val + 3 ≤ input.length := hh3
        have hntok_lt : ntok.val < out.length := by
          have : emitted pos.val pl.val ≤ pos.val := by unfold emitted; split <;> omega
          scalar_tac
        step*
        -- `step*` leaves behind a handful of side goals it can't close on its
        -- own: array-bound (`hbound`) and arithmetic-overflow (`hmax`) checks
        -- for the *second* write in case A specifically, whose margin needs
        -- `pl ≥ 3` (⟹ `ntok ≤ pos - 1`, one more byte than `hntok_lt` gives
        -- generically) or a fact hidden inside `Found`/`Pending`. Try every
        -- combination rather than name the exact tag, since which check is
        -- outstanding (if any) depends on which of the six branches produced
        -- the goal.
        all_goals first
          | scalar_tac
          | (rcases hfound with h | ⟨_, _, _, _, _, _, _⟩ <;> scalar_tac)
          | (rcases hpd with h | ⟨_, _, _, _, _, _, _, _⟩ <;> scalar_tac)
          | (rcases hfound with h | ⟨_, _, _, _, _, _, _⟩ <;>
             rcases hpd with h2 | ⟨_, _, _, _, _, _, _, _⟩ <;> scalar_tac)
          | (rw [emitted_ge (by scalar_tac : (3 : Nat) ≤ pl.val)] at hnt; scalar_tac)
          | (rcases hfound with h | ⟨_, _, _, _, _, _, _⟩ <;>
             rw [emitted_ge (by scalar_tac : (3 : Nat) ≤ pl.val)] at hnt <;> scalar_tac)
          | (rw [__post2]
             have hlen_eq : (out.set ntok i2).length = out.length := by
               simp [Std.Slice.set_val_eq]
             rw [hlen_eq, ntok1_post]
             rw [emitted_ge (by scalar_tac : (3 : Nat) ≤ pl.val)] at hnt
             scalar_tac)
          | skip
        all_goals first
        | ( -- B: beaten pending, defer
            rcases hpd with h | ⟨hpos1, hl3, hlmax, hend, hd1, hdmax, hdpos, hmatch⟩
            · exfalso; scalar_tac
            rw [emitted_ge hl3] at hnt hde
            have hcur3 : 3 ≤ cur_len.val := by scalar_tac
            have hposlen : pos.val - 1 < input.length := by scalar_tac
            have hi : i.val = pos.val - 1 := by scalar_tac
            have hval : i2.val = (bytes input)[pos.val - 1]! := by
              rw [bytes_getElem! input (pos.val - 1) hposlen, i2_post, Std.U8.cast_U32_val_eq, i1_post]
              simp only [hi]
            refine ⟨by scalar_tac, ?_, by rw [__post2]; simpa [Std.Slice.set_val_eq] using hlen,
              hlim3, pending_of_found input n pos _ cur_len cur_dist (by scalar_tac) hfound,
              ?_, by scalar_tac⟩
            · rw [emitted_ge hcur3]; scalar_tac
            · rw [emitted_ge hcur3, __post2, show ntok1.val = ntok.val + 1 by scalar_tac,
                toks_update out ntok i2 hntok_lt, hval,
                show pos1.val - 1 = (pos.val - 1) + 1 by scalar_tac]
              exact LZ77.valid_lit (bytes input) (toks out ntok.val) (pos.val - 1) hde
                (by rw [bytes_length]; scalar_tac) (by rw [← hval]; scalar_tac) )
        | ( -- D: no pending, immediate accept
            have hpl3 : pl.val < 3 := by scalar_tac
            rw [emitted_lt hpl3] at hnt hde
            rcases hfound with hfl | ⟨hfl3, hflmax, hfend, hfd1, hfdmax, hfdpos, hfmatch⟩
            · exfalso; scalar_tac
            have htok : i6.val = LZ77.mkMatch cur_dist.val cur_len.val := by
              simp only [LZ77.mkMatch, LZ77.MATCH_BASE, i6_post, i3_post, i2_post,
                i5_post, i1_post, i4_post1, i_post1, Std.UScalar.cast_val_eq]
              scalar_tac
            refine ⟨by scalar_tac, ?_, by rw [s_post]; simpa [Std.Slice.set_val_eq] using hlen,
              head2_post, Or.inl hpl3, ?_, by scalar_tac⟩
            · rw [emitted_lt hpl3]; scalar_tac
            · rw [emitted_lt hpl3, s_post, show ntok1.val = ntok.val + 1 by scalar_tac,
                toks_update out ntok i6 hntok_lt, htok, show «end».val = pos.val + cur_len.val by scalar_tac]
              refine LZ77.valid_match (bytes input) (toks out ntok.val) pos.val
                cur_dist.val cur_len.val hde hfd1 hfdpos
                (by simpa [LZ77.MAX_DIST] using hfdmax) hfl3
                (by simpa [LZ77.MAX_LEN] using hflmax) (by rw [bytes_length]; scalar_tac) ?_
              intro k hk
              exact (bytes_congr input _ _ (by scalar_tac) (by scalar_tac) (hfmatch k hk)).symm )
        | ( -- E: no pending, defer
            rcases hpd with h | ⟨hpos1, hl3, _⟩
            · rw [emitted_lt h] at hnt hde
              have hcur3 : 3 ≤ cur_len.val := by scalar_tac
              refine ⟨by scalar_tac, ?_, hlen, hlim3,
                pending_of_found input n pos _ cur_len cur_dist (by scalar_tac) hfound,
                ?_, by scalar_tac⟩
              · rw [emitted_ge hcur3]; scalar_tac
              · rw [emitted_ge hcur3]; convert hde using 3; scalar_tac
            · exfalso; scalar_tac )
        | ( -- F: plain literal
            rcases hpd with h | ⟨hpos1, hl3, _⟩
            · rw [emitted_lt h] at hnt hde
              have hposlen : pos.val < input.length := by scalar_tac
              have hval : i1.val = (bytes input)[pos.val]! := by
                rw [bytes_getElem! input pos.val hposlen, i1_post,
                  Std.U8.cast_U32_val_eq, i_post]
              refine ⟨by scalar_tac, ?_, by rw [s_post]; simpa [Std.Slice.set_val_eq] using hlen,
                hlim3, Or.inl h, ?_, by scalar_tac⟩
              · rw [emitted_lt h]; scalar_tac
              · rw [emitted_lt h, s_post, show ntok1.val = ntok.val + 1 by scalar_tac,
                  toks_update out ntok i1 hntok_lt, hval,
                  show pos1.val = pos.val + 1 by scalar_tac]
                exact LZ77.valid_lit (bytes input) (toks out ntok.val) pos.val hde
                  (by rw [bytes_length]; scalar_tac) (by rw [← hval]; scalar_tac)
            · exfalso; scalar_tac )
        | ( -- A: beaten pending, immediate accept -- literal at pos-1, then the match at pos
            rcases hpd with h | ⟨hpos1, hl3, hlmax, hend, hd1, hdmax, hdpos, hmatch⟩
            · exfalso; scalar_tac
            rw [emitted_ge hl3] at hnt hde
            have hcur3 : 3 ≤ cur_len.val := by scalar_tac
            have hposlen : pos.val - 1 < input.length := by scalar_tac
            have hi : i.val = pos.val - 1 := by scalar_tac
            have hval : i2.val = (bytes input)[pos.val - 1]! := by
              rw [bytes_getElem! input (pos.val - 1) hposlen, i2_post, Std.U8.cast_U32_val_eq, i1_post]
              simp only [hi]
            have hstep1 : LZ77.decode (toks (out.set ntok i2) ntok1.val) =
                some ((bytes input).take pos.val) := by
              rw [show ntok1.val = ntok.val + 1 by scalar_tac, toks_update out ntok i2 hntok_lt, hval,
                show pos.val = (pos.val - 1) + 1 by scalar_tac]
              exact LZ77.valid_lit (bytes input) (toks out ntok.val) (pos.val - 1) hde
                (by rw [bytes_length]; scalar_tac) (by rw [← hval]; scalar_tac)
            rcases hfound with hfl | ⟨hfl3, hflmax, hfend, hfd1, hfdmax, hfdpos, hfmatch⟩
            · exfalso; scalar_tac
            have htok : i9.val = LZ77.mkMatch cur_dist.val cur_len.val := by
              simp only [LZ77.mkMatch, LZ77.MATCH_BASE, i9_post, i6_post, i5_post, i4_post,
                i3_post1, i8_post, i7_post1, Std.UScalar.cast_val_eq]
              scalar_tac
            have hlen_set : (out.set ntok i2).length = out.length := by
              simp [Std.Slice.set_val_eq]
            have hntok1_lt : ntok1.val < (out.set ntok i2).length := by
              rw [hlen_set]; scalar_tac
            refine ⟨by scalar_tac, ?_, by rw [s_post, __post2]; simpa [Std.Slice.set_val_eq] using hlen,
              head2_post, Or.inl (by scalar_tac), ?_, by scalar_tac⟩
            · rw [emitted_lt (by scalar_tac)]; scalar_tac
            · rw [emitted_lt (by scalar_tac), s_post, __post2,
                show ntok2.val = ntok1.val + 1 by scalar_tac,
                toks_update (out.set ntok i2) ntok1 i9 hntok1_lt, htok,
                show «end».val = pos.val + cur_len.val by scalar_tac]
              refine LZ77.valid_match (bytes input) (toks (out.set ntok i2) ntok1.val) pos.val
                cur_dist.val cur_len.val hstep1 hfd1 hfdpos
                (by simpa [LZ77.MAX_DIST] using hfdmax) hfl3
                (by simpa [LZ77.MAX_LEN] using hflmax) (by rw [bytes_length]; scalar_tac) ?_
              intro k hk
              exact (bytes_congr input _ _ (by scalar_tac) (by scalar_tac) (hfmatch k hk)).symm )
        | ( -- C: pending wins
            rcases hpd with h | ⟨hpos1, hl3, hlmax, hend, hd1, hdmax, hdpos, hmatch⟩
            · exfalso; scalar_tac
            rw [emitted_ge hl3] at hnt hde
            have htok : i6.val = LZ77.mkMatch pd.val pl.val := by
              simp only [LZ77.mkMatch, LZ77.MATCH_BASE, i6_post, i3_post, i2_post,
                i5_post, i1_post, i4_post1, i_post1, Std.UScalar.cast_val_eq]
              scalar_tac
            refine ⟨by scalar_tac, ?_, by rw [s_post]; simpa [Std.Slice.set_val_eq] using hlen,
              head2_post, Or.inl (by scalar_tac), ?_, by scalar_tac⟩
            · rw [emitted_lt (by scalar_tac)]; scalar_tac
            · rw [emitted_lt (by scalar_tac), s_post, show ntok1.val = ntok.val + 1 by scalar_tac,
                toks_update out ntok i6 hntok_lt, htok,
                show «end».val = (pos.val - 1) + pl.val by scalar_tac]
              refine LZ77.valid_match (bytes input) (toks out ntok.val) (pos.val - 1)
                pd.val pl.val hde hd1 hdpos
                (by simpa [LZ77.MAX_DIST] using hdmax) hl3
                (by simpa [LZ77.MAX_LEN] using hlmax) (by rw [bytes_length]; scalar_tac) ?_
              intro k hk
              exact (bytes_congr input _ _ (by scalar_tac) (by scalar_tac) (hmatch k hk)).symm )
    case isFalse hge =>
      have hpn : pos.val = n.val := by scalar_tac
      have hpl : pl.val < 3 := by
        rcases hpd with h | ⟨_, hl3, _, hend, _⟩
        · exact h
        · exfalso; omega
      rw [emitted_lt hpl] at hnt hde
      refine ⟨hpl, by scalar_tac, hlen, ?_⟩
      rw [hde, hpn, hn]
      simp
  · exact ⟨hpos, hntok, rfl, hlim, hpend, hdec⟩

/-! ## The obligation -/

theorem parse_spec (input : Slice Std.U8) (out : Slice Std.U32)
    (hlen : input.length ≤ out.length) :
    slot.parse input out ⦃ fun r =>
      r.1.val ≤ input.length ∧
      r.2.length = out.length ∧
      LZ77.Valid (bytes input) (toks r.2 r.1.val) ⦄ := by
  rw [slot.parse]
  apply Std.WP.spec_bind (Pₘ := fun r => r.1 = true → r.2.val + 3 ≤ input.length)
  · split
    case isTrue h3 =>
      have hmax : input.length ≤ Std.Usize.max := Std.Slice.length_ineq input
      step*
    case isFalse h3 =>
      intro hc; exact absurd hc (by simp)
  · rintro ⟨has3, lim⟩ hlim
    apply Std.WP.spec_bind (parse_loop0_spec input out (Std.Slice.len input) lim
      (Std.Array.repeat 32768#usize 0#u32) (Std.Array.repeat 32768#usize 0#u32)
      0#usize 0#usize 0#usize 0#usize has3
      (by simp) hlen hlim (by scalar_tac) (by simp [emitted]) (Or.inl (by scalar_tac))
      (by simp [toks, LZ77.decode, emitted]))
    rintro ⟨out1, ntok, pl, pd⟩ ⟨hpl, hntok, hlen1, hdec⟩
    step*
    exact ⟨hntok, hlen1, hdec⟩

end Submission