5GZYDL…FPthgF

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

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

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

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

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

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

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

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

/// The engine for this input: its index in `parse`. Shares are compared per 100000 sampled bytes.
pub fn route(input: &[u8]) -> usize {
    let n = input.len();
    if n < R_TINY {
        return 1;
    }
    if n < R_SAMPLE {
        return 1;
    }
    let s = R_SAMPLE;
    let s64 = s as u64;
    let mut hist = [0u32; 256];
    r_hist(input, s, &mut hist);
    let f_alpha = r_alpha(&hist);
    let f_brace = hist[123] as u64;
    let f_digit = r_sum(&hist, 48, 58);
    let f_dot = hist[46] as u64;
    let f_eq = hist[61] as u64;
    let f_hi = r_sum(&hist, 128, 256);
    let f_letter = r_sum(&hist, 65, 91).wrapping_add(r_sum(&hist, 97, 123));
    let f_lt = hist[60] as u64;
    let f_quote = hist[34] as u64;
    let f_slash = hist[47] as u64;
    let f_space = hist[32] as u64;
    if f_lt.wrapping_mul(100000) <= 266u64.wrapping_mul(s64) {
        if f_digit.wrapping_mul(100000) <= 19943u64.wrapping_mul(s64) {
            if f_dot.wrapping_mul(100000) <= 4241u64.wrapping_mul(s64) {
                if f_space.wrapping_mul(100000) <= 25614u64.wrapping_mul(s64) {
                    0
                } else {
                    1
                }
            } else {
                1
            }
        } else {
            if f_alpha <= 65 {
                if f_space.wrapping_mul(100000) <= 3009u64.wrapping_mul(s64) {
                    0
                } else {
                    1
                }
            } else {
                if f_slash.wrapping_mul(100000) <= 1209u64.wrapping_mul(s64) {
                    1
                } else {
                    0
                }
            }
        }
    } else {
        if f_letter.wrapping_mul(100000) <= 20871u64.wrapping_mul(s64) {
            if f_brace.wrapping_mul(100000) <= 244u64.wrapping_mul(s64) {
                if f_eq.wrapping_mul(100000) <= 10208u64.wrapping_mul(s64) {
                    0
                } else {
                    1
                }
            } else {
                if f_hi.wrapping_mul(100000) <= 51383u64.wrapping_mul(s64) {
                    1
                } else {
                    0
                }
            }
        } else {
            if f_quote.wrapping_mul(100000) <= 83u64.wrapping_mul(s64) {
                1
            } else {
                if f_eq.wrapping_mul(100000) <= 135u64.wrapping_mul(s64) {
                    1
                } else {
                    0
                }
            }
        }
    }
}

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


// ===== engine a: y23_eu32.rs =====

pub const A_DEPTH: usize = 32;
pub const A_DEPTH2: usize = 4;
pub const A_GOOD: usize = 3;
pub const A_LAZY: usize = 258;
pub const A_NICE: usize = 258;
pub const A_IH: usize = 258;
pub const A_IT: usize = 64;
pub const A_ACC: u64 = 6;
pub const A_STEPMAX: usize = 32;
pub const A_LITQ: usize = 28;
pub const A_LADJ: usize = 2;
pub const A_HLOW: usize = 900;
pub const A_HSL: u32 = 0;
pub const A_ELO: usize = 400;
pub const A_H3HI: usize = 50;
pub const A_H3CTL: usize = 100;
pub const A_H3E: usize = 1700;
pub const A_ACCL: u64 = 63;
pub const A_H3: usize = 1;
pub const A_MAX3: usize = 4096;
pub const A_H3INS: usize = 1;
pub const A_C0Q: usize = 44;
pub const A_C0L: usize = 44;
pub const A_DEPTHL: usize = 12;
pub const A_M3: usize = 0;
pub const A_DEPTH3M: usize = 12;
pub const A_M3E: usize = 1900;
pub const A_M3Z: usize = 15;
pub const A_LZB: usize = 0;
pub const A_BONUS: usize = 0;
pub const A_EXT: usize = 1;
pub const A_DIGN: usize = 200;
pub const A_DN: usize = 4;
pub const A_P2N: usize = 8;
pub const A_LQN: usize = 20;
pub const A_NBIG: usize = 65536;
pub const A_GOODL: usize = 258;
pub const A_P2G: usize = 2;
pub const A_NSMALL: usize = 65536;
pub const A_BIAS: usize = 4096;

// ------------------------------------------------------------------ loads and compares (search only)

/// Little-endian 4-byte load at `p`; 0 when out of range.
pub fn a_ld4(input: &[u8], p: usize) -> u32 {
    let n = input.len();
    if n < 4 || p > n - 4 {
        return 0;
    }
    ((input[p + 3] as u32) << 24) | ((input[p + 2] as u32) << 16) | ((input[p + 1] as u32) << 8) | (input[p] as u32)
}

/// Little-endian 8-byte load at `p` (two u32 halves, highest byte read first); 0 when out of range.
pub fn a_ld8(input: &[u8], p: usize) -> u64 {
    let n = input.len();
    if n < 8 || p > n - 8 {
        return 0;
    }
    let hi = ((input[p + 7] as u32) << 24) | ((input[p + 6] as u32) << 16) | ((input[p + 5] as u32) << 8) | (input[p + 4] as u32);
    let lo = ((input[p + 3] as u32) << 24) | ((input[p + 2] as u32) << 16) | ((input[p + 1] as u32) << 8) | (input[p] as u32);
    ((hi as u64) << 32) | (lo as u64)
}

/// Index (0..7) of the first differing byte of two little-endian words, given their xor (!= 0).
pub fn a_first_diff(x: u64) -> usize {
    let low = x & 0u64.wrapping_sub(x);
    (63u32.wrapping_sub(low.leading_zeros()) / 8) as usize
}

/// Common prefix of positions `a < b`, up to `cap` (search only; never trusted).
pub fn a_fast_len(input: &[u8], a: usize, b: usize, cap: usize) -> usize {
    let mut l = 0usize;
    let mut go = 1usize;
    let mut it = 0usize;
    while go == 1 && it < 40 {
        if l < cap {
            let x = a_ld8(input, a.wrapping_add(l)) ^ a_ld8(input, b.wrapping_add(l));
            let k = if x == 0 { 8 } else { a_first_diff(x) };
            l = l.wrapping_add(k);
            go = if x == 0 { 1 } else { 0 };
        } else {
            go = 0;
        }
        it += 1;
    }
    if l > cap { cap } else { l }
}

/// Hash of the first (64 - hs) / 8 bytes at `p` into 16 bits.
#[inline(always)]
pub fn a_hashp(input: &[u8], p: usize, hs: u32) -> usize {
    if hs == 32 {
        return (a_ld4(input, p).wrapping_mul(2654435761) >> 16) as usize;
    }
    let v = a_ld8(input, p) << (hs % 64);
    (v.wrapping_mul(0x9E3779B97F4A7C15) >> 48) as usize
}

/// Hash of the low 3 bytes of a word into 14 bits.
pub fn a_hash3(w: u32) -> usize {
    ((w << 8).wrapping_mul(2654435761) >> 18) as usize
}

// ------------------------------------------------------------------ cost model (search only)

/// DEFLATE distance extra bits of `d`.
pub fn a_dextra(d: usize) -> usize {
    if d <= 4 {
        0
    } else {
        let x = (d.wrapping_sub(1) as u32) | 1;
        (31u32.wrapping_sub(x.leading_zeros()) as usize).wrapping_sub(1)
    }
}

/// DEFLATE length extra bits of `l`.
pub fn a_lextra(l: usize) -> usize {
    if l < 11 || l >= 258 {
        0
    } else {
        let x = (l.wrapping_sub(3) as u32) | 1;
        (31u32.wrapping_sub(x.leading_zeros()) as usize).wrapping_sub(2)
    }
}

/// Estimated saving (quarter bits, offset by A_BIAS) of coding `l` bytes as a match at `d`.
/// `cq` packs the literal cost (low 8 bits) and the match base cost (bits 8..).
pub fn a_score(l: usize, d: usize, cq: usize) -> usize {
    let cost = (cq / 256).wrapping_add(a_dextra(d).wrapping_add(a_lextra(l)).wrapping_mul(4));
    l.wrapping_mul(cq % 256).wrapping_add(A_BIAS).wrapping_sub(cost)
}

/// Fixed-point log2 with 8 fractional bits (linear between powers of two).
pub fn a_lg8(x: u32) -> u64 {
    let y = x | 1;
    let e = 31u32.wrapping_sub(y.leading_zeros()) % 32;
    let m = if e >= 8 { (y >> ((e.wrapping_sub(8)) % 32)) & 255 } else { (y << ((8u32.wrapping_sub(e)) % 32)) & 255 };
    (e as u64).wrapping_mul(256).wrapping_add(m as u64)
}

/// Histogram of a strided sample of the input (about 4096 bytes).
pub fn a_sample(input: &[u8], h: &mut [u32; 256]) {
    let n = input.len();
    let st = n / 4096 + 1;
    let mut k = 0usize;
    let mut c = 0usize;
    while k < n && c < 8192 {
        let b = (input[k] as usize) % 256;
        h[b] = h[b].wrapping_add(1);
        k = k.wrapping_add(st);
        c += 1;
    }
}

/// Order-0 entropy of the histogram in 1/256 bits per symbol.
pub fn a_entropy256(h: &[u32; 256]) -> usize {
    let mut tot = 0u64;
    let mut acc = 0u64;
    let mut i = 0usize;
    while i < 256 {
        let c = h[i];
        tot = tot.wrapping_add(c as u64);
        acc = if c > 0 { acc.wrapping_add((c as u64).wrapping_mul(a_lg8(c))) } else { acc };
        i += 1;
    }
    let t32 = if tot > 4000000000 { 4000000000u32 } else { tot as u32 };
    let a = a_lg8(t32);
    let b = if tot == 0 { a } else { acc / tot };
    if a > b { (a - b) as usize } else { 0 }
}

/// Per mille of the sampled bytes in `lo .. hi`.
pub fn a_share(h: &[u32; 256], lo: usize, hi: usize) -> usize {
    let mut t = 0usize;
    let mut s = 0usize;
    let mut i = 0usize;
    while i < 256 {
        let c = h[i] as usize;
        t = t.wrapping_add(c);
        s = if i >= lo && i < hi { s.wrapping_add(c) } else { s };
        i += 1;
    }
    if t == 0 { 0 } else { s.wrapping_mul(1000) / t }
}

/// 1 when the sampled entropy `e` marks a genome-like input (few cheap literals).
pub fn a_low_mode(e: usize) -> usize {
    if e >= A_ELO && e < A_HLOW { 1 } else { 0 }
}

/// Literal cost (quarter bits): from the sampled entropy in low mode, else A_LITQ.
pub fn a_lit_cost(e: usize, low: usize) -> usize {
    let q = (e / 64).wrapping_add(A_LADJ);
    let q2 = if q < 6 { 6 } else if q > 36 { 36 } else { q };
    if low == 1 { q2 } else { A_LITQ }
}

/// 1 when the input should use 3-byte hash chains (A_M3 = 2: always; 1: by rule).
pub fn a_m3_mode(h: &[u32; 256], e: usize) -> usize {
    let z = a_share(h, 0, 1);
    let a = if e >= A_M3E { 1usize } else { 0usize };
    let b = if z >= A_M3Z { 1usize } else { 0usize };
    if A_M3 == 2 { 1 } else if A_M3 == 1 { a & b } else { 0 }
}

/// 1 when the 3-byte table should be used: binary-ish or non-ASCII input of moderate entropy.
pub fn a_h3_mode(h: &[u32; 256], e: usize) -> usize {
    let hi = a_share(h, 128, 256);
    let ctl = a_share(h, 0, 9);
    let a = if hi >= A_H3HI { 1usize } else { 0usize };
    let b = if ctl >= A_H3CTL { 1usize } else { 0usize };
    let c = if e < A_H3E { 1usize } else { 0usize };
    if A_H3 == 2 { 1 } else if A_H3 == 1 { (a | b) & c } else { 0 }
}

/// 1 for large numeric text: at least A_DIGN per mille digits, few bytes >= 128 or < 9, not genome-like.
pub fn a_numeric(h: &[u32; 256], n: usize, low: usize) -> usize {
    let dig = a_share(h, 48, 58);
    let hi = a_share(h, 128, 256);
    let ctl = a_share(h, 0, 9);
    let txt = if hi < 50 && ctl < 50 { 1usize } else { 0usize };
    let big = if n >= A_NBIG { 1usize } else { 0usize };
    let d = if dig >= A_DIGN { 1usize } else { 0usize };
    if low == 1 { 0 } else { txt & big & d }
}

// ------------------------------------------------------------------ match finding (search only)

/// Walk the chain from `start` (pos+1 encoded, 0 = none) for the candidate with the best score
/// among those longer than `bl0` and scoring more than `bs0`. Returns `len | dist << 9 | score << 25`
/// (0 if none). Candidates stay inside the 32K window; the walk stops at `A_NICE` or `cap`.
pub fn a_walk(input: &[u8], prev: &[u32; 65536], pos: usize, start: usize, cap: usize, probes: usize, bl0: usize, bs0: usize, litq: usize) -> usize {
    let lim = pos.saturating_sub(32768);
    let stop = if cap < A_NICE { cap } else { A_NICE };
    let mut cur = start;
    let mut k = 0usize;
    let mut bl = bl0;
    let mut bs = bs0;
    let mut bd = 0usize;
    let mut off = if bl >= 3 { bl - 3 } else { 0 };
    let mut want = a_ld4(input, pos.wrapping_add(off));
    while k < probes && cur > lim && cur <= pos && bl < stop {
        let c = cur - 1;
        let next = prev[c % 65536] as usize;
        if a_ld4(input, c.wrapping_add(off)) == want {
            let l = a_fast_len(input, c, pos, cap);
            let d = pos - c;
            let s = a_score(l, d, litq);
            let better = if l > bl { if s > bs { 1usize } else { 0usize } } else { 0usize };
            if better == 1 {
            bd = if better == 1 { d } else { bd };
            bs = if better == 1 { s } else { bs };
            bl = if better == 1 { l } else { bl };
            off = if bl >= 3 { bl - 3 } else { 0 };
            want = a_ld4(input, pos.wrapping_add(off));
            }
        }
        cur = next;
        k += 1;
    }
    if bd > 0 {
        bl | bd.wrapping_mul(512) | bs.wrapping_mul(33554432)
    } else {
        0
    }
}

/// Lazy-path copy of `walk` (a separate function keeps both inlined at their single call sites).
/// Walk the chain from `start` (pos+1 encoded, 0 = none) for the candidate with the best score
/// among those longer than `bl0` and scoring more than `bs0`. Returns `len | dist << 9 | score << 25`
/// (0 if none). Candidates stay inside the 32K window; the walk stops at `A_NICE` or `cap`.
pub fn a_lwalk(input: &[u8], prev: &[u32; 65536], pos: usize, start: usize, cap: usize, probes: usize, bl0: usize, bs0: usize, litq: usize) -> usize {
    let lim = pos.saturating_sub(32768);
    let stop = if cap < A_NICE { cap } else { A_NICE };
    let mut cur = start;
    let mut k = 0usize;
    let mut bl = bl0;
    let mut bs = bs0;
    let mut bd = 0usize;
    let mut off = if bl >= 3 { bl - 3 } else { 0 };
    let mut want = a_ld4(input, pos.wrapping_add(off));
    while k < probes && cur > lim && cur <= pos && bl < stop {
        let c = cur - 1;
        let next = prev[c % 65536] as usize;
        if a_ld4(input, c.wrapping_add(off)) == want {
            let l = a_fast_len(input, c, pos, cap);
            let d = pos - c;
            let s = a_score(l, d, litq);
            let better = if l > bl { if s > bs { 1usize } else { 0usize } } else { 0usize };
            if better == 1 {
            bd = if better == 1 { d } else { bd };
            bs = if better == 1 { s } else { bs };
            bl = if better == 1 { l } else { bl };
            off = if bl >= 3 { bl - 3 } else { 0 };
            want = a_ld4(input, pos.wrapping_add(off));
            }
        }
        cur = next;
        k += 1;
    }
    if bd > 0 {
        bl | bd.wrapping_mul(512) | bs.wrapping_mul(33554432)
    } else {

import Lz77
import Slot

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

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

set_option maxRecDepth 8192
set_option maxHeartbeats 4000000



/-!
jprover (cand/J-fast): proof of a fast greedy/lazy LZ77 parser (hash chains, word compares,
cost-aware lazy choices). All search code is untrusted: every lemma about it has postcondition
`True` and proves only termination and the absence of panics (one uniform recipe per loop).
Emission happens inside the main loop through trusted helpers that re-verify every match with the
byte-wise `match_len`, so the main loop's invariant is the template's.
-/

namespace EA
open Aeneas Aeneas.Std Result ControlFlow

set_option maxRecDepth 8192
set_option maxHeartbeats 4000000

open LZ77 (toks bytes bytes_length bytes_getElem! Matches emit_lit emit_match ite_ok)

theorem decode_nil (input : Slice Std.U8) (out : Slice Std.U32) :
    LZ77.decode (toks out (0#usize).val) = some ((bytes input).take (0#usize).val) := by
  simp [toks, LZ77.decode]

/-- A parse that reached the input end is valid. -/
theorem valid_of_decode {input : Slice Std.U8} {o : Slice Std.U32} {t p : Std.Usize}
    (hde : LZ77.decode (toks o t.val) = some ((bytes input).take p.val)) (hp : p.val = input.length) :
    LZ77.Valid (bytes input) (toks o t.val) := by
  unfold LZ77.Valid
  rw [hde, hp]
  simp

/-- Case split on an `if` without `split`. -/
theorem spec_ite_cut {α : Type} (c : Prop) [Decidable c] (a b : Result α) (Q : α → Prop)
    (ha : c → a ⦃ Q ⦄) (hb : ¬c → b ⦃ Q ⦄) : (if c then a else b) ⦃ Q ⦄ := by
  by_cases h : c
  · rw [if_pos h]; exact ha h
  · rw [if_neg h]; exact hb h


/-- Search-state updates in the main loop (tuple-valued `if`s) are kept opaque. -/
theorem ite_prod_spec {α β : Type} (c : Prop) [Decidable c] (A B : Result (α × β))
    (hA : c → A ⦃ fun _ => True ⦄) (hB : ¬c → B ⦃ fun _ => True ⦄) :
    (if c then A else B) ⦃ fun _ => True ⦄ := by
  by_cases h : c
  · rw [if_pos h]; exact hA h
  · rw [if_neg h]; exact hB h


/-- Every bind-position `if` of the (untrusted) main-loop state computation is kept opaque. -/
theorem ite_true_spec {α : Type} (c : Prop) [Decidable c] (A B : Result α)
    (hA : c → A ⦃ fun _ => True ⦄) (hB : ¬c → B ⦃ fun _ => True ⦄) :
    (if c then A else B) ⦃ fun _ => True ⦄ := by
  by_cases h : c
  · rw [if_pos h]; exact hA h
  · rw [if_neg h]; exact hB h


@[local step]
theorem ld4_spec (input : Slice Std.U8) (p : Std.Usize) :
    slot.a_ld4 input p ⦃ fun _ => True ⦄ := by
  rw [slot.a_ld4]
  try simp only [lift, Array.to_slice_mut]
  step*
  repeat (first
    | (intro hc; (try step*))
    | (split <;> (try step*))
    | (guard_hyp x :~ _ × _ × _ × _ × _ × _; obtain ⟨r1, r2, r3, r4, r5, r6⟩ := x; try step*)
    | (guard_hyp x :~ _ × _ × _ × _ × _; obtain ⟨r1, r2, r3, r4, r5⟩ := x; try step*)
    | (guard_hyp x :~ _ × _ × _ × _; obtain ⟨r1, r2, r3, r4⟩ := x; try step*)
    | (guard_hyp x :~ _ × _ × _; obtain ⟨r1, r2, r3⟩ := x; try step*)
    | (guard_hyp x :~ _ × _; obtain ⟨r1, r2⟩ := x; try step*)
    | (apply spec_ite_cut <;> intro hc <;> try step*)
    | (apply Std.WP.spec_bind (Pₘ := fun _ => True))
    | (intro y _; repeat (obtain ⟨_, y⟩ : _ × _ := y); try step*))
  all_goals scalar_tac

@[local step]
theorem ld8_spec (input : Slice Std.U8) (p : Std.Usize) :
    slot.a_ld8 input p ⦃ fun _ => True ⦄ := by
  rw [slot.a_ld8]
  try simp only [lift, Array.to_slice_mut]
  step*
  repeat (first
    | (intro hc; (try step*))
    | (split <;> (try step*))
    | (guard_hyp x :~ _ × _ × _ × _ × _ × _; obtain ⟨r1, r2, r3, r4, r5, r6⟩ := x; try step*)
    | (guard_hyp x :~ _ × _ × _ × _ × _; obtain ⟨r1, r2, r3, r4, r5⟩ := x; try step*)
    | (guard_hyp x :~ _ × _ × _ × _; obtain ⟨r1, r2, r3, r4⟩ := x; try step*)
    | (guard_hyp x :~ _ × _ × _; obtain ⟨r1, r2, r3⟩ := x; try step*)
    | (guard_hyp x :~ _ × _; obtain ⟨r1, r2⟩ := x; try step*)
    | (apply spec_ite_cut <;> intro hc <;> try step*)
    | (apply Std.WP.spec_bind (Pₘ := fun _ => True))
    | (intro y _; repeat (obtain ⟨_, y⟩ : _ × _ := y); try step*))
  all_goals scalar_tac

@[local step]
theorem first_diff_spec (x : Std.U64) :
    slot.a_first_diff x ⦃ fun _ => True ⦄ := by
  rw [slot.a_first_diff]
  try simp only [lift, Array.to_slice_mut]
  step*
  repeat (first
    | (intro hc; (try step*))
    | (split <;> (try step*))
    | (guard_hyp x :~ _ × _ × _ × _ × _ × _; obtain ⟨r1, r2, r3, r4, r5, r6⟩ := x; try step*)
    | (guard_hyp x :~ _ × _ × _ × _ × _; obtain ⟨r1, r2, r3, r4, r5⟩ := x; try step*)
    | (guard_hyp x :~ _ × _ × _ × _; obtain ⟨r1, r2, r3, r4⟩ := x; try step*)
    | (guard_hyp x :~ _ × _ × _; obtain ⟨r1, r2, r3⟩ := x; try step*)
    | (guard_hyp x :~ _ × _; obtain ⟨r1, r2⟩ := x; try step*)
    | (apply spec_ite_cut <;> intro hc <;> try step*)
    | (apply Std.WP.spec_bind (Pₘ := fun _ => True))
    | (intro y _; repeat (obtain ⟨_, y⟩ : _ × _ := y); try step*))
  all_goals scalar_tac

@[local step]
theorem fast_len_loop_spec (input : Slice Std.U8) (a : Std.Usize) (b : Std.Usize) (cap : Std.Usize) (l : Std.Usize) (go : Std.Usize) (it : Std.Usize)  :
    slot.a_fast_len_loop input a b cap l go it ⦃ fun _ => True ⦄ := by
  rw [slot.a_fast_len_loop]
  apply Std.loop.spec_decr_nat
    (measure := fun s => 40 - s.2.2.val)
    (inv := fun s => True)
  · rintro ⟨x0, x1, x2⟩ _
    simp only [slot.a_fast_len_loop.body, lift, Array.to_slice_mut]
    step*
    repeat (first
      | (intro hc; (try step*))
      | (split <;> (try step*))
      | (guard_hyp x :~ _ × _ × _ × _ × _ × _; obtain ⟨r1, r2, r3, r4, r5, r6⟩ := x; try step*)
      | (guard_hyp x :~ _ × _ × _ × _ × _; obtain ⟨r1, r2, r3, r4, r5⟩ := x; try step*)
      | (guard_hyp x :~ _ × _ × _ × _; obtain ⟨r1, r2, r3, r4⟩ := x; try step*)
      | (guard_hyp x :~ _ × _ × _; obtain ⟨r1, r2, r3⟩ := x; try step*)
      | (guard_hyp x :~ _ × _; obtain ⟨r1, r2⟩ := x; try step*)
      | (apply spec_ite_cut <;> intro hc <;> try step*)
      | (apply Std.WP.spec_bind (Pₘ := fun _ => True))
      | (intro y _; repeat (obtain ⟨_, y⟩ : _ × _ := y); try step*))
    all_goals scalar_tac
  · trivial

@[local step]
theorem fast_len_spec (input : Slice Std.U8) (a : Std.Usize) (b : Std.Usize) (cap : Std.Usize) :
    slot.a_fast_len input a b cap ⦃ fun _ => True ⦄ := by
  rw [slot.a_fast_len]
  step*
  repeat (first
    | (intro hc; (try step*))
    | (split <;> (try step*))
    | (guard_hyp x :~ _ × _ × _ × _ × _ × _; obtain ⟨r1, r2, r3, r4, r5, r6⟩ := x; try step*)
    | (guard_hyp x :~ _ × _ × _ × _ × _; obtain ⟨r1, r2, r3, r4, r5⟩ := x; try step*)
    | (guard_hyp x :~ _ × _ × _ × _; obtain ⟨r1, r2, r3, r4⟩ := x; try step*)
    | (guard_hyp x :~ _ × _ × _; obtain ⟨r1, r2, r3⟩ := x; try step*)
    | (guard_hyp x :~ _ × _; obtain ⟨r1, r2⟩ := x; try step*)
    | (apply spec_ite_cut <;> intro hc <;> try step*)
    | (apply Std.WP.spec_bind (Pₘ := fun _ => True))
    | (intro y _; repeat (obtain ⟨_, y⟩ : _ × _ := y); try step*))
  all_goals scalar_tac

@[local step]
theorem hashp_spec (input : Slice Std.U8) (p : Std.Usize) (hs : Std.U32) :
    slot.a_hashp input p hs ⦃ fun _ => True ⦄ := by
  rw [slot.a_hashp]
  try simp only [lift, Array.to_slice_mut]
  step*
  repeat (first
    | (intro hc; (try step*))
    | (split <;> (try step*))
    | (guard_hyp x :~ _ × _ × _ × _ × _ × _; obtain ⟨r1, r2, r3, r4, r5, r6⟩ := x; try step*)
    | (guard_hyp x :~ _ × _ × _ × _ × _; obtain ⟨r1, r2, r3, r4, r5⟩ := x; try step*)
    | (guard_hyp x :~ _ × _ × _ × _; obtain ⟨r1, r2, r3, r4⟩ := x; try step*)
    | (guard_hyp x :~ _ × _ × _; obtain ⟨r1, r2, r3⟩ := x; try step*)
    | (guard_hyp x :~ _ × _; obtain ⟨r1, r2⟩ := x; try step*)
    | (apply spec_ite_cut <;> intro hc <;> try step*)
    | (apply Std.WP.spec_bind (Pₘ := fun _ => True))
    | (intro y _; repeat (obtain ⟨_, y⟩ : _ × _ := y); try step*))
  all_goals scalar_tac

@[local step]
theorem hash3_spec (w : Std.U32) :
    slot.a_hash3 w ⦃ fun _ => True ⦄ := by
  rw [slot.a_hash3]
  try simp only [lift, Array.to_slice_mut]
  step*
  repeat (first
    | (intro hc; (try step*))
    | (split <;> (try step*))
    | (guard_hyp x :~ _ × _ × _ × _ × _ × _; obtain ⟨r1, r2, r3, r4, r5, r6⟩ := x; try step*)
    | (guard_hyp x :~ _ × _ × _ × _ × _; obtain ⟨r1, r2, r3, r4, r5⟩ := x; try step*)
    | (guard_hyp x :~ _ × _ × _ × _; obtain ⟨r1, r2, r3, r4⟩ := x; try step*)
    | (guard_hyp x :~ _ × _ × _; obtain ⟨r1, r2, r3⟩ := x; try step*)
    | (guard_hyp x :~ _ × _; obtain ⟨r1, r2⟩ := x; try step*)
    | (apply spec_ite_cut <;> intro hc <;> try step*)
    | (apply Std.WP.spec_bind (Pₘ := fun _ => True))
    | (intro y _; repeat (obtain ⟨_, y⟩ : _ × _ := y); try step*))
  all_goals scalar_tac

@[local step]
theorem dextra_spec (d : Std.Usize) :
    slot.a_dextra d ⦃ fun _ => True ⦄ := by
  rw [slot.a_dextra]
  try simp only [lift, Array.to_slice_mut]
  step*
  repeat (first
    | (intro hc; (try step*))
    | (split <;> (try step*))
    | (guard_hyp x :~ _ × _ × _ × _ × _ × _; obtain ⟨r1, r2, r3, r4, r5, r6⟩ := x; try step*)
    | (guard_hyp x :~ _ × _ × _ × _ × _; obtain ⟨r1, r2, r3, r4, r5⟩ := x; try step*)
    | (guard_hyp x :~ _ × _ × _ × _; obtain ⟨r1, r2, r3, r4⟩ := x; try step*)
    | (guard_hyp x :~ _ × _ × _; obtain ⟨r1, r2, r3⟩ := x; try step*)
    | (guard_hyp x :~ _ × _; obtain ⟨r1, r2⟩ := x; try step*)
    | (apply spec_ite_cut <;> intro hc <;> try step*)
    | (apply Std.WP.spec_bind (Pₘ := fun _ => True))
    | (intro y _; repeat (obtain ⟨_, y⟩ : _ × _ := y); try step*))
  all_goals scalar_tac

@[local step]
theorem lextra_spec (l : Std.Usize) :
    slot.a_lextra l ⦃ fun _ => True ⦄ := by
  rw [slot.a_lextra]
  try simp only [lift, Array.to_slice_mut]
  step*
  repeat (first
    | (intro hc; (try step*))
    | (split <;> (try step*))
    | (guard_hyp x :~ _ × _ × _ × _ × _ × _; obtain ⟨r1, r2, r3, r4, r5, r6⟩ := x; try step*)
    | (guard_hyp x :~ _ × _ × _ × _ × _; obtain ⟨r1, r2, r3, r4, r5⟩ := x; try step*)
    | (guard_hyp x :~ _ × _ × _ × _; obtain ⟨r1, r2, r3, r4⟩ := x; try step*)
    | (guard_hyp x :~ _ × _ × _; obtain ⟨r1, r2, r3⟩ := x; try step*)
    | (guard_hyp x :~ _ × _; obtain ⟨r1, r2⟩ := x; try step*)
    | (apply spec_ite_cut <;> intro hc <;> try step*)
    | (apply Std.WP.spec_bind (Pₘ := fun _ => True))
    | (intro y _; repeat (obtain ⟨_, y⟩ : _ × _ := y); try step*))
  all_goals scalar_tac

@[local step]
theorem score_spec (l : Std.Usize) (d : Std.Usize) (cq : Std.Usize) :
    slot.a_score l d cq ⦃ fun _ => True ⦄ := by
  rw [slot.a_score]
  try simp only [lift, Array.to_slice_mut]
  step*
  repeat (first
    | (intro hc; (try step*))
    | (split <;> (try step*))
    | (guard_hyp x :~ _ × _ × _ × _ × _ × _; obtain ⟨r1, r2, r3, r4, r5, r6⟩ := x; try step*)
    | (guard_hyp x :~ _ × _ × _ × _ × _; obtain ⟨r1, r2, r3, r4, r5⟩ := x; try step*)
    | (guard_hyp x :~ _ × _ × _ × _; obtain ⟨r1, r2, r3, r4⟩ := x; try step*)
    | (guard_hyp x :~ _ × _ × _; obtain ⟨r1, r2, r3⟩ := x; try step*)
    | (guard_hyp x :~ _ × _; obtain ⟨r1, r2⟩ := x; try step*)
    | (apply spec_ite_cut <;> intro hc <;> try step*)
    | (apply Std.WP.spec_bind (Pₘ := fun _ => True))
    | (intro y _; repeat (obtain ⟨_, y⟩ : _ × _ := y); try step*))
  all_goals scalar_tac

@[local step]
theorem lg8_spec (x : Std.U32) :
    slot.a_lg8 x ⦃ fun _ => True ⦄ := by
  rw [slot.a_lg8]
  try simp only [lift, Array.to_slice_mut]
  step*
  repeat (first
    | (intro hc; (try step*))
    | (split <;> (try step*))
    | (guard_hyp x :~ _ × _ × _ × _ × _ × _; obtain ⟨r1, r2, r3, r4, r5, r6⟩ := x; try step*)
    | (guard_hyp x :~ _ × _ × _ × _ × _; obtain ⟨r1, r2, r3, r4, r5⟩ := x; try step*)
    | (guard_hyp x :~ _ × _ × _ × _; obtain ⟨r1, r2, r3, r4⟩ := x; try step*)
    | (guard_hyp x :~ _ × _ × _; obtain ⟨r1, r2, r3⟩ := x; try step*)
    | (guard_hyp x :~ _ × _; obtain ⟨r1, r2⟩ := x; try step*)
    | (apply spec_ite_cut <;> intro hc <;> try step*)
    | (apply Std.WP.spec_bind (Pₘ := fun _ => True))
    | (intro y _; repeat (obtain ⟨_, y⟩ : _ × _ := y); try step*))
  all_goals scalar_tac

@[local step]
theorem sample_loop_spec (input : Slice Std.U8) (h : Array Std.U32 256#usize) (n : Std.Usize) (st : Std.Usize) (k : Std.Usize) (c : Std.Usize) (hn : n.val = input.length) :
    slot.a_sample_loop input h n st k c ⦃ fun _ => True ⦄ := by
  rw [slot.a_sample_loop]
  apply Std.loop.spec_decr_nat
    (measure := fun s => 8192 - s.2.2.val)
    (inv := fun s => True)
  · rintro ⟨x0, x1, x2⟩ _
    simp only [slot.a_sample_loop.body, lift, Array.to_slice_mut]
    step*
    repeat (first
      | (intro hc; (try step*))
      | (split <;> (try step*))
      | (guard_hyp x :~ _ × _ × _ × _ × _ × _; obtain ⟨r1, r2, r3, r4, r5, r6⟩ := x; try step*)
      | (guard_hyp x :~ _ × _ × _ × _ × _; obtain ⟨r1, r2, r3, r4, r5⟩ := x; try step*)
      | (guard_hyp x :~ _ × _ × _ × _; obtain ⟨r1, r2, r3, r4⟩ := x; try step*)
      | (guard_hyp x :~ _ × _ × _; obtain ⟨r1, r2, r3⟩ := x; try step*)
      | (guard_hyp x :~ _ × _; obtain ⟨r1, r2⟩ := x; try step*)
      | (apply spec_ite_cut <;> intro hc <;> try step*)
      | (apply Std.WP.spec_bind (Pₘ := fun _ => True))
      | (intro y _; repeat (obtain ⟨_, y⟩ : _ × _ := y); try step*))
    all_goals scalar_tac
  · trivial

@[local step]
theorem sample_spec (input : Slice Std.U8) (h : Array Std.U32 256#usize) :
    slot.a_sample input h ⦃ fun _ => True ⦄ := by
  rw [slot.a_sample]
  step*
  repeat (first
    | (intro hc; (try step*))
    | (split <;> (try step*))
    | (guard_hyp x :~ _ × _ × _ × _ × _ × _; obtain ⟨r1, r2, r3, r4, r5, r6⟩ := x; try step*)
    | (guard_hyp x :~ _ × _ × _ × _ × _; obtain ⟨r1, r2, r3, r4, r5⟩ := x; try step*)
    | (guard_hyp x :~ _ × _ × _ × _; obtain ⟨r1, r2, r3, r4⟩ := x; try step*)
    | (guard_hyp x :~ _ × _ × _; obtain ⟨r1, r2, r3⟩ := x; try step*)
    | (guard_hyp x :~ _ × _; obtain ⟨r1, r2⟩ := x; try step*)
    | (apply spec_ite_cut <;> intro hc <;> try step*)
    | (apply Std.WP.spec_bind (Pₘ := fun _ => True))
    | (intro y _; repeat (obtain ⟨_, y⟩ : _ × _ := y); try step*))
  all_goals scalar_tac

@[local step]
theorem entropy256_loop_spec (h : Array Std.U32 256#usize) (tot : Std.U64) (acc : Std.U64) (i : Std.Usize)  :
    slot.a_entropy256_loop h tot acc i ⦃ fun _ => True ⦄ := by
  rw [slot.a_entropy256_loop]
  apply Std.loop.spec_decr_nat
    (measure := fun s => 256 - s.2.2.val)
    (inv := fun s => True)
  · rintro ⟨x0, x1, x2⟩ _
    simp only [slot.a_entropy256_loop.body, lift, Array.to_slice_mut]
    step*
    repeat (first
      | (intro hc; (try step*))
      | (split <;> (try step*))
      | (guard_hyp x :~ _ × _ × _ × _ × _ × _; obtain ⟨r1, r2, r3, r4, r5, r6⟩ := x; try step*)
      | (guard_hyp x :~ _ × _ × _ × _ × _; obtain ⟨r1, r2, r3, r4, r5⟩ := x; try step*)
      | (guard_hyp x :~ _ × _ × _ × _; obtain ⟨r1, r2, r3, r4⟩ := x; try step*)
      | (guard_hyp x :~ _ × _ × _; obtain ⟨r1, r2, r3⟩ := x; try step*)
      | (guard_hyp x :~ _ × _; obtain ⟨r1, r2⟩ := x; try step*)
      | (apply spec_ite_cut <;> intro hc <;> try step*)
      | (apply Std.WP.spec_bind (Pₘ := fun _ => True))
      | (intro y _; repeat (obtain ⟨_, y⟩ : _ × _ := y); try step*))
    all_goals scalar_tac
  · trivial

@[local step]
theorem entropy256_spec (h : Array Std.U32 256#usize) :
    slot.a_entropy256 h ⦃ fun _ => True ⦄ := by
  rw [slot.a_entropy256]
  step*
  repeat (first
    | (intro hc; (try step*))
    | (split <;> (try step*))
    | (guard_hyp x :~ _ × _ × _ × _ × _ × _; obtain ⟨r1, r2, r3, r4, r5, r6⟩ := x; try step*)
    | (guard_hyp x :~ _ × _ × _ × _ × _; obtain ⟨r1, r2, r3, r4, r5⟩ := x; try step*)
    | (guard_hyp x :~ _ × _ × _ × _; obtain ⟨r1, r2, r3, r4⟩ := x; try step*)
    | (guard_hyp x :~ _ × _ × _; obtain ⟨r1, r2, r3⟩ := x; try step*)
    | (guard_hyp x :~ _ × _; obtain ⟨r1, r2⟩ := x; try step*)
    | (apply spec_ite_cut <;> intro hc <;> try step*)
    | (apply Std.WP.spec_bind (Pₘ := fun _ => True))
    | (intro y _; repeat (obtain ⟨_, y⟩ : _ × _ := y); try step*))
  all_goals scalar_tac

@[local step]
theorem share_loop_spec (h : Array Std.U32 256#usize) (lo : Std.Usize) (hi : Std.Usize) (t : Std.Usize) (s : Std.Usize) (i : Std.Usize)  :
    slot.a_share_loop h lo hi t s i ⦃ fun _ => True ⦄ := by
  rw [slot.a_share_loop]
  apply Std.loop.spec_decr_nat
    (measure := fun s => 256 - s.2.2.val)
    (inv := fun s => True)
  · rintro ⟨x0, x1, x2⟩ _
    simp only [slot.a_share_loop.body, lift, Array.to_slice_mut]
    step*
    repeat (first
      | (intro hc; (try step*))
      | (split <;> (try step*))
      | (guard_hyp x :~ _ × _ × _ × _ × _ × _; obtain ⟨r1, r2, r3, r4, r5, r6⟩ := x; try step*)
      | (guard_hyp x :~ _ × _ × _ × _ × _; obtain ⟨r1, r2, r3, r4, r5⟩ := x; try step*)
      | (guard_hyp x :~ _ × _ × _ × _; obtain ⟨r1, r2, r3, r4⟩ := x; try step*)
      | (guard_hyp x :~ _ × _ × _; obtain ⟨r1, r2, r3⟩ := x; try step*)
      | (guard_hyp x :~ _ × _; obtain ⟨r1, r2⟩ := x; try step*)
      | (apply spec_ite_cut <;> intro hc <;> try step*)
      | (apply Std.WP.spec_bind (Pₘ := fun _ => True))
      | (intro y _; repeat (obtain ⟨_, y⟩ : _ × _ := y); try step*))
    all_goals scalar_tac
  · trivial

@[local step]
theorem share_spec (h : Array Std.U32 256#usize) (lo : Std.Usize) (hi : Std.Usize) :
    slot.a_share h lo hi ⦃ fun _ => True ⦄ := by
  rw [slot.a_share]
  try simp only [lift, Array.to_slice_mut]
  step*
  repeat (first
    | (intro hc; (try step*))
    | (split <;> (try step*))
    | (guard_hyp x :~ _ × _ × _ × _ × _ × _; obtain ⟨r1, r2, r3, r4, r5, r6⟩ := x; try step*)
    | (guard_hyp x :~ _ × _ × _ × _ × _; obtain ⟨r1, r2, r3, r4, r5⟩ := x; try step*)
    | (guard_hyp x :~ _ × _ × _ × _; obtain ⟨r1, r2, r3, r4⟩ := x; try step*)
    | (guard_hyp x :~ _ × _ × _; obtain ⟨r1, r2, r3⟩ := x; try step*)
    | (guard_hyp x :~ _ × _; obtain ⟨r1, r2⟩ := x; try step*)
    | (apply spec_ite_cut <;> intro hc <;> try step*)
    | (apply Std.WP.spec_bind (Pₘ := fun _ => True))
    | (intro y _; repeat (obtain ⟨_, y⟩ : _ × _ := y); try step*))
  all_goals scalar_tac

@[local step]
theorem low_mode_spec (e : Std.Usize) :
    slot.a_low_mode e ⦃ fun _ => True ⦄ := by
  rw [slot.a_low_mode]
  step*
  repeat (first
    | (intro hc; (try step*))
    | (split <;> (try step*))
    | (guard_hyp x :~ _ × _ × _ × _ × _ × _; obtain ⟨r1, r2, r3, r4, r5, r6⟩ := x; try step*)
    | (guard_hyp x :~ _ × _ × _ × _ × _; obtain ⟨r1, r2, r3, r4, r5⟩ := x; try step*)
    | (guard_hyp x :~ _ × _ × _ × _; obtain ⟨r1, r2, r3, r4⟩ := x; try step*)
    | (guard_hyp x :~ _ × _ × _; obtain ⟨r1, r2, r3⟩ := x; try step*)
    | (guard_hyp x :~ _ × _; obtain ⟨r1, r2⟩ := x; try step*)
    | (apply spec_ite_cut <;> intro hc <;> try step*)
    | (apply Std.WP.spec_bind (Pₘ := fun _ => True))
    | (intro y _; repeat (obtain ⟨_, y⟩ : _ × _ := y); try step*))
  all_goals scalar_tac

@[local step]
theorem lit_cost_spec (e : Std.Usize) (low : Std.Usize) :
    slot.a_lit_cost e low ⦃ fun _ => True ⦄ := by
  rw [slot.a_lit_cost]
  try simp only [lift, Array.to_slice_mut]
  step*
  repeat (first
    | (intro hc; (try step*))
    | (split <;> (try step*))
    | (guard_hyp x :~ _ × _ × _ × _ × _ × _; obtain ⟨r1, r2, r3, r4, r5, r6⟩ := x; try step*)
    | (guard_hyp x :~ _ × _ × _ × _ × _; obtain ⟨r1, r2, r3, r4, r5⟩ := x; try step*)
    | (guard_hyp x :~ _ × _ × _ × _; obtain ⟨r1, r2, r3, r4⟩ := x; try step*)
    | (guard_hyp x :~ _ × _ × _; obtain ⟨r1, r2, r3⟩ := x; try step*)
    | (guard_hyp x :~ _ × _; obtain ⟨r1, r2⟩ := x; try step*)
    | (apply spec_ite_cut <;> intro hc <;> try step*)
    | (apply Std.WP.spec_bind (Pₘ := fun _ => True))
    | (intro y _; repeat (obtain ⟨_, y⟩ : _ × _ := y); try step*))
  all_goals scalar_tac

@[local step]
theorem m3_mode_spec (h : Array Std.U32 256#usize) (e : Std.Usize) :
    slot.a_m3_mode h e ⦃ fun _ => True ⦄ := by
  rw [slot.a_m3_mode]
  step*
  repeat (first
    | (intro hc; (try step*))
    | (split <;> (try step*))
    | (guard_hyp x :~ _ × _ × _ × _ × _ × _; obtain ⟨r1, r2, r3, r4, r5, r6⟩ := x; try step*)
    | (guard_hyp x :~ _ × _ × _ × _ × _; obtain ⟨r1, r2, r3, r4, r5⟩ := x; try step*)
    | (guard_hyp x :~ _ × _ × _ × _; obtain ⟨r1, r2, r3, r4⟩ := x; try step*)
    | (guard_hyp x :~ _ × _ × _; obtain ⟨r1, r2, r3⟩ := x; try step*)
    | (guard_hyp x :~ _ × _; obtain ⟨r1, r2⟩ := x; try step*)
    | (apply spec_ite_cut <;> intro hc <;> try step*)
    | (apply Std.WP.spec_bind (Pₘ := fun _ => True))
    | (intro y _; repeat (obtain ⟨_, y⟩ : _ × _ := y); try step*))
  all_goals scalar_tac

@[local step]
theorem h3_mode_spec (h : Array Std.U32 256#usize) (e : Std.Usize) :
    slot.a_h3_mode h e ⦃ fun _ => True ⦄ := by
  rw [slot.a_h3_mode]
  try simp only [lift, Array.to_slice_mut]
  step*
  repeat (first
    | (intro hc; (try step*))
    | (split <;> (try step*))
    | (guard_hyp x :~ _ × _ × _ × _ × _ × _; obtain ⟨r1, r2, r3, r4, r5, r6⟩ := x; try step*)
    | (guard_hyp x :~ _ × _ × _ × _ × _; obtain ⟨r1, r2, r3, r4, r5⟩ := x; try step*)
    | (guard_hyp x :~ _ × _ × _ × _; obtain ⟨r1, r2, r3, r4⟩ := x; try step*)
    | (guard_hyp x :~ _ × _ × _; obtain ⟨r1, r2, r3⟩ := x; try step*)
    | (guard_hyp x :~ _ × _; obtain ⟨r1, r2⟩ := x; try step*)
    | (apply spec_ite_cut <;> intro hc <;> try step*)
    | (apply Std.WP.spec_bind (Pₘ := fun _ => True))
    | (intro y _; repeat (obtain ⟨_, y⟩ : _ × _ := y); try step*))
  all_goals scalar_tac

@[local step]
theorem numeric_spec (h : Array Std.U32 256#usize) (n : Std.Usize) (low : Std.Usize) :
    slot.a_numeric h n low ⦃ fun _ => True ⦄ := by
  rw [slot.a_numeric]
  try simp only [lift, Array.to_slice_mut]
  step*
  repeat (first
    | (intro hc; (try step*))
    | (split <;> (try step*))
    | (guard_hyp x :~ _ × _ × _ × _ × _ × _; obtain ⟨r1, r2, r3, r4, r5, r6⟩ := x; try step*)
    | (guard_hyp x :~ _ × _ × _ × _ × _; obtain ⟨r1, r2, r3, r4, r5⟩ := x; try step*)
    | (guard_hyp x :~ _ × _ × _ × _; obtain ⟨r1, r2, r3, r4⟩ := x; try step*)
    | (guard_hyp x :~ _ × _ × _; obtain ⟨r1, r2, r3⟩ := x; try step*)
    | (guard_hyp x :~ _ × _; obtain ⟨r1, r2⟩ := x; try step*)