From 9418517dc9ae65602e089f10a9a1816f1e5416c0 Mon Sep 17 00:00:00 2001 From: Brooklyn Zelenka Date: Fri, 12 Jun 2026 17:31:35 -0700 Subject: [PATCH 1/2] Basic specs --- .github/workflows/lean-proofs.yml | 38 +++++ .gitignore | 3 + README.md | 24 +++- flake.nix | 56 ++++++-- lean/Bijou.lean | 29 ++++ lean/Bijou/Bytes.lean | 161 +++++++++++++++++++++ lean/Bijou/Canonical.lean | 133 +++++++++++++++++ lean/Bijou/Family.lean | 228 ++++++++++++++++++++++++++++++ lean/Bijou/Instances.lean | 134 ++++++++++++++++++ lean/Bijou/Order.lean | 67 +++++++++ lean/Bijou/RoundTrip.lean | 49 +++++++ lean/Bijou/Spec.lean | 96 +++++++++++++ lean/lake-manifest.json | 5 + lean/lakefile.toml | 6 + lean/lean-toolchain | 1 + 15 files changed, 1021 insertions(+), 9 deletions(-) create mode 100644 .github/workflows/lean-proofs.yml create mode 100644 lean/Bijou.lean create mode 100644 lean/Bijou/Bytes.lean create mode 100644 lean/Bijou/Canonical.lean create mode 100644 lean/Bijou/Family.lean create mode 100644 lean/Bijou/Instances.lean create mode 100644 lean/Bijou/Order.lean create mode 100644 lean/Bijou/RoundTrip.lean create mode 100644 lean/Bijou/Spec.lean create mode 100644 lean/lake-manifest.json create mode 100644 lean/lakefile.toml create mode 100644 lean/lean-toolchain diff --git a/.github/workflows/lean-proofs.yml b/.github/workflows/lean-proofs.yml new file mode 100644 index 0000000..66698a2 --- /dev/null +++ b/.github/workflows/lean-proofs.yml @@ -0,0 +1,38 @@ +name: Lean Proofs + +# Checks the formal proofs in `lean/` via the flake's hermetic +# `lean-proofs` check. The proofs cover round-trip, canonicality +# (bijectivity by construction), and lexicographic order preservation +# for the whole bijou family, plus every SPEC test vector. + +on: + push: + branches: + - main + pull_request: + +concurrency: + group: ${{ github.workflow }}-${{ github.ref }} + cancel-in-progress: true + +jobs: + lean-proofs: + runs-on: ubuntu-latest + steps: + - uses: actions/checkout@v4 + + - name: Install Nix + uses: DeterminateSystems/nix-installer-action@v21 + + - name: Setup Nix cache + uses: DeterminateSystems/magic-nix-cache-action@v13 + + - name: Setup Cachix + uses: cachix/cachix-action@v15 + if: ${{ !github.event.pull_request.head.repo.fork }} + with: + name: inkandswitch + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + + - name: Build lean-proofs flake check + run: nix build .#checks.x86_64-linux.lean-proofs --print-build-logs diff --git a/.gitignore b/.gitignore index a3eb111..9063e6f 100644 --- a/.gitignore +++ b/.gitignore @@ -16,6 +16,9 @@ rust_out # nix direnv .direnv +# lean / lake build artifacts +/lean/.lake/ + # wasm / npm artifacts **/dist/ **/node_modules/ diff --git a/README.md b/README.md index f18e569..49939b3 100644 --- a/README.md +++ b/README.md @@ -68,9 +68,10 @@ toolchain and dev tooling. nix develop # enter the dev shell (prints a command menu) build # cargo build --workspace test # cargo test --workspace -ci # fmt + clippy + test + no_std + wasm32 +ci # fmt + clippy + test + no_std + wasm32 + Lean proofs bench:shootout # criterion shootout vs other varints bench:gungraun # gungraun instruction-count benchmarks +proofs # check the Lean 4 proofs in lean/ ``` Without Nix: @@ -84,6 +85,27 @@ The workspace targets stable Rust (see `rust-version` in `Cargo.toml`) and supports `wasm32-unknown-unknown` via the toolchain shipped in the flake. +## Formal proofs + +The [`lean/`](./lean) directory contains a Lean 4 model of the format, +parametrized over the tier count so one development covers all three +width variants. Machine-checked theorems include: + +- _Round-trip_: decoding an encoding returns the original value. +- _Canonicality by construction_: any byte string the decoder accepts + is exactly the canonical encoding of the value it returns — there is + no overlong encoding to reject. +- _Bijectivity_: `encode` is injective, and fully-consumed buffers + decoding to the same value are identical. +- _Order preservation_: lexicographic byte order equals numeric order. + +Every test vector in the three `SPEC.md` documents is also checked by +reduction. Run the proofs with `proofs` inside the dev shell, or +hermetically via `nix build .#checks..lean-proofs`. The proofs +describe the specified format, not the Rust implementation; the Rust +crates are checked against the same SPEC vectors and property-tested +with `bolero`. + ## Other implementations The community has ported the `bijou64` wire format to several languages and ecosystems. These are diff --git a/flake.nix b/flake.nix index f2640f8..107a6a5 100644 --- a/flake.nix +++ b/flake.nix @@ -177,6 +177,28 @@ wasm = command-utils.wasm.${system}; cmd = command-utils.cmd.${system}; + # Lean 4 toolchain for the formal proofs in `lean/`. Taken from + # nixos-unstable for a recent compiler; `lean/lean-toolchain` is + # pinned to the same version so elan users (non-Nix contributors) + # get an identical toolchain. + lean4 = unstable.lean4; + + # Hermetic proof check. The Lean project has no external Lake + # dependencies (no Mathlib), so `lake build` works in the Nix + # sandbox without vendoring. + lean-proofs = pkgs.stdenv.mkDerivation { + name = "bijou-lean-proofs"; + src = ./lean; + nativeBuildInputs = [ lean4 ]; + + buildPhase = '' + export HOME="$TMPDIR" + lake build + ''; + + installPhase = "touch $out"; + }; + # Python environment for benchmark chart generation (analyze.py) bench-charts-python = pkgs.python3.withPackages (ps: [ ps.matplotlib @@ -445,50 +467,62 @@ ${pkgs.pnpm}/bin/pnpm exec playwright show-report ''; - "ci" = cmd "Run full CI suite (fmt, clippy, test, no_std, wasm32, wasm-pack, JS package)" '' + "proofs" = cmd "Check the Lean 4 proofs in lean/" '' set -e + cd "$WORKSPACE_ROOT/lean" + ${lean4}/bin/lake build + echo "" + echo "✓ Lean proofs OK" + ''; - echo "===> [1/7] Checking formatting..." + "ci" = cmd "Run full CI suite (fmt, clippy, test, no_std, wasm32, wasm-pack, JS package, Lean proofs)" '' + set -e + + echo "===> [1/8] Checking formatting..." ${pkgs.cargo}/bin/cargo fmt --check echo "✓ Formatting OK" echo "" - echo "===> [2/7] Running Clippy..." + echo "===> [2/8] Running Clippy..." ${pkgs.cargo}/bin/cargo clippy --workspace --all-targets --all-features -- -D warnings echo "✓ Clippy OK" echo "" - echo "===> [3/7] Running host tests..." + echo "===> [3/8] Running host tests..." ${pkgs.cargo}/bin/cargo test --workspace --all-features echo "✓ Host tests OK" echo "" - echo "===> [4/7] Checking no_std..." + echo "===> [4/8] Checking no_std..." ${pkgs.cargo}/bin/cargo check --package bijou32 --no-default-features ${pkgs.cargo}/bin/cargo check --package bijou64 --no-default-features ${pkgs.cargo}/bin/cargo check --package bijou128 --no-default-features echo "✓ no_std OK" echo "" - echo "===> [5/7] Checking wasm32 build..." + echo "===> [5/8] Checking wasm32 build..." ${pkgs.cargo}/bin/cargo check --workspace --target wasm32-unknown-unknown echo "✓ wasm32 OK" echo "" - echo "===> [6/7] Running wasm-pack tests in Node.js..." + echo "===> [6/8] Running wasm-pack tests in Node.js..." ${pkgs.wasm-pack}/bin/wasm-pack test --node bijou32_wasm ${pkgs.wasm-pack}/bin/wasm-pack test --node bijou64_wasm ${pkgs.wasm-pack}/bin/wasm-pack test --node bijou128_wasm echo "✓ wasm-pack tests OK" echo "" - echo "===> [7/7] Running JS-package tests (Node + browsers)..." + echo "===> [7/8] Running JS-package tests (Node + browsers)..." "test:js:32" "test:js" "test:js:128" echo "✓ JS-package tests OK" echo "" + echo "===> [8/8] Checking Lean proofs..." + proofs + echo "" + echo "✓ All CI checks passed" ''; }; @@ -533,6 +567,10 @@ inherit gungraun-runner wasm-bodge; }; + checks = { + inherit lean-proofs; + }; + devShells.default = pkgs.mkShell { name = "bijou_shell"; @@ -545,6 +583,8 @@ rust-toolchain nightly-rustfmt + lean4 # Lean 4 + lake, for the formal proofs in lean/ + pkgs.binaryen pkgs.esbuild # wasm-bodge spawns esbuild as a subprocess for bundling pkgs.gnuplot diff --git a/lean/Bijou.lean b/lean/Bijou.lean new file mode 100644 index 0000000..75e578e --- /dev/null +++ b/lean/Bijou.lean @@ -0,0 +1,29 @@ +import Bijou.Bytes +import Bijou.Canonical +import Bijou.Family +import Bijou.Instances +import Bijou.Order +import Bijou.RoundTrip +import Bijou.Spec + +/-! +# Bijou: machine-checked format proofs + +A Lean 4 model of the bijou family of bijective variable-length +integer encodings, parametrized over the tier count so that one +development covers `bijou32`, `bijou64`, and `bijou128`. + +Headline theorems (all in `Bijou.Family`): + +- `decode_encode` — round-trip: decoding an encoding returns the + original value, with or without trailing bytes. +- `decode_ok` — canonicality by construction: any byte string the + decoder accepts is exactly `encode` of the returned value. There is + no overlong encoding to reject. +- `encode_injective` / `decode_canonical` — `encode` is a bijection + between `[0, 256 ^ tiers)` and the accepted byte strings. +- `encode_lex_iff` — lexicographic byte order equals numeric order. + +`Bijou.Instances` instantiates the three specified variants and checks +every test vector from the SPEC documents by reduction. +-/ diff --git a/lean/Bijou/Bytes.lean b/lean/Bijou/Bytes.lean new file mode 100644 index 0000000..4989d9f --- /dev/null +++ b/lean/Bijou/Bytes.lean @@ -0,0 +1,161 @@ +/-! +# Big-endian byte strings + +Fixed-width big-endian encoding of natural numbers, its inverse, and a +strict lexicographic order on byte strings. + +bijou payloads are big-endian so that lexicographic byte comparison +agrees with numeric comparison; the key fact is `beBytes_lex_beBytes`. + +Bytes are modelled as `Nat` with explicit `< 256` hypotheses where +required, which keeps every side condition within `omega`'s reach. +-/ + +namespace Bijou + +/-- The `w`-byte big-endian representation of `n`, most significant byte +first. Truncates if `n ≥ 256 ^ w`; callers establish the bound. -/ +def beBytes : Nat → Nat → List Nat + | 0, _ => [] + | w + 1, n => n / 256 ^ w :: beBytes w (n % 256 ^ w) + +/-- Interpret a byte string as a big-endian natural number. -/ +def fromBe : List Nat → Nat + | [] => 0 + | b :: bs => b * 256 ^ bs.length + fromBe bs + +@[simp] +theorem beBytes_length (w n : Nat) : (beBytes w n).length = w := by + induction w generalizing n with + | zero => rfl + | succ w ih => simp [beBytes, ih] + +theorem beBytes_lt_256 {w n : Nat} (h : n < 256 ^ w) : + ∀ b ∈ beBytes w n, b < 256 := by + induction w generalizing n with + | zero => simp [beBytes] + | succ w ih => + intro b hb + have hpos : 0 < 256 ^ w := Nat.pow_pos (by omega) + simp only [beBytes, List.mem_cons] at hb + cases hb with + | inl hhead => + subst hhead + have hpow : 256 ^ (w + 1) = 256 ^ w * 256 := by rw [Nat.pow_succ] + exact Nat.div_lt_of_lt_mul (by omega) + | inr htail => exact ih (Nat.mod_lt n hpos) b htail + +/-- Decoding inverts encoding: `fromBe ∘ beBytes w` is the identity on +`[0, 256 ^ w)`. -/ +theorem fromBe_beBytes {w n : Nat} (h : n < 256 ^ w) : + fromBe (beBytes w n) = n := by + induction w generalizing n with + | zero => + simp only [beBytes, fromBe] + omega + | succ w ih => + have hpos : 0 < 256 ^ w := Nat.pow_pos (by omega) + simp only [beBytes, fromBe, beBytes_length, ih (Nat.mod_lt n hpos)] + rw [Nat.mul_comm] + exact Nat.div_add_mod n (256 ^ w) + +theorem fromBe_lt {bs : List Nat} (h : ∀ b ∈ bs, b < 256) : + fromBe bs < 256 ^ bs.length := by + induction bs with + | nil => simp [fromBe] + | cons b bs ih => + have hb : b < 256 := h b (List.mem_cons_self ..) + have hr : fromBe bs < 256 ^ bs.length := + ih fun x hx => h x (List.mem_cons_of_mem _ hx) + have hpow : 256 ^ (bs.length + 1) = 256 ^ bs.length * 256 := by rw [Nat.pow_succ] + have hmul : (b + 1) * 256 ^ bs.length ≤ 256 * 256 ^ bs.length := + Nat.mul_le_mul (by omega) (Nat.le_refl _) + simp only [fromBe, List.length_cons] + have hsucc : (b + 1) * 256 ^ bs.length = b * 256 ^ bs.length + 256 ^ bs.length := by + rw [Nat.succ_mul] + omega + +/-- Encoding inverts decoding: every `w`-byte string is the encoding of +its value. This is the structural-canonicality workhorse. -/ +theorem beBytes_fromBe {bs : List Nat} (h : ∀ b ∈ bs, b < 256) : + beBytes bs.length (fromBe bs) = bs := by + induction bs with + | nil => rfl + | cons b bs ih => + have hr : fromBe bs < 256 ^ bs.length := + fromBe_lt fun x hx => h x (List.mem_cons_of_mem _ hx) + have hpos : 0 < 256 ^ bs.length := Nat.pow_pos (by omega) + have hdiv : (fromBe bs + b * 256 ^ bs.length) / 256 ^ bs.length = b := by + rw [Nat.add_mul_div_right _ _ hpos, Nat.div_eq_of_lt hr, Nat.zero_add] + have hmod : (fromBe bs + b * 256 ^ bs.length) % 256 ^ bs.length = fromBe bs := by + rw [Nat.add_mul_mod_self_right, Nat.mod_eq_of_lt hr] + simp only [List.length_cons, beBytes, fromBe, Nat.add_comm (b * 256 ^ bs.length), + hdiv, hmod, ih fun x hx => h x (List.mem_cons_of_mem _ hx)] + +theorem take_append_length (as bs : List α) : (as ++ bs).take as.length = as := by + induction as with + | nil => rfl + | cons a as ih => simp [List.take_succ_cons, ih] + +theorem mem_of_mem_take {l : List α} {n : Nat} {a : α} (h : a ∈ l.take n) : a ∈ l := by + induction l generalizing n with + | nil => simp at h + | cons x xs ih => + cases n with + | zero => simp at h + | succ n => + simp only [List.take_succ_cons, List.mem_cons] at h + cases h with + | inl h => simp [h] + | inr h => exact List.mem_cons_of_mem _ (ih h) + +/-- Strict lexicographic order on byte strings. -/ +inductive Lex : List Nat → List Nat → Prop + | nil {b : Nat} {bs : List Nat} : Lex [] (b :: bs) + | head {a b : Nat} {as bs : List Nat} : a < b → Lex (a :: as) (b :: bs) + | tail {a : Nat} {as bs : List Nat} : Lex as bs → Lex (a :: as) (a :: bs) + +theorem Lex.irrefl : ∀ (bs : List Nat), ¬Lex bs bs := by + intro bs h + induction bs with + | nil => cases h + | cons b bs ih => + cases h with + | head h => omega + | tail h => exact ih h + +theorem Lex.asymm {as bs : List Nat} (h : Lex as bs) : ¬Lex bs as := by + induction h with + | nil => intro h2; cases h2 + | head h => + intro h2 + cases h2 with + | head h2 => omega + | tail _ => omega + | tail h ih => + intro h2 + cases h2 with + | head h2 => omega + | tail h2 => exact ih h2 + +/-- Big-endian encoding is strictly monotone with respect to +lexicographic order: numeric order and byte order agree. -/ +theorem beBytes_lex_beBytes {w m n : Nat} (hn : n < 256 ^ w) (h : m < n) : + Lex (beBytes w m) (beBytes w n) := by + induction w generalizing m n with + | zero => + simp only [Nat.pow_zero] at hn + omega + | succ w ih => + have hpos : 0 < 256 ^ w := Nat.pow_pos (by omega) + have hdm := Nat.div_add_mod m (256 ^ w) + have hdn := Nat.div_add_mod n (256 ^ w) + have hle : m / 256 ^ w ≤ n / 256 ^ w := Nat.div_le_div_right (Nat.le_of_lt h) + simp only [beBytes] + by_cases hd : m / 256 ^ w = n / 256 ^ w + · rw [hd] + rw [hd] at hdm + exact Lex.tail (ih (Nat.mod_lt n hpos) (by omega)) + · exact Lex.head (by omega) + +end Bijou diff --git a/lean/Bijou/Canonical.lean b/lean/Bijou/Canonical.lean new file mode 100644 index 0000000..176dc5f --- /dev/null +++ b/lean/Bijou/Canonical.lean @@ -0,0 +1,133 @@ +import Bijou.RoundTrip + +/-! +# Canonicality, by construction + +The SPEC's defining claim: every value has exactly one encoding, and +every byte string the decoder accepts *is* the canonical encoding of +the value it returns. There are no overlong encodings to reject — the +per-tier offset arithmetic makes them unrepresentable. + +- `decode_ok`: anything the decoder accepts is, byte for byte, the + output of `encode` (and the value is in range). +- `encode_injective`: distinct values have distinct encodings. +- `decode_canonical`: two fully-consumed buffers decoding to the same + value are equal. +-/ + +namespace Bijou.Family + +variable (F : Family) + +/-- If `decode bs = ok (v, n)` then the `n` bytes consumed are exactly +`encode v`: the decoder only ever accepts canonical encodings. -/ +theorem decode_ok {bs : List Nat} {v n : Nat} + (hbytes : ∀ b ∈ bs, b < 256) + (h : F.decode bs = .ok (v, n)) : + v < 256 ^ F.tiers ∧ n = F.encodedLen v ∧ bs.take n = F.encode v := by + match bs with + | [] => simp [decode] at h + | tag :: rest => + simp only [decode] at h + by_cases htag : tag < F.threshold + · rw [if_pos htag] at h + simp only [Except.ok.injEq, Prod.mk.injEq] at h + have hv : tag = v := h.1 + have hn : 1 = n := h.2 + subst hv + subst hn + have h256 := F.le_pow_tiers + have hthr := F.threshold_lt + refine ⟨by omega, ?_, ?_⟩ + · simp [encodedLen, htag] + · simp [encode, htag] + · rw [if_neg htag] at h + by_cases hlen : tag - F.threshold + 1 ≤ rest.length + · rw [if_pos hlen] at h + by_cases hov : + F.offset (tag - F.threshold + 1) + + fromBe (rest.take (tag - F.threshold + 1)) + < 256 ^ F.tiers + · rw [if_pos hov] at h + simp only [Except.ok.injEq, Prod.mk.injEq] at h + have hv := h.1 + have hn := h.2 + subst hv + subst hn + -- Abbreviations (as facts, since `set` is unavailable). + have htlen : (rest.take (tag - F.threshold + 1)).length + = tag - F.threshold + 1 := by + simp only [List.length_take] + omega + have hpb : ∀ b ∈ rest.take (tag - F.threshold + 1), b < 256 := fun b hb => + hbytes b (List.mem_cons_of_mem _ (mem_of_mem_take hb)) + have hpay : fromBe (rest.take (tag - F.threshold + 1)) + < 256 ^ (tag - F.threshold + 1) := by + have h' := fromBe_lt hpb + rwa [htlen] at h' + -- The value lands inside tier `tag - threshold + 1`. + have hub : F.offset (tag - F.threshold + 1) + + fromBe (rest.take (tag - F.threshold + 1)) + < F.offset (tag - F.threshold + 1 + 1) := by + rw [F.offset_succ (tag - F.threshold + 1), + F.capacity_eq_pow (show 0 < tag - F.threshold + 1 by omega)] + omega + -- The accepted tier is the tier of the value. + have htier : F.tierOf + (F.offset (tag - F.threshold + 1) + + fromBe (rest.take (tag - F.threshold + 1))) + = tag - F.threshold + 1 := + F.tierOf_eq hov (Nat.le_add_right _ _) hub + -- The value is multi-byte: at or above the threshold. + have hge : F.threshold + ≤ F.offset (tag - F.threshold + 1) + + fromBe (rest.take (tag - F.threshold + 1)) := by + have h1 : F.offset 1 ≤ F.offset (tag - F.threshold + 1) := + F.offset_le_offset (by omega) + rw [F.offset_one] at h1 + omega + have hnlt : ¬(F.offset (tag - F.threshold + 1) + + fromBe (rest.take (tag - F.threshold + 1)) + < F.threshold) := by omega + refine ⟨hov, ?_, ?_⟩ + · simp only [encodedLen, if_neg hnlt, htier] + · simp only [encode, if_neg hnlt, htier] + have htag' : tag - F.threshold + 2 = (tag - F.threshold + 1) + 1 := by omega + rw [htag', List.take_succ_cons] + have hhead : F.threshold + (tag - F.threshold + 1 - 1) = tag := by omega + have hsub : F.offset (tag - F.threshold + 1) + + fromBe (rest.take (tag - F.threshold + 1)) + - F.offset (tag - F.threshold + 1) + = fromBe (rest.take (tag - F.threshold + 1)) := by omega + rw [hhead, hsub] + have hbe := beBytes_fromBe hpb + rw [htlen] at hbe + rw [hbe] + · rw [if_neg hov] at h + simp at h + · rw [if_neg hlen] at h + simp at h + +/-- Distinct values never share an encoding. -/ +theorem encode_injective {v₁ v₂ : Nat} + (h₁ : v₁ < 256 ^ F.tiers) (h₂ : v₂ < 256 ^ F.tiers) + (h : F.encode v₁ = F.encode v₂) : v₁ = v₂ := by + have d₁ := F.decode_encode' h₁ + have d₂ := F.decode_encode' h₂ + rw [h, d₂] at d₁ + simp only [Except.ok.injEq, Prod.mk.injEq] at d₁ + exact d₁.1.symm + +/-- Two fully-consumed valid buffers decoding to the same value are +identical: there is exactly one byte representation per value. -/ +theorem decode_canonical {bs₁ bs₂ : List Nat} {v : Nat} + (hb₁ : ∀ b ∈ bs₁, b < 256) (hb₂ : ∀ b ∈ bs₂, b < 256) + (h₁ : F.decode bs₁ = .ok (v, bs₁.length)) + (h₂ : F.decode bs₂ = .ok (v, bs₂.length)) : + bs₁ = bs₂ := by + have c₁ := (F.decode_ok hb₁ h₁).2.2 + have c₂ := (F.decode_ok hb₂ h₂).2.2 + rw [List.take_length] at c₁ c₂ + rw [c₁, c₂] + +end Bijou.Family diff --git a/lean/Bijou/Family.lean b/lean/Bijou/Family.lean new file mode 100644 index 0000000..3a4ff45 --- /dev/null +++ b/lean/Bijou/Family.lean @@ -0,0 +1,228 @@ +/-! +# The bijou format family + +A bijou format is determined by a single parameter: the number of +multi-byte tiers. The tag-byte threshold is derived (`256 - tiers`), +so the multi-byte tags exactly fill the top of the byte range, and the +value domain is `[0, 256 ^ tiers)`. + +| Variant | tiers | threshold | domain | +|----------|-------|-----------|-------------| +| bijou32 | 4 | 252 | `[0, 2^32)` | +| bijou64 | 8 | 248 | `[0, 2^64)` | +| bijou128 | 16 | 240 | `[0, 2^128)`| + +Each tier `t ≥ 1` carries `256 ^ t` values starting at `offset t`, and +tier 0 (single byte) carries values `0 .. threshold - 1`. The offsets +tile the naturals contiguously, which is what makes the encoding +bijective: there is exactly one tier for every value. +-/ + +namespace Bijou + +/-- A bijou format family, parametrized by the number of multi-byte +tiers (4 for bijou32, 8 for bijou64, 16 for bijou128). -/ +structure Family where + /-- Number of multi-byte tiers. -/ + tiers : Nat + tiers_pos : 0 < tiers + tiers_lt : tiers < 256 + +namespace Family + +variable (F : Family) + +/-- Tag-byte threshold: values below this encode as a single byte, and +tags `threshold .. 255` introduce tiers `1 .. tiers`. -/ +def threshold : Nat := 256 - F.tiers + +theorem threshold_pos : 0 < F.threshold := by + have := F.tiers_lt + simp only [threshold] + omega + +theorem threshold_lt : F.threshold < 256 := by + have := F.tiers_pos + simp only [threshold] + omega + +/-- Number of values representable by tier `t` alone. -/ +def capacity : Nat → Nat + | 0 => F.threshold + | t + 1 => 256 ^ (t + 1) + +theorem capacity_pos (t : Nat) : 0 < F.capacity t := by + cases t with + | zero => exact F.threshold_pos + | succ t => exact Nat.pow_pos (by omega) + +theorem capacity_eq_pow {t : Nat} (h : 0 < t) : F.capacity t = 256 ^ t := by + cases t with + | zero => omega + | succ t => rfl + +/-- First value requiring tier `t`: the cumulative capacity of all +previous tiers. This is the SPEC's `OFFSET` table. -/ +def offset : Nat → Nat + | 0 => 0 + | t + 1 => offset t + F.capacity t + +@[simp] +theorem offset_zero : F.offset 0 = 0 := rfl + +theorem offset_succ (t : Nat) : F.offset (t + 1) = F.offset t + F.capacity t := rfl + +theorem offset_one : F.offset 1 = F.threshold := by + simp [offset, capacity] + +theorem offset_lt_succ (t : Nat) : F.offset t < F.offset (t + 1) := by + have := F.capacity_pos t + rw [offset_succ] + omega + +theorem offset_le_offset {s t : Nat} (h : s ≤ t) : F.offset s ≤ F.offset t := by + induction h with + | refl => exact Nat.le_refl _ + | step _ ih => exact Nat.le_trans ih (Nat.le_of_lt (F.offset_lt_succ _)) + +theorem offset_lt_offset {s t : Nat} (h : s < t) : F.offset s < F.offset t := + Nat.lt_of_lt_of_le (F.offset_lt_succ s) (F.offset_le_offset h) + +/-- Offsets stay strictly below the tier's own capacity ceiling, so +every tier has room: `offset t ≤ v < offset t + 256 ^ t` is satisfiable +for all `t ≥ 1`. -/ +theorem offset_lt_pow : ∀ {t : Nat}, 0 < t → F.offset t < 256 ^ t := by + intro t + induction t with + | zero => omega + | succ t ih => + intro _ + cases Nat.eq_zero_or_pos t with + | inl h0 => + subst h0 + have := F.threshold_lt + rw [F.offset_one, Nat.pow_one] + omega + | inr hpos => + have ih' := ih hpos + have hx : 0 < 256 ^ t := Nat.pow_pos (by omega) + have hpow : 256 ^ (t + 1) = 256 ^ t * 256 := by rw [Nat.pow_succ] + rw [F.offset_succ, F.capacity_eq_pow hpos] + omega + +/-- Tiers beyond `tiers` start past the value domain; the decoder's +overflow check rejects them with no special-casing. -/ +theorem pow_le_offset {t : Nat} (h : F.tiers < t) : 256 ^ F.tiers ≤ F.offset t := by + have h1 : 256 ^ F.tiers ≤ F.offset (F.tiers + 1) := by + rw [F.offset_succ, F.capacity_eq_pow F.tiers_pos] + omega + exact Nat.le_trans h1 (F.offset_le_offset h) + +theorem le_pow_tiers : 256 ≤ 256 ^ F.tiers := by + have h := F.tiers_pos + cases ht : F.tiers with + | zero => omega + | succ t => + have hx : 0 < 256 ^ t := Nat.pow_pos (by omega) + have hpow : 256 ^ (t + 1) = 256 ^ t * 256 := by rw [Nat.pow_succ] + omega + +/-- Largest tier `s ≤ t` whose offset is at most `v`. -/ +def tierSearch (v : Nat) : Nat → Nat + | 0 => 0 + | t + 1 => if F.offset (t + 1) ≤ v then t + 1 else tierSearch v t + +theorem tierSearch_le (v t : Nat) : F.tierSearch v t ≤ t := by + induction t with + | zero => exact Nat.le_refl _ + | succ t ih => + simp only [tierSearch] + split + · exact Nat.le_refl _ + · exact Nat.le_succ_of_le ih + +theorem offset_tierSearch_le (v t : Nat) : F.offset (F.tierSearch v t) ≤ v := by + induction t with + | zero => simp [tierSearch] + | succ t ih => + simp only [tierSearch] + split + · assumption + · exact ih + +theorem tierSearch_spec (v t : Nat) : + v < F.offset (F.tierSearch v t + 1) ∨ F.tierSearch v t = t := by + induction t with + | zero => exact Or.inr rfl + | succ t ih => + simp only [tierSearch] + split + · exact Or.inr rfl + · rename_i hno + cases ih with + | inl h => exact Or.inl h + | inr h => exact Or.inl (by rw [h]; omega) + +theorem tierSearch_pos {v : Nat} (hv : F.threshold ≤ v) : + ∀ {t : Nat}, 0 < t → 0 < F.tierSearch v t := by + intro t + induction t with + | zero => omega + | succ t ih => + intro _ + simp only [tierSearch] + split + · omega + · rename_i hno + cases Nat.eq_zero_or_pos t with + | inl h0 => + subst h0 + rw [Nat.zero_add, F.offset_one] at hno + omega + | inr hpos => exact ih hpos + +/-- The tier of `v`: for `v < 256 ^ tiers`, the unique `t` with +`offset t ≤ v < offset (t + 1)`. -/ +def tierOf (v : Nat) : Nat := F.tierSearch v F.tiers + +theorem tierOf_le (v : Nat) : F.tierOf v ≤ F.tiers := + F.tierSearch_le v F.tiers + +theorem offset_tierOf_le (v : Nat) : F.offset (F.tierOf v) ≤ v := + F.offset_tierSearch_le v F.tiers + +theorem lt_offset_tierOf_succ {v : Nat} (hv : v < 256 ^ F.tiers) : + v < F.offset (F.tierOf v + 1) := by + cases F.tierSearch_spec v F.tiers with + | inl h => exact h + | inr h => + have h1 : 256 ^ F.tiers ≤ F.offset (F.tiers + 1) := by + rw [F.offset_succ, F.capacity_eq_pow F.tiers_pos] + omega + simp only [tierOf] + rw [h] + omega + +theorem tierOf_pos {v : Nat} (hv : F.threshold ≤ v) : 0 < F.tierOf v := + F.tierSearch_pos hv F.tiers_pos + +/-- Tier ranges are disjoint: any `t` whose range contains `v` is +*the* tier of `v`. -/ +theorem tierOf_eq {v t : Nat} (hv : v < 256 ^ F.tiers) + (h1 : F.offset t ≤ v) (h2 : v < F.offset (t + 1)) : F.tierOf v = t := by + have ha := F.offset_tierOf_le v + have hb := F.lt_offset_tierOf_succ hv + cases Nat.lt_trichotomy (F.tierOf v) t with + | inl hlt => + have := F.offset_le_offset (show F.tierOf v + 1 ≤ t from hlt) + omega + | inr h' => + cases h' with + | inl heq => exact heq + | inr hgt => + have := F.offset_le_offset (show t + 1 ≤ F.tierOf v from hgt) + omega + +end Family + +end Bijou diff --git a/lean/Bijou/Instances.lean b/lean/Bijou/Instances.lean new file mode 100644 index 0000000..87dd61a --- /dev/null +++ b/lean/Bijou/Instances.lean @@ -0,0 +1,134 @@ +import Bijou.Canonical +import Bijou.Order + +/-! +# The three specified width variants + +`bijou32`, `bijou64`, and `bijou128` instantiate the family, and every +test vector from the three SPEC documents is checked by reduction +(`rfl`). The general theorems (`decode_encode`, `decode_ok`, +`encode_injective`, `decode_canonical`, `encode_lex_iff`) apply to all +three instances directly. +-/ + +namespace Bijou + +/-- bijou32: 4 multi-byte tiers, threshold 252, domain `[0, 2^32)`. -/ +def bijou32 : Family := ⟨4, by decide, by decide⟩ + +/-- bijou64: 8 multi-byte tiers, threshold 248, domain `[0, 2^64)`. -/ +def bijou64 : Family := ⟨8, by decide, by decide⟩ + +/-- bijou128: 16 multi-byte tiers, threshold 240, domain `[0, 2^128)`. -/ +def bijou128 : Family := ⟨16, by decide, by decide⟩ + +/-! ## Derived parameters match the SPECs -/ + +example : bijou32.threshold = 252 := rfl +example : bijou64.threshold = 248 := rfl +example : bijou128.threshold = 240 := rfl + +example : 256 ^ bijou32.tiers = 2 ^ 32 := by decide +example : 256 ^ bijou64.tiers = 2 ^ 64 := by decide +example : 256 ^ bijou128.tiers = 2 ^ 128 := by decide + +/-! ## bijou64 offset table (SPEC.md "Offset Table") -/ + +example : bijou64.offset 1 = 0xF8 := by decide +example : bijou64.offset 2 = 0x1F8 := by decide +example : bijou64.offset 3 = 0x101F8 := by decide +example : bijou64.offset 4 = 0x10101F8 := by decide +example : bijou64.offset 5 = 0x1010101F8 := by decide +example : bijou64.offset 6 = 0x101010101F8 := by decide +example : bijou64.offset 7 = 0x10101010101F8 := by decide +example : bijou64.offset 8 = 0x1010101010101F8 := by decide + +/-! ## bijou64 test vectors (SPEC.md "Test Vectors") -/ + +example : bijou64.encode 0 = [0x00] := rfl +example : bijou64.encode 1 = [0x01] := rfl +example : bijou64.encode 42 = [0x2A] := rfl +example : bijou64.encode 247 = [0xF7] := rfl +example : bijou64.encode 248 = [0xF8, 0x00] := rfl +example : bijou64.encode 300 = [0xF8, 0x34] := rfl +example : bijou64.encode 503 = [0xF8, 0xFF] := rfl +example : bijou64.encode 504 = [0xF9, 0x00, 0x00] := rfl +example : bijou64.encode 1000 = [0xF9, 0x01, 0xF0] := rfl +example : bijou64.encode 65535 = [0xF9, 0xFE, 0x07] := rfl +example : bijou64.encode 66039 = [0xF9, 0xFF, 0xFF] := rfl +example : bijou64.encode 66040 = [0xFA, 0x00, 0x00, 0x00] := rfl +example : bijou64.encode 67000 = [0xFA, 0x00, 0x03, 0xC0] := rfl +example : bijou64.encode 16843255 = [0xFA, 0xFF, 0xFF, 0xFF] := rfl +example : bijou64.encode 16843256 = [0xFB, 0x00, 0x00, 0x00, 0x00] := rfl +example : bijou64.encode 4311810551 = [0xFB, 0xFF, 0xFF, 0xFF, 0xFF] := rfl +example : bijou64.encode 72340172838076920 + = [0xFF, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00] := rfl +example : bijou64.encode 18446744073709551615 + = [0xFF, 0xFE, 0xFE, 0xFE, 0xFE, 0xFE, 0xFE, 0xFE, 0x07] := rfl + +example : bijou64.decode [0xF8, 0x34, 0xFF] = .ok (300, 2) := rfl +example : bijou64.decode [0xFF, 0xFE, 0xFE, 0xFE, 0xFE, 0xFE, 0xFE, 0xFE, 0x07] + = .ok (18446744073709551615, 9) := rfl + +/-! ## bijou64 error vectors (SPEC.md "Error Test Vectors") -/ + +example : bijou64.decode [] = .error .bufferTooShort := rfl +example : bijou64.decode [0xF9, 0x00] = .error .bufferTooShort := rfl +example : bijou64.decode [0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF] + = .error .overflow := rfl + +/-! ## bijou32 test vectors (bijou32/SPEC.md) -/ + +example : bijou32.encode 0 = [0x00] := rfl +example : bijou32.encode 1 = [0x01] := rfl +example : bijou32.encode 42 = [0x2A] := rfl +example : bijou32.encode 247 = [0xF7] := rfl +example : bijou32.encode 251 = [0xFB] := rfl +example : bijou32.encode 252 = [0xFC, 0x00] := rfl +example : bijou32.encode 300 = [0xFC, 0x30] := rfl +example : bijou32.encode 507 = [0xFC, 0xFF] := rfl +example : bijou32.encode 508 = [0xFD, 0x00, 0x00] := rfl +example : bijou32.encode 1000 = [0xFD, 0x01, 0xEC] := rfl +example : bijou32.encode 65535 = [0xFD, 0xFE, 0x03] := rfl +example : bijou32.encode 66043 = [0xFD, 0xFF, 0xFF] := rfl +example : bijou32.encode 66044 = [0xFE, 0x00, 0x00, 0x00] := rfl +example : bijou32.encode 67000 = [0xFE, 0x00, 0x03, 0xBC] := rfl +example : bijou32.encode 16843259 = [0xFE, 0xFF, 0xFF, 0xFF] := rfl +example : bijou32.encode 16843260 = [0xFF, 0x00, 0x00, 0x00, 0x00] := rfl +example : bijou32.encode 4294967295 = [0xFF, 0xFE, 0xFE, 0xFE, 0x03] := rfl + +example : bijou32.decode [] = .error .bufferTooShort := rfl +example : bijou32.decode [0xFD, 0x00] = .error .bufferTooShort := rfl +example : bijou32.decode [0xFF, 0xFF, 0xFF, 0xFF, 0xFF] = .error .overflow := rfl + +/-! ## bijou128 test vectors (bijou128/SPEC.md) -/ + +example : bijou128.encode 0 = [0x00] := rfl +example : bijou128.encode 1 = [0x01] := rfl +example : bijou128.encode 42 = [0x2A] := rfl +example : bijou128.encode 239 = [0xEF] := rfl +example : bijou128.encode 240 = [0xF0, 0x00] := rfl +example : bijou128.encode 241 = [0xF0, 0x01] := rfl +example : bijou128.encode 495 = [0xF0, 0xFF] := rfl +example : bijou128.encode 496 = [0xF1, 0x00, 0x00] := rfl +example : bijou128.encode 65535 = [0xF1, 0xFE, 0x0F] := rfl +example : bijou128.encode 66031 = [0xF1, 0xFF, 0xFF] := rfl +example : bijou128.encode 66032 = [0xF2, 0x00, 0x00, 0x00] := rfl +example : bijou128.encode 67000 = [0xF2, 0x00, 0x03, 0xC8] := rfl +example : bijou128.encode 16843247 = [0xF2, 0xFF, 0xFF, 0xFF] := rfl +example : bijou128.encode 16843248 = [0xF3, 0x00, 0x00, 0x00, 0x00] := rfl +example : bijou128.encode (2 ^ 32 - 1) = [0xF3, 0xFE, 0xFE, 0xFE, 0x0F] := rfl +example : bijou128.encode (2 ^ 64 - 1) + = [0xF7, 0xFE, 0xFE, 0xFE, 0xFE, 0xFE, 0xFE, 0xFE, 0x0F] := rfl +example : bijou128.encode (2 ^ 128 - 1) + = [0xFF, 0xFE, 0xFE, 0xFE, 0xFE, 0xFE, 0xFE, 0xFE, 0xFE, + 0xFE, 0xFE, 0xFE, 0xFE, 0xFE, 0xFE, 0xFE, 0x0F] := rfl + +example : bijou128.decode [] = .error .bufferTooShort := rfl +example : bijou128.decode [0xF1, 0x00] = .error .bufferTooShort := rfl +example : bijou128.decode + [0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, + 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF] + = .error .overflow := rfl + +end Bijou diff --git a/lean/Bijou/Order.lean b/lean/Bijou/Order.lean new file mode 100644 index 0000000..fac6a99 --- /dev/null +++ b/lean/Bijou/Order.lean @@ -0,0 +1,67 @@ +import Bijou.Spec + +/-! +# Order preservation + +Encodings sort in the same order as the values they represent: +lexicographic byte comparison equals numeric comparison. This is the +SPEC's "big-endian byte order" design goal — sorted storage and binary +search work directly on encoded bytes, without decoding. + +The argument splits on tiers. Distinct tiers are separated by their +tag bytes (tier-0 values are below the threshold, and multi-byte tags +grow with the tier), while within a tier the big-endian payload +inherits numeric order (`beBytes_lex_beBytes`). +-/ + +namespace Bijou.Family + +variable (F : Family) + +theorem lex_encode_of_lt {v₁ v₂ : Nat} (h₂ : v₂ < 256 ^ F.tiers) (h : v₁ < v₂) : + Lex (F.encode v₁) (F.encode v₂) := by + by_cases ha : v₁ < F.threshold + · by_cases hb : v₂ < F.threshold + · simp only [encode, if_pos ha, if_pos hb] + exact Lex.head h + · have ht₂ := F.tierOf_pos (Nat.le_of_not_lt hb) + simp only [encode, if_pos ha, if_neg hb] + exact Lex.head (by omega) + · have hb : ¬v₂ < F.threshold := by omega + have h₁ : v₁ < 256 ^ F.tiers := by omega + have ht₁ := F.tierOf_pos (Nat.le_of_not_lt ha) + have ht₂ := F.tierOf_pos (Nat.le_of_not_lt hb) + have ho₁l := F.offset_tierOf_le v₁ + have ho₁r := F.lt_offset_tierOf_succ h₁ + have ho₂l := F.offset_tierOf_le v₂ + have ho₂r := F.lt_offset_tierOf_succ h₂ + simp only [encode, if_neg ha, if_neg hb] + cases Nat.lt_trichotomy (F.tierOf v₁) (F.tierOf v₂) with + | inl hlt => exact Lex.head (by omega) + | inr h' => + cases h' with + | inl heq => + rw [heq] at ho₁l ho₁r ⊢ + rw [F.offset_succ, F.capacity_eq_pow ht₂] at ho₂r + exact Lex.tail (beBytes_lex_beBytes (by omega) (by omega)) + | inr hgt => + have := F.offset_le_offset (show F.tierOf v₂ + 1 ≤ F.tierOf v₁ from hgt) + omega + +/-- Numeric order and lexicographic byte order coincide. -/ +theorem encode_lex_iff {v₁ v₂ : Nat} + (h₁ : v₁ < 256 ^ F.tiers) (h₂ : v₂ < 256 ^ F.tiers) : + v₁ < v₂ ↔ Lex (F.encode v₁) (F.encode v₂) := by + constructor + · exact F.lex_encode_of_lt h₂ + · intro hlex + cases Nat.lt_trichotomy v₁ v₂ with + | inl h => exact h + | inr h' => + cases h' with + | inl heq => + subst heq + exact absurd hlex (Lex.irrefl _) + | inr hgt => exact absurd hlex (Lex.asymm (F.lex_encode_of_lt h₁ hgt)) + +end Bijou.Family diff --git a/lean/Bijou/RoundTrip.lean b/lean/Bijou/RoundTrip.lean new file mode 100644 index 0000000..2ff4ecd --- /dev/null +++ b/lean/Bijou/RoundTrip.lean @@ -0,0 +1,49 @@ +import Bijou.Spec + +/-! +# Round-trip + +Decoding an encoding returns the original value and consumes exactly +`encodedLen v` bytes, regardless of trailing data. +-/ + +namespace Bijou.Family + +variable (F : Family) + +theorem decode_encode {v : Nat} (hv : v < 256 ^ F.tiers) (rest : List Nat) : + F.decode (F.encode v ++ rest) = .ok (v, F.encodedLen v) := by + by_cases h : v < F.threshold + · simp [encode, decode, encodedLen, h] + · have ht1 : 0 < F.tierOf v := F.tierOf_pos (by omega) + have ho1 := F.offset_tierOf_le v + have ho2 := F.lt_offset_tierOf_succ hv + rw [F.offset_succ, F.capacity_eq_pow ht1] at ho2 + have htag : ¬F.threshold + (F.tierOf v - 1) < F.threshold := by omega + have hT : F.threshold + (F.tierOf v - 1) - F.threshold + 1 = F.tierOf v := by omega + have hT2 : F.threshold + (F.tierOf v - 1) - F.threshold + 2 = F.tierOf v + 1 := by + omega + simp only [encode, encodedLen, if_neg h, List.cons_append, decode, if_neg htag, + hT, hT2] + have hlen : + F.tierOf v ≤ (beBytes (F.tierOf v) (v - F.offset (F.tierOf v)) ++ rest).length := by + simp + rw [if_pos hlen] + have htake : + (beBytes (F.tierOf v) (v - F.offset (F.tierOf v)) ++ rest).take (F.tierOf v) + = beBytes (F.tierOf v) (v - F.offset (F.tierOf v)) := by + have h' := take_append_length (beBytes (F.tierOf v) (v - F.offset (F.tierOf v))) rest + rwa [beBytes_length] at h' + rw [htake, fromBe_beBytes (by omega)] + have hval : F.offset (F.tierOf v) + (v - F.offset (F.tierOf v)) = v := by omega + rw [hval, if_pos hv] + +/-- An encoding alone (no trailing bytes) decodes fully: the consumed +count is the entire buffer. -/ +theorem decode_encode' {v : Nat} (hv : v < 256 ^ F.tiers) : + F.decode (F.encode v) = .ok (v, (F.encode v).length) := by + have h := F.decode_encode hv [] + rw [List.append_nil] at h + rw [h, F.encode_length] + +end Bijou.Family diff --git a/lean/Bijou/Spec.lean b/lean/Bijou/Spec.lean new file mode 100644 index 0000000..4231eb4 --- /dev/null +++ b/lean/Bijou/Spec.lean @@ -0,0 +1,96 @@ +import Bijou.Bytes +import Bijou.Family + +/-! +# Encoding and decoding + +Direct transcriptions of the SPEC's Encoding and Decoding sections, +over `Nat` (values bounded by `256 ^ tiers`, bytes by `256`). + +- `Family.encode`: tier 0 emits the value as a single byte; tier `t` + emits tag `threshold + (t - 1)` followed by the `t`-byte big-endian + payload `v - offset t`. +- `Family.decode`: reads the tag, takes `tag - threshold + 1` payload + bytes, and returns `offset t + payload` plus the consumed length. + The only error conditions are a short buffer and top-tier overflow, + exactly as the SPEC's "Minimal Decoder Obligations" demands. +-/ + +namespace Bijou + +/-- The only two decode failures a conforming decoder may signal. +There is no "non-canonical encoding" error: non-canonical encodings +are structurally impossible. -/ +inductive DecodeError where + | bufferTooShort + | overflow +deriving DecidableEq, Repr + +namespace Family + +variable (F : Family) + +/-- Encode `v < 256 ^ tiers` as a bijou byte string. -/ +def encode (v : Nat) : List Nat := + if v < F.threshold then [v] + else + (F.threshold + (F.tierOf v - 1)) + :: beBytes (F.tierOf v) (v - F.offset (F.tierOf v)) + +/-- The number of bytes `encode v` produces. -/ +def encodedLen (v : Nat) : Nat := + if v < F.threshold then 1 else F.tierOf v + 1 + +/-- Decode a value from the front of `bs`, returning it together with +the number of bytes consumed. -/ +def decode (bs : List Nat) : Except DecodeError (Nat × Nat) := + match bs with + | [] => .error .bufferTooShort + | tag :: rest => + if tag < F.threshold then .ok (tag, 1) + else if tag - F.threshold + 1 ≤ rest.length then + if F.offset (tag - F.threshold + 1) + fromBe (rest.take (tag - F.threshold + 1)) + < 256 ^ F.tiers then + .ok + ( F.offset (tag - F.threshold + 1) + fromBe (rest.take (tag - F.threshold + 1)) + , tag - F.threshold + 2 + ) + else .error .overflow + else .error .bufferTooShort + +@[simp] +theorem encode_length (v : Nat) : (F.encode v).length = F.encodedLen v := by + simp only [encode, encodedLen] + split + · rfl + · simp + +/-- The encoder emits genuine bytes. -/ +theorem encode_bytes_lt {v : Nat} (hv : v < 256 ^ F.tiers) : + ∀ b ∈ F.encode v, b < 256 := by + intro b hb + simp only [encode] at hb + split at hb + · have := F.threshold_lt + simp only [List.mem_cons, List.not_mem_nil, or_false] at hb + omega + · rename_i hge + simp only [List.mem_cons] at hb + cases hb with + | inl h => + have ht := F.tierOf_le v + have h1 := F.tiers_lt + have h2 := F.tiers_pos + subst h + simp only [threshold] + omega + | inr h => + have h1 := F.offset_tierOf_le v + have h2 := F.lt_offset_tierOf_succ hv + have h3 : 0 < F.tierOf v := F.tierOf_pos (by omega) + rw [F.offset_succ, F.capacity_eq_pow h3] at h2 + exact beBytes_lt_256 (by omega) b h + +end Family + +end Bijou diff --git a/lean/lake-manifest.json b/lean/lake-manifest.json new file mode 100644 index 0000000..bf466c1 --- /dev/null +++ b/lean/lake-manifest.json @@ -0,0 +1,5 @@ +{"version": "1.1.0", + "packagesDir": ".lake/packages", + "packages": [], + "name": "bijou", + "lakeDir": ".lake"} diff --git a/lean/lakefile.toml b/lean/lakefile.toml new file mode 100644 index 0000000..e6aab3c --- /dev/null +++ b/lean/lakefile.toml @@ -0,0 +1,6 @@ +name = "bijou" +version = "0.1.0" +defaultTargets = ["Bijou"] + +[[lean_lib]] +name = "Bijou" diff --git a/lean/lean-toolchain b/lean/lean-toolchain new file mode 100644 index 0000000..33e0c08 --- /dev/null +++ b/lean/lean-toolchain @@ -0,0 +1 @@ +leanprover/lean4:v4.29.1 From d3abbd0082125aa78f876b96dd6395253749e555 Mon Sep 17 00:00:00 2001 From: Brooklyn Zelenka Date: Fri, 19 Jun 2026 14:44:43 -0700 Subject: [PATCH 2/2] Aeneas --- .gitignore | 1 + Cargo.toml | 5 + README.md | 28 +++- bijou64/src/kani_proofs.rs | 162 ++++++++++++++++++ bijou64/src/lib.rs | 6 + flake.nix | 42 +++++ lean-aeneas/BijouAeneas.lean | 21 +++ lean-aeneas/BijouAeneas/Generated.lean | 200 ++++++++++++++++++++++ lean-aeneas/BijouAeneas/Refinement.lean | 78 +++++++++ lean-aeneas/lake-manifest.json | 106 ++++++++++++ lean-aeneas/lakefile.toml | 17 ++ lean-aeneas/lean-toolchain | 1 + lean/Bijou.lean | 15 +- lean/Bijou/Bytes.lean | 16 ++ lean/Bijou/Canonical.lean | 66 ++++++++ lean/Bijou/Instances.lean | 214 ++++++++++++++---------- lean/Bijou/Order.lean | 12 ++ lean/Bijou/Spec.lean | 55 ++++++ 18 files changed, 946 insertions(+), 99 deletions(-) create mode 100644 bijou64/src/kani_proofs.rs create mode 100644 lean-aeneas/BijouAeneas.lean create mode 100644 lean-aeneas/BijouAeneas/Generated.lean create mode 100644 lean-aeneas/BijouAeneas/Refinement.lean create mode 100644 lean-aeneas/lake-manifest.json create mode 100644 lean-aeneas/lakefile.toml create mode 100644 lean-aeneas/lean-toolchain diff --git a/.gitignore b/.gitignore index 9063e6f..03d132c 100644 --- a/.gitignore +++ b/.gitignore @@ -18,6 +18,7 @@ rust_out # lean / lake build artifacts /lean/.lake/ +/lean-aeneas/.lake/ # wasm / npm artifacts **/dist/ diff --git a/Cargo.toml b/Cargo.toml index 2459adf..c3d9c23 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -54,6 +54,11 @@ unused_extern_crates = "deny" unsafe_code = "forbid" +# `kani` is a known cfg, set by the Kani verifier when it compiles the +# `#[cfg(kani)]` harnesses in bijou64/src/kani_proofs.rs. Register it so +# normal builds don't warn (which would fail `-D warnings` in CI). +unexpected_cfgs = { level = "warn", check-cfg = ['cfg(kani)'] } + [workspace.lints.clippy] dbg_macro = "warn" expect_used = "warn" diff --git a/README.md b/README.md index 49939b3..6a2ed6e 100644 --- a/README.md +++ b/README.md @@ -97,14 +97,32 @@ width variants. Machine-checked theorems include: no overlong encoding to reject. - _Bijectivity_: `encode` is injective, and fully-consumed buffers decoding to the same value are identical. -- _Order preservation_: lexicographic byte order equals numeric order. +- _Order preservation_: lexicographic byte order equals numeric order + (a strict total order on encodings). +- _Framing_: encoding length is determined by the first byte alone + (O(1) skipping), never exceeds `maxBytes` (9/5/17), and overflow can + occur only at the top tier (tag `0xFF`). Every test vector in the three `SPEC.md` documents is also checked by reduction. Run the proofs with `proofs` inside the dev shell, or -hermetically via `nix build .#checks..lean-proofs`. The proofs -describe the specified format, not the Rust implementation; the Rust -crates are checked against the same SPEC vectors and property-tested -with `bolero`. +hermetically via `nix build .#checks..lean-proofs`. + +This model describes the specified _format_. Connecting it to the +_actual Rust_ is a second, in-progress layer: + +- **Aeneas** ([`lean-aeneas/`](./lean-aeneas)) translates `bijou64`'s + Rust to Lean via Charon and proves it refines the model above. + `encode` and `encoded_len` translate cleanly; run with `proofs:aeneas` + (needs network for Mathlib + Aeneas on first build). +- **Kani** (`bijou64/src/kani_proofs.rs`) bounded-model-checks `decode`, + whose slice patterns are outside Aeneas's current support. It verifies + totality, canonicality (no overlong encodings), round-trip, and the + error conditions. Run with `proofs:kani` (needs upstream Kani, which + is not packaged for NixOS). + +Both Phase-2 layers run outside the hermetic Nix `ci` (heavy toolchains, +network, non-NixOS Kani). Until they fully land, "the Rust matches the +model" also rests on shared SPEC vectors and `bolero` property tests. ## Other implementations diff --git a/bijou64/src/kani_proofs.rs b/bijou64/src/kani_proofs.rs new file mode 100644 index 0000000..8c9df33 --- /dev/null +++ b/bijou64/src/kani_proofs.rs @@ -0,0 +1,162 @@ +//! Kani proof harnesses. +//! +//! These verify `decode` — the one core function that the Aeneas +//! pipeline cannot translate (its `&[a, ..]` subslice rest-patterns are +//! unsupported; see `../../.ignore/aeneas/SPIKE.md`). Kani handles all +//! of Rust, including those patterns, via bounded model checking. +//! +//! Decode reads at most `MAX_BYTES` (9) bytes and ignores any trailing +//! input, so a symbolic buffer of length `0..=MAX_BYTES` exercises every +//! control-flow path. Harnesses are `#[cfg(kani)]`, so they never enter +//! a normal build, test, or clippy run. +//! +//! Run with upstream Kani (not packaged for NixOS — run elsewhere or in +//! the Kani container): +//! +//! ```sh +//! cargo kani -p bijou64 +//! ``` +#![allow(clippy::indexing_slicing, clippy::unwrap_used)] + +use crate::{DecodeError, MAX_BYTES, TAG_THRESHOLD, decode, encode, encoded_bytes, encoded_len}; +use alloc::vec::Vec; + +/// A symbolic buffer of length `0..=MAX_BYTES`: enough to drive every +/// path through `decode`, since it never inspects beyond byte `MAX_BYTES`. +fn symbolic_buf() -> ([u8; MAX_BYTES], usize) { + let bytes: [u8; MAX_BYTES] = kani::any(); + let len: usize = kani::any(); + kani::assume(len <= MAX_BYTES); + (bytes, len) +} + +/// `decode` is total: it never panics, overflows, or indexes +/// out of bounds on any input. (Kani checks these automatically.) +#[kani::proof] +fn decode_never_panics() { + let (bytes, len) = symbolic_buf(); + let _ = decode(&bytes[..len]); +} + +/// Whatever `decode` accepts, it consumes a sane number of bytes: +/// at least the tag, never more than the buffer, never more than +/// `MAX_BYTES`. +#[kani::proof] +fn decode_consumes_within_bounds() { + let (bytes, len) = symbolic_buf(); + if let Ok((_, consumed)) = decode(&bytes[..len]) { + assert!(consumed >= 1); + assert!(consumed <= len); + assert!(consumed <= MAX_BYTES); + } +} + +/// Canonicality, by construction: anything `decode` accepts is exactly +/// the encoding of the value it returns. There are no overlong +/// encodings to accept. This is the property whose Rust shape blocks +/// Aeneas, so verifying it here is the point of the Kani layer. +#[kani::proof] +fn decode_accepts_only_canonical() { + let (bytes, len) = symbolic_buf(); + if let Ok((value, consumed)) = decode(&bytes[..len]) { + let re = encoded_bytes(value); + assert!(re.len() == consumed); + assert!(re.as_slice() == &bytes[..consumed]); + } +} + +/// Round-trip: every value encodes to bytes that decode back to it, +/// consuming exactly the encoded length. +#[kani::proof] +fn roundtrip_encode_decode() { + let value: u64 = kani::any(); + let enc = encoded_bytes(value); + let (decoded, consumed) = decode(enc.as_slice()).unwrap(); + assert!(decoded == value); + assert!(consumed == enc.len()); +} + +/// Round-trip through the allocating `encode`/`Vec` path (the API most +/// callers use) — distinct from `encoded_bytes`, so it needs its own +/// check. May require `#[kani::unwind(MAX_BYTES + 2)]` when run, since +/// `Vec` growth is a loop. +#[kani::proof] +fn roundtrip_vec_encode_decode() { + let value: u64 = kani::any(); + let mut buf = Vec::new(); + encode(value, &mut buf); + let (decoded, consumed) = decode(&buf).unwrap(); + assert!(decoded == value); + assert!(consumed == buf.len()); +} + +/// `encoded_len` agrees with the actual encoded length and stays within +/// `1..=MAX_BYTES`. (Aeneas only *translates* `encoded_len`; this is its +/// only correctness check.) +#[kani::proof] +fn encoded_len_matches_encoding() { + let value: u64 = kani::any(); + let len = encoded_len(value); + assert!(len >= 1); + assert!(len <= MAX_BYTES); + assert!(len == encoded_bytes(value).len()); +} + +/// Length is determined entirely by the first byte: the bytes a +/// successful `decode` consumes are a function of the tag alone (the +/// SPEC's O(1)-skip property). Mirrors `Bijou.Family.decode_consumed_from_tag`. +#[kani::proof] +fn decode_length_from_first_byte() { + let (bytes, len) = symbolic_buf(); + if let Ok((_, consumed)) = decode(&bytes[..len]) { + let tag = bytes[0]; // len >= 1, since decode succeeded + let expected = if tag < TAG_THRESHOLD { + 1 + } else { + (tag as usize - TAG_THRESHOLD as usize) + 2 + }; + assert!(consumed == expected); + } +} + +/// Trailing bytes are ignored: appending arbitrary data after a valid +/// encoding changes neither the decoded value nor the consumed length. +#[kani::proof] +fn roundtrip_ignores_trailing() { + let value: u64 = kani::any(); + let enc = encoded_bytes(value); + let n = enc.len(); + + let mut buf = [0u8; MAX_BYTES * 2]; + let tail: [u8; MAX_BYTES] = kani::any(); + buf[..n].copy_from_slice(enc.as_slice()); + buf[n..n + MAX_BYTES].copy_from_slice(&tail); + + let (decoded, consumed) = decode(&buf[..n + MAX_BYTES]).unwrap(); + assert!(decoded == value); + assert!(consumed == n); +} + +/// The two error conditions are the only ones, and they are +/// distinguishable exactly as the SPEC says: a short buffer is rejected, +/// and only tier 8 (tag `0xFF`) can overflow. +#[kani::proof] +fn decode_errors_match_spec() { + let (bytes, len) = symbolic_buf(); + match decode(&bytes[..len]) { + Err(DecodeError::BufferTooShort) => { + // Either empty, or the tag demands more payload bytes than provided. + // A multi-byte tag needs `tag - (TAG_THRESHOLD - 1)` payload bytes. + assert!( + len == 0 + || (bytes[0] >= TAG_THRESHOLD + && len < (bytes[0] as usize - (TAG_THRESHOLD as usize - 1)) + 1) + ); + } + Err(DecodeError::Overflow) => { + // Overflow is reachable only at the top tier (tag 0xFF). + assert!(bytes[0] == u8::MAX); + } + Ok(_) => {} + } +} diff --git a/bijou64/src/lib.rs b/bijou64/src/lib.rs index f67cf3e..947998b 100644 --- a/bijou64/src/lib.rs +++ b/bijou64/src/lib.rs @@ -665,6 +665,12 @@ pub enum DecodeError { Overflow, } +/// Kani proof harnesses for `decode` (verified here because Aeneas +/// cannot translate its slice rest-patterns). Compiled only under +/// `--cfg kani`; see the module for how to run them. +#[cfg(kani)] +mod kani_proofs; + #[cfg(test)] #[allow(clippy::indexing_slicing, clippy::needless_range_loop, clippy::panic)] mod tests { diff --git a/flake.nix b/flake.nix index 107a6a5..f77fb30 100644 --- a/flake.nix +++ b/flake.nix @@ -199,6 +199,14 @@ installPhase = "touch $out"; }; + # Phase 2 verification (Aeneas + Kani) is intentionally NOT a + # hermetic Nix check. The Aeneas-translated proofs in + # `lean-aeneas/` depend on the Aeneas Lean library + Mathlib + # (fetched by Lake via `elan`, needs network + a different Lean + # toolchain than `lean/`); Kani is not packaged for NixOS. Both + # are exposed as dev-shell commands instead — see `proofs:aeneas` + # and `proofs:kani`, and `.ignore/aeneas/SPIKE.md`. + # Python environment for benchmark chart generation (analyze.py) bench-charts-python = pkgs.python3.withPackages (ps: [ ps.matplotlib @@ -475,6 +483,40 @@ echo "✓ Lean proofs OK" ''; + "proofs:aeneas" = cmd "Check the Aeneas-translated proofs in lean-aeneas/ (Phase 2; needs network on first run for Mathlib + Aeneas)" '' + set -e + cd "$WORKSPACE_ROOT/lean-aeneas" + # elan reads lean-aeneas/lean-toolchain (Lean 4.30.0-rc2, to + # match the Aeneas Lean library) and provisions it on demand. + # First run fetches deps and the Mathlib olean cache. + if [ ! -d .lake/packages/mathlib ]; then + echo "===> First run: resolving deps (Aeneas + Mathlib)..." + ${pkgs.elan}/bin/lake update + ${pkgs.elan}/bin/lake exe cache get || true + fi + ${pkgs.elan}/bin/lake build + echo "" + echo "✓ Aeneas refinement proofs OK" + ''; + + "proofs:kani" = cmd "Run the Kani harnesses for bijou64::decode (requires upstream Kani; not packaged for NixOS)" '' + set -e + if ! command -v cargo-kani >/dev/null 2>&1; then + echo "cargo-kani not found on PATH." + echo "" + echo "Kani is not packaged for NixOS. Run these harnesses with" + echo "upstream Kani on another platform or in the Kani container:" + echo "" + echo " cargo kani -p bijou64" + echo "" + echo "Harnesses live in bijou64/src/kani_proofs.rs (cfg(kani))." + exit 1 + fi + cargo kani -p bijou64 + echo "" + echo "✓ Kani harnesses OK" + ''; + "ci" = cmd "Run full CI suite (fmt, clippy, test, no_std, wasm32, wasm-pack, JS package, Lean proofs)" '' set -e diff --git a/lean-aeneas/BijouAeneas.lean b/lean-aeneas/BijouAeneas.lean new file mode 100644 index 0000000..8a8ba42 --- /dev/null +++ b/lean-aeneas/BijouAeneas.lean @@ -0,0 +1,21 @@ +import BijouAeneas.Generated +import BijouAeneas.Refinement + +/-! +# BijouAeneas + +Phase 2 of the bijou formal-verification effort: proofs about the +*actual Rust* in `bijou64/src/lib.rs`, as translated to Lean by Charon + +Aeneas. + +- `BijouAeneas.Generated` — the Aeneas output (auto-generated; do not + edit). Covers `encode`, `encoded_len`, and the offset machinery. See + its header for the exact pipeline and tool versions. +- `BijouAeneas.Refinement` — proofs that the generated functions satisfy + their specifications and refine the format model from the (separate) + `lean/` project. + +`decode` is verified with Kani instead of Aeneas (its slice +rest-patterns are unsupported by this Aeneas version); see +`../.ignore/aeneas/SPIKE.md`. +-/ diff --git a/lean-aeneas/BijouAeneas/Generated.lean b/lean-aeneas/BijouAeneas/Generated.lean new file mode 100644 index 0000000..0beba0b --- /dev/null +++ b/lean-aeneas/BijouAeneas/Generated.lean @@ -0,0 +1,200 @@ +-- PROVENANCE: This file is AUTO-GENERATED by Aeneas. Do not edit by hand. +-- +-- Pipeline (see ../.ignore/aeneas/reproduce.sh and SPIKE.md): +-- charon cargo --preset=aeneas \ +-- --start-from 'crate::encode' --start-from 'crate::encoded_len' -- --lib +-- aeneas -backend lean -namespace BijouRust bijou64_enc.llbc +-- +-- Tooling: Charon 0.1.212, Aeneas 0.1.0 (github:aeneasverif/aeneas +-- rev bf13c42e7c34d07fc396baffad39c93023b12914), rustc nightly-2026-06-01. +-- +-- `decode` is intentionally NOT translated here: its `&[a, ..]` subslice +-- rest-patterns are unsupported by this Aeneas version. `decode` is +-- verified separately with Kani (see ../bijou64/ Kani harnesses). +-- +-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS +-- [bijou64] +import Aeneas +open Aeneas Aeneas.Std Result ControlFlow Error +set_option linter.dupNamespace false +set_option linter.hashCommand false +set_option linter.unusedVariables false + +/- You can set the `maxHeartbeats` value with the `-max-heartbeats` CLI option -/ +set_option maxHeartbeats 1000000 + +/- You can set the `maxRecDepth` value with the `-max-recdepth` CLI option -/ +set_option maxRecDepth 2048 + +/- You can remove the following line by using the CLI option `-all-computable`: -/ +noncomputable section + +namespace BijouRust + +/-- [core::num::{u64}::saturating_mul]: + Source: '/rustc/library/core/src/num/uint_macros.rs', lines 2516:8-2516:60 + Name pattern: [core::num::{u64}::saturating_mul] + Visibility: public -/ +@[rust_fun "core::num::{u64}::saturating_mul"] +axiom core.num.U64.saturating_mul : Std.U64 → Std.U64 → Result Std.U64 + +/-- [alloc::vec::{alloc::vec::Vec}::truncate]: + Source: '/rustc/library/alloc/src/vec/mod.rs', lines 1814:4-1814:42 + Name pattern: [alloc::vec::{alloc::vec::Vec<@T>}::truncate] + Visibility: public -/ +@[rust_fun "alloc::vec::{alloc::vec::Vec<@T>}::truncate"] +axiom alloc.vec.Vec.truncate + {T : Type} (A : Type) : + alloc.vec.Vec T → Std.Usize → Result (alloc.vec.Vec T) + +/-- [bijou64::TAG_THRESHOLD] + Source: 'bijou64/src/lib.rs', lines 86:0-86:30 -/ +@[global_simps, irreducible] def TAG_THRESHOLD : Std.U8 := 248#u8 + +/-- [bijou64::NUM_TIERS] + Source: 'bijou64/src/lib.rs', lines 89:0-89:27 -/ +@[global_simps, irreducible] def NUM_TIERS : Std.Usize := 8#usize + +/-- [bijou64::tier_offset]: loop body 0: + Source: 'bijou64/src/lib.rs', lines 107:4-111:5 -/ +@[rust_loop_body] +def tier_offset_loop.body + (n : Std.Usize) (result : Std.U64) (power : Std.U64) (i : Std.Usize) : + Result (ControlFlow (Std.U64 × Std.U64 × Std.Usize) Std.U64) + := do + if i <= n + then + let power1 ← core.num.U64.saturating_mul power 256#u64 + let result1 ← lift (core.num.U64.saturating_add result power1) + let i1 ← i + 1#usize + ok (cont (result1, power1, i1)) + else ok (done result) + +/-- [bijou64::tier_offset]: loop 0: + Source: 'bijou64/src/lib.rs', lines 107:4-111:5 -/ +@[rust_loop] +def tier_offset_loop + (n : Std.Usize) (result : Std.U64) (power : Std.U64) (i : Std.Usize) : + Result Std.U64 + := do + loop + (fun (result1, power1, i1) => tier_offset_loop.body n result1 power1 i1) + (result, power, i) + +/-- [bijou64::tier_offset]: + Source: 'bijou64/src/lib.rs', lines 96:0-113:1 -/ +def tier_offset (n : Std.Usize) : Result Std.U64 := do + if n = 0#usize + then ok 0#u64 + else + if n = 1#usize + then ok (UScalar.cast .U64 TAG_THRESHOLD) + else + let result ← lift (UScalar.cast .U64 TAG_THRESHOLD) + tier_offset_loop n result 1#u64 2#usize + +/-- [bijou64::OFFSETS] + Source: 'bijou64/src/lib.rs', lines 119:0-129:2 -/ +@[global_simps, irreducible] +def OFFSETS : Result (Array Std.U64 9#usize) := do + let i ← tier_offset 0#usize + let i1 ← tier_offset 1#usize + let i2 ← tier_offset 2#usize + let i3 ← tier_offset 3#usize + let i4 ← tier_offset 4#usize + let i5 ← tier_offset 5#usize + let i6 ← tier_offset 6#usize + let i7 ← tier_offset 7#usize + let i8 ← tier_offset 8#usize + ok (Array.make 9#usize [ i, i1, i2, i3, i4, i5, i6, i7, i8 ]) + +/-- [bijou64::BOUNDS] + Source: 'bijou64/src/lib.rs', lines 136:0-146:2 -/ +@[global_simps, irreducible] +def BOUNDS : Result (Array Std.U64 9#usize) := do + let i ← tier_offset 1#usize + let i1 ← tier_offset 2#usize + let i2 ← tier_offset 3#usize + let i3 ← tier_offset 4#usize + let i4 ← tier_offset 5#usize + let i5 ← tier_offset 6#usize + let i6 ← tier_offset 7#usize + let i7 ← tier_offset 8#usize + ok (Array.make 9#usize [ i, i1, i2, i3, i4, i5, i6, i7, core.num.U64.MAX ]) + +/-- [bijou64::encoded_len]: + Source: 'bijou64/src/lib.rs', lines 168:0-198:1 + Visibility: public -/ +def encoded_len (value : Std.U64) : Result Std.Usize := do + let a ← BOUNDS + let i ← Array.index_usize a 0#usize + if value < i + then ok 1#usize + else + let i1 ← lift (core.num.U64.leading_zeros value) + let bw ← 64#u32 - i1 + let i2 ← bw - 1#u32 + let i3 ← i2 / 8#u32 + let i4 ← i3 + 2#u32 + let candidate ← lift (UScalar.cast .Usize i4) + let i5 ← candidate - 2#usize + let i6 ← Array.index_usize a i5 + if value < i6 + then candidate - 1#usize + else ok candidate + +/-- [bijou64::encode]: + Source: 'bijou64/src/lib.rs', lines 214:0-233:1 + Visibility: public -/ +def encode + (value : Std.U64) (buf : alloc.vec.Vec Std.U8) : + Result (alloc.vec.Vec Std.U8) + := do + let a ← BOUNDS + let i ← Array.index_usize a 0#usize + if value < i + then + let i1 ← lift (value &&& 255#u64) + let i2 ← lift (UScalar.cast .U8 i1) + alloc.vec.Vec.push buf i2 + else + let i1 ← lift (core.num.U64.leading_zeros value) + let bw ← 64#u32 - i1 + let i2 ← bw - 1#u32 + let i3 ← i2 / 8#u32 + let i4 ← i3 + 1#u32 + let tier ← lift (UScalar.cast .Usize i4) + let i5 ← tier - 1#usize + let i6 ← Array.index_usize a i5 + let tier1 ← if value < i6 + then ok i5 + else ok tier + let i7 ← lift (UScalar.cast .Usize TAG_THRESHOLD) + let i8 ← i7 + tier1 + let i9 ← i8 - 1#usize + let tag ← lift (UScalar.cast .U8 i9) + let a1 ← OFFSETS + let i10 ← Array.index_usize a1 tier1 + let i11 ← value - i10 + let i12 ← NUM_TIERS - tier1 + let i13 ← 8#usize * i12 + let payload ← i11 <<< i13 + let pb ← lift (core.num.U64.to_be_bytes payload) + let original_len := alloc.vec.Vec.len buf + let i14 ← Array.index_usize pb 0#usize + let i15 ← Array.index_usize pb 1#usize + let i16 ← Array.index_usize pb 2#usize + let i17 ← Array.index_usize pb 3#usize + let i18 ← Array.index_usize pb 4#usize + let i19 ← Array.index_usize pb 5#usize + let i20 ← Array.index_usize pb 6#usize + let i21 ← Array.index_usize pb 7#usize + let s ← + lift (Array.to_slice + (Array.make 9#usize [ tag, i14, i15, i16, i17, i18, i19, i20, i21 ])) + let buf1 ← alloc.vec.Vec.extend_from_slice core.clone.CloneU8 buf s + let i22 ← original_len + tier1 + let i23 ← i22 + 1#usize + alloc.vec.Vec.truncate Global buf1 i23 + +end BijouRust diff --git a/lean-aeneas/BijouAeneas/Refinement.lean b/lean-aeneas/BijouAeneas/Refinement.lean new file mode 100644 index 0000000..31abe6c --- /dev/null +++ b/lean-aeneas/BijouAeneas/Refinement.lean @@ -0,0 +1,78 @@ +import BijouAeneas.Generated + +/-! +# Refinement: generated Rust ⟶ format model + +Proofs that the Aeneas-translated `bijou64` functions in +`BijouAeneas.Generated` satisfy their specifications, and ultimately +that they refine the parametrized format model in the `lean/` project +(`Bijou.Family`, instantiated at `bijou64`). + +## Status + +The pipeline (Charon → Aeneas → Lean) and this project's toolchain are +proven working: `BijouAeneas.Generated` typechecks against the real +Aeneas runtime library. The refinement proofs below are developed +incrementally; this module contains no `sorry`. + +The loop-free base cases of `tier_offset` are proven here and matched to +the model's offset table (`Bijou.Family.offset` at `bijou64`: `offset 0 += 0`, `offset 1 = 248`). The remaining obligations are genuine work, +recorded in `../.ignore/TODO.md`; the two blockers are: + +1. The generated `OFFSETS`/`BOUNDS` globals are built by a loop over + `core.num.U64.saturating_mul`, which this Aeneas version emits as an + un-specified `axiom`. Reasoning about them (even totality) first + needs a trusted spec for that intrinsic. +2. `encode`/`encoded_len` tier dispatch goes through `leading_zeros` + (modelled as `Nat.log 2`); relating `(bw-1)/8+2` to the tier is the + crux lemma, a good `bv_decide`/`omega` target. +-/ + +namespace BijouAeneas + +open Aeneas Aeneas.Std Result +open BijouRust + +/-- The bijou64 offset recurrence, restated locally. The `lean/` model +(`Bijou.Family.offset` at `bijou64`) lives in a separate, Mathlib-free +project on a different Lean toolchain, so it can't be imported here; we +mirror it and keep both honest with the shared SPEC offset table, which +`#guard` checks below. -/ +def modelOffset : Nat → Nat + | 0 => 0 + | 1 => 248 + | (n + 2) => modelOffset (n + 1) + 256 ^ (n + 1) + +-- `modelOffset` reproduces the SPEC.md "Offset Table" for bijou64. +#guard modelOffset 0 = 0 +#guard modelOffset 1 = 0xF8 +#guard modelOffset 2 = 0x1F8 +#guard modelOffset 3 = 0x101F8 +#guard modelOffset 8 = 0x1010101010101F8 + +/-- Tier 0 has offset 0. -/ +@[simp] +theorem tier_offset_zero : tier_offset 0#usize = ok 0#u64 := by + simp [tier_offset] + +/-- Tier 1 has offset 248 (the tag threshold) — the first value that no +longer fits in a single byte. -/ +@[simp] +theorem tier_offset_one : tier_offset 1#usize = ok 248#u64 := by + simp only [tier_offset, TAG_THRESHOLD] + rfl + +/-- The generated `tier_offset` agrees with the local `modelOffset` at +tier 0 — an in-project, machine-checked correspondence between the +translated Rust and the offset model. -/ +theorem tier_offset_zero_matches_model : + ∃ x : Std.U64, tier_offset 0#usize = ok x ∧ x.val = modelOffset 0 := + ⟨0#u64, tier_offset_zero, by decide⟩ + +/-- The generated `tier_offset` agrees with `modelOffset` at tier 1. -/ +theorem tier_offset_one_matches_model : + ∃ x : Std.U64, tier_offset 1#usize = ok x ∧ x.val = modelOffset 1 := + ⟨248#u64, tier_offset_one, by decide⟩ + +end BijouAeneas diff --git a/lean-aeneas/lake-manifest.json b/lean-aeneas/lake-manifest.json new file mode 100644 index 0000000..134d039 --- /dev/null +++ b/lean-aeneas/lake-manifest.json @@ -0,0 +1,106 @@ +{"version": "1.2.0", + "packagesDir": ".lake/packages", + "packages": + [{"url": "https://github.com/AeneasVerif/aeneas", + "type": "git", + "subDir": "backends/lean", + "scope": "", + "rev": "bf13c42e7c34d07fc396baffad39c93023b12914", + "name": "Aeneas", + "manifestFile": "lake-manifest.json", + "inputRev": "bf13c42e7c34d07fc396baffad39c93023b12914", + "inherited": false, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover-community/mathlib4.git", + "type": "git", + "subDir": null, + "scope": "", + "rev": "5450b53e5ddc75d46418fabb605edbf36bd0beb6", + "name": "mathlib", + "manifestFile": "lake-manifest.json", + "inputRev": "v4.30.0-rc2", + "inherited": true, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover-community/plausible", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "86210d4ad1b08b086d0bd638637a75246523dbb8", + "name": "plausible", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/LeanSearchClient", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "c5d5b8fe6e5158def25cd28eb94e4141ad97c843", + "name": "LeanSearchClient", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/import-graph", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "cdab3938ccabbdb044be6896e251b5814bec932e", + "name": "importGraph", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/ProofWidgets4", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "2db6054a44326f8c0230ee0570e2ddb894816511", + "name": "proofwidgets", + "manifestFile": "lake-manifest.json", + "inputRev": "v0.0.98", + "inherited": true, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover-community/aesop", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "f0c6e183ea26531e82773feb4b73ab6595ca17a5", + "name": "aesop", + "manifestFile": "lake-manifest.json", + "inputRev": "v4.30.0-rc2", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/quote4", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "1cc7e819b9b9bc1e87c9edcccb62e0269e00a809", + "name": "Qq", + "manifestFile": "lake-manifest.json", + "inputRev": "v4.30.0-rc2", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/batteries", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "5c57f3857ba81924a88b2cdf4f062e34ec04ff11", + "name": "batteries", + "manifestFile": "lake-manifest.json", + "inputRev": "v4.30.0-rc2", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover/lean4-cli", + "type": "git", + "subDir": null, + "scope": "leanprover", + "rev": "13567aed1ac4f12aea9484178e07e51f8c9f7658", + "name": "Cli", + "manifestFile": "lake-manifest.json", + "inputRev": "v4.30.0-rc2", + "inherited": true, + "configFile": "lakefile.toml"}], + "name": "bijouAeneas", + "lakeDir": ".lake", + "fixedToolchain": false} diff --git a/lean-aeneas/lakefile.toml b/lean-aeneas/lakefile.toml new file mode 100644 index 0000000..2f50260 --- /dev/null +++ b/lean-aeneas/lakefile.toml @@ -0,0 +1,17 @@ +name = "bijouAeneas" +defaultTargets = ["BijouAeneas"] + +# The Aeneas Lean library (runtime for Charon/Aeneas-generated code). +# It transitively requires Mathlib v4.30.0-rc2, which is why this project +# is separate from the deliberately Mathlib-free `lean/` model and pins a +# different toolchain (see lean-toolchain). Rev must match the Aeneas +# binary used to generate BijouAeneas/Generated.lean — see that file's +# header and ../.ignore/aeneas/SPIKE.md. +[[require]] +name = "Aeneas" +git = "https://github.com/AeneasVerif/aeneas" +rev = "bf13c42e7c34d07fc396baffad39c93023b12914" +subDir = "backends/lean" + +[[lean_lib]] +name = "BijouAeneas" diff --git a/lean-aeneas/lean-toolchain b/lean-aeneas/lean-toolchain new file mode 100644 index 0000000..6c7e31f --- /dev/null +++ b/lean-aeneas/lean-toolchain @@ -0,0 +1 @@ +leanprover/lean4:v4.30.0-rc2 diff --git a/lean/Bijou.lean b/lean/Bijou.lean index 75e578e..5c64e1a 100644 --- a/lean/Bijou.lean +++ b/lean/Bijou.lean @@ -20,10 +20,17 @@ Headline theorems (all in `Bijou.Family`): - `decode_ok` — canonicality by construction: any byte string the decoder accepts is exactly `encode` of the returned value. There is no overlong encoding to reject. -- `encode_injective` / `decode_canonical` — `encode` is a bijection - between `[0, 256 ^ tiers)` and the accepted byte strings. -- `encode_lex_iff` — lexicographic byte order equals numeric order. +- `encode_injective` / `decode_canonical` / `encode_bijection` — + `encode` is a bijection between `[0, 256 ^ tiers)` and the accepted + byte strings. +- `encode_lex_iff` / `encode_lex_trichotomy` — lexicographic byte order + equals numeric order, and is a strict total order on encodings. +- `decode_consumed_from_tag` — encoding length is a function of the + first byte alone (O(1) framing). +- `encodedLen_le` — encodings never exceed `maxBytes` (`tiers + 1`). +- `decode_overflow_max_tag` — overflow is possible only at the top tier. `Bijou.Instances` instantiates the three specified variants and checks -every test vector from the SPEC documents by reduction. +every test vector from the SPEC documents (and the offset tables and +`maxBytes`) by reduction. -/ diff --git a/lean/Bijou/Bytes.lean b/lean/Bijou/Bytes.lean index 4989d9f..3332d70 100644 --- a/lean/Bijou/Bytes.lean +++ b/lean/Bijou/Bytes.lean @@ -138,6 +138,22 @@ theorem Lex.asymm {as bs : List Nat} (h : Lex as bs) : ¬Lex bs as := by | head h2 => omega | tail h2 => exact ih h2 +/-- `Lex` is transitive. With `irrefl` and `asymm`, this makes it a +strict order — so sorting byte strings by `Lex` is well-defined. -/ +theorem Lex.trans {as bs cs : List Nat} (h₁ : Lex as bs) : Lex bs cs → Lex as cs := by + induction h₁ generalizing cs with + | nil => intro h₂; cases h₂ <;> exact Lex.nil + | head hab => + intro h₂ + cases h₂ with + | head hbc => exact Lex.head (by omega) + | tail _ => exact Lex.head hab + | tail _ ih => + intro h₂ + cases h₂ with + | head hbc => exact Lex.head hbc + | tail h₂' => exact Lex.tail (ih h₂') + /-- Big-endian encoding is strictly monotone with respect to lexicographic order: numeric order and byte order agree. -/ theorem beBytes_lex_beBytes {w m n : Nat} (hn : n < 256 ^ w) (h : m < n) : diff --git a/lean/Bijou/Canonical.lean b/lean/Bijou/Canonical.lean index 176dc5f..8f0c9bc 100644 --- a/lean/Bijou/Canonical.lean +++ b/lean/Bijou/Canonical.lean @@ -130,4 +130,70 @@ theorem decode_canonical {bs₁ bs₂ : List Nat} {v : Nat} rw [List.take_length] at c₁ c₂ rw [c₁, c₂] +/-- Overflow is signalled only at the maximal tag `255` (`0xFF`) — the +top tier. Lower tiers cannot overflow, because their entire value range +sits below `256 ^ tiers`. This is the SPEC's "Minimal Decoder +Obligations": the overflow check is needed only for the widest tier. -/ +theorem decode_overflow_max_tag {tag : Nat} {rest : List Nat} + (hbytes : ∀ b ∈ tag :: rest, b < 256) + (h : F.decode (tag :: rest) = .error .overflow) : + tag = 255 := by + have htag256 : tag < 256 := hbytes tag (List.mem_cons_self ..) + have hthr : F.threshold = 256 - F.tiers := rfl + have htiers := F.tiers_pos + have htierslt := F.tiers_lt + simp only [decode] at h + by_cases htag : tag < F.threshold + · rw [if_pos htag] at h; simp at h + · rw [if_neg htag] at h + by_cases hlen : tag - F.threshold + 1 ≤ rest.length + · rw [if_pos hlen] at h + by_cases hov : + F.offset (tag - F.threshold + 1) + fromBe (rest.take (tag - F.threshold + 1)) + < 256 ^ F.tiers + · rw [if_pos hov] at h; simp at h + · -- Overflow branch: the decoded value is ≥ 256 ^ tiers. + have htpos : 0 < tag - F.threshold + 1 := by omega + have htle : tag - F.threshold + 1 ≤ F.tiers := by omega + have hnov : 256 ^ F.tiers + ≤ F.offset (tag - F.threshold + 1) + fromBe (rest.take (tag - F.threshold + 1)) := + Nat.not_lt.mp hov + have htlen : (rest.take (tag - F.threshold + 1)).length = tag - F.threshold + 1 := by + simp only [List.length_take]; omega + have hpb : ∀ b ∈ rest.take (tag - F.threshold + 1), b < 256 := fun b hb => + hbytes b (List.mem_cons_of_mem _ (mem_of_mem_take hb)) + have hpay : fromBe (rest.take (tag - F.threshold + 1)) < 256 ^ (tag - F.threshold + 1) := by + have := fromBe_lt hpb + rwa [htlen] at this + -- A tier strictly below the top fits entirely under `256 ^ tiers`, + -- so it cannot overflow. Hence the tier must be the top one. + have hfull : ¬ tag - F.threshold + 1 < F.tiers := by + intro htlt + have hsucc : F.offset (tag - F.threshold + 1 + 1) + = F.offset (tag - F.threshold + 1) + 256 ^ (tag - F.threshold + 1) := by + rw [F.offset_succ, F.capacity_eq_pow htpos] + have hmono : F.offset (tag - F.threshold + 1 + 1) ≤ F.offset F.tiers := + F.offset_le_offset (by omega) + have htop : F.offset F.tiers < 256 ^ F.tiers := F.offset_lt_pow F.tiers_pos + omega + omega + · rw [if_neg hlen] at h; simp at h + +/-- The bijection, packaged. On the value domain `[0, 256 ^ tiers)`: +`encode` is injective; `decode` recovers the value it encoded +(round-trip); and `decode` accepts nothing but canonical encodings. +Together these state that `encode` is a bijection from the value domain +onto the set of decodable byte strings. (Stated elementarily so the +development stays Mathlib-free.) -/ +theorem encode_bijection : + (∀ {v₁ v₂ : Nat}, v₁ < 256 ^ F.tiers → v₂ < 256 ^ F.tiers → + F.encode v₁ = F.encode v₂ → v₁ = v₂) + ∧ (∀ {v : Nat}, v < 256 ^ F.tiers → + F.decode (F.encode v) = .ok (v, (F.encode v).length)) + ∧ (∀ {bs : List Nat} {v n : Nat}, (∀ b ∈ bs, b < 256) → F.decode bs = .ok (v, n) → + v < 256 ^ F.tiers ∧ bs.take n = F.encode v) := + ⟨fun h₁ h₂ h => F.encode_injective h₁ h₂ h, + fun hv => F.decode_encode' hv, + fun hb h => ⟨(F.decode_ok hb h).1, (F.decode_ok hb h).2.2⟩⟩ + end Bijou.Family diff --git a/lean/Bijou/Instances.lean b/lean/Bijou/Instances.lean index 87dd61a..8ac9459 100644 --- a/lean/Bijou/Instances.lean +++ b/lean/Bijou/Instances.lean @@ -5,8 +5,8 @@ import Bijou.Order # The three specified width variants `bijou32`, `bijou64`, and `bijou128` instantiate the family, and every -test vector from the three SPEC documents is checked by reduction -(`rfl`). The general theorems (`decode_encode`, `decode_ok`, +test vector from the three SPEC documents is checked at compile time +with `#guard`. The general theorems (`decode_encode`, `decode_ok`, `encode_injective`, `decode_canonical`, `encode_lex_iff`) apply to all three instances directly. -/ @@ -24,111 +24,145 @@ def bijou128 : Family := ⟨16, by decide, by decide⟩ /-! ## Derived parameters match the SPECs -/ -example : bijou32.threshold = 252 := rfl -example : bijou64.threshold = 248 := rfl -example : bijou128.threshold = 240 := rfl +#guard bijou32.threshold = 252 +#guard bijou64.threshold = 248 +#guard bijou128.threshold = 240 -example : 256 ^ bijou32.tiers = 2 ^ 32 := by decide -example : 256 ^ bijou64.tiers = 2 ^ 64 := by decide -example : 256 ^ bijou128.tiers = 2 ^ 128 := by decide +#guard 256 ^ bijou32.tiers = 2 ^ 32 +#guard 256 ^ bijou64.tiers = 2 ^ 64 +#guard 256 ^ bijou128.tiers = 2 ^ 128 + +/-! ## Maximum encoding length (SPEC "maximum encoding length") -/ + +#guard bijou32.maxBytes = 5 +#guard bijou64.maxBytes = 9 +#guard bijou128.maxBytes = 17 /-! ## bijou64 offset table (SPEC.md "Offset Table") -/ -example : bijou64.offset 1 = 0xF8 := by decide -example : bijou64.offset 2 = 0x1F8 := by decide -example : bijou64.offset 3 = 0x101F8 := by decide -example : bijou64.offset 4 = 0x10101F8 := by decide -example : bijou64.offset 5 = 0x1010101F8 := by decide -example : bijou64.offset 6 = 0x101010101F8 := by decide -example : bijou64.offset 7 = 0x10101010101F8 := by decide -example : bijou64.offset 8 = 0x1010101010101F8 := by decide +#guard bijou64.offset 1 = 0xF8 +#guard bijou64.offset 2 = 0x1F8 +#guard bijou64.offset 3 = 0x101F8 +#guard bijou64.offset 4 = 0x10101F8 +#guard bijou64.offset 5 = 0x1010101F8 +#guard bijou64.offset 6 = 0x101010101F8 +#guard bijou64.offset 7 = 0x10101010101F8 +#guard bijou64.offset 8 = 0x1010101010101F8 + +/-! ## bijou32 / bijou128 offset tables (their SPEC.md vector tables) -/ + +#guard bijou32.offset 1 = 252 +#guard bijou32.offset 2 = 508 +#guard bijou32.offset 3 = 66044 +#guard bijou32.offset 4 = 16843260 + +#guard bijou128.offset 1 = 240 +#guard bijou128.offset 2 = 496 +#guard bijou128.offset 3 = 66032 +#guard bijou128.offset 4 = 16843248 /-! ## bijou64 test vectors (SPEC.md "Test Vectors") -/ -example : bijou64.encode 0 = [0x00] := rfl -example : bijou64.encode 1 = [0x01] := rfl -example : bijou64.encode 42 = [0x2A] := rfl -example : bijou64.encode 247 = [0xF7] := rfl -example : bijou64.encode 248 = [0xF8, 0x00] := rfl -example : bijou64.encode 300 = [0xF8, 0x34] := rfl -example : bijou64.encode 503 = [0xF8, 0xFF] := rfl -example : bijou64.encode 504 = [0xF9, 0x00, 0x00] := rfl -example : bijou64.encode 1000 = [0xF9, 0x01, 0xF0] := rfl -example : bijou64.encode 65535 = [0xF9, 0xFE, 0x07] := rfl -example : bijou64.encode 66039 = [0xF9, 0xFF, 0xFF] := rfl -example : bijou64.encode 66040 = [0xFA, 0x00, 0x00, 0x00] := rfl -example : bijou64.encode 67000 = [0xFA, 0x00, 0x03, 0xC0] := rfl -example : bijou64.encode 16843255 = [0xFA, 0xFF, 0xFF, 0xFF] := rfl -example : bijou64.encode 16843256 = [0xFB, 0x00, 0x00, 0x00, 0x00] := rfl -example : bijou64.encode 4311810551 = [0xFB, 0xFF, 0xFF, 0xFF, 0xFF] := rfl -example : bijou64.encode 72340172838076920 - = [0xFF, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00] := rfl -example : bijou64.encode 18446744073709551615 - = [0xFF, 0xFE, 0xFE, 0xFE, 0xFE, 0xFE, 0xFE, 0xFE, 0x07] := rfl - -example : bijou64.decode [0xF8, 0x34, 0xFF] = .ok (300, 2) := rfl -example : bijou64.decode [0xFF, 0xFE, 0xFE, 0xFE, 0xFE, 0xFE, 0xFE, 0xFE, 0x07] - = .ok (18446744073709551615, 9) := rfl +#guard bijou64.encode 0 = [0x00] +#guard bijou64.encode 1 = [0x01] +#guard bijou64.encode 42 = [0x2A] +#guard bijou64.encode 247 = [0xF7] +#guard bijou64.encode 248 = [0xF8, 0x00] +#guard bijou64.encode 300 = [0xF8, 0x34] +#guard bijou64.encode 503 = [0xF8, 0xFF] +#guard bijou64.encode 504 = [0xF9, 0x00, 0x00] +#guard bijou64.encode 1000 = [0xF9, 0x01, 0xF0] +#guard bijou64.encode 65535 = [0xF9, 0xFE, 0x07] +#guard bijou64.encode 66039 = [0xF9, 0xFF, 0xFF] +#guard bijou64.encode 66040 = [0xFA, 0x00, 0x00, 0x00] +#guard bijou64.encode 67000 = [0xFA, 0x00, 0x03, 0xC0] +#guard bijou64.encode 16843255 = [0xFA, 0xFF, 0xFF, 0xFF] +#guard bijou64.encode 16843256 = [0xFB, 0x00, 0x00, 0x00, 0x00] +#guard bijou64.encode 4311810551 = [0xFB, 0xFF, 0xFF, 0xFF, 0xFF] +#guard bijou64.encode 72340172838076920 + = [0xFF, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00] +#guard bijou64.encode 18446744073709551615 + = [0xFF, 0xFE, 0xFE, 0xFE, 0xFE, 0xFE, 0xFE, 0xFE, 0x07] + +#guard bijou64.decode [0xF8, 0x34, 0xFF] = .ok (300, 2) +#guard bijou64.decode [0xFF, 0xFE, 0xFE, 0xFE, 0xFE, 0xFE, 0xFE, 0xFE, 0x07] + = .ok (18446744073709551615, 9) /-! ## bijou64 error vectors (SPEC.md "Error Test Vectors") -/ -example : bijou64.decode [] = .error .bufferTooShort := rfl -example : bijou64.decode [0xF9, 0x00] = .error .bufferTooShort := rfl -example : bijou64.decode [0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF] - = .error .overflow := rfl +#guard bijou64.decode [] = .error .bufferTooShort +#guard bijou64.decode [0xF9, 0x00] = .error .bufferTooShort +#guard bijou64.decode [0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF] + = .error .overflow + +/-! ## No overlong encodings — executable evidence + +In VARU64, `[0xF8, 0x00]` is an overlong encoding of `0` that the +decoder must actively reject; forgetting the check silently accepts +it. In bijou the same bytes simply *mean a different value* — the tier +offset is load-bearing, so there is nothing to reject and nothing to +forget (SPEC.md "Canonicality"). +-/ + +#guard bijou64.decode [0xF8, 0x00] = .ok (248, 2) +#guard bijou64.decode [0xF9, 0x00, 0x00] = .ok (504, 3) +#guard bijou64.decode [0xFF, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00] + = .ok (72340172838076920, 9) +#guard bijou32.decode [0xFC, 0x00] = .ok (252, 2) +#guard bijou128.decode [0xF0, 0x00] = .ok (240, 2) /-! ## bijou32 test vectors (bijou32/SPEC.md) -/ -example : bijou32.encode 0 = [0x00] := rfl -example : bijou32.encode 1 = [0x01] := rfl -example : bijou32.encode 42 = [0x2A] := rfl -example : bijou32.encode 247 = [0xF7] := rfl -example : bijou32.encode 251 = [0xFB] := rfl -example : bijou32.encode 252 = [0xFC, 0x00] := rfl -example : bijou32.encode 300 = [0xFC, 0x30] := rfl -example : bijou32.encode 507 = [0xFC, 0xFF] := rfl -example : bijou32.encode 508 = [0xFD, 0x00, 0x00] := rfl -example : bijou32.encode 1000 = [0xFD, 0x01, 0xEC] := rfl -example : bijou32.encode 65535 = [0xFD, 0xFE, 0x03] := rfl -example : bijou32.encode 66043 = [0xFD, 0xFF, 0xFF] := rfl -example : bijou32.encode 66044 = [0xFE, 0x00, 0x00, 0x00] := rfl -example : bijou32.encode 67000 = [0xFE, 0x00, 0x03, 0xBC] := rfl -example : bijou32.encode 16843259 = [0xFE, 0xFF, 0xFF, 0xFF] := rfl -example : bijou32.encode 16843260 = [0xFF, 0x00, 0x00, 0x00, 0x00] := rfl -example : bijou32.encode 4294967295 = [0xFF, 0xFE, 0xFE, 0xFE, 0x03] := rfl - -example : bijou32.decode [] = .error .bufferTooShort := rfl -example : bijou32.decode [0xFD, 0x00] = .error .bufferTooShort := rfl -example : bijou32.decode [0xFF, 0xFF, 0xFF, 0xFF, 0xFF] = .error .overflow := rfl +#guard bijou32.encode 0 = [0x00] +#guard bijou32.encode 1 = [0x01] +#guard bijou32.encode 42 = [0x2A] +#guard bijou32.encode 247 = [0xF7] +#guard bijou32.encode 251 = [0xFB] +#guard bijou32.encode 252 = [0xFC, 0x00] +#guard bijou32.encode 300 = [0xFC, 0x30] +#guard bijou32.encode 507 = [0xFC, 0xFF] +#guard bijou32.encode 508 = [0xFD, 0x00, 0x00] +#guard bijou32.encode 1000 = [0xFD, 0x01, 0xEC] +#guard bijou32.encode 65535 = [0xFD, 0xFE, 0x03] +#guard bijou32.encode 66043 = [0xFD, 0xFF, 0xFF] +#guard bijou32.encode 66044 = [0xFE, 0x00, 0x00, 0x00] +#guard bijou32.encode 67000 = [0xFE, 0x00, 0x03, 0xBC] +#guard bijou32.encode 16843259 = [0xFE, 0xFF, 0xFF, 0xFF] +#guard bijou32.encode 16843260 = [0xFF, 0x00, 0x00, 0x00, 0x00] +#guard bijou32.encode 4294967295 = [0xFF, 0xFE, 0xFE, 0xFE, 0x03] + +#guard bijou32.decode [] = .error .bufferTooShort +#guard bijou32.decode [0xFD, 0x00] = .error .bufferTooShort +#guard bijou32.decode [0xFF, 0xFF, 0xFF, 0xFF, 0xFF] = .error .overflow /-! ## bijou128 test vectors (bijou128/SPEC.md) -/ -example : bijou128.encode 0 = [0x00] := rfl -example : bijou128.encode 1 = [0x01] := rfl -example : bijou128.encode 42 = [0x2A] := rfl -example : bijou128.encode 239 = [0xEF] := rfl -example : bijou128.encode 240 = [0xF0, 0x00] := rfl -example : bijou128.encode 241 = [0xF0, 0x01] := rfl -example : bijou128.encode 495 = [0xF0, 0xFF] := rfl -example : bijou128.encode 496 = [0xF1, 0x00, 0x00] := rfl -example : bijou128.encode 65535 = [0xF1, 0xFE, 0x0F] := rfl -example : bijou128.encode 66031 = [0xF1, 0xFF, 0xFF] := rfl -example : bijou128.encode 66032 = [0xF2, 0x00, 0x00, 0x00] := rfl -example : bijou128.encode 67000 = [0xF2, 0x00, 0x03, 0xC8] := rfl -example : bijou128.encode 16843247 = [0xF2, 0xFF, 0xFF, 0xFF] := rfl -example : bijou128.encode 16843248 = [0xF3, 0x00, 0x00, 0x00, 0x00] := rfl -example : bijou128.encode (2 ^ 32 - 1) = [0xF3, 0xFE, 0xFE, 0xFE, 0x0F] := rfl -example : bijou128.encode (2 ^ 64 - 1) - = [0xF7, 0xFE, 0xFE, 0xFE, 0xFE, 0xFE, 0xFE, 0xFE, 0x0F] := rfl -example : bijou128.encode (2 ^ 128 - 1) - = [0xFF, 0xFE, 0xFE, 0xFE, 0xFE, 0xFE, 0xFE, 0xFE, 0xFE, - 0xFE, 0xFE, 0xFE, 0xFE, 0xFE, 0xFE, 0xFE, 0x0F] := rfl - -example : bijou128.decode [] = .error .bufferTooShort := rfl -example : bijou128.decode [0xF1, 0x00] = .error .bufferTooShort := rfl -example : bijou128.decode +#guard bijou128.encode 0 = [0x00] +#guard bijou128.encode 1 = [0x01] +#guard bijou128.encode 42 = [0x2A] +#guard bijou128.encode 239 = [0xEF] +#guard bijou128.encode 240 = [0xF0, 0x00] +#guard bijou128.encode 241 = [0xF0, 0x01] +#guard bijou128.encode 495 = [0xF0, 0xFF] +#guard bijou128.encode 496 = [0xF1, 0x00, 0x00] +#guard bijou128.encode 65535 = [0xF1, 0xFE, 0x0F] +#guard bijou128.encode 66031 = [0xF1, 0xFF, 0xFF] +#guard bijou128.encode 66032 = [0xF2, 0x00, 0x00, 0x00] +#guard bijou128.encode 67000 = [0xF2, 0x00, 0x03, 0xC8] +#guard bijou128.encode 16843247 = [0xF2, 0xFF, 0xFF, 0xFF] +#guard bijou128.encode 16843248 = [0xF3, 0x00, 0x00, 0x00, 0x00] +#guard bijou128.encode (2 ^ 32 - 1) = [0xF3, 0xFE, 0xFE, 0xFE, 0x0F] +#guard bijou128.encode (2 ^ 64 - 1) + = [0xF7, 0xFE, 0xFE, 0xFE, 0xFE, 0xFE, 0xFE, 0xFE, 0x0F] +#guard bijou128.encode (2 ^ 128 - 1) + = [0xFF, 0xFE, 0xFE, 0xFE, 0xFE, 0xFE, 0xFE, 0xFE, 0xFE, + 0xFE, 0xFE, 0xFE, 0xFE, 0xFE, 0xFE, 0xFE, 0x0F] + +#guard bijou128.decode [] = .error .bufferTooShort +#guard bijou128.decode [0xF1, 0x00] = .error .bufferTooShort +#guard bijou128.decode [0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF] - = .error .overflow := rfl + = .error .overflow end Bijou diff --git a/lean/Bijou/Order.lean b/lean/Bijou/Order.lean index fac6a99..107041a 100644 --- a/lean/Bijou/Order.lean +++ b/lean/Bijou/Order.lean @@ -64,4 +64,16 @@ theorem encode_lex_iff {v₁ v₂ : Nat} exact absurd hlex (Lex.irrefl _) | inr hgt => exact absurd hlex (Lex.asymm (F.lex_encode_of_lt h₁ hgt)) +/-- Any two in-range encodings are comparable: byte order is total, so +encoded values can be sorted directly on their bytes. -/ +theorem encode_lex_trichotomy {v₁ v₂ : Nat} + (h₁ : v₁ < 256 ^ F.tiers) (h₂ : v₂ < 256 ^ F.tiers) : + Lex (F.encode v₁) (F.encode v₂) + ∨ F.encode v₁ = F.encode v₂ + ∨ Lex (F.encode v₂) (F.encode v₁) := by + rcases Nat.lt_trichotomy v₁ v₂ with h | h | h + · exact Or.inl (F.lex_encode_of_lt h₂ h) + · exact Or.inr (Or.inl (by rw [h])) + · exact Or.inr (Or.inr (F.lex_encode_of_lt h₁ h)) + end Bijou.Family diff --git a/lean/Bijou/Spec.lean b/lean/Bijou/Spec.lean index 4231eb4..8bde048 100644 --- a/lean/Bijou/Spec.lean +++ b/lean/Bijou/Spec.lean @@ -26,6 +26,11 @@ inductive DecodeError where | overflow deriving DecidableEq, Repr +-- Needed so the decode test vectors in `Bijou.Instances` (whose results +-- are `Except DecodeError (Nat × Nat)`) can be checked with `#guard`. +-- Lean core derives `DecidableEq` for `Except` only on demand. +deriving instance DecidableEq for Except + namespace Family variable (F : Family) @@ -91,6 +96,56 @@ theorem encode_bytes_lt {v : Nat} (hv : v < 256 ^ F.tiers) : rw [F.offset_succ, F.capacity_eq_pow h3] at h2 exact beBytes_lt_256 (by omega) b h +/-- Values below the threshold encode as the single byte equal to the +value (SPEC: "values 0–247 are encoded as a single byte equal to the +value"). -/ +theorem encode_lt_threshold {v : Nat} (h : v < F.threshold) : F.encode v = [v] := by + simp [encode, h] + +/-- Every encoding is at least one byte long. -/ +theorem encodedLen_pos (v : Nat) : 1 ≤ F.encodedLen v := by + simp only [encodedLen] + split <;> omega + +/-- Maximum encoding length, as a parameter of the family: `tiers + 1` +bytes (9 for bijou64, 5 for bijou32, 17 for bijou128). -/ +def maxBytes : Nat := F.tiers + 1 + +/-- The encoding never exceeds `maxBytes` (SPEC: "maximum encoding +length is 9 bytes"). -/ +theorem encodedLen_le (v : Nat) : F.encodedLen v ≤ F.maxBytes := by + have := F.tierOf_le v + simp only [encodedLen, maxBytes] + split <;> omega + +/-- The total encoding length, recovered from the tag byte alone. -/ +def lenFromTag (tag : Nat) : Nat := + if tag < F.threshold then 1 else tag - F.threshold + 2 + +/-- Length is determined entirely by the first byte: the count of bytes +a successful `decode` consumes is a function of the tag alone, with no +inspection of the payload. This is the SPEC design goal that enables +`O(1)` skipping and streaming framing. -/ +theorem decode_consumed_from_tag {tag : Nat} {rest : List Nat} {v n : Nat} + (h : F.decode (tag :: rest) = .ok (v, n)) : n = F.lenFromTag tag := by + simp only [decode] at h + simp only [lenFromTag] + by_cases htag : tag < F.threshold + · rw [if_pos htag] at h ⊢ + simp only [Except.ok.injEq, Prod.mk.injEq] at h + omega + · rw [if_neg htag] at h ⊢ + by_cases hlen : tag - F.threshold + 1 ≤ rest.length + · rw [if_pos hlen] at h + by_cases hov : + F.offset (tag - F.threshold + 1) + fromBe (rest.take (tag - F.threshold + 1)) + < 256 ^ F.tiers + · rw [if_pos hov] at h + simp only [Except.ok.injEq, Prod.mk.injEq] at h + omega + · rw [if_neg hov] at h; simp at h + · rw [if_neg hlen] at h; simp at h + end Family end Bijou