5CAkr5…FDPt3n

//! # The slot: LZ77 parsing.
//!
//! 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`. The arithmetic encoding (rather
//! than shifts and masks) is deliberate: `Nat` `+`, `*`, `/` and `%` are what
//! `omega` reasons about on the Lean side, and `&&&`/`<<<` are not.
//!
//! The only thing that must be proved is that the token stream **decodes back to
//! `input`**, and that `parse` neither panics nor diverges.
//!
//! ## What is *not* constrained
//!
//! Nothing about the search. The hash chains below could be a suffix automaton, a
//! binary tree, or a full optimal-parse dynamic program and the proof would not
//! grow, because correctness rests only on the bytes `match_len` actually
//! compared before a match was emitted. `hash3_spec` in the proof says the hash
//! lands in range and says nothing whatever about what it computes.
//!
//! ## Prover-friendly Rust — the rules
//!
//! 1. No labelled `break`/`continue`, no early `return` from a nested loop, no
//!    trait objects, no iterator adapters. Indices, `while`, and plain `if`.
//! 2. Prefer `i <= n - k` to `i + k <= n`. In the extracted model a slice may
//!    have length `usize::MAX`, and then the *addition* overflows and the program
//!    is not total. The guarded subtraction cannot.
//! 3. Bound every array index with `%`, not `&`. `h % 32768 < 32768` is one
//!    `omega` step; the same fact about `h & 0x7fff` is a bitvector argument.
//! 4. Give every loop a decreasing counter that does not depend on the data. The
//!    chain walk below terminates because `probes` increases, not because the
//!    chain is acyclic — which it need not be.

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

/// How far down a hash chain to look. The whole speed/ratio dial.
pub const MAX_PROBES: usize = 16;

/// Hash of the three bytes at a position. Any function of the right range works;
/// `% 32768` rather than `& 0x7fff` so that the index bound is arithmetic.
pub fn hash3(a: u8, b: u8, c: u8) -> usize {
    let x = (a as u32)
        .wrapping_mul(2654435761)
        .wrapping_add((b as u32).wrapping_mul(2246822519))
        .wrapping_add((c as u32).wrapping_mul(3266489917));
    ((x >> 15) % 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.
///
/// A separate function rather than a loop inside `parse`, and that is **not**
/// cosmetic: Aeneas reports `Unimplemented` for a second loop nested in the body
/// of `parse`'s outer loop when that loop also reads a local array of the
/// enclosing scope. Lifting it out, with the array as a `&[u32]` parameter,
/// translates. Prover-friendly rule 5.
///
/// `prev` must be at least 32768 long; `parse` passes a `[u32; 32768]`.
pub fn find_match(
    input: &[u8],
    prev: &[u32],
    pos: usize,
    cap: usize,
    start: usize,
) -> (usize, usize) {
    let mut best_len = 0usize;
    let mut best_dist = 0usize;
    let mut cur = start;
    let mut probes = 0usize;
    while probes < 16 && cur > 0 && cur <= pos {
        let cpos = cur - 1;
        if pos - cpos <= 32768 {
            // A candidate can improve best_len only if its next byte agrees.
            // The cap guard also keeps both lookahead indices in bounds.
            if best_len < cap && input[cpos + best_len] == input[pos + best_len] {
                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 {
            // Everything further down the chain is older still, so the walk is
            // over. `cur = 0` ends it without a `break`.
            cur = 0;
        }
        probes += 1;
    }
    (best_len, best_dist)
}

/// Greedy matching over hash chains.
///
/// `head[h]` is the most recent position whose three bytes hash to `h`, plus one
/// (zero means "none"). `prev[p % 32768]` is the position before `p` in the same
/// chain, plus one. The `+ 1` is what lets zero be the sentinel without a
/// separate occupancy array, and `% 32768` keeps `prev` a fixed-size array rather
/// than one allocation per input.
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 };
    while pos < n {
        let mut best_len = 0usize;
        let mut best_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;
            }
            // The chain walk. It terminates on `probes`, never on the chain
            // being acyclic — a truncated `as u32` can point anywhere, and the
            // byte comparison inside `match_len` is what keeps that harmless.
            let found = find_match(input, &prev, pos, cap, start);
            best_len = found.0;
            best_dist = found.1;
        }
        if best_len >= 3 {
            out[ntok] = 16777216u32 + ((best_dist - 1) as u32) * 256 + ((best_len - 3) as u32);
            ntok += 1;
            let end = pos + best_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 {
            out[ntok] = input[pos] as u32;
            ntok += 1;
            pos += 1;
        }
    }
    ntok
}

import Lz77
import Slot

/-!
# The submission's proof

This file is what a **miner** writes. Everything it imports is fixed: `Lz77` is
the published contract and its lemmas, `Slot` is `charon`+`aeneas` output that the
verifier regenerates from the submitted `parse.rs` and never takes on trust.

The obligation is `parse_spec` at the bottom, whose statement is pinned by the
verifier. Nothing else in this file is checked, so a miner may restructure it
freely.
-/

namespace Submission
open Aeneas Aeneas.Std Result ControlFlow

set_option maxRecDepth 8192
set_option maxHeartbeats 1000000

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

Nothing about correctness depends on what `hash3` computes, only that it lands in
range: a wrong hash finds a worse match, never an invalid one. That is the
property that lets a miner replace the whole search with anything they like. -/

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

/-! ## The match-length loop

The one function whose *result* the proof depends on. Its postcondition is
precisely the hypothesis `LZ77.valid_match` wants, which is why the rest of the
submission never mentions `copyN`. -/

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 hash-insert loop

Pure bookkeeping: it writes into the search structure and nothing else, so its
postcondition is `True`. What still has to be proved is that it *terminates* and
never fails — which is the price of total correctness, and the reason a miner's
search structure is free but not free of obligations. -/

@[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

/-! ## The search

`find_match` walks a hash chain. Its whole postcondition is `Found`, and `Found`
is also its loop invariant — which is the point of the design: a submission that
replaces this with a suffix automaton or an optimal parse rewrites *this lemma
only*, and everything below is untouched.

Note what is **not** proved: nothing says the chain is acyclic, nothing says
`prev` points anywhere sensible, and nothing says the match found is the best one.
The walk terminates because `probes` counts up, and a wrong candidate is harmless
because `match_len` compares the bytes.
-/

theorem find_match_loop_spec (input : Slice Std.U8) (prev : Slice Std.U32)
    (n pos 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) (h0len : bl0.val ≤ cap.val) :
    slot.find_match_loop input prev pos 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 => slot.MAX_PROBES.val - s.2.2.2.val)
    (inv := fun s => Found input n pos s.1 s.2.1 ∧ s.1.val ≤ cap.val)
  · 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 ∧ r.1.val ≤ cap.val)
    · split
      case isTrue hw =>
        apply Std.WP.spec_bind (Pₘ := fun r => Found input n pos r.1 r.2 ∧ r.1.val ≤ cap.val)
        · split
          case isTrue hlt =>
            step*
            refine ⟨?_, by scalar_tac⟩
            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*
        · rintro ⟨bl1, bd1⟩ hf
          step*
      case isFalse => exact hinv
    · rintro ⟨bl1, bd1, cur1⟩ hf
      step*
  · exact ⟨h0, h0len⟩

@[local step]
theorem find_match_spec (input : Slice Std.U8) (prev : Slice Std.U32)
    (n pos cap start : 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
      ⦃ fun r => Found input n pos r.1 r.2 ⦄ :=
  find_match_loop_spec input prev n pos cap 0#usize 0#usize start 0#usize
    hn hprev hcap hcap258 (Or.inl (by scalar_tac)) (by scalar_tac)

/-! ## The parse loop

The invariant is one line of English: *the tokens written so far decode to the
input consumed so far*. Everything else in it — `pos ≤ n`, `ntok ≤ pos`, the
buffer keeps its length — is bookkeeping that exists to make the writes legal. -/

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 : 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 ≤ pos0.val)
    (hdec : LZ77.decode (toks out0 ntok0.val) = some ((bytes input).take pos0.val)) :
    slot.parse_loop0 input out0 n head0 prev0 ntok0 pos0 has30 lim ⦃ fun r =>
      r.1.val ≤ input.length ∧ r.2.length = out0.length ∧
      LZ77.decode (toks r.2 r.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 ≤ s.2.2.2.2.1.val ∧
      s.1.length = out0.length ∧
      (s.2.2.2.2.2 = true → lim.val + 3 ≤ input.length) ∧
      LZ77.decode (toks s.1 s.2.2.2.1.val) = some ((bytes input).take s.2.2.2.2.1.val))
  · rintro ⟨out, hd, pv, ntok, pos, h3⟩ ⟨hp, hnt, hlen, hh3, hde⟩
    simp only at hp hnt hlen hh3 hde
    have hmax : input.length ≤ Std.Usize.max := Std.Slice.length_ineq input
    simp only [slot.parse_loop0.body]
    split
    case isTrue hposlt =>
      -- `step*` will not enter a `do` block whose first statement is an `if`, so
      -- the search is cut off here with its own postcondition. That is also the
      -- right division of labour: `Found` is everything the emission needs to
      -- know, and it is all a *different* search would have to establish.
      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*
            -- `if b then ok x else ok y` is a choice of *value*; `step*` needs
            -- it in that form before it will go on.
            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*
            -- `find_match`'s two range preconditions, on the capped length
            · split <;> scalar_tac
            · split <;> scalar_tac
          case isFalse => exact Or.inl (by scalar_tac)
        case isFalse => exact Or.inl (by scalar_tac)
      · rintro ⟨head1, prev1, best_len, best_dist⟩ hfound
        have hntok_lt : ntok.val < out.length := by scalar_tac
        have hlim3 : h3 = true → lim.val + 3 ≤ input.length := hh3
        replace hfound : Found input n pos best_len best_dist := hfound
        simp only [Found] at hfound
        step*
        -- Unfolding `Found` before `step*` is worth doing: its side-goal solver
        -- then case-splits the disjunction itself and discharges all five range
        -- obligations of the token encoding, leaving only the two invariants.
        -- The invariant, after emitting a match.
        · rcases hfound with _ | ⟨hl3, hlmax, hend, hd1, hdmax, hdpos, hmatch⟩
          · exfalso; scalar_tac
          have htok : i6.val = LZ77.mkMatch best_dist.val best_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 scalar_tac, by rw [s_post]; simpa [Std.Slice.set_val_eq] using hlen, head2_post, ?_,
            by scalar_tac⟩
          rw [s_post, show ntok1.val = ntok.val + 1 by scalar_tac,
            toks_update out ntok i6 hntok_lt, htok,
            show «end».val = pos.val + best_len.val by scalar_tac]
          refine LZ77.valid_match (bytes input) (toks out ntok.val) pos.val
            best_dist.val best_len.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
        -- The invariant, after emitting a literal.
        · 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 scalar_tac, by rw [s_post]; simpa [Std.Slice.set_val_eq] using hlen, hlim3, ?_,
            by scalar_tac⟩
          rw [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)
    case isFalse hge =>
      have hpn : pos.val = n.val := by scalar_tac
      refine ⟨by scalar_tac, hlen, ?_⟩
      rw [hde, hpn, hn]
      simp
  · exact ⟨hpos, hntok, rfl, hlim, hdec⟩

/-! ## The obligation

This is the statement the verifier pins. A submission is accepted when *this*
theorem, with this statement, elaborates against a `Slot` the verifier generated
itself, and `#print axioms` on it shows nothing but Lean's own three.

Read it as: `parse` writes `ntok` tokens into `out`, does not disturb its length,
never fails and always terminates, and **the tokens it wrote decode back to the
input**. -/

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
    exact 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 has3
      (by simp) hlen hlim (by scalar_tac) (by scalar_tac)
      (by simp [toks, LZ77.decode])

end Submission