diff --git a/Algolean.lean b/Algolean.lean index e516a67..afffc37 100644 --- a/Algolean.lean +++ b/Algolean.lean @@ -2,6 +2,7 @@ module -- shake: keep-all --deprecated_module: ignore public import Algolean.AddWriter.Basic public import Algolean.AddWriter.Transformer +public import Algolean.AddWriter.WP public import Algolean.Algorithms.BoyerMooreMajorityVote public import Algolean.Algorithms.Circuits.FanInTwo.LogAnd public import Algolean.Algorithms.KMPPatternSearch @@ -13,13 +14,22 @@ public import Algolean.Algorithms.MergeSort public import Algolean.Algorithms.NaivePatternSearch public import Algolean.Algorithms.VecBubbleSort public import Algolean.Algorithms.VecSearch -public import Algolean.Algorithms.WordRAMLinearSearch +public import Algolean.Algorithms.WordRAM.Basic +public import Algolean.Algorithms.WordRAM.BinarySearch.Algorithm +public import Algolean.Algorithms.WordRAM.BinarySearch.Common +public import Algolean.Algorithms.WordRAM.BinarySearch.Complexity +public import Algolean.Algorithms.WordRAM.BinarySearch.Correctness +public import Algolean.Algorithms.WordRAM.LinearSearch.Algorithm +public import Algolean.Algorithms.WordRAM.LinearSearch.Common +public import Algolean.Algorithms.WordRAM.LinearSearch.Complexity +public import Algolean.Algorithms.WordRAM.LinearSearch.Correctness public import Algolean.Complexity.Basic public import Algolean.Complexity.PolytimeBasicClasses public import Algolean.FreeWP.Effects public import Algolean.FreeWP.WP public import Algolean.LowerBounds.ComparisonSort public import Algolean.ModelM +public import Algolean.ModelStateM public import Algolean.Models.Arithmetic public import Algolean.Models.Circuits public import Algolean.Models.Comparison @@ -36,5 +46,8 @@ public import Algolean.Models.ReadWriteVec public import Algolean.Models.RobertsonWebb public import Algolean.Models.SingleTapeTM public import Algolean.Models.WordRAM +public import Algolean.Models.WordRAMSyntax +public import Algolean.Problems.Basic +public import Algolean.Problems.Search public import Algolean.QueryComposition public import Algolean.QueryModel diff --git a/Algolean/AddWriter/Transformer.lean b/Algolean/AddWriter/Transformer.lean index 549e631..1dfea4a 100644 --- a/Algolean/AddWriter/Transformer.lean +++ b/Algolean/AddWriter/Transformer.lean @@ -120,6 +120,25 @@ theorem cost_bind [Monad m] [LawfulMonad m] [Add Cost] pure (a.tell + b.tell)) := by simp only [cost, run_bind, map_bind, map_pure] +/-- Joint writer/state bind at a concrete state, without opaque intermediate pair matches. -/ +@[simp, grind =] theorem run_bind_state [Add Cost] + (x : AddWriterT Cost (StateM σ) α) (f : α → AddWriterT Cost (StateM σ) β) (s : σ) : + (x >>= f).run s = + let first := x.run s + let rest := (f first.fst.ret).run first.snd + ((⟨rest.fst.ret, first.fst.tell + rest.fst.tell⟩ : AddWriter Cost β), rest.snd) := rfl + +/-- Pure writer/state execution produces no cost. -/ +@[simp, grind =] theorem run_pure_state [Zero Cost] (a : α) (s : σ) : + (pure a : AddWriterT Cost (StateM σ) α).run s = + ((⟨a, 0⟩ : AddWriter Cost α), s) := rfl + +/-- Mapping changes the result while preserving the cost and state. -/ +@[simp, grind =] theorem run_map_state (f : α → β) + (x : AddWriterT Cost (StateM σ) α) (s : σ) : + (f <$> x).run s = + ((⟨f (x.run s).fst.ret, (x.run s).fst.tell⟩ : AddWriter Cost β), (x.run s).snd) := rfl + @[ext] protected theorem ext (x y : AddWriterT Cost m α) (h : x.run = y.run) : x = y := h diff --git a/Algolean/AddWriter/WP.lean b/Algolean/AddWriter/WP.lean new file mode 100644 index 0000000..b7fcbbd --- /dev/null +++ b/Algolean/AddWriter/WP.lean @@ -0,0 +1,87 @@ +/- +Copyright (c) 2026 Shreyas Srinivas. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Shreyas Srinivas +-/ + +module + +public import Algolean.AddWriter.Transformer +public import Std.Do + +/-! +# Weakest preconditions for additive writer computations + +The extra postcondition argument is an accumulated cost. Starting it at zero gives the cost +reported by `run`; an arbitrary initial cost permits compositional reasoning across binds. +-/ + +@[expose] public section + +namespace Algolean.AddWriterT + +open Std.Do Std.Do.WPMonad + +variable {Cost : Type u} {m : Type u → Type v} {ps : PostShape.{u}} + +/-- Interpret the writer output as an increment to a logical cost accumulator. -/ +def toStateT [Functor m] [Add Cost] (x : AddWriterT Cost m α) : StateT Cost m α := + fun initial => (fun a => (a.ret, initial + a.tell)) <$> x.run + +/-- Expose the accumulated cost without unfolding the state transformer. -/ +@[simp] theorem toStateT_run [Functor m] [Add Cost] + (x : AddWriterT Cost m α) (initial : Cost) : + x.toStateT.run initial = (fun a => (a.ret, initial + a.tell)) <$> x.run := rfl + +@[simp] theorem toStateT_pure [Monad m] [LawfulMonad m] [AddZeroClass Cost] (a : α) : + toStateT (pure a : AddWriterT Cost m α) = pure a := by + funext initial + simp [toStateT] + rfl + +@[simp] theorem toStateT_bind [Monad m] [LawfulMonad m] [AddSemigroup Cost] + (x : AddWriterT Cost m α) (f : α → AddWriterT Cost m β) : + toStateT (x >>= f) = (toStateT x >>= fun a => toStateT (f a)) := by + apply StateT.ext + intro initial + rw [StateT.run_bind] + simp [toStateT, StateT.run, bind_map_left, add_assoc] + +/-- Writer weakest preconditions expose accumulated cost before the underlying post-shape. -/ +instance [Functor m] [Add Cost] [WP m ps] : WP (AddWriterT Cost m) (.arg Cost ps) where + wp x := wp x.toStateT + +/-- The cost-accumulator interpretation respects pure and bind. -/ +instance [Monad m] [AddMonoid Cost] [WPMonad m ps] : + WPMonad (AddWriterT Cost m) (.arg Cost ps) where + wp_pure a := by + change wp (toStateT (pure a : AddWriterT Cost m _)) = _ + rw [toStateT_pure, wp_pure] + wp_bind x f := by + change wp (toStateT (x >>= f)) = _ + rw [toStateT_bind, wp_bind] + rfl + +/-- Expose the underlying state interpretation to verification condition generation. -/ +theorem wp_eq_wp_toStateT [Functor m] [Add Cost] [WP m ps] + (x : AddWriterT Cost m α) : wp x = wp x.toStateT := rfl + +/-- A writer over state exposes its result, accumulated cost, and final physical state. -/ +@[simp] theorem wp_apply_state [Add Cost] (x : AddWriterT Cost (StateM σ) α) + (Q : PostCond α (.arg Cost (.arg σ .pure))) (initial : Cost) (s : σ) : + (wp x).apply Q initial s = + Q.fst (x.run s).fst.ret (initial + (x.run s).fst.tell) (x.run s).snd := rfl + +/-- Optional state execution exposes either the exact joint result or its failure postcondition. -/ +@[simp] theorem wp_apply_state_option [Add Cost] (x : AddWriterT Cost (StateT σ Option) α) + (Q : PostCond α (.arg Cost (.arg σ (.except PUnit .pure)))) (initial : Cost) (s : σ) : + (wp x).apply Q initial s = + match x.run s with + | none => Q.snd.fst PUnit.unit + | some (result, final) => Q.fst result.ret (initial + result.tell) final := by + dsimp [wp_eq_wp_toStateT, wp, toStateT, PredTrans.apply] + simp only [StateT.run_map] + dsimp only [StateT.run] + cases x.run s <;> rfl + +end Algolean.AddWriterT diff --git a/Algolean/Algorithms/WordRAM/Basic.lean b/Algolean/Algorithms/WordRAM/Basic.lean new file mode 100644 index 0000000..cd930d1 --- /dev/null +++ b/Algolean/Algorithms/WordRAM/Basic.lean @@ -0,0 +1,110 @@ +/- +Copyright (c) 2026 Shreyas Srinivas. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Shreyas Srinivas +-/ + +module + +public import Algolean.Models.WordRAM +public import Algolean.Problems.Search + +/-! +# Supporting definitions for WordRAM search algorithms + +Search representations, the linear-search input layout and state constructor, output decoding, +and input memory regions are defined together in `Algolean.Problems.Search`. + +This file supplies the bounds and initial memory layout used by binary search, word-address +arithmetic, sorted-array lemmas, and `Executes`, the completed-execution relation used by +both algorithms' correctness and complexity proofs. +-/ + +@[expose] public section + +namespace Algolean.Algorithms.WordRAM + +/-- The abstract sortedness relation instantiated with unsigned word order. -/ +abbrev SortedWords (input : Array (Word w)) : Prop := + Search.SortedBy (fun a b => a.toNat ≤ b.toNat) input + +/-- Search inputs constrain the array and key register, not scratch registers or flags. -/ +structure RepresentsSearchInput (input : Search.Input (Word w)) (key : Register k) + (s : RAMState w k) : Prop extends RepresentsArray input.data s.Memory where + /-- The designated register contains the abstract key. -/ + key_eq : s.Registers key = input.key + +/-- Runtime bounds for a search: an inclusive last address and a nonempty flag. +This represents empty arrays and all `2^w` cells, even when `w = 0`. -/ +structure RepresentsBoundedSearchInput (input : Search.Input (Word w)) + (key last : Register k) (s : RAMState w k) : Prop + extends RepresentsSearchInput input key s where + /-- Last input address; ignored for an empty input. -/ + last_eq : s.Registers last = BitVec.ofNat w (input.data.size - 1) + /-- The initial less-than flag indicates whether there is an interval to search. -/ + nonempty_eq : s.Flags .ult = decide (input.data.size ≠ 0) + +/-- Array layout used by the initial machine state. -/ +def arrayMemory (input : Array (BitVec w)) : Memory w := + fun addr => input[addr.toNat]?.getD 0 + +@[grind =] theorem wordAddress_toNat (i : Nat) (hi : i < 2 ^ w) : + (BitVec.ofNat w i).toNat = i := Nat.mod_eq_of_lt hi + +@[simp, grind =] theorem arrayMemory_ofNat (input : Array (BitVec w)) + (hfits : input.size ≤ 2 ^ w) (i : Nat) (hi : i < input.size) : + arrayMemory input (BitVec.ofNat w i) = input[i] := by + simp [arrayMemory, BitVec.toNat_ofNat, Nat.mod_eq_of_lt (lt_of_lt_of_le hi hfits), hi] + +/-- If the array fits in memory, `arrayMemory` stores each element at its index. -/ +@[simp] theorem arrayMemory_represents (input : Array (Word w)) (hfits : input.size ≤ 2 ^ w) : + RepresentsArray input (arrayMemory input) := + ⟨hfits, fun i hi => arrayMemory_ofNat input hfits i hi⟩ + +@[grind =] theorem wordAddress_succ (i : Nat) : + BitVec.ofNat w i + 1 = BitVec.ofNat w (i + 1) := (BitVec.ofNat_add i 1).symm + +/-- In a sorted word array, words at or before a value below the key cannot match it. -/ +@[grind →] theorem SortedWords.exclude_left {input : Array (Word w)} (h : SortedWords input) + {target : Word w} {pivot : Nat} (hp : pivot < input.size) + (hlt : input[pivot].toNat < target.toNat) (i : Nat) (hi : i ≤ pivot) : + input[i]? ≠ some target := by + have hib : i < input.size := by lia + have hs := h i pivot hib hp hi + intro heq + have heq' : input[i] = target := by simpa [hib] using heq + rw [heq'] at hs + lia + +/-- In a sorted word array, words at or after a value above the key cannot match it. -/ +@[grind →] theorem SortedWords.exclude_right {input : Array (Word w)} (h : SortedWords input) + {target : Word w} {pivot : Nat} (hp : pivot < input.size) + (hlt : target.toNat < input[pivot].toNat) (i : Nat) (hi : pivot ≤ i) + (hib : i < input.size) : input[i]? ≠ some target := by + have hs := h pivot i hp hib hi + intro heq + have heq' : input[i] = target := by simpa [hib] using heq + rw [heq'] at hs + lia + +/-- Subtracting one converts a positive address to the preceding index without wrapping. -/ +theorem word_pred_toNat (x : BitVec w) (hx : 0 < x.toNat) : + (x - 1).toNat = x.toNat - 1 := by + have h := BitVec.ofNat_sub_ofNat_of_le (w := w) x.toNat 1 (by have := x.isLt; lia) hx + have h' := congrArg BitVec.toNat h + simpa [Nat.mod_eq_of_lt (show x.toNat - 1 < 2 ^ w by have := x.isLt; lia)] using h' + +/-- Completed execution in the time-and-space model, hiding interpreter fuel. +Unused fuel is allowed and is not charged as time. -/ +def Executes (program : Prog (WordRAM w k) Unit) (s : RAMState w k) + (cost : RAMCost w k) (t : RAMState w k) : Prop := + ∃ fuel remaining, execute fuel program s = some (⟨(), cost⟩, ⟨t, remaining⟩) + +/-- If a program's instructions finish with the stated cost and final state, +the program satisfies `Executes` with that same cost and state. -/ +theorem Completes.executes {program : Prog (WordRAM w k) Unit} + (h : Completes (instructions program) s cost t) : Executes program s cost t := by + obtain ⟨fuel, hr⟩ := h.execute + exact ⟨fuel, 0, hr⟩ + +end Algolean.Algorithms.WordRAM diff --git a/Algolean/Algorithms/WordRAM/BinarySearch/Algorithm.lean b/Algolean/Algorithms/WordRAM/BinarySearch/Algorithm.lean new file mode 100644 index 0000000..8f9c414 --- /dev/null +++ b/Algolean/Algorithms/WordRAM/BinarySearch/Algorithm.lean @@ -0,0 +1,91 @@ +/- +Copyright (c) 2026 Shreyas Srinivas. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Shreyas Srinivas +-/ + +module + +public import Algolean.Algorithms.WordRAM.Basic +public import Algolean.Models.WordRAMSyntax + +/-! +# Binary search in the word-RAM model + +The program searches a sorted array using six registers and no extra memory. +The initial state supplies the search key, the last array address, and a flag indicating +whether the array is nonempty. The same program handles every input size that fits in +memory at word width `w`, including arrays that use all `2 ^ w` cells. + +The midpoint is `lo + (hi - lo) / 2`. Bounds checks prevent address arithmetic from wrapping. + +Adapted from https://github.com/Shreyas4991/Algolean/pull/89. +-/ + +@[expose] public section + +namespace Algolean.Algorithms.WordRAM + +open scoped WordRAM Prog + +namespace BinarySearch + +/-- Register holding the first address still to search. -/ +abbrev lower : Register 6 := 0 +/-- Register holding the last address still to search. -/ +abbrev upper : Register 6 := 1 +/-- Register holding the midpoint address, or a matching address when found. -/ +abbrev middle : Register 6 := 2 +/-- Register holding the word loaded from the midpoint address. -/ +abbrev value : Register 6 := 3 +/-- Register holding the search key. -/ +abbrev key : Register 6 := 4 +/-- Register holding the constant one. -/ +abbrev one : Register 6 := 5 + +/-- One machine iteration, with its continuation indicated by the less-than flag. -/ +def body (w : Nat) : Prog (WordRAM w 6) Unit := do [WordRAM w 6] + middle ←ᵣ upper - lower + middle ←ᵣ middle >>> one + middle ←ᵣ lower + middle + value ←ᵣ mem[middle] + ifₚ value =ᵣ key then + reset .ult + else + ifₚ value <ᵣ key then + ifₚ middle <ᵣ upper then + lower ←ᵣ middle + one + else + nop + else + ifₚ lower <ᵣ middle then + upper ←ᵣ middle - one + else + nop + +/-- Initialize the lower endpoint and increment constant; the upper endpoint is runtime input. -/ +def setup (w : Nat) : Prog (WordRAM w 6) Unit := do [WordRAM w 6] + lower ←ᵣ imm[0] + one ←ᵣ imm[1] + +end BinarySearch + +/-- Uniform binary search: width determines code; memory, key, last address, and the +nonempty flag supply the runtime input. -/ +def binarySearch (w : Nat) : Prog (WordRAM w 6) Unit := do [WordRAM w 6] + reset .eq + ifₚ flag .ult then + BinarySearch.setup w + whileₚ .ult do + BinarySearch.body w + else + nop + +/-- Store the input array and search key, and initialize the bounds and flags for binary search. -/ +def binarySearchState (input : Array (Word w)) (target : Word w) : RAMState w 6 := + ⟨arrayMemory input, + fun r => if r = BinarySearch.key then target + else if r = BinarySearch.upper then BitVec.ofNat w (input.size - 1) else 0, + fun op => if op = .ult then decide (input.size ≠ 0) else false⟩ + +end Algolean.Algorithms.WordRAM diff --git a/Algolean/Algorithms/WordRAM/BinarySearch/Common.lean b/Algolean/Algorithms/WordRAM/BinarySearch/Common.lean new file mode 100644 index 0000000..112bc09 --- /dev/null +++ b/Algolean/Algorithms/WordRAM/BinarySearch/Common.lean @@ -0,0 +1,401 @@ +/- +Copyright (c) 2026 Shreyas Srinivas. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Shreyas Srinivas +-/ + +module + +public import Algolean.Algorithms.WordRAM.BinarySearch.Algorithm +public import Mathlib.Data.Nat.Log + +/-! +# Shared proofs for binary search + +Lemmas about address arithmetic, each loop iteration, and the complete search, +used by the correctness and complexity proofs. +-/ + +@[expose] public section + +namespace Algolean.Algorithms.WordRAM + +open scoped WordRAM Prog + +@[simp] theorem binarySearchState_represents (input : Array (Word w)) (target : Word w) + (hfits : input.size ≤ 2 ^ w) : + RepresentsBoundedSearchInput ⟨input, target⟩ BinarySearch.key BinarySearch.upper + (binarySearchState input target) := + ⟨⟨arrayMemory_represents input hfits, by simp [binarySearchState]⟩, + by simp [binarySearchState, BinarySearch.upper, BinarySearch.key], + by simp [binarySearchState]⟩ + +open BinarySearch + +attribute [local simp] lower upper middle value key one CmpOp.eval BinOp.eval wordAddress_toNat + +/-- The word midpoint agrees with the natural midpoint, even when input fills memory. -/ +@[grind =] theorem wordAddress_mid (lo hi : Nat) (hlo : lo ≤ hi) (hhi : hi < 2 ^ w) : + BitVec.ofNat w lo + ((BitVec.ofNat w hi - BitVec.ofNat w lo) >>> (1 : Word w).toNat) = + BitVec.ofNat w (lo + (hi - lo) / 2) := by + rw [BitVec.ofNat_sub_ofNat_of_le hi lo (by lia) hlo, BitVec.ofNat_add] + congr 1 + apply BitVec.eq_of_toNat_eq + cases w with + | zero => simp; lia + | succ w => + have hd : hi - lo < 2 ^ (w + 1) := by lia + have hh : (hi - lo) / 2 < 2 ^ (w + 1) := by lia + simp [BitVec.toNat_ushiftRight, Nat.shiftRight_eq_div_pow, + Nat.mod_eq_of_lt hd, Nat.mod_eq_of_lt hh] + +attribute [local simp] wordAddress_mid wordAddress_toNat + +/-- Decrementing a positive representable address does not wrap. -/ +@[grind =] theorem wordAddress_pred (i : Nat) (hi : i < 2 ^ w) (hpos : 0 < i) : + BitVec.ofNat w i - 1 = BitVec.ofNat w (i - 1) := + BitVec.ofNat_sub_ofNat_of_le i 1 (by lia) hpos + +/-- Equality of representable natural addresses is preserved by word conversion. -/ +@[simp] theorem wordAddress_eq_iff (i j : Nat) (hi : i < 2 ^ w) (hj : j < 2 ^ w) : + BitVec.ofNat w i = BitVec.ofNat w j ↔ i = j := by + constructor + · intro h + have := congrArg BitVec.toNat h + grind + · exact congrArg (BitVec.ofNat w) + +private def midpoint (s : RAMState w 6) : Word w := + s.Registers lower + ((s.Registers upper - s.Registers lower) >>> (s.Registers one).toNat) + +private def checked (s : RAMState w 6) (found active : Bool) : RAMState w 6 := + (((s.writeRegister middle (midpoint s)).writeRegister value (s.Memory (midpoint s))).writeFlag + .eq found).writeFlag .ult active + +@[simp, grind =] private theorem checked_memory (s : RAMState w 6) (found active : Bool) : + (checked s found active).Memory = s.Memory := rfl + +@[simp, grind =] private theorem checked_registers (s : RAMState w 6) (found active : Bool) + (r : Register 6) : (checked s found active).Registers r = + if r = value then s.Memory (midpoint s) + else if r = middle then midpoint s else s.Registers r := by + simp [checked] + +@[simp, grind =] private theorem checked_flags (s : RAMState w 6) (found active : Bool) + (op : CmpOp) : (checked s found active).Flags op = + if op = .ult then active else found := by + cases op <;> simp [checked] + +private theorem body_found (s : RAMState w 6) + (h : s.Memory (midpoint s) = s.Registers key) : + Completes (instructions (body w)) s ⟨6, {midpoint s}⟩ (checked s true false) := +by + simp only [midpoint, lower, upper, key, one] at h + exact ⟨7, by simp [body, checked, branch, runCode, step, midpoint, h]⟩ + +private theorem body_right (s : RAMState w 6) + (h : s.Memory (midpoint s) ≠ s.Registers key) + (hlt : (s.Memory (midpoint s)).toNat < (s.Registers key).toNat) + (hb : (midpoint s).toNat < (s.Registers upper).toNat) : + Completes (instructions (body w)) s ⟨8, {midpoint s}⟩ + ((checked s false true).writeRegister lower (midpoint s + s.Registers one)) := +by + simp only [midpoint, lower, upper, key, one, + BitVec.toNat_add, BitVec.toNat_sub, BitVec.toNat_ushiftRight] at h hlt hb + exact ⟨11, by simp [body, checked, branch, runCode, step, midpoint, h, hlt, hb]⟩ + +private theorem body_stop_right (s : RAMState w 6) + (h : s.Memory (midpoint s) ≠ s.Registers key) + (hlt : (s.Memory (midpoint s)).toNat < (s.Registers key).toNat) + (hb : ¬(midpoint s).toNat < (s.Registers upper).toNat) : + Completes (instructions (body w)) s ⟨8, {midpoint s}⟩ + (checked s false false) := +by + simp only [midpoint, lower, upper, key, one, + BitVec.toNat_add, BitVec.toNat_sub, BitVec.toNat_ushiftRight] at h hlt hb + exact ⟨11, by simp [body, checked, branch, runCode, step, midpoint, h, hlt, hb]⟩ + +private theorem body_left (s : RAMState w 6) + (h : s.Memory (midpoint s) ≠ s.Registers key) + (hlt : ¬(s.Memory (midpoint s)).toNat < (s.Registers key).toNat) + (hb : (s.Registers lower).toNat < (midpoint s).toNat) : + Completes (instructions (body w)) s ⟨8, {midpoint s}⟩ + ((checked s false true).writeRegister upper (midpoint s - s.Registers one)) := +by + simp only [midpoint, lower, upper, key, one, + BitVec.toNat_add, BitVec.toNat_sub, BitVec.toNat_ushiftRight] at h hlt hb + exact ⟨11, by simp [body, checked, branch, runCode, step, midpoint, h, hlt, hb]⟩ + +private theorem body_stop_left (s : RAMState w 6) + (h : s.Memory (midpoint s) ≠ s.Registers key) + (hlt : ¬(s.Memory (midpoint s)).toNat < (s.Registers key).toNat) + (hb : ¬(s.Registers lower).toNat < (midpoint s).toNat) : + Completes (instructions (body w)) s ⟨8, {midpoint s}⟩ + (checked s false false) := +by + simp only [midpoint, lower, upper, key, one, + BitVec.toNat_add, BitVec.toNat_sub, BitVec.toNat_ushiftRight] at h hlt hb + exact ⟨11, by simp [body, checked, branch, runCode, step, midpoint, h, hlt, hb]⟩ + + +private theorem log2_half_bound (n k : Nat) (hn : 2 ≤ n) (hk : k ≤ n / 2) : + k.log2 + 1 ≤ n.log2 := by + have h : k.log2 ≤ (n / 2).log2 := by + simpa only [Nat.log2_eq_log_two] using Nat.log_mono_right (b := 2) hk + rw [Nat.log2_def n, if_pos hn] + lia + +/-- One charged iteration plus a half-sized recursive search preserves the logarithmic bound. -/ +private theorem step_time_bound {time size remaining : Nat} + (ht : time ≤ 8 * remaining.log2 + 8) (hsize : 2 ≤ size) (hhalf : remaining ≤ size / 2) : + 8 + time ≤ 8 * size.log2 + 8 := by + have := log2_half_bound size remaining hsize hhalf + lia + +private theorem pivot_bounds {lo hi : Nat} (h : lo ≤ hi) : + lo ≤ lo + (hi - lo) / 2 ∧ lo + (hi - lo) / 2 ≤ hi := by lia + +@[simp, grind =] private theorem right_length {lo hi : Nat} + (h : lo + (hi - lo) / 2 < hi) : + hi - (lo + (hi - lo) / 2 + 1) + 1 = (hi - lo + 1) / 2 := by lia + +@[simp, grind =] private theorem left_length {lo hi : Nat} + (h : lo < lo + (hi - lo) / 2) : + lo + (hi - lo) / 2 - 1 - lo + 1 = (hi - lo) / 2 := by lia + +/-- On a nonempty right half, exactly one logarithmic level has been consumed. -/ +private theorem right_log {lo hi : Nat} + (h : lo + (hi - lo) / 2 < hi) : + 8 + (8 * (hi - (lo + (hi - lo) / 2 + 1) + 1).log2 + 8) = + 8 * (hi - lo + 1).log2 + 8 := by + rw [right_length h, Nat.log2_def (hi - lo + 1), if_pos (by lia : 2 ≤ hi - lo + 1)] + lia + +private structure Summary (input : Array (Word w)) (target : Word w) (lo hi : Nat) + (s t : RAMState w 6) (cost : RAMCost w 6) : Prop where + memory : t.Memory = s.Memory + addresses : cost.addresses ⊆ inputRegion input + found : t.Flags .eq = true → + let i := (t.Registers middle).toNat + lo ≤ i ∧ i ≤ hi ∧ input[i]? = some target + not_found : t.Flags .eq = false → SortedWords input → + ∀ i, lo ≤ i → i ≤ hi → input[i]? ≠ some target + time : cost.time ≤ 8 * (hi - lo + 1).log2 + 8 + worst : 0 < w → s.Memory = (fun _ => 0) → s.Registers key = 1 → + cost.time = 8 * (hi - lo + 1).log2 + 8 + +private theorem loop_spec (input : Array (Word w)) (target : Word w) (n lo hi : Nat) + (hlo : lo ≤ hi) (hhi : hi < input.size) (hn : hi - lo < n) (s : RAMState w 6) + (hmem : RepresentsArray input s.Memory) + (hl : s.Registers lower = BitVec.ofNat w lo) + (hh : s.Registers upper = BitVec.ofNat w hi) (hk : s.Registers key = target) + (h1 : s.Registers one = 1) (ha : s.Flags .ult = true) : + ∃ cost t, Completes (instructions (whileLoop .ult (body w))) s cost t ∧ + Summary input target lo hi s t cost := by + induction n generalizing lo hi s with + | zero => lia + | succ n ih => + let pivot := lo + (hi - lo) / 2 + have hp := pivot_bounds hlo + have hpi : pivot < input.size := by lia + have hm : midpoint s = BitVec.ofNat w pivot := by + simpa only [midpoint, hl, hh, h1] using wordAddress_mid lo hi hlo (hmem.index_lt hhi) + have hread := hmem.read_of_eq hpi hm + have hprobe := ofNat_mem_inputRegion input pivot hpi + have hpn := hmem.toNat_of_eq hpi hm + have hln := hmem.toNat_of_eq (by lia : lo < input.size) hl + have hhn := hmem.toNat_of_eq hhi hh + by_cases heq : input[pivot] = target + · have heq' : s.Memory (midpoint s) = s.Registers key := by simpa only [hread, hk] using heq + have hb := body_found s heq' + refine ⟨_, _, hb.while_stop ha (by simp), ?_⟩ + constructor + · simp + · simpa only [add_zero, Finset.singleton_subset_iff, hm] using hprobe + · intro _ + simpa [hpn, hpi, heq, pivot] using hp + · simp + · dsimp; lia + · intro hw hz hk1 + have hbad : (0 : Word w) = 1 := by simpa [hz, hk1] using heq' + simp [ne_of_gt hw] at hbad + · have hne : s.Memory (midpoint s) ≠ s.Registers key := by simpa only [hread, hk] using heq + by_cases hlt : input[pivot].toNat < target.toNat + · have hcmp : (s.Memory (midpoint s)).toNat < (s.Registers key).toNat := by + simpa only [hread, hk] using hlt + by_cases hright : pivot < hi + · let next := (checked s false true).writeRegister lower (BitVec.ofNat w (pivot + 1)) + have hb : Completes (instructions (body w)) s ⟨8, {BitVec.ofNat w pivot}⟩ next := by + simpa only [next, hm, h1, wordAddress_succ] using body_right s hne hcmp + (by simpa only [hpn, hhn] using hright) + obtain ⟨cost, t, hr, hs⟩ := ih (pivot + 1) hi (by lia) hhi (by lia) next + (by simpa [next] using hmem) (by simp [next]) (by simp [next, hh]) + (by simp [next, hk]) (by simp [next, h1]) (by simp [next]) + refine ⟨_, t, completes_while_true .ult (body w) ha hb hr, ?_⟩ + constructor + · simpa [next] using hs.memory + · exact Finset.union_subset (Finset.singleton_subset_iff.mpr hprobe) hs.addresses + · intro hf + obtain ⟨hi₁, hi₂, hm⟩ := hs.found hf + exact ⟨by lia, hi₂, hm⟩ + · intro hf hsorted i hil hih + by_cases hip : i ≤ pivot + · exact hsorted.exclude_left hpi hlt i hip + · exact hs.not_found hf hsorted i (by lia) hih + · exact step_time_bound hs.time (by lia) (by simp [pivot, right_length hright]) + · intro hw hz hk1 + simpa only [RAMCost.mk_add, hs.worst hw (by simp [next, hz]) + (by simp [next, hk1])] using right_log hright + · have hb := body_stop_right s hne hcmp (by simpa only [hpn, hhn] using hright) + refine ⟨_, _, hb.while_stop ha (by simp), ?_⟩ + constructor + · simp + · simpa only [add_zero, Finset.singleton_subset_iff, hm] using hprobe + · simp + · intro _ hsorted i hil hih + exact hsorted.exclude_left hpi hlt i (by lia) + · dsimp; lia + · intro _ _ _ + have hlen : hi - lo + 1 = 1 := by dsimp [pivot] at *; lia + simp [hlen, Nat.log2_def] + · have hcmp : ¬(s.Memory (midpoint s)).toNat < (s.Registers key).toNat := by + simpa only [hread, hk] using hlt + have hgt : target.toNat < input[pivot].toNat := by grind [BitVec.toNat_inj] + by_cases hleft : lo < pivot + · let next := (checked s false true).writeRegister upper (BitVec.ofNat w (pivot - 1)) + have hb : Completes (instructions (body w)) s ⟨8, {BitVec.ofNat w pivot}⟩ next := by + simpa only [next, hm, h1, wordAddress_pred pivot (hmem.index_lt hpi) (by lia)] using + body_left s hne hcmp (by simpa only [hln, hpn] using hleft) + obtain ⟨cost, t, hr, hs⟩ := ih lo (pivot - 1) (by lia) (by lia) (by lia) next + (by simpa [next] using hmem) (by simp [next, hl]) (by simp [next]) + (by simp [next, hk]) (by simp [next, h1]) (by simp [next]) + refine ⟨_, t, completes_while_true .ult (body w) ha hb hr, ?_⟩ + constructor + · simpa [next] using hs.memory + · exact Finset.union_subset (Finset.singleton_subset_iff.mpr hprobe) hs.addresses + · intro hf + obtain ⟨hi₁, hi₂, hm⟩ := hs.found hf + exact ⟨hi₁, by lia, hm⟩ + · intro hf hsorted i hil hih + by_cases hip : pivot ≤ i + · exact hsorted.exclude_right hpi hgt i hip (by lia) + · exact hs.not_found hf hsorted i hil (by lia) + · apply step_time_bound hs.time (by lia) + simpa only [pivot, left_length hleft] using + Nat.div_le_div_right (by lia : hi - lo ≤ hi - lo + 1) + · intro hw hz hk1 + simp [hz, hk1, BitVec.toNat_one hw] at hcmp + · have hb := body_stop_left s hne hcmp (by simpa only [hln, hpn] using hleft) + refine ⟨_, _, hb.while_stop ha (by simp), ?_⟩ + constructor + · simp + · simpa only [add_zero, Finset.singleton_subset_iff, hm] using hprobe + · simp + · intro _ hsorted i hil hih + exact hsorted.exclude_right hpi hgt i (by lia) (by lia) + · dsimp; lia + · intro hw hz hk1 + simp [hz, hk1, BitVec.toNat_one hw] at hcmp + +/-- Exact worst-case primitive count, including interval initialization. -/ +def binarySearchTime (n : Nat) : Nat := if n = 0 then 2 else 8 * n.log2 + 11 + +@[simp] private def initialized (s : RAMState w 6) : RAMState w 6 := + (s.writeRegister lower 0).writeRegister one 1 + +private theorem setup_completes (s : RAMState w 6) : + Completes (instructions (setup w)) s ⟨2, ∅⟩ (initialized s) := + ⟨2, by simp [setup, runCode, step]⟩ + +private structure ResultSpec (input : Search.Input (Word w)) + (s t : RAMState w 6) (cost : RAMCost w 6) : Prop where + correct : SortedWords input.data → Search.search.spec input (searchOutput middle t) + memory : t.Memory = s.Memory + addresses : cost.addresses ⊆ inputRegion input.data + time : cost.time ≤ binarySearchTime input.data.size + worst : 0 < w → s.Memory = (fun _ => 0) → s.Registers key = 1 → + cost.time = binarySearchTime input.data.size + +private theorem search_spec (input : Search.Input (Word w)) (s : RAMState w 6) + (hinput : RepresentsBoundedSearchInput input key upper s) : + ∃ cost t, Completes (instructions (binarySearch w)) s cost t ∧ ResultSpec input s t cost := by + let start := s.writeFlag .eq false + let rest : Prog (WordRAM w 6) Unit := do setup w; whileLoop .ult (body w) + have hclear : Completes [.clearFlag .eq] s ⟨1, ∅⟩ start := + ⟨1, by simp [runCode, step, start]⟩ + have hactive := hinput.nonempty_eq + have hlast := hinput.last_eq + have hkey := hinput.key_eq + by_cases hn : input.data.size = 0 + · have hb : Completes (instructions (branch .ult rest (do [WordRAM w 6] nop))) + start ⟨1, ∅⟩ start := + completes_branch (by simp [start, hactive, hn]) + have hc := hclear.append hb + refine ⟨⟨1, ∅⟩ + ⟨1, ∅⟩, start, ?_, ?_⟩ + · simpa only [binarySearch, ifThenElse_flag, rest, instructions_lift_bind, + List.singleton_append] using hc + constructor + · intro _ + simp only [searchOutput, start, RAMState.writeFlag_flags, ↓reduceIte, + Bool.false_eq_true, Search.search_spec_none] + grind [Array.mem_iff_getElem?] + · simp [start] + · simp + · simp [binarySearchTime, hn] + · intro _ _ _; simp [binarySearchTime, hn] + · obtain ⟨cost, t, hr, hs⟩ := loop_spec input.data input.key input.data.size 0 + (input.data.size - 1) (by lia) (by lia) (by lia) (initialized start) + (by simpa [start] using hinput.toRepresentsSearchInput.toRepresentsArray) + (by simp) (by simp [start, hlast]) (by simp [start, hkey]) + (by simp) (by simp [start, hactive, hn]) + have hb : Completes (instructions (branch .ult rest (do [WordRAM w 6] nop))) + start (⟨2, ∅⟩ + cost) t := + completes_branch (by simpa [rest, start, hactive, hn] using (setup_completes start).append hr) + have hc := hclear.append hb + refine ⟨⟨1, ∅⟩ + (⟨2, ∅⟩ + cost), t, ?_, ?_⟩ + · simpa only [binarySearch, ifThenElse_flag, rest, instructions_lift_bind, + List.singleton_append] using hc + constructor + · intro hsorted + simp only [searchOutput] + split_ifs with hf + · obtain ⟨_, hbound, hmatch⟩ := hs.found hf + exact ⟨by lia, hmatch⟩ + · have hnone := hs.not_found (by simpa using hf) hsorted + simp only [Search.search_spec_none] + grind [Array.mem_iff_getElem?] + · simpa [start] using hs.memory + · simpa using hs.addresses + · have ht := hs.time + have hlen : input.data.size - 1 - 0 + 1 = input.data.size := by lia + simp only [RAMCost.mk_add, binarySearchTime, if_neg hn] + rw [hlen] at ht + lia + · intro hw hz hk1 + have ht := hs.worst hw (by simp [start, hz]) (by simp [start, hk1]) + have hlen : input.data.size - 1 - 0 + 1 = input.data.size := by lia + simp only [RAMCost.mk_add, binarySearchTime, if_neg hn] + rw [hlen] at ht + lia + +private theorem arrayMemory_replicate_zero (n : Nat) : + arrayMemory (Array.replicate n (0 : Word w)) = fun _ => 0 := by + funext addr + simp only [arrayMemory, Array.getElem?_replicate] + split <;> rfl + +/-- Joint correctness and resource guarantees for a completed execution of the uniform program. -/ +theorem binarySearch_run_spec (input : Search.Input (Word w)) (s : RAMState w 6) + (hinput : RepresentsBoundedSearchInput input key upper s) + {fuel : Nat} {result : AddWriter (RAMCost w 6) Unit} {final : ExecutionState w 6} + (hrun : execute fuel (binarySearch w) s = some (result, final)) : + let t := final.ram + let cost := result.tell + (SortedWords input.data → Search.search.spec input (searchOutput middle t)) ∧ + t.Memory = s.Memory ∧ cost.addresses ⊆ inputRegion input.data ∧ + cost.time ≤ binarySearchTime input.data.size := by + obtain ⟨cost, t, hc, hs⟩ := search_spec input s hinput + obtain ⟨hcost, hstate⟩ := hc.unique (by simpa only [execute_eq_runCode] using hrun) + simpa only [hcost, hstate] using ⟨hs.correct, hs.memory, hs.addresses, hs.time⟩ + +end Algolean.Algorithms.WordRAM diff --git a/Algolean/Algorithms/WordRAM/BinarySearch/Complexity.lean b/Algolean/Algorithms/WordRAM/BinarySearch/Complexity.lean new file mode 100644 index 0000000..46ae8d9 --- /dev/null +++ b/Algolean/Algorithms/WordRAM/BinarySearch/Complexity.lean @@ -0,0 +1,120 @@ +/- +Copyright (c) 2026 Shreyas Srinivas. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Shreyas Srinivas +-/ + +module + +public import Algolean.Algorithms.WordRAM.BinarySearch.Common +import all Algolean.Algorithms.WordRAM.BinarySearch.Common + +/-! +# Time and space used by binary search + +The execution bounds assume that the initial state satisfies +`RepresentsBoundedSearchInput` and execution finishes. The array need not be sorted. +Let `n` be the input size. Time counts charged operations. +Space counts memory cells, excluding registers. + +- `binarySearch_time_le`: time is at most `binarySearchTime n`, which is + `2` for empty input and `8 * n.log2 + 11` otherwise. +- `binarySearch_addresses_subset`: every accessed cell belongs to the input array. +- `binarySearch_auxiliarySpace`: no memory outside the input array is used. +- `binarySearch_totalSpace`: total space is `n`, including unread input cells. +- `binarySearch_runsWithin`: the program terminates on every valid input state, + and every completed execution meets the time bound and uses no auxiliary memory. +- `binarySearch_worstCase`: for `0 < w` and `n ≤ 2 ^ w`, searching for `1` in + an array of `n` zeros takes exactly `binarySearchTime n`. +- `binarySearch_exists_worstCase`: for `0 < w` and `n ≤ 2 ^ w`, there is a sorted + array of size `n` and an absent key for which execution takes exactly + `binarySearchTime n`. +-/ + +@[expose] public section + +namespace Algolean.Algorithms.WordRAM + +open scoped WordRAM Prog + +open BinarySearch + +attribute [local simp] lower upper middle value key one CmpOp.eval BinOp.eval wordAddress_toNat + +/-- The logarithmic time bound does not require sortedness. -/ +theorem binarySearch_time_le (input : Search.Input (Word w)) (s : RAMState w 6) + (hinput : RepresentsBoundedSearchInput input key upper s) + {fuel : Nat} {result : AddWriter (RAMCost w 6) Unit} {final : ExecutionState w 6} + (hrun : execute fuel (binarySearch w) s = some (result, final)) : + result.tell.time ≤ binarySearchTime input.data.size := + (binarySearch_run_spec input s hinput hrun).right.right.right + +/-- All memory probes belong to the input array. -/ +theorem binarySearch_addresses_subset (input : Search.Input (Word w)) (s : RAMState w 6) + (hinput : RepresentsBoundedSearchInput input key upper s) + {fuel : Nat} {result : AddWriter (RAMCost w 6) Unit} {final : ExecutionState w 6} + (hrun : execute fuel (binarySearch w) s = some (result, final)) : + result.tell.addresses ⊆ inputRegion input.data := + (binarySearch_run_spec input s hinput hrun).right.right.left + +/-- The six registers use no auxiliary memory cells. -/ +theorem binarySearch_auxiliarySpace (input : Search.Input (Word w)) (s : RAMState w 6) + (hinput : RepresentsBoundedSearchInput input key upper s) + {fuel : Nat} {result : AddWriter (RAMCost w 6) Unit} {final : ExecutionState w 6} + (hrun : execute fuel (binarySearch w) s = some (result, final)) : + result.tell.auxiliarySpace (inputRegion input.data) = 0 := by + simp only [RAMCost.auxiliarySpace, Finset.sdiff_eq_empty_iff_subset.mpr + (binarySearch_addresses_subset input s hinput hrun), Finset.card_empty] + +/-- The total footprint equals the input size, including unread input cells. -/ +theorem binarySearch_totalSpace (input : Search.Input (Word w)) (s : RAMState w 6) + (hinput : RepresentsBoundedSearchInput input key upper s) + {fuel : Nat} {result : AddWriter (RAMCost w 6) Unit} {final : ExecutionState w 6} + (hrun : execute fuel (binarySearch w) s = some (result, final)) : + result.tell.totalSpace (inputRegion input.data) = input.data.size := by + simp only [RAMCost.totalSpace, Finset.union_eq_right.mpr + (binarySearch_addresses_subset input s hinput hrun), inputRegion_card input.data hinput.fits] + +/-- Termination, the worst-case time bound, and zero auxiliary memory for every represented +input. Resource guarantees do not require sortedness. -/ +theorem binarySearch_runsWithin (w : Nat) : + let repInput := fun input => RepresentsBoundedSearchInput input key upper + let bound := fun (input : Search.Input (Word w)) (cost : RAMCost w 6) => + cost.time ≤ binarySearchTime input.data.size ∧ + cost.auxiliarySpace (inputRegion input.data) = 0 + Search.RunsWithin (binarySearch w) Executes repInput bound := by + constructor + · intro input s _ hi + obtain ⟨cost, t, hc, _⟩ := search_spec input s hi + exact ⟨cost, t, hc.executes⟩ + · intro input s _ hi cost t hr + obtain ⟨fuel, remaining, hr⟩ := hr + exact ⟨binarySearch_time_le input s hi hr, binarySearch_auxiliarySpace input s hi hr⟩ + +/-- Zeros searched for one attain the time bound at every fitting length and positive width. -/ +theorem binarySearch_worstCase (w n : Nat) (hw : 0 < w) (hn : n ≤ 2 ^ w) : + let input := Array.replicate n (0 : Word w) + let s := binarySearchState input 1 + ∃ fuel cost t, execute fuel (binarySearch w) s = some (⟨(), cost⟩, ⟨t, 0⟩) ∧ + cost.time = binarySearchTime n := by + let input := Array.replicate n (0 : Word w) + have hrep := binarySearchState_represents input 1 (by simpa [input] using hn) + obtain ⟨cost, t, hc, hs⟩ := search_spec ⟨input, 1⟩ _ hrep + obtain ⟨fuel, hf⟩ := hc.execute + refine ⟨fuel, cost, t, hf, ?_⟩ + simpa [input] using hs.worst hw (arrayMemory_replicate_zero n) + (by simp [binarySearchState]) + +/-- Every fitting length has a sorted worst-case input for this same uniform program. -/ +theorem binarySearch_exists_worstCase (w n : Nat) (hw : 0 < w) (hn : n ≤ 2 ^ w) : + ∃ (input : Array (Word w)) (target : Word w), + input.size = n ∧ input.size ≤ 2 ^ w ∧ SortedWords input ∧ target ∉ input ∧ + ∃ fuel cost t, + execute fuel (binarySearch w) (binarySearchState input target) = + some (⟨(), cost⟩, ⟨t, 0⟩) ∧ cost.time = binarySearchTime n := by + refine ⟨Array.replicate n 0, 1, by simp, by simpa using hn, ?_, ?_, ?_⟩ + · simp [SortedWords, Search.SortedBy] + · simp [ne_of_gt hw] + · exact binarySearch_worstCase w n hw hn + +end Algolean.Algorithms.WordRAM diff --git a/Algolean/Algorithms/WordRAM/BinarySearch/Correctness.lean b/Algolean/Algorithms/WordRAM/BinarySearch/Correctness.lean new file mode 100644 index 0000000..e0397c1 --- /dev/null +++ b/Algolean/Algorithms/WordRAM/BinarySearch/Correctness.lean @@ -0,0 +1,103 @@ +/- +Copyright (c) 2026 Shreyas Srinivas. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Shreyas Srinivas +-/ + +module + +public import Algolean.Algorithms.WordRAM.BinarySearch.Common +import all Algolean.Algorithms.WordRAM.BinarySearch.Common + +/-! +# Correctness of binary search + +These theorems assume that the initial machine state stores the input array, key, +and array bounds as specified by `RepresentsBoundedSearchInput`. + +- `binarySearch_terminates`: there is enough fuel for the search to finish, + even if the array is not sorted. +- `binarySearch_correct_of_execute`: if the array is sorted and execution finishes, + the decoded output identifies a match, or is `none` if the key is absent. +- `binarySearch_none_iff`: on sorted input, after execution finishes, the equality + flag is false exactly when the key is absent. +- `binarySearch_of_some`: on sorted input, if execution finishes with the equality + flag true, the middle register holds a valid array index containing the key. +- `binarySearch_memory`: execution preserves every memory cell, even if the + array is not sorted. +- `binarySearch_correct`: `binarySearch w` satisfies `Problem.Solves` for + `Search.binarySearch`: it terminates on every valid sorted input state, and + every completed execution gives a correct answer. +-/ + +@[expose] public section + +namespace Algolean.Algorithms.WordRAM + +open scoped WordRAM Prog + +open BinarySearch + +attribute [local simp] lower upper middle value key one CmpOp.eval BinOp.eval wordAddress_toNat + +/-- Binary search terminates on every representing state, even without sortedness. -/ +theorem binarySearch_terminates (input : Search.Input (Word w)) (s : RAMState w 6) + (hinput : RepresentsBoundedSearchInput input key upper s) : + ∃ fuel cost t, execute fuel (binarySearch w) s = some (⟨(), cost⟩, ⟨t, 0⟩) := by + obtain ⟨cost, t, hc, _⟩ := search_spec input s hinput + obtain ⟨fuel, hf⟩ := hc.execute + exact ⟨fuel, cost, t, hf⟩ + +/-- On sorted input, binary search implements the abstract search problem. -/ +theorem binarySearch_correct_of_execute (input : Search.Input (Word w)) (s : RAMState w 6) + (hinput : RepresentsBoundedSearchInput input key upper s) + {fuel : Nat} {result : AddWriter (RAMCost w 6) Unit} {final : ExecutionState w 6} + (hrun : execute fuel (binarySearch w) s = some (result, final)) : + let problem := Search.binarySearch (fun a b : Word w => a.toNat ≤ b.toNat) + problem.admissible input → problem.spec input (searchOutput middle final.ram) := by + simpa using (binarySearch_run_spec input s hinput hrun).left + +/-- A cleared equality flag characterizes absence on sorted input. -/ +theorem binarySearch_none_iff (input : Search.Input (Word w)) (s : RAMState w 6) + (hinput : RepresentsBoundedSearchInput input key upper s) (hsorted : SortedWords input.data) + {fuel : Nat} {result : AddWriter (RAMCost w 6) Unit} {final : ExecutionState w 6} + (hrun : execute fuel (binarySearch w) s = some (result, final)) : + final.ram.Flags .eq = false ↔ input.key ∉ input.data := by + simpa [searchOutput] using Search.search_none_iff + (binarySearch_correct_of_execute input s hinput hrun (by simpa using hsorted)) + +/-- The middle register holds an in-bounds matching address when equality is set. -/ +theorem binarySearch_of_some (input : Search.Input (Word w)) (s : RAMState w 6) + (hinput : RepresentsBoundedSearchInput input key upper s) (hsorted : SortedWords input.data) + {fuel : Nat} {result : AddWriter (RAMCost w 6) Unit} {final : ExecutionState w 6} + (hrun : execute fuel (binarySearch w) s = some (result, final)) + (hfound : final.ram.Flags .eq = true) : + let i := (final.ram.Registers middle).toNat + i < input.data.size ∧ input.data[i]? = some input.key := by + simpa only [Search.binarySearch_spec, searchOutput_of_found middle _ hfound, + Search.search_spec_some, Search.IsMatch] using + binarySearch_correct_of_execute input s hinput hrun (by simpa using hsorted) + +/-- Binary search preserves every memory cell. -/ +theorem binarySearch_memory (input : Search.Input (Word w)) (s : RAMState w 6) + (hinput : RepresentsBoundedSearchInput input key upper s) + {fuel : Nat} {result : AddWriter (RAMCost w 6) Unit} {final : ExecutionState w 6} + (hrun : execute fuel (binarySearch w) s = some (result, final)) : + final.ram.Memory = s.Memory := (binarySearch_run_spec input s hinput hrun).right.left + +/-- Total correctness of this fixed, runtime-size-independent program on every representing +state. The output remains in the machine's registers and flags. -/ +theorem binarySearch_correct (w : Nat) : + let problem := (Search.binarySearch (fun a b : Word w => a.toNat ≤ b.toNat)) + let repInput := fun input => RepresentsBoundedSearchInput input key upper + problem.Solves (binarySearch w) Executes repInput (RepresentsSearchOutput middle) := by + constructor + · intro input s _ hi + obtain ⟨cost, t, hc, _⟩ := search_spec input s hi + exact ⟨cost, t, hc.executes⟩ + · intro input s ha hi cost t hr + obtain ⟨fuel, remaining, hr⟩ := hr + exact ⟨searchOutput middle t, representsSearchOutput_searchOutput middle t, + binarySearch_correct_of_execute input s hi hr ha⟩ + +end Algolean.Algorithms.WordRAM diff --git a/Algolean/Algorithms/WordRAM/LinearSearch/Algorithm.lean b/Algolean/Algorithms/WordRAM/LinearSearch/Algorithm.lean new file mode 100644 index 0000000..dbacb0e --- /dev/null +++ b/Algolean/Algorithms/WordRAM/LinearSearch/Algorithm.lean @@ -0,0 +1,102 @@ +/- +Copyright (c) 2026 Shreyas Srinivas. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Shreyas Srinivas +-/ + +module + +public import Algolean.Algorithms.WordRAM.Basic +public import Algolean.Models.WordRAMSyntax + +/-! +# Linear search in the word-RAM model + +The program uses five registers and no extra memory. Memory cell `0` stores the array size +`n`, and cells `1` through `n` store its elements. The initial state supplies the search key +in its register. The program initializes the other registers and flags, starts searching +at address `1`, and converts a found address to a zero-based array index. +The same program handles every input size that fits in memory at word width `w`. +-/ + +@[expose] public section + +namespace Algolean.Algorithms.WordRAM + +open scoped WordRAM Prog + +namespace LinearSearch + +/-- Current address, and the result register on success. -/ +abbrev index : Register 5 := 0 +/-- Search key supplied by the initial machine state. -/ +abbrev key : Register 5 := 1 +/-- Scratch register for the loaded input word. -/ +abbrev value : Register 5 := 2 +/-- Register holding the constant one. -/ +abbrev one : Register 5 := 3 +/-- Inclusive last input address, loaded from the size header. -/ +abbrev last : Register 5 := 4 + +/-- Inspect one cell, stopping at the first match or the inclusive last address. -/ +def body (w : Nat) : Prog (WordRAM w 5) Unit := do [WordRAM w 5] + value ←ᵣ mem[index] + ifₚ value =ᵣ key then + reset .ult + else + ifₚ index <ᵣ last then + index ←ᵣ index + one + else + nop + +namespace ForReview + +/-- The same search step as `body`, using ordinary `do` notation and explicit operations. -/ +def bodyExplicit (w : Nat) : Prog (WordRAM w 5) Unit := do + (.load value index : WordRAM w 5 Unit) + (.cmp .eq value key : WordRAM w 5 Unit) + branch .eq + (do + (.clearFlag .ult : WordRAM w 5 Unit) + pure ()) + (do + (.cmp .ult index last : WordRAM w 5 Unit) + branch .ult + (do + (.binop .add index index one : WordRAM w 5 Unit) + pure ()) + (do + (.nop : WordRAM w 5 Unit) + pure ())) + +/-- The explicit version is definitionally equal to the version written with notation. -/ +theorem bodyExplicit_eq_body (w : Nat) : bodyExplicit w = body w := rfl + +end ForReview + +/-- Read the size header and initialize the search at address one. -/ +def setup (w : Nat) : Prog (WordRAM w 5) Unit := do [WordRAM w 5] + reset .eq + index ←ᵣ imm[0] + last ←ᵣ mem[index] + cmp (w := w) .ult index last + one ←ᵣ imm[1] + index ←ᵣ imm[1] + +/-- Convert a found memory address to a zero-based array index. -/ +def finish (w : Nat) : Prog (WordRAM w 5) Unit := do [WordRAM w 5] + ifₚ flag .eq then + index ←ᵣ index - one + else + nop + +end LinearSearch + +/-- One fixed program for all representable input lengths at word width `w`. -/ +def linearSearch (w : Nat) : Prog (WordRAM w 5) Unit := do [WordRAM w 5] + LinearSearch.setup w + whileₚ .ult do + LinearSearch.body w + LinearSearch.finish w + +end Algolean.Algorithms.WordRAM diff --git a/Algolean/Algorithms/WordRAM/LinearSearch/Common.lean b/Algolean/Algorithms/WordRAM/LinearSearch/Common.lean new file mode 100644 index 0000000..5deba44 --- /dev/null +++ b/Algolean/Algorithms/WordRAM/LinearSearch/Common.lean @@ -0,0 +1,260 @@ +/- +Copyright (c) 2026 Shreyas Srinivas. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Shreyas Srinivas +-/ + +module + +public import Algolean.Algorithms.WordRAM.LinearSearch.Algorithm + +/-! +# Shared proofs for linear search + +Lemmas about each loop iteration and the complete search, used by the correctness +and complexity proofs. +-/ + +@[expose] public section + +namespace Algolean.Algorithms.WordRAM + +open scoped WordRAM Prog + +open LinearSearch + +attribute [local simp] index key value one last CmpOp.eval BinOp.eval wordAddress_toNat + +private def checked (s : RAMState w 5) (found active : Bool) : RAMState w 5 := + ((s.writeRegister value (s.Memory (s.Registers index))).writeFlag .eq found).writeFlag + .ult active + +@[simp, grind =] private theorem checked_memory (s : RAMState w 5) (found active : Bool) : + (checked s found active).Memory = s.Memory := rfl + +@[simp, grind =] private theorem checked_registers (s : RAMState w 5) (found active : Bool) + (r : Register 5) : (checked s found active).Registers r = + if r = value then s.Memory (s.Registers index) else s.Registers r := by + simp [checked] + +@[simp, grind =] private theorem checked_flags (s : RAMState w 5) (found active : Bool) + (op : CmpOp) : (checked s found active).Flags op = + if op = .ult then active else found := by + cases op <;> simp [checked] + +private theorem body_found (s : RAMState w 5) + (h : s.Memory (s.Registers index) = s.Registers key) : + Completes (instructions (body w)) s ⟨3, {s.Registers index}⟩ (checked s true false) := + ⟨4, by simp [body, checked, branch, runCode, step, h]⟩ + +private theorem body_advance (s : RAMState w 5) + (h : s.Memory (s.Registers index) ≠ s.Registers key) + (hlt : (s.Registers index).toNat < (s.Registers last).toNat) : + Completes (instructions (body w)) s ⟨4, {s.Registers index}⟩ + ((checked s false true).writeRegister index (s.Registers index + s.Registers one)) := + ⟨6, by simp [body, checked, branch, runCode, step, h, hlt]⟩ + +private theorem body_last (s : RAMState w 5) + (h : s.Memory (s.Registers index) ≠ s.Registers key) + (hlt : ¬(s.Registers index).toNat < (s.Registers last).toNat) : + Completes (instructions (body w)) s ⟨4, {s.Registers index}⟩ (checked s false false) := + ⟨6, by simp [body, checked, branch, runCode, step, h, hlt]⟩ + +/-- The invariant describes the remaining suffix and the exact cost from its first address. -/ +private def Summary (input : Array (Word w)) (target : Word w) (start n : Nat) + (s t : RAMState w 5) (cost : RAMCost w 5) : Prop := + t.Memory = s.Memory ∧ cost.addresses ⊆ inputRegion input ∧ + if t.Flags .eq then + let i := (t.Registers index).toNat + start ≤ i ∧ i < start + n ∧ input[i]? = some target ∧ + (∀ j, start ≤ j → j < i → input[j]? ≠ some target) ∧ + cost.time = 4 * (i - start) + 3 + else + (∀ j, start ≤ j → j < start + n → input[j]? ≠ some target) ∧ + cost.time = 4 * n + +private theorem loop_spec (input : Array (Word w)) (target : Word w) (n start : Nat) + (hn : 0 < n) (hsize : start + n = input.size) (s : RAMState w 5) + (hmem : RepresentsArray input s.Memory) + (hi : s.Registers index = BitVec.ofNat w start) + (hk : s.Registers key = target) (h1 : s.Registers one = 1) + (hl : s.Registers last = BitVec.ofNat w (input.size - 1)) (ha : s.Flags .ult = true) : + ∃ cost t, Completes (instructions (whileLoop .ult (body w))) s cost t ∧ + Summary input target start n s t cost ∧ t.Registers one = 1 := by + induction n generalizing start s with + | zero => lia + | succ n ih => + have hstart : start < input.size := by lia + have hread := hmem.read_of_eq hstart hi + have hprobe := ofNat_mem_inputRegion input start hstart + by_cases heq : input[start] = target + · have hb := body_found s (by simpa [hread, hk] using heq) + refine ⟨_, _, hb.while_stop ha (by simp), ?_, by simp [h1]⟩ + suffices ∀ j, start ≤ j → j < start → input[j]? ≠ some target by + simpa [Summary, hi, Nat.mod_eq_of_lt (hmem.index_lt hstart), hprobe, heq, hstart] using this + intro j hj hj' + lia + · have hmiss : input[start]? ≠ some target := by simpa [hstart] using heq + by_cases hn0 : n = 0 + · subst n + have hb := body_last s (by simpa [hread, hk] using heq) + (by grind only [RepresentsArray.fits, wordAddress_toNat]) + refine ⟨_, _, hb.while_stop ha (by simp), ?_, by simp [h1]⟩ + simp only [Summary, checked_memory, Finset.singleton_subset_iff, hi, hprobe, + true_and, checked_flags] + exact ⟨by grind only, trivial⟩ + · let next := (checked s false true).writeRegister index (BitVec.ofNat w (start + 1)) + have hb : Completes (instructions (body w)) s ⟨4, {BitVec.ofNat w start}⟩ next := by + simpa only [next, hi, h1, wordAddress_succ] using body_advance s + (by simpa [hread, hk] using heq) + (by grind only [RepresentsArray.fits, wordAddress_toNat]) + obtain ⟨cost, t, hr, hs, htone⟩ := ih (start + 1) (by lia) (by lia) next + (by simpa [next] using hmem) (by simp [next]) (by simp [next, hk]) + (by simp [next, h1]) (by simp [next, hl]) (by simp [next]) + refine ⟨_, t, completes_while_true .ult (body w) ha hb hr, ?_, htone⟩ + simp only [Summary, next, RAMState.writeRegister_memory, checked_memory, + RAMCost.mk_add] at hs ⊢ + obtain ⟨hm, hp, hs⟩ := hs + refine ⟨hm, Finset.union_subset (Finset.singleton_subset_iff.mpr hprobe) hp, ?_⟩ + split_ifs at hs ⊢ <;> grind only + +/-- Maximum time, attained by a missing key when the word width is positive. -/ +def linearSearchTime (n : Nat) : Nat := 4 * n + 7 + +/-- Exact time, including setup and conversion to a zero-based result. -/ +def linearSearchCost (n : Nat) : Option Nat → Nat + | none => linearSearchTime n + | some i => 4 * i + 10 + +private def initialized (n : Nat) (s : RAMState w 5) : RAMState w 5 := + ⟨s.Memory, fun r => if r = index then 1 else if r = one then 1 + else if r = last then BitVec.ofNat w n else s.Registers r, + fun op => if op = .ult then decide (n ≠ 0) else false⟩ + +attribute [local simp] initialized + +private theorem setup_completes (input : Search.Input (Word w)) (s : RAMState w 5) + (hi : RepresentsSizedSearchInput input key s) : + Completes (instructions (setup w)) s ⟨6, {0}⟩ (initialized input.data.size s) := by + have hh := hi.header + have hn := hi.size_lt + refine ⟨6, ?_⟩ + simp only [setup, index, Fin.isValue, BitVec.ofNat_eq_ofNat, last, one, instructions_bind, + instructions_lift, + List.cons_append, List.nil_append, runCode, step, RAMState.writeFlag, + RAMState.writeRegister, Function.update, + ↓reduceDIte, hh, CmpOp.eval, Fin.reduceEq, BitVec.toNat_ofNat, Nat.zero_mod, + Nat.mod_eq_of_lt hn, + Nat.pos_iff_ne_zero, ne_eq, Array.size_eq_zero_iff, decide_not, runCode_nil, + RAMCost.mk_add, Finset.empty_union, + Option.pure_def, Option.bind_eq_bind, Option.bind_some, RAMCost.zero_time, add_zero, + RAMCost.zero_addresses, + Nat.reduceAdd, Finset.singleton_union, insert_empty_eq, initialized, Bool.if_false_right, + Option.some.injEq, + Prod.mk.injEq, ExecutionState.mk.injEq, RAMState.mk.injEq, true_and, and_true] + constructor + · funext r + simp only [Function.update_apply] + split_ifs <;> simp_all only [Fin.reduceEq] + · funext op + cases op <;> simp + +private def finished (s : RAMState w 5) : RAMState w 5 := + if s.Flags .eq then s.writeRegister index (s.Registers index - 1) else s + +private theorem finish_completes (s : RAMState w 5) (h1 : s.Registers one = 1) : + Completes (instructions (finish w)) s ⟨1, ∅⟩ (finished s) := by + refine ⟨2, ?_⟩ + cases hf : s.Flags .eq <;> simp [finish, finished, branch, runCode, step, hf, h1] + +@[simp] private theorem finished_memory (s : RAMState w 5) : (finished s).Memory = s.Memory := by + simp [finished]; split <;> rfl + +@[simp] private theorem finished_flags (s : RAMState w 5) (op : CmpOp) : + (finished s).Flags op = s.Flags op := by + simp [finished]; split <;> rfl + +private theorem finished_output (s : RAMState w 5) (hf : s.Flags .eq = true) + (hp : 0 < (s.Registers index).toNat) : + searchOutput index (finished s) = some ((s.Registers index).toNat - 1) := by + simp only [finished, hf, ↓reduceIte, searchOutput, RAMState.writeRegister_flags, + RAMState.writeRegister_registers] + rw [word_pred_toNat _ hp] + +private theorem search_spec (input : Search.Input (Word w)) (s : RAMState w 5) + (hinput : RepresentsSizedSearchInput input key s) : + ∃ cost t, Completes (instructions (linearSearch w)) s cost t ∧ + Search.linearSearch.spec input (searchOutput index t) ∧ t.Memory = s.Memory ∧ + cost.addresses ⊆ sizedInputRegion input.data ∧ + cost.time = linearSearchCost input.data.size (searchOutput index t) := by + have hkey := hinput.key_eq + by_cases hn : input.data.size = 0 + · have hr := completes_while_false .ult (body w) (initialized input.data.size s) (by simp [hn]) + have hc := (setup_completes input s hinput).append + (hr.append (finish_completes _ (by simp))) + refine ⟨⟨6, {0}⟩ + (0 + ⟨1, ∅⟩), finished (initialized input.data.size s), + ?_, ?_, ?_, ?_, ?_⟩ + · simpa only [linearSearch, instructions_bind] using hc + · simp [finished, searchOutput, Search.linearSearch_spec_none, + Array.eq_empty_of_size_eq_zero hn] + · simp + · simp [RAMCost.mk_add] + · simp [finished, searchOutput, linearSearchCost, linearSearchTime, hn, RAMCost.mk_add] + · obtain ⟨cost, t, hr, hs, htone⟩ := loop_spec (withSize input.data) input.key input.data.size 1 + (by lia) (by simp [Nat.add_comm]) (initialized input.data.size s) + (by simpa using hinput.toRepresentsArray) + (by simp) (by simp [hkey]) (by simp) (by simp) (by simp [hn]) + have hc := (setup_completes input s hinput).append (hr.append (finish_completes t htone)) + refine ⟨⟨6, {0}⟩ + (cost + ⟨1, ∅⟩), finished t, ?_, ?_, ?_, ?_, ?_⟩ + · simpa only [linearSearch, instructions_bind] using hc + all_goals simp only [Summary, initialized] at hs + · obtain ⟨_, _, hs⟩ := hs + cases hf : t.Flags .eq with + | false => + simp only [hf, Bool.false_eq_true, ↓reduceIte] at hs + simp only [searchOutput, finished_flags, hf, Bool.false_eq_true, ↓reduceIte, + Search.linearSearch_spec_none] + rw [Array.mem_iff_getElem?] + rintro ⟨i, hi⟩ + have hib : i < input.data.size := by + exact Array.getElem?_eq_some_iff.mp hi |>.choose + exact hs.left (i + 1) (by lia) (by lia) (by simpa using hi) + | true => + simp only [hf, ↓reduceIte] at hs + rw [finished_output t hf (by lia)] + refine ⟨by lia, ?_, ?_⟩ + · rw [← withSize_getElem?_succ, Nat.sub_add_cancel (by lia : 1 ≤ (t.Registers index).toNat)] + exact hs.right.right.left + · intro j hj + simpa using hs.right.right.right.left (j + 1) (by lia) (by lia) + · simpa using hs.left + · simpa [RAMCost.add_addresses, sizedInputRegion] using + Finset.insert_subset (zero_mem_sizedInputRegion input.data) hs.right.left + · obtain ⟨_, _, hs⟩ := hs + cases hf : t.Flags .eq with + | false => + simp only [hf, Bool.false_eq_true, ↓reduceIte] at hs + simp [searchOutput, hf, linearSearchCost, linearSearchTime, RAMCost.mk_add, hs.right] + lia + | true => + simp only [hf, ↓reduceIte] at hs + rw [finished_output t hf (by lia)] + simp only [linearSearchCost, RAMCost.add_time] + lia + +/-- A successful fuelled execution satisfies the specification, exact time formula, and +memory footprint on every representing state. -/ +theorem linearSearch_run_spec (input : Search.Input (Word w)) (s : RAMState w 5) + (hinput : RepresentsSizedSearchInput input key s) + {fuel : Nat} {result : AddWriter (RAMCost w 5) Unit} {final : ExecutionState w 5} + (hrun : execute fuel (linearSearch w) s = some (result, final)) : + let t := final.ram + let cost := result.tell + Search.linearSearch.spec input (searchOutput index t) ∧ t.Memory = s.Memory ∧ + cost.addresses ⊆ sizedInputRegion input.data ∧ + cost.time = linearSearchCost input.data.size (searchOutput index t) := by + obtain ⟨cost, t, hc, hs⟩ := search_spec input s hinput + obtain ⟨hcost, hstate⟩ := hc.unique (by simpa only [execute_eq_runCode] using hrun) + simpa only [hcost, hstate] using hs + +end Algolean.Algorithms.WordRAM diff --git a/Algolean/Algorithms/WordRAM/LinearSearch/Complexity.lean b/Algolean/Algorithms/WordRAM/LinearSearch/Complexity.lean new file mode 100644 index 0000000..13ea881 --- /dev/null +++ b/Algolean/Algorithms/WordRAM/LinearSearch/Complexity.lean @@ -0,0 +1,143 @@ +/- +Copyright (c) 2026 Shreyas Srinivas. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Shreyas Srinivas +-/ + +module + +public import Algolean.Algorithms.WordRAM.LinearSearch.Common +import all Algolean.Algorithms.WordRAM.LinearSearch.Common +public import Algolean.Algorithms.WordRAM.LinearSearch.Correctness + +/-! +# Time and space used by linear search + +The execution bounds assume that the initial state satisfies +`RepresentsSizedSearchInput` and execution finishes. Let `n` be the input size. +Time counts charged operations. Space counts memory cells, excluding registers. + +- `linearSearch_time`: the exact time is `linearSearchCost n` applied to the + decoded output. +- `linearSearch_time_le`: time is at most `linearSearchTime n`, which is + `4 * n + 7`, including `7` for empty input. +- `linearSearch_time_of_not_mem`: an absent key takes exactly `linearSearchTime n`. +- `linearSearch_time_of_some`: finding the first match at index `i` takes + exactly `4 * i + 10` operations. +- `linearSearch_addresses_subset`: every accessed cell belongs to the size header or array. +- `linearSearch_auxiliarySpace`: no memory outside the size header and array is used. +- `linearSearch_totalSpace`: total space is `n + 1`, including the header and unread input cells. +- `linearSearch_runsWithin`: the program terminates on every valid input state, + and every completed execution meets the time bound and uses no auxiliary memory. +- `linearSearch_worstCase`: for `0 < w` and `n < 2 ^ w`, searching for `1` in + an array of `n` zeros takes exactly `linearSearchTime n`. +-/ + +@[expose] public section + +namespace Algolean.Algorithms.WordRAM + +open scoped WordRAM Prog + +open LinearSearch + +attribute [local simp] index key value one last CmpOp.eval BinOp.eval wordAddress_toNat + +/-- The exact time depends on the first match, or on the length when the key is absent. -/ +theorem linearSearch_time (input : Search.Input (Word w)) (s : RAMState w 5) + (hinput : RepresentsSizedSearchInput input key s) + {fuel : Nat} {result : AddWriter (RAMCost w 5) Unit} {final : ExecutionState w 5} + (hrun : execute fuel (linearSearch w) s = some (result, final)) : + result.tell.time = linearSearchCost input.data.size (searchOutput index final.ram) := + (linearSearch_run_spec input s hinput hrun).right.right.right + +/-- At most four primitive operations per unsuccessful cell, plus setup and exit costs. -/ +theorem linearSearch_time_le (input : Search.Input (Word w)) (s : RAMState w 5) + (hinput : RepresentsSizedSearchInput input key s) + {fuel : Nat} {result : AddWriter (RAMCost w 5) Unit} {final : ExecutionState w 5} + (hrun : execute fuel (linearSearch w) s = some (result, final)) : + result.tell.time ≤ linearSearchTime input.data.size := by + have hs := linearSearch_correct_of_execute input s hinput hrun + rw [linearSearch_time input s hinput hrun] + cases ho : searchOutput index final.ram with + | none => exact Nat.le_refl _ + | some i => + simp only [ho, Search.linearSearch_spec_some, Search.IsFirstMatch] at hs + simp only [linearSearchCost, linearSearchTime] + lia + +/-- An absent key attains the length-dependent upper bound. -/ +theorem linearSearch_time_of_not_mem (input : Search.Input (Word w)) (s : RAMState w 5) + (hinput : RepresentsSizedSearchInput input key s) (hnot : input.key ∉ input.data) + {fuel : Nat} {result : AddWriter (RAMCost w 5) Unit} {final : ExecutionState w 5} + (hrun : execute fuel (linearSearch w) s = some (result, final)) : + result.tell.time = linearSearchTime input.data.size := by + have hf := (linearSearch_none_iff input s hinput hrun).mpr hnot + simpa [hf, linearSearchCost] using linearSearch_time input s hinput hrun + +/-- A first match at index `i` costs exactly `4 * i + 10`. -/ +theorem linearSearch_time_of_some (input : Search.Input (Word w)) (s : RAMState w 5) + (hinput : RepresentsSizedSearchInput input key s) + {fuel : Nat} {result : AddWriter (RAMCost w 5) Unit} {final : ExecutionState w 5} + (hrun : execute fuel (linearSearch w) s = some (result, final)) + (hfound : final.ram.Flags .eq = true) : + result.tell.time = 4 * (final.ram.Registers index).toNat + 10 := by + simpa [hfound, linearSearchCost] using linearSearch_time input s hinput hrun + +/-- Every probed address belongs to the size header or array. -/ +theorem linearSearch_addresses_subset (input : Search.Input (Word w)) (s : RAMState w 5) + (hinput : RepresentsSizedSearchInput input key s) + {fuel : Nat} {result : AddWriter (RAMCost w 5) Unit} {final : ExecutionState w 5} + (hrun : execute fuel (linearSearch w) s = some (result, final)) : + result.tell.addresses ⊆ sizedInputRegion input.data := + (linearSearch_run_spec input s hinput hrun).right.right.left + +/-- Only input memory is probed; registers do not count as auxiliary memory. -/ +theorem linearSearch_auxiliarySpace (input : Search.Input (Word w)) (s : RAMState w 5) + (hinput : RepresentsSizedSearchInput input key s) + {fuel : Nat} {result : AddWriter (RAMCost w 5) Unit} {final : ExecutionState w 5} + (hrun : execute fuel (linearSearch w) s = some (result, final)) : + result.tell.auxiliarySpace (sizedInputRegion input.data) = 0 := by + simp only [RAMCost.auxiliarySpace, Finset.sdiff_eq_empty_iff_subset.mpr + (linearSearch_addresses_subset input s hinput hrun), Finset.card_empty] + +/-- Total memory includes the size header and all array cells, even those not read. -/ +theorem linearSearch_totalSpace (input : Search.Input (Word w)) (s : RAMState w 5) + (hinput : RepresentsSizedSearchInput input key s) + {fuel : Nat} {result : AddWriter (RAMCost w 5) Unit} {final : ExecutionState w 5} + (hrun : execute fuel (linearSearch w) s = some (result, final)) : + result.tell.totalSpace (sizedInputRegion input.data) = input.data.size + 1 := by + simp only [RAMCost.totalSpace, Finset.union_eq_right.mpr + (linearSearch_addresses_subset input s hinput hrun), + sizedInputRegion_card input.data hinput.size_lt] + +/-- Termination, the worst-case time bound, and zero auxiliary memory for every represented +input. Resource guarantees do not require sortedness. -/ +theorem linearSearch_runsWithin (w : Nat) : + let repInput := fun input => RepresentsSizedSearchInput input key + let bound := fun (input : Search.Input (Word w)) (cost : RAMCost w 5) => + cost.time ≤ linearSearchTime input.data.size ∧ + cost.auxiliarySpace (sizedInputRegion input.data) = 0 + Search.RunsWithin (linearSearch w) Executes repInput bound := by + constructor + · intro input s _ hi + obtain ⟨cost, t, hc, _⟩ := search_spec input s hi + exact ⟨cost, t, hc.executes⟩ + · intro input s _ hi cost t hr + obtain ⟨fuel, remaining, hr⟩ := hr + exact ⟨linearSearch_time_le input s hi hr, linearSearch_auxiliarySpace input s hi hr⟩ + +/-- Every fitting length has a worst-case instance at positive word width. -/ +theorem linearSearch_worstCase (w n : Nat) (hw : 0 < w) (hn : n < 2 ^ w) : + let input := Array.replicate n (0 : Word w) + let s := linearSearchState input 1 key + ∃ fuel cost t, execute fuel (linearSearch w) s = some (⟨(), cost⟩, ⟨t, 0⟩) ∧ + cost.time = linearSearchTime n := by + let input := Array.replicate n (0 : Word w) + have hrep := linearSearchState_represents input 1 key (by simpa [input] using hn) + obtain ⟨fuel, cost, t, hr⟩ := linearSearch_terminates ⟨input, 1⟩ _ hrep + refine ⟨fuel, cost, t, hr, ?_⟩ + simpa [input] using linearSearch_time_of_not_mem ⟨input, 1⟩ _ hrep + (by simp [input, ne_of_gt hw]) hr + +end Algolean.Algorithms.WordRAM diff --git a/Algolean/Algorithms/WordRAM/LinearSearch/Correctness.lean b/Algolean/Algorithms/WordRAM/LinearSearch/Correctness.lean new file mode 100644 index 0000000..6bbbda0 --- /dev/null +++ b/Algolean/Algorithms/WordRAM/LinearSearch/Correctness.lean @@ -0,0 +1,99 @@ +/- +Copyright (c) 2026 Shreyas Srinivas. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Shreyas Srinivas +-/ + +module + +public import Algolean.Algorithms.WordRAM.LinearSearch.Common +import all Algolean.Algorithms.WordRAM.LinearSearch.Common + +/-! +# Correctness of linear search + +These theorems assume that memory stores the size followed by the array, and the key +register holds the search key, as specified by `RepresentsSizedSearchInput`. +The program initializes its own bounds and flags. + +- `linearSearch_terminates`: there is enough fuel for the search to finish. +- `linearSearch_correct_of_execute`: if execution finishes, the decoded output + identifies the first match, or is `none` if the key is absent. +- `linearSearch_none_iff`: after execution finishes, the equality flag is false + exactly when the key is absent. +- `linearSearch_some_iff`: after execution finishes, the equality flag is true + exactly when the index register holds the position of the first match. +- `linearSearch_memory`: execution preserves every memory cell. +- `linearSearch_correct`: `linearSearch w` satisfies `Problem.Solves` for + `Search.linearSearch`: it terminates on every valid input state, and every + completed execution gives a correct answer. +-/ + +@[expose] public section + +namespace Algolean.Algorithms.WordRAM + +open scoped WordRAM Prog + +open LinearSearch + +attribute [local simp] index key value one last CmpOp.eval BinOp.eval wordAddress_toNat + +/-- Every representing input state has sufficient interpreter fuel for termination. -/ +theorem linearSearch_terminates (input : Search.Input (Word w)) (s : RAMState w 5) + (hinput : RepresentsSizedSearchInput input key s) : + ∃ fuel cost t, execute fuel (linearSearch w) s = some (⟨(), cost⟩, ⟨t, 0⟩) := by + obtain ⟨cost, t, hc, _⟩ := search_spec input s hinput + obtain ⟨fuel, hf⟩ := hc.execute + exact ⟨fuel, cost, t, hf⟩ + +/-- Uniform linear search returns the first match, or certifies absence. -/ +theorem linearSearch_correct_of_execute (input : Search.Input (Word w)) (s : RAMState w 5) + (hinput : RepresentsSizedSearchInput input key s) + {fuel : Nat} {result : AddWriter (RAMCost w 5) Unit} {final : ExecutionState w 5} + (hrun : execute fuel (linearSearch w) s = some (result, final)) : + Search.linearSearch.spec input (searchOutput index final.ram) := + (linearSearch_run_spec input s hinput hrun).left + +/-- The equality flag is clear exactly when the key is absent. -/ +theorem linearSearch_none_iff (input : Search.Input (Word w)) (s : RAMState w 5) + (hinput : RepresentsSizedSearchInput input key s) + {fuel : Nat} {result : AddWriter (RAMCost w 5) Unit} {final : ExecutionState w 5} + (hrun : execute fuel (linearSearch w) s = some (result, final)) : + final.ram.Flags .eq = false ↔ input.key ∉ input.data := by + have h := linearSearch_correct_of_execute input s hinput hrun + simpa [searchOutput] using Search.search_none_iff (Search.linearSearch_spec_search _ _ h) + +/-- A set equality flag identifies the first matching address. -/ +theorem linearSearch_some_iff (input : Search.Input (Word w)) (s : RAMState w 5) + (hinput : RepresentsSizedSearchInput input key s) + {fuel : Nat} {result : AddWriter (RAMCost w 5) Unit} {final : ExecutionState w 5} + (hrun : execute fuel (linearSearch w) s = some (result, final)) : + final.ram.Flags .eq = true ↔ + Search.IsFirstMatch input.data input.key (final.ram.Registers index).toNat := by + simpa [searchOutput] using Search.linearSearch_some_iff + (linearSearch_correct_of_execute input s hinput hrun) (final.ram.Registers index).toNat + +/-- Loads and register operations preserve the entire input and background memory. -/ +theorem linearSearch_memory (input : Search.Input (Word w)) (s : RAMState w 5) + (hinput : RepresentsSizedSearchInput input key s) + {fuel : Nat} {result : AddWriter (RAMCost w 5) Unit} {final : ExecutionState w 5} + (hrun : execute fuel (linearSearch w) s = some (result, final)) : + final.ram.Memory = s.Memory := (linearSearch_run_spec input s hinput hrun).right.left + +/-- Total correctness of this fixed, runtime-size-independent program on every representing +state. The output remains in the machine's registers and flags. -/ +theorem linearSearch_correct (w : Nat) : + let problem := Search.linearSearch + let repInput := fun input => RepresentsSizedSearchInput input key + problem.Solves (linearSearch w) Executes repInput (RepresentsSearchOutput index) := by + constructor + · intro input s _ hi + obtain ⟨cost, t, hc, _⟩ := search_spec input s hi + exact ⟨cost, t, hc.executes⟩ + · intro input s ha hi cost t hr + obtain ⟨fuel, remaining, hr⟩ := hr + exact ⟨searchOutput index t, representsSearchOutput_searchOutput index t, + linearSearch_correct_of_execute input s hi hr⟩ + +end Algolean.Algorithms.WordRAM diff --git a/Algolean/Algorithms/WordRAMLinearSearch.lean b/Algolean/Algorithms/WordRAMLinearSearch.lean deleted file mode 100644 index 3a05cb9..0000000 --- a/Algolean/Algorithms/WordRAMLinearSearch.lean +++ /dev/null @@ -1,308 +0,0 @@ -/- -Copyright (c) 2026 Shreyas Srinivas. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Shreyas Srinivas --/ - -module - -public import Algolean.Models.WordRAM - -/-! -# Linear search on the word RAM - -`linearSearch` searches an array laid out in consecutive memory cells by `arrayMemory`. -It returns the first matching address and preserves memory. The correctness and complexity section -proves the result specification, exact successful and unsuccessful query counts, a tight linear -worst-case time bound, and zero auxiliary RAM footprint. Total space including the input equals -the input size. --/ - -@[expose] public section - -namespace Algolean.Algorithms.WordRAM - -/-- Lay out an array in consecutive RAM cells starting at address zero, with zero elsewhere. -This specifies the initial memory supplied to the interpreter; it is not part of the search cost. -/ -def arrayMemory (input : Array (BitVec w)) : Memory w := - fun addr => input[addr.toNat]?.getD 0 - -/-- Search the array stored in `arrayMemory input`, returning the first matching address. -The size bound ensures every input element has a distinct word-sized address. The program uses -only the array's length; element access, key comparison, and address arithmetic are queries. - -A match at index `i` costs `3 * i + 2` queries and touches `i + 1` cells. An unsuccessful search -costs `3 * input.size` queries and touches every input cell. The final address increment on a miss -may wrap when the array fills the address space, but no further load is performed. --/ -def linearSearch (input : Array (BitVec w)) (key : BitVec w) - (_fits : input.size ≤ 2 ^ w) : Prog (WordRAM w) (Option (Word w)) := do - let mut addr : Word w := 0 - for _ in List.range input.size do - let value : Word w ← load addr - let found : Bool ← cmp .eq value key - if found then - return some addr - addr ← binop .add addr 1 - return none - -/-! -## Correctness and complexity of linear search - -The proofs apply to every input fitting in the address space, including a full address space. -They preserve the original `for` loop by proving it equal to a recursive loop for induction. -The final results establish first-match correctness, a tight linear time bound, zero auxiliary -RAM footprint, and total space equal to the input length. The word width may grow with input size. --/ - -section CorrectnessAndComplexity - -open Cslib - -/-- Recursive form of the search loop, used only to prove properties of the `for` loop. -/ -private def searchLoop (key : Word w) : Nat → Word w → Prog (WordRAM w) (Option (Word w)) - | 0, _ => pure none - | n + 1, addr => do - let value : Word w ← load addr - let found : Bool ← cmp .eq value key - if found then - return some addr - let next : Word w ← binop .add addr 1 - searchLoop key n next - -/-- The elaborated `for` loop with an arbitrary list of iterations and starting address. -/ -private def searchFor (key : Word w) (steps : List Nat) (addr : Word w) : - Prog (WordRAM w) (Option (Word w)) := do - let mut addr := addr - for _ in steps do - let value : Word w ← load addr - let found : Bool ← cmp .eq value key - if found then - return some addr - addr ← binop .add addr 1 - return none - -private theorem searchFor_eq_searchLoop (key : Word w) (steps : List Nat) (addr : Word w) : - searchFor key steps addr = searchLoop key steps.length addr := by - induction steps generalizing addr with - | nil => simp [searchFor, searchLoop] - | cons x xs ih => - simp only [searchFor, List.forIn_cons, List.length_cons, searchLoop, bind_assoc] - congr 1 - funext value - congr 1 - funext found - cases found <;> simp only [Bool.false_eq_true, ↓reduceIte, BitVec.ofNat_eq_ofNat, - bind_pure_comp, bind_map_left, pure_bind] - congr 1 - funext next - exact ih next - -private theorem linearSearch_eq_searchLoop (input : Array (BitVec w)) (key : BitVec w) - (hfits : input.size ≤ 2 ^ w) : - linearSearch input key hfits = searchLoop key input.size 0 := by - change searchFor key (List.range input.size) 0 = _ - rw [searchFor_eq_searchLoop, List.length_range] - -@[simp, grind =] -private theorem searchLoop_eval_zero (key : Word w) (addr : Word w) (mem : Memory w) : - (searchLoop key 0 addr).evalM timeAndSpaceCost mem = (none (α := Word w), mem) := rfl - -@[grind =] -private theorem searchLoop_eval_succ (key : Word w) (n : Nat) (addr : Word w) - (mem : Memory w) : - (searchLoop key (n + 1) addr).evalM timeAndSpaceCost mem = - if mem addr = key then (some addr, mem) - else (searchLoop key n (addr + 1)).evalM timeAndSpaceCost mem := by - by_cases h : mem addr = key <;> simp [searchLoop, CmpOp.eval, BinOp.eval, h] - -@[simp, grind =] -private theorem searchLoop_cost_zero (key : Word w) (addr : Word w) (mem : Memory w) : - (searchLoop key 0 addr).costM timeAndSpaceCost mem = ((0 : RAMCost w), mem) := rfl - -@[grind =] -private theorem searchLoop_cost_succ (key : Word w) (n : Nat) (addr : Word w) - (mem : Memory w) : - (searchLoop key (n + 1) addr).costM timeAndSpaceCost mem = - if mem addr = key then (⟨2, {addr}⟩, mem) - else - let rest := (searchLoop key n (addr + 1)).costM timeAndSpaceCost mem - (⟨3, {addr}⟩ + rest.1, rest.2) := by - by_cases h : mem addr = key <;> - simp [searchLoop, CmpOp.eval, BinOp.eval, h, ← Nat.add_assoc] - -private theorem searchLoop_memory (key : Word w) (n : Nat) (addr : Word w) (mem : Memory w) : - ((searchLoop key n addr).evalM timeAndSpaceCost mem).2 = mem := by - induction n generalizing addr <;> grind - -private theorem searchLoop_time_le (key : Word w) (n : Nat) (addr : Word w) (mem : Memory w) : - ((searchLoop key n addr).costM timeAndSpaceCost mem).1.time ≤ 3 * n := by - induction n generalizing addr <;> grind - -private theorem searchLoop_time_of_none (key : Word w) (n : Nat) (addr : Word w) - (mem : Memory w) (hnone : ((searchLoop key n addr).evalM timeAndSpaceCost mem).1 = none) : - ((searchLoop key n addr).costM timeAndSpaceCost mem).1.time = 3 * n := by - induction n generalizing addr <;> grind - -/-- An index within the address space survives conversion to a word without wrapping. -/ -@[grind =] -private theorem wordAddress_toNat (i : Nat) (hi : i < 2 ^ w) : - (BitVec.ofNat w i).toNat = i := Nat.mod_eq_of_lt hi - -@[simp, grind =] -private theorem arrayMemory_ofNat (input : Array (BitVec w)) (hfits : input.size ≤ 2 ^ w) - (i : Nat) (hi : i < input.size) : - arrayMemory input (BitVec.ofNat w i) = input[i] := by - simp [arrayMemory, BitVec.toNat_ofNat, Nat.mod_eq_of_lt (lt_of_lt_of_le hi hfits), hi] - -@[simp, grind =] -private theorem wordAddress_succ (i : Nat) : - BitVec.ofNat w i + 1#w = BitVec.ofNat w (i + 1) := by - simp [BitVec.ofNat_add] - -/-- The returned address points to the key, and every earlier element differs from the key. -/ -def IsFirstMatch (input : Array (BitVec w)) (key : BitVec w) (addr : Word w) : Prop := - addr.toNat < input.size ∧ input[addr.toNat]? = some key ∧ - ∀ i, i < addr.toNat → input[i]? ≠ some key - -private theorem searchLoop_correct (input : Array (BitVec w)) (key : BitVec w) - (hfits : input.size ≤ 2 ^ w) (n start : Nat) (hbound : start + n ≤ input.size) : - match ((searchLoop key n (BitVec.ofNat w start)).evalM timeAndSpaceCost - (arrayMemory input)).1 with - | none => ∀ i, start ≤ i → i < start + n → input[i]? ≠ some key - | some addr => start ≤ addr.toNat ∧ addr.toNat < start + n ∧ - input[addr.toNat]? = some key ∧ - ∀ i, start ≤ i → i < addr.toNat → input[i]? ≠ some key := by - induction n generalizing start <;> grind - -/-- Linear search returns the first match, or certifies that no array index contains the key. -/ -theorem linearSearch_correct (input : Array (BitVec w)) (key : BitVec w) - (hfits : input.size ≤ 2 ^ w) : - match ((linearSearch input key hfits).evalM timeAndSpaceCost (arrayMemory input)).1 with - | none => ∀ i, i < input.size → input[i]? ≠ some key - | some addr => IsFirstMatch input key addr := by - rw [linearSearch_eq_searchLoop] - have h := searchLoop_correct input key hfits input.size 0 (by omega) - grind [IsFirstMatch] - -/-- Search preserves every memory cell. -/ -theorem linearSearch_memory (input : Array (BitVec w)) (key : BitVec w) - (hfits : input.size ≤ 2 ^ w) (mem : Memory w) : - ((linearSearch input key hfits).evalM timeAndSpaceCost mem).2 = mem := by - rw [linearSearch_eq_searchLoop] - exact searchLoop_memory key input.size 0 mem - -/-- A particular address is returned exactly when it is the first occurrence of the key. -/ -theorem linearSearch_some_iff (input : Array (BitVec w)) (key : BitVec w) - (hfits : input.size ≤ 2 ^ w) (addr : Word w) : - ((linearSearch input key hfits).evalM timeAndSpaceCost (arrayMemory input)).1 = some addr ↔ - IsFirstMatch input key addr := by - have hcorrect := linearSearch_correct input key hfits - grind [IsFirstMatch, BitVec.eq_of_toNat_eq] - -/-- Uniform linear time bound: at most three primitive queries per input element. -/ -theorem linearSearch_time_le (input : Array (BitVec w)) (key : BitVec w) - (hfits : input.size ≤ 2 ^ w) : - ((linearSearch input key hfits).costM timeAndSpaceCost (arrayMemory input)).1.time ≤ - 3 * input.size := by - rw [linearSearch_eq_searchLoop] - exact searchLoop_time_le key input.size 0 (arrayMemory input) - -/-- The search fails exactly when the key is absent from the input array. -/ -theorem linearSearch_none_iff (input : Array (BitVec w)) (key : BitVec w) - (hfits : input.size ≤ 2 ^ w) : - ((linearSearch input key hfits).evalM timeAndSpaceCost (arrayMemory input)).1 = none ↔ - key ∉ input := by - have hcorrect := linearSearch_correct input key hfits - grind [IsFirstMatch, Array.mem_iff_getElem?] - -/-- An absent key forces exactly three queries per element, attaining the linear upper bound. -/ -theorem linearSearch_time_of_not_mem (input : Array (BitVec w)) (key : BitVec w) - (hfits : input.size ≤ 2 ^ w) (hnot : key ∉ input) : - ((linearSearch input key hfits).costM timeAndSpaceCost (arrayMemory input)).1.time = - 3 * input.size := by - have hnone := (linearSearch_none_iff input key hfits).mpr hnot - rw [linearSearch_eq_searchLoop] at hnone ⊢ - exact searchLoop_time_of_none key input.size 0 (arrayMemory input) hnone - -private theorem searchLoop_time_of_some (input : Array (BitVec w)) (key : BitVec w) - (hfits : input.size ≤ 2 ^ w) (n start : Nat) (hbound : start + n ≤ input.size) - (addr : Word w) - (hfound : ((searchLoop key n (BitVec.ofNat w start)).evalM timeAndSpaceCost - (arrayMemory input)).1 = some addr) : - ((searchLoop key n (BitVec.ofNat w start)).costM timeAndSpaceCost - (arrayMemory input)).1.time + 3 * start = 3 * addr.toNat + 2 := by - induction n generalizing start <;> grind - -/-- A match at address `i` takes exactly `3 * i + 2` queries. -/ -theorem linearSearch_time_of_some (input : Array (BitVec w)) (key : BitVec w) - (hfits : input.size ≤ 2 ^ w) (addr : Word w) - (hfound : ((linearSearch input key hfits).evalM timeAndSpaceCost - (arrayMemory input)).1 = some addr) : - ((linearSearch input key hfits).costM timeAndSpaceCost (arrayMemory input)).1.time = - 3 * addr.toNat + 2 := by - rw [linearSearch_eq_searchLoop] at hfound ⊢ - simpa using searchLoop_time_of_some input key hfits input.size 0 (by omega) addr hfound - -/-- Addresses occupied by the input array, including cells not visited by an early return. -/ -def inputRegion (input : Array (BitVec w)) : Finset (Word w) := - (Finset.range input.size).image (BitVec.ofNat w) - -/-- Every valid array index belongs to the input's memory region. -/ -@[simp, grind ←] -theorem ofNat_mem_inputRegion (input : Array (BitVec w)) (i : Nat) (hi : i < input.size) : - BitVec.ofNat w i ∈ inputRegion input := - Finset.mem_image.mpr ⟨i, Finset.mem_range.mpr hi, rfl⟩ - -private theorem searchLoop_addresses_subset (input : Array (BitVec w)) (key : BitVec w) - (n start : Nat) (mem : Memory w) (hbound : start + n ≤ input.size) : - ((searchLoop key n (BitVec.ofNat w start)).costM timeAndSpaceCost mem).1.addresses ⊆ - inputRegion input := by - induction n generalizing start <;> grind - -/-- Every address accessed by the search lies in the input region. -/ -theorem linearSearch_addresses_subset (input : Array (BitVec w)) (key : BitVec w) - (hfits : input.size ≤ 2 ^ w) : - ((linearSearch input key hfits).costM timeAndSpaceCost (arrayMemory input)).1.addresses ⊆ - inputRegion input := by - rw [linearSearch_eq_searchLoop] - exact searchLoop_addresses_subset input key input.size 0 (arrayMemory input) (by omega) - -/-- Auxiliary RAM space is exactly zero: the search only accesses input cells. -/ -theorem linearSearch_auxiliarySpace (input : Array (BitVec w)) (key : BitVec w) - (hfits : input.size ≤ 2 ^ w) : - ((linearSearch input key hfits).costM timeAndSpaceCost (arrayMemory input)).1.auxiliarySpace - (inputRegion input) = 0 := by - unfold RAMCost.auxiliarySpace - rw [Finset.sdiff_eq_empty_iff_subset.mpr (linearSearch_addresses_subset input key hfits)] - rfl - -/-- Under the size bound, the input occupies exactly one cell per array element. -/ -theorem inputRegion_card (input : Array (BitVec w)) (hfits : input.size ≤ 2 ^ w) : - (inputRegion input).card = input.size := by - unfold inputRegion - rw [Finset.card_image_of_injOn (by - intro i hi j hj heq - have := congrArg BitVec.toNat heq - grind), Finset.card_range] - -/-- Total space including the input is exactly its length, even after an early return. -/ -theorem linearSearch_totalSpace (input : Array (BitVec w)) (key : BitVec w) - (hfits : input.size ≤ 2 ^ w) : - ((linearSearch input key hfits).costM timeAndSpaceCost (arrayMemory input)).1.totalSpace - (inputRegion input) = input.size := by - unfold RAMCost.totalSpace - rw [Finset.union_eq_right.mpr (linearSearch_addresses_subset input key hfits)] - exact inputRegion_card input hfits - -/-- For every representable length and positive word width, an all-zero input searched for one -attains the upper bound. Thus the worst-case query time is linear, uniformly in the word width. -/ -theorem linearSearch_worstCase (w n : Nat) (hw : 0 < w) (hn : n ≤ 2 ^ w) : - ((linearSearch (Array.replicate n (0 : BitVec w)) 1 (by simpa using hn)).costM - timeAndSpaceCost (arrayMemory (Array.replicate n 0))).1.time = 3 * n := by - simpa using linearSearch_time_of_not_mem (Array.replicate n (0 : BitVec w)) 1 - (by simpa using hn) (by simp [ne_of_gt hw]) - -end CorrectnessAndComplexity - -end Algolean.Algorithms.WordRAM diff --git a/Algolean/FreeWP/WP.lean b/Algolean/FreeWP/WP.lean index 6a5164f..e4849a3 100644 --- a/Algolean/FreeWP/WP.lean +++ b/Algolean/FreeWP/WP.lean @@ -167,6 +167,11 @@ instance instWPMonadFreeM [HasHandler F ps] : WPMonad (FreeM F) ps where wp_pure _ := rfl wp_bind x f := wpH_bind _ x f +/-- The WP of a primitive query is the predicate transformer selected by its handler. -/ +@[simp] theorem wp_lift [HasHandler F ps] (op : F α) : + wp (lift op : FreeM F α) = HasHandler.handler op := + wpH_lift _ op + /-- The generic Hoare rule for a primitive `FreeM` operation. Its precondition is exactly the predicate transformer assigned by the selected logical handler. Its low `mvcgen` priority lets effect-specific rules expose more useful preconditions when available. -/ diff --git a/Algolean/ModelM.lean b/Algolean/ModelM.lean index c906287..3ce8d83 100644 --- a/Algolean/ModelM.lean +++ b/Algolean/ModelM.lean @@ -196,7 +196,7 @@ section State (q : Q α) (f : α → Prog Q β) (s : σ) : evalM (FreeM.lift q >>= f) M s = let result := M.evalQuery q s - (f result.1).evalM M result.2 := rfl + (f result.fst).evalM M result.snd := rfl /-- A pure program has zero cost and leaves the state unchanged. -/ @[simp] theorem costM_pure_state [AddZero Cost] @@ -208,8 +208,8 @@ section State (q : Q α) (f : α → Prog Q β) (s : σ) : costM (FreeM.lift q >>= f) M s = let result := M.evalQuery q s - let rest := (f result.1).costM M result.2 - (M.cost q + rest.1, rest.2) := rfl + let rest := (f result.fst).costM M result.snd + (M.cost q + rest.fst, rest.snd) := rfl end State diff --git a/Algolean/ModelStateM.lean b/Algolean/ModelStateM.lean new file mode 100644 index 0000000..7c10206 --- /dev/null +++ b/Algolean/ModelStateM.lean @@ -0,0 +1,375 @@ +/- +Copyright (c) 2026 Tanner Duve. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Tanner Duve +-/ + +module + +public import Algolean.AddWriter.WP +public import Algolean.ModelM + +/-! +# Monadic query models with joint state and cost semantics + +`ModelStateM` interprets each query with its result and cost in the same monadic execution. +Unlike `ModelM`, costs may depend on the state or on the query outcome. The monad remains generic: +stateful and probabilistic interpretations both retain the correlation between results and costs. +`Prog.evalStateM` evaluates a program, `Prog.runStateM` records its result and accumulated cost, +and `Prog.costStateM` returns the accumulated cost. + +`ModelStateM.handler` and `ModelStateM.hasHandler` provide weakest-precondition semantics +for `mvcgen` when the monad has a `Std.Do.WPMonad` instance. +-/ + +@[expose] public section + +namespace Algolean.Algorithms + +open Cslib + +/-- A query model whose queries are evaluated in the monad `m`. -/ +structure ModelStateM (Q : Type u → Type v) (m : Type u → Type w) (Cost : Type u) where + /-- Execute a query, retaining its result and cost in the same effect branch. -/ + runQuery : Q α → AddWriterT Cost m α + +namespace ModelStateM + +variable {Q : Type u → Type v} {m : Type u → Type w} {Cost : Type u} + +/-- Evaluate a query, forgetting its cost. -/ +def evalQuery [Functor m] (M : ModelStateM Q m Cost) (q : Q α) : m α := + (M.runQuery q).value + +/-- Construct a model whose query costs are independent of execution. -/ +def ofCost [Functor m] (evalQuery : {α : Type u} → Q α → m α) + (cost : {α : Type u} → Q α → Cost) : ModelStateM Q m Cost where + runQuery q := AddWriterT.mk ((fun a => ⟨a, cost q⟩) <$> evalQuery q) + +@[simp] theorem ofCost_evalQuery [Functor m] [LawfulFunctor m] + (evalQuery : {α : Type u} → Q α → m α) (cost : {α : Type u} → Q α → Cost) (q : Q α) : + (ofCost @evalQuery @cost).evalQuery q = evalQuery q := by + simp [ofCost, ModelStateM.evalQuery, AddWriterT.value] + +@[simp] theorem ofCost_runQuery [Functor m] + (evalQuery : {α : Type u} → Q α → m α) (cost : {α : Type u} → Q α → Cost) (q : Q α) : + ((ofCost @evalQuery @cost).runQuery q).run = + (fun a => (⟨a, cost q⟩ : AddWriter Cost α)) <$> evalQuery q := rfl + +/-- Fixed-cost query execution at a concrete state. -/ +@[simp, grind =] theorem ofCost_runQuery_state + (evalQuery : {α : Type u} → Q α → StateM σ α) + (cost : {α : Type u} → Q α → Cost) (q : Q α) (s : σ) : + ((ofCost @evalQuery @cost).runQuery q).run s = + ((⟨(evalQuery q s).fst, cost q⟩ : AddWriter Cost α), (evalQuery q s).snd) := rfl + +@[simp] theorem runQuery_value [Functor m] (M : ModelStateM Q m Cost) (q : Q α) : + (M.runQuery q).value = M.evalQuery q := rfl + +/-- Regard a `Model` as a `ModelStateM` over `Id`. -/ +def ofModel (M : Algolean.Algorithms.Model Q Cost) : ModelStateM Q Id Cost := + ofCost (fun q => M.evalQuery q) M.cost + +@[simp] theorem ofModel_evalQuery (M : Algolean.Algorithms.Model Q Cost) (q : Q α) : + (ofModel M).evalQuery q = M.evalQuery q := rfl + +@[simp] theorem ofModel_runQuery (M : Algolean.Algorithms.Model Q Cost) (q : Q α) : + ((ofModel M).runQuery q).run = ⟨M.evalQuery q, M.cost q⟩ := rfl + +/-- Sum query languages, preserving each branch's joint interpretation. -/ +def sum {Q₂ : Type u → Type x} (M₁ : ModelStateM Q m Cost) (M₂ : ModelStateM Q₂ m Cost) : + ModelStateM (fun α => Sum (Q α) (Q₂ α)) m Cost where + runQuery + | .inl q => M₁.runQuery q + | .inr q => M₂.runQuery q + +@[simp] theorem sum_runQuery_inl {Q₂ : Type u → Type x} + (M₁ : ModelStateM Q m Cost) (M₂ : ModelStateM Q₂ m Cost) (q : Q α) : + (M₁.sum M₂).runQuery (.inl q) = M₁.runQuery q := rfl + +@[simp] theorem sum_runQuery_inr {Q₂ : Type u → Type x} + (M₁ : ModelStateM Q m Cost) (M₂ : ModelStateM Q₂ m Cost) (q : Q₂ α) : + (M₁.sum M₂).runQuery (.inr q) = M₂.runQuery q := rfl + +@[simp] theorem sum_evalQuery_inl [Functor m] {Q₂ : Type u → Type x} + (M₁ : ModelStateM Q m Cost) (M₂ : ModelStateM Q₂ m Cost) (q : Q α) : + (M₁.sum M₂).evalQuery (.inl q) = M₁.evalQuery q := rfl + +@[simp] theorem sum_evalQuery_inr [Functor m] {Q₂ : Type u → Type x} + (M₁ : ModelStateM Q m Cost) (M₂ : ModelStateM Q₂ m Cost) (q : Q₂ α) : + (M₁.sum M₂).evalQuery (.inr q) = M₂.evalQuery q := rfl + +end ModelStateM + +namespace Prog + +variable {Q : Type u → Type v} {m : Type u → Type w} {Cost : Type u} + +/-- Evaluate a query program in the semantic monad of `M`. -/ +def evalStateM [Monad m] (P : Prog Q α) (M : ModelStateM Q m Cost) : m α := + P.liftM M.evalQuery + +/-- Evaluate a query program while recording the accumulated query cost with each result. -/ +def runStateM [Monad m] [AddZero Cost] + (P : Prog Q α) (M : ModelStateM Q m Cost) : AddWriterT Cost m α := + P.liftM M.runQuery + +/-- The accumulated query cost of each execution of a program. -/ +def costStateM [Monad m] [AddZero Cost] + (P : Prog Q α) (M : ModelStateM Q m Cost) : m Cost := + (P.runStateM M).cost + +@[simp] theorem evalStateM_pure [Monad m] (a : α) (M : ModelStateM Q m Cost) : + evalStateM (pure a : Prog Q α) M = pure a := rfl + +@[simp] theorem evalStateM_liftBind [Monad m] + (q : Q α) (f : α → Prog Q β) (M : ModelStateM Q m Cost) : + evalStateM (FreeM.lift q >>= f) M = (M.evalQuery q >>= fun a => evalStateM (f a) M) := rfl + +@[simp] theorem evalStateM_lift [Monad m] [LawfulMonad m] + (q : Q α) (M : ModelStateM Q m Cost) : + evalStateM (FreeM.lift q) M = M.evalQuery q := by + simp [evalStateM] + +@[simp] theorem evalStateM_bind [Monad m] [LawfulMonad m] + (P : Prog Q α) (f : α → Prog Q β) (M : ModelStateM Q m Cost) : + evalStateM (P >>= f) M = (evalStateM P M >>= fun a => evalStateM (f a) M) := by + simp [evalStateM] + +@[simp] theorem evalStateM_map [Monad m] [LawfulMonad m] + (f : α → β) (P : Prog Q α) (M : ModelStateM Q m Cost) : + evalStateM (f <$> P) M = f <$> evalStateM P M := by + simp [evalStateM] + +@[simp] theorem runStateM_pure [Monad m] [AddZero Cost] + (a : α) (M : ModelStateM Q m Cost) : + runStateM (pure a : Prog Q α) M = pure a := rfl + +@[simp] theorem runStateM_liftBind [Monad m] [AddZero Cost] + (q : Q α) (f : α → Prog Q β) (M : ModelStateM Q m Cost) : + runStateM (FreeM.lift q >>= f) M = (M.runQuery q >>= fun a => runStateM (f a) M) := rfl + +@[simp] theorem runStateM_lift [Monad m] [LawfulMonad m] [AddMonoid Cost] + (q : Q α) (M : ModelStateM Q m Cost) : + runStateM (FreeM.lift q) M = M.runQuery q := by + simp [runStateM] + +@[simp] theorem runStateM_bind [Monad m] [LawfulMonad m] [AddMonoid Cost] + (P : Prog Q α) (f : α → Prog Q β) (M : ModelStateM Q m Cost) : + runStateM (P >>= f) M = (runStateM P M >>= fun a => runStateM (f a) M) := by + simp [runStateM] + +@[simp] theorem runStateM_map [Monad m] [LawfulMonad m] [AddMonoid Cost] + (f : α → β) (P : Prog Q α) (M : ModelStateM Q m Cost) : + runStateM (f <$> P) M = f <$> runStateM P M := by + simp [runStateM] + +/-- Forgetting the cost component of the joint semantics recovers `evalStateM`. -/ +@[simp] theorem runStateM_value [Monad m] [LawfulMonad m] [AddZero Cost] + (P : Prog Q α) (M : ModelStateM Q m Cost) : + (P.runStateM M).value = P.evalStateM M := by + induction P with + | pure a => simp + | liftBind q f ih => + simp only [runStateM, evalStateM, FreeM.liftM, AddWriterT.value_bind] at ih ⊢ + simp only [AddWriterT.value] at ih + simp only [ModelStateM.evalQuery, AddWriterT.value, bind_map_left, ih] + +@[simp] theorem costStateM_pure [Monad m] [LawfulMonad m] [AddZero Cost] + (a : α) (M : ModelStateM Q m Cost) : + costStateM (pure a : Prog Q α) M = pure 0 := by + simp [costStateM] + +@[simp] theorem costStateM_liftBind [Monad m] [LawfulMonad m] [AddZero Cost] + (q : Q α) (f : α → Prog Q β) (M : ModelStateM Q m Cost) : + costStateM (FreeM.lift q >>= f) M = + ((M.runQuery q).run >>= fun a => (a.tell + ·) <$> costStateM (f a.ret) M) := by + simp [costStateM, runStateM, AddWriterT.cost, AddWriterT.run_bind] + +@[simp] theorem costStateM_lift [Monad m] [LawfulMonad m] [AddMonoid Cost] + (q : Q α) (M : ModelStateM Q m Cost) : + costStateM (FreeM.lift q) M = (M.runQuery q).cost := by + simp [costStateM] + +@[simp] theorem costStateM_map [Monad m] [LawfulMonad m] [AddMonoid Cost] + (f : α → β) (P : Prog Q α) (M : ModelStateM Q m Cost) : + costStateM (f <$> P) M = costStateM P M := by + simp [costStateM] + +section State + +/-- Joint execution of a pure program preserves the state and records zero cost. -/ +@[simp, grind =] theorem runStateM_pure_state [AddZero Cost] + (M : ModelStateM Q (StateM σ) Cost) (a : α) (s : σ) : + ((pure a : Prog Q α).runStateM M).run s = ((⟨a, 0⟩ : AddWriter Cost α), s) := rfl + +/-- Joint execution supplies the same query outcome to the continuation and the cost sum. -/ +@[simp, grind =] theorem runStateM_liftBind_state [AddZero Cost] + (M : ModelStateM Q (StateM σ) Cost) (q : Q α) (f : α → Prog Q β) (s : σ) : + (runStateM (FreeM.liftBind q f) M).run s = + let first := (M.runQuery q).run s + let rest := ((f first.fst.ret).runStateM M).run first.snd + ((⟨rest.fst.ret, first.fst.tell + rest.fst.tell⟩ : AddWriter Cost β), rest.snd) := rfl + +/-- Joint execution rule for the lifted-query bind notation. -/ +@[simp, grind =] theorem runStateM_lift_bind_state [AddZero Cost] + (M : ModelStateM Q (StateM σ) Cost) (q : Q α) (f : α → Prog Q β) (s : σ) : + (runStateM (FreeM.lift q >>= f) M).run s = + let first := (M.runQuery q).run s + let rest := ((f first.fst.ret).runStateM M).run first.snd + ((⟨rest.fst.ret, first.fst.tell + rest.fst.tell⟩ : AddWriter Cost β), rest.snd) := rfl + +/-- Execute the selected branch without hiding the conditional inside the interpreter. -/ +@[simp] theorem runStateM_ite_state [AddZero Cost] + (condition : Prop) [Decidable condition] (yes no : Prog Q α) + (M : ModelStateM Q (StateM σ) Cost) (s : σ) : + (runStateM (if condition then yes else no) M).run s = + if condition then (yes.runStateM M).run s else (no.runStateM M).run s := by + split <;> rfl + +/-- Recover evaluation from joint execution at a concrete state. -/ +@[simp, grind =] theorem evalStateM_eq_runStateM_state [AddZero Cost] + (P : Prog Q α) (M : ModelStateM Q (StateM σ) Cost) (s : σ) : + P.evalStateM M s = (((P.runStateM M).run s).fst.ret, ((P.runStateM M).run s).snd) := by + rw [← runStateM_value] + rfl + +/-- Recover cost from joint execution at a concrete state. -/ +@[simp, grind =] theorem costStateM_eq_runStateM_state [AddZero Cost] + (P : Prog Q α) (M : ModelStateM Q (StateM σ) Cost) (s : σ) : + P.costStateM M s = (((P.runStateM M).run s).fst.tell, ((P.runStateM M).run s).snd) := rfl + +/-- Cost accounting preserves the final state of ordinary evaluation. -/ +@[simp] theorem costStateM_state [AddZero Cost] (P : Prog Q α) + (M : ModelStateM Q (StateM σ) Cost) (s : σ) : + (P.costStateM M s).snd = (P.evalStateM M s).snd := by + simp + +end State + +section OfModel + +/-- Evaluating with `ofModel M` is the same as evaluating with `M`. -/ +@[simp] theorem evalStateM_ofModel (P : Prog Q α) (M : Algolean.Algorithms.Model Q Cost) : + Id.run (P.evalStateM (ModelStateM.ofModel M)) = P.eval M := rfl + +/-- The cost of a query followed by a program under `ofModel`. -/ +@[simp] theorem costStateM_ofModel_liftBind [AddZero Cost] + (q : Q α) (f : α → Prog Q β) (M : Algolean.Algorithms.Model Q Cost) : + Id.run (Prog.costStateM (FreeM.lift q >>= f) (ModelStateM.ofModel M)) = + M.cost q + Id.run ((f (M.evalQuery q)).costStateM (ModelStateM.ofModel M)) := rfl + +/-- Computing cost with `ofModel M` gives `Prog.time M`. -/ +@[simp] theorem costStateM_ofModel [AddZero Cost] + (P : Prog Q α) (M : Algolean.Algorithms.Model Q Cost) : + Id.run (P.costStateM (ModelStateM.ofModel M)) = P.time M := by + induction P with + | pure a => rfl + | liftBind q f ih => exact congrArg (M.cost q + ·) (ih (M.evalQuery q)) + +end OfModel + +section Reduction + +variable {Q₁ Q₂ : Type u → Type u} + +/-- A query reduction preserving each query also preserves program evaluation. -/ +theorem reduceProg_evalStateM [Monad m] [LawfulMonad m] + (P : Prog Q₁ α) (red : Reduction Q₁ Q₂) + (M₁ : ModelStateM Q₁ m Cost₁) (M₂ : ModelStateM Q₂ m Cost₂) + (hCorrect : ∀ {ι} (q : Q₁ ι), (red.reduce q).evalStateM M₂ = M₁.evalQuery q) : + (P.reduceProg red).evalStateM M₂ = P.evalStateM M₁ := + reduceProg_liftM P red M₁.evalQuery M₂.evalQuery hCorrect + +/-- A query reduction preserving `runStateM` also preserves `runStateM` for every program. -/ +theorem reduceProg_runStateM [Monad m] [LawfulMonad m] [AddMonoid Cost] + (P : Prog Q₁ α) (red : Reduction Q₁ Q₂) + (M₁ : ModelStateM Q₁ m Cost) (M₂ : ModelStateM Q₂ m Cost) + (hCorrect : ∀ {ι} (q : Q₁ ι), (red.reduce q).runStateM M₂ = M₁.runQuery q) : + (P.reduceProg red).runStateM M₂ = P.runStateM M₁ := + reduceProg_liftM P red M₁.runQuery M₂.runQuery hCorrect + +/-- A query reduction preserving `runStateM` also preserves accumulated program costs. -/ +theorem reduceProg_costStateM [Monad m] [LawfulMonad m] [AddMonoid Cost] + (P : Prog Q₁ α) (red : Reduction Q₁ Q₂) + (M₁ : ModelStateM Q₁ m Cost) (M₂ : ModelStateM Q₂ m Cost) + (hCorrect : ∀ {ι} (q : Q₁ ι), (red.reduce q).runStateM M₂ = M₁.runQuery q) : + (P.reduceProg red).costStateM M₂ = P.costStateM M₁ := + congrArg AddWriterT.cost (reduceProg_runStateM P red M₁ M₂ hCorrect) + +end Reduction + +end Prog + +section WeakestPrecondition + +open Cslib.FreeM Std.Do + +variable {ps : PostShape.{u}} + +namespace ModelStateM + +/-- A handler exposing both query results and accumulated costs to postconditions. -/ +def costHandler [Functor m] [Add Cost] [WP m ps] (M : ModelStateM Q m Cost) : + LHandler Q (.arg Cost ps) := + LHandler.ofInterp (m := AddWriterT Cost m) (fun _ q => M.runQuery q) + +/-- Evaluate a cost-aware state-model query's postcondition from its joint outcome. -/ +@[simp] theorem costHandler_apply_state [Add Cost] + (M : ModelStateM Q (StateM σ) Cost) (q : Q α) + (post : PostCond α (.arg Cost (.arg σ .pure))) (initial : Cost) (s : σ) : + (M.costHandler q).apply post initial s = + post.fst ((M.runQuery q).run s).fst.ret + (initial + ((M.runQuery q).run s).fst.tell) ((M.runQuery q).run s).snd := rfl + +/-- Register joint execution for cost-aware `mvcgen` reasoning. -/ +@[reducible] def hasCostHandler [Functor m] [Add Cost] [WP m ps] + (M : ModelStateM Q m Cost) : HasHandler Q (.arg Cost ps) where + handler := M.costHandler + +/-- The cost-aware handler agrees with joint program execution. -/ +theorem wp_eq_wp_runStateM [Monad m] [AddMonoid Cost] [WPMonad m ps] + (M : ModelStateM Q m Cost) (P : Prog Q α) : + wpH M.costHandler P = wp (P.runStateM M) := + wpH_ofInterp_eq_wp_liftM (m := AddWriterT Cost m) (fun _ q => M.runQuery q) P + +/-- The logical handler induced by `M.evalQuery`. -/ +def handler [Functor m] [WP m ps] (M : ModelStateM Q m Cost) : LHandler Q ps := + LHandler.ofInterp (m := m) (fun _ q => M.evalQuery q) + +@[simp] theorem handler_sum [Functor m] [WP m ps] {Q₂ : Type u → Type x} + (M₁ : ModelStateM Q m Cost) (M₂ : ModelStateM Q₂ m Cost) (q : Q α ⊕ Q₂ α) : + (M₁.sum M₂).handler q = LHandler.sum M₁.handler M₂.handler q := by + cases q <;> rfl + +/-- Use `M.handler` as the logical handler for `Prog Q`. -/ +@[reducible] def hasHandler [Functor m] [WP m ps] (M : ModelStateM Q m Cost) : HasHandler Q ps where + handler := M.handler + +/-- The weakest precondition given by `M.handler` agrees with that of `Prog.evalStateM M`. -/ +theorem wp_eq_wp_evalStateM [Monad m] [WPMonad m ps] + (M : ModelStateM Q m Cost) (P : Prog Q α) : + wpH M.handler P = wp (P.evalStateM M) := + wpH_ofInterp_eq_wp_liftM (m := m) (fun _ q => M.evalQuery q) P + +end ModelStateM + +/-- The query rule stated directly through the semantic monad's weakest precondition. -/ +theorem ModelStateM.query_spec [Monad m] [WPMonad m ps] + (M : ModelStateM Q m Cost) (q : Q α) {Q' : PostCond α ps} : + let _ : HasHandler Q ps := M.hasHandler + Triple (FreeM.lift q : Prog Q α) (wp⟦M.evalQuery q⟧ Q') Q' := by + let _inst := M.hasHandler + exact Cslib.FreeM.Spec.lift_FreeM q + +/-- The query rule for postconditions that also observe accumulated cost. -/ +theorem ModelStateM.cost_query_spec [Monad m] [AddMonoid Cost] [WPMonad m ps] + (M : ModelStateM Q m Cost) (q : Q α) {Q' : PostCond α (.arg Cost ps)} : + let _ : HasHandler Q (.arg Cost ps) := M.hasCostHandler + Triple (FreeM.lift q : Prog Q α) (wp⟦M.runQuery q⟧ Q') Q' := by + let _inst := M.hasCostHandler + exact Cslib.FreeM.Spec.lift_FreeM q + +end WeakestPrecondition + +end Algolean.Algorithms diff --git a/Algolean/Models/WordRAM.lean b/Algolean/Models/WordRAM.lean index a26428f..496b9a3 100644 --- a/Algolean/Models/WordRAM.lean +++ b/Algolean/Models/WordRAM.lean @@ -6,37 +6,67 @@ Authors: Shreyas Srinivas module -public import Algolean.ModelM +public import Algolean.ModelStateM public import Mathlib.Data.Finset.Card /-! -# Word-RAM queries +# Word-RAM model -`WordRAM w` provides memory access, arithmetic, bitwise operations, and comparisons on -`w`-bit words. `WordRAM.natCost` interprets these queries in mutable memory and -charges one per query. Algorithms use the usual `Prog (WordRAM w)` combinators. -`WordRAM.timeAndSpaceCost` also records the set of addresses accessed. Its cost algebra adds time -and unions address sets, so repeated accesses increase time without counting a cell more than once. +`WordRAM w k` describes a machine with `k` registers and `2 ^ w` memory cells. +Each register and memory cell holds a `w`-bit word. -Words and addresses have the same fixed width. Arithmetic wraps modulo `2 ^ w`; comparisons -are unsigned; shifts are logical and return zero when the shift amount is at least `w`. -All `2 ^ w` addresses are available. The caller supplies initial memory, with `Memory.zero` -as a convenient starting point. Allocation and input encoding are not part of this query type. -The definitions also support the degenerate width zero; ordinary word-RAM applications use `w > 0`. +Inputs are supplied in the initial machine state's memory and registers. +A `Prog` cannot directly read or modify either: it must use WordRAM queries. -Costs count primitive queries. Sequencing and branching are supplied by `Prog` combinators and carry -no additional cost. Runtime word operations must be exposed as queries to contribute to this count; -arbitrary Lean computation in continuations is not charged. +Instructions load and store words, set and copy registers, perform arithmetic and +bitwise operations, and compare registers. Comparisons store their results in flags. +Branches and loops check those flags. Every query returns `Unit`; computed words +remain in the machine's registers and memory. -`RAMCost.space` counts distinct accessed cells in words. `RAMCost.auxiliarySpace` excludes an input -region. `RAMCost.totalSpace` includes that region even if some input cells are unread. -This is an accessed-memory footprint, not peak live allocation or storage in Lean continuations. +Arithmetic wraps modulo `2 ^ w`. Comparisons treat words as unsigned numbers. +Shifts fill with zeros and return zero when the shift amount is at least `w`. + +## Running programs + +`RAMState` holds the memory, registers, and flags. +`execute fuel program state` runs a program using `timeAndSpaceCost`. + +Fuel limits the number of execution steps. Each instruction, branch selection, +and loop test consumes one unit. Running out of fuel returns `none`. +A completed run returns the program's result, cost, final state, and unused fuel. + +## Time and space + +Each load, store, register operation, comparison, and `nop` costs one time unit. +Choosing a branch or testing an existing flag costs no time. +Fuel is counted separately from time. + +`RAMCost` records time and the set of memory cells accessed. + +- `space` counts distinct accessed cells. +- `auxiliarySpace` counts accessed cells outside the input. +- `totalSpace` counts input cells and accessed cells, including unread input cells. + +Registers and flags do not count toward space. Program size and the Lean +computation used to construct a program are not counted. + +## Main theorems + +- `execute_eq_runCode`: running a program agrees with running its instruction list. +- `execute_add_fuel`: adding fuel to a completed run preserves its final state and cost. +- `Completes.unique`: completed runs of the same code from the same state agree + on the final state and cost. +- `Completes.execute`: a proof of completion supplies enough fuel to run the program. +- `execute_ret_independent`: completed runs of a fixed program return the same Lean + value, regardless of the initial machine state. + +Program notation is defined in `Algolean.Models.WordRAMSyntax`. ## References * Pat Morin, *Open Data Structures*, §1.4: https://opendatastructures.org/ods-java/1_4_Model_Computation.html -* Harvard CS125, Lecture 6, §§6.6–6.7 (word-RAM instructions and modular arithmetic): +* Harvard CS125, Lecture 6, §§6.6–6.7: https://people.seas.harvard.edu/~cs125/fall16/lec6.pdf -/ @@ -44,16 +74,100 @@ This is an accessed-memory footprint, not peak live allocation or storage in Lea namespace Algolean.Algorithms +namespace Prog + +section ControlFlowDefinitions + +/-- A model-controlled condition. Choosing a branch never returns its decision to Lean. +The condition may execute queries before selecting a `Unit` body. -/ +abbrev Condition (Q : Type u → Type v) := + Prog Q Unit → Prog Q Unit → Prog Q Unit + +/-- Execute the body selected by a model-controlled condition. -/ +def ifThenElse (condition : Condition Q) (yes no : Prog Q Unit) : Prog Q Unit := + condition yes no + +/-- Execute a body only when the model-controlled condition holds. -/ +def when (condition : Condition Q) (body : Prog Q Unit) : Prog Q Unit := + ifThenElse condition body (pure ()) + +/-- Execute a body only when the model-controlled condition does not hold. -/ +def unlessDo (condition : Condition Q) (body : Prog Q Unit) : Prog Q Unit := + ifThenElse condition (pure ()) body + +/-- Negate a condition without exposing its decision. -/ +def Condition.not (condition : Condition Q) : Condition Q := + fun yes no => condition no yes + +@[simp, grind =] theorem ifThenElse_not (condition : Condition Q) (yes no : Prog Q Unit) : + ifThenElse condition.not yes no = ifThenElse condition no yes := rfl + +@[simp] theorem Condition.not_not (condition : Condition Q) : condition.not.not = condition := rfl + +/-- Run at most `fuel` iterations, testing before each body. Zero fuel performs no test. +A condition that performs queries executes those queries anew on every test. -/ +def repeatLoop (condition : Condition Q) (body : Prog Q Unit) : Nat → Prog Q Unit + | 0 => pure () + | fuel + 1 => ifThenElse condition (do body; repeatLoop condition body fuel) (pure ()) + +@[simp, grind =] theorem repeatLoop_zero (condition : Condition Q) (body : Prog Q Unit) : + repeatLoop condition body 0 = pure () := rfl + +@[simp, grind =] theorem repeatLoop_succ + (condition : Condition Q) (body : Prog Q Unit) (fuel : Nat) : + repeatLoop condition body (fuel + 1) = + ifThenElse condition (do body; repeatLoop condition body fuel) (pure ()) := rfl + +end ControlFlowDefinitions + +end Prog + namespace WordRAM /-- A fixed-width word, used for both data and addresses. -/ -abbrev Word (w : Nat) := BitVec w +abbrev Word (w : ℕ) := BitVec w + +/-- A register identifier, not a word value. There are exactly `k` available registers. -/ +abbrev Register (k : ℕ) := Fin k + +/-- The contents of the word-addressed memory. -/ +abbrev Memory (w : ℕ) := Word w → Word w -/-- The contents of every address in the word-sized address space. -/ -abbrev Memory (w : Nat) := Word w → Word w +/-- Word comparisons; ordering is unsigned. -/ +inductive CmpOp where + | eq | ult + deriving DecidableEq, Repr -/-- Initial memory with every cell set to zero. -/ -def Memory.zero : Memory w := fun _ => 0 +/-- Machine words live in memory or one of the fixed `k` register slots. -/ +structure RAMState (w k : ℕ) where + /-- The word stored at each memory address. -/ + Memory : Word w → Word w + /-- The words held in the fixed register file. -/ + Registers : Register k → Word w + /-- One comparison flag per operation, separate from word registers. -/ + Flags : CmpOp → Bool := fun _ => false + +/-- Zero-initialized memory and registers, with cleared comparison flags. -/ +def RAMState.zero : RAMState w k := ⟨fun _ => 0, fun _ => 0, fun _ => false⟩ + +/-- Update a register; values are computed from the old state before this update. -/ +def RAMState.writeRegister (s : RAMState w k) (r : Register k) (value : Word w) : RAMState w k := + { s with Registers := Function.update s.Registers r value } + +@[simp, grind =] theorem RAMState.writeRegister_memory (s : RAMState w k) + (r : Register k) (value : Word w) : (s.writeRegister r value).Memory = s.Memory := rfl + +@[simp, grind =] theorem RAMState.writeRegister_registers (s : RAMState w k) + (r : Register k) (value : Word w) (r' : Register k) : + (s.writeRegister r value).Registers r' = if r' = r then value else s.Registers r' := by + simp [RAMState.writeRegister, Function.update_apply] + +/-- A second write to the same register replaces the first. -/ +@[simp, grind =] theorem RAMState.writeRegister_overwrite (s : RAMState w k) + (r : Register k) (a b : Word w) : + (s.writeRegister r a).writeRegister r b = s.writeRegister r b := by + cases s + simp [RAMState.writeRegister, Function.update_idem] /-- Binary word operations in the basic instruction set. -/ inductive BinOp where @@ -62,10 +176,9 @@ inductive BinOp where | shl | shr deriving DecidableEq, Repr -/-- Word comparisons; ordering is unsigned. -/ -inductive CmpOp where - | eq | ult - deriving DecidableEq, Repr +@[simp, grind =] theorem RAMState.writeRegister_self (s : RAMState w k) (r : Register k) : + s.writeRegister r (s.Registers r) = s := by + simp [RAMState.writeRegister, Function.update_eq_self] /-- Evaluate a binary operation. Shift amounts use the full unsigned value of the second word. -/ def BinOp.eval : BinOp → Word w → Word w → Word w @@ -84,43 +197,92 @@ def CmpOp.eval : CmpOp → Word w → Word w → Bool end WordRAM -/-- Primitive word-RAM queries, indexed by the type of their result. -/ -inductive WordRAM (w : Nat) : Type → Type where - | load (addr : WordRAM.Word w) : WordRAM w (WordRAM.Word w) - | store (addr value : WordRAM.Word w) : WordRAM w Unit - | binop (op : WordRAM.BinOp) (x y : WordRAM.Word w) : WordRAM w (WordRAM.Word w) - | bnot (x : WordRAM.Word w) : WordRAM w (WordRAM.Word w) - | cmp (op : WordRAM.CmpOp) (x y : WordRAM.Word w) : WordRAM w Bool +/-- Register-based instructions with machine-local comparison flags and structured branches. +All instructions return `Unit`, including comparisons and branches. -/ +inductive WordRAM (w k : Nat) : Type → Type where + /-- Leave the machine state unchanged, costing one time unit. -/ + | nop : WordRAM w k Unit + | set (dst : WordRAM.Register k) (value : WordRAM.Word w) : WordRAM w k Unit + | copy (dst src : WordRAM.Register k) : WordRAM w k Unit + | load (dst addr : WordRAM.Register k) : WordRAM w k Unit + | store (addr src : WordRAM.Register k) : WordRAM w k Unit + | binop (op : WordRAM.BinOp) (dst x y : WordRAM.Register k) : WordRAM w k Unit + | bnot (dst src : WordRAM.Register k) : WordRAM w k Unit + | cmp (op : WordRAM.CmpOp) (x y : WordRAM.Register k) : WordRAM w k Unit + | clearFlag (op : WordRAM.CmpOp) : WordRAM w k Unit + | branchCode (op : WordRAM.CmpOp) (yes no : List (WordRAM w k Unit)) : WordRAM w k Unit + | whileCode (op : WordRAM.CmpOp) (body : List (WordRAM w k Unit)) : WordRAM w k Unit namespace WordRAM -/-- Stateful word-RAM semantics with unit cost for every primitive query. -/ -@[simps] -def natCost : ModelM (WordRAM w) (StateM (Memory w)) Nat where - evalQuery - | .load addr => do - let mem ← get - pure (mem addr) - | .store addr value => modify (fun mem => Function.update mem addr value) - | .binop op x y => pure (op.eval x y) - | .bnot x => pure (~~~x) - | .cmp op x y => pure (op.eval x y) - cost _ := 1 - -/-- Concrete-state semantics of each word-RAM query. -/ -@[simp] theorem natCost_evalQuery_state (q : WordRAM w α) (mem : Memory w) : - natCost.evalQuery q mem = match q with - | .load addr => (mem addr, mem) - | .store addr value => ((), Function.update mem addr value) - | .binop op x y => (op.eval x y, mem) - | .bnot x => (~~~x, mem) - | .cmp op x y => (op.eval x y, mem) := by +/-- Every instruction returns `Unit`; machine data never enters a continuation. -/ +theorem result_type (q : WordRAM w k α) : α = Unit := by cases q <;> rfl +/-- Change one flag without altering memory, word registers, or other flags. -/ +def RAMState.writeFlag (s : RAMState w k) (op : CmpOp) (flag : Bool) : RAMState w k := + { s with Flags := Function.update s.Flags op flag } + +@[simp, grind =] theorem RAMState.writeFlag_memory (s : RAMState w k) (op : CmpOp) (b : Bool) : + (s.writeFlag op b).Memory = s.Memory := rfl + +@[simp, grind =] theorem RAMState.writeFlag_registers (s : RAMState w k) (op : CmpOp) (b : Bool) : + (s.writeFlag op b).Registers = s.Registers := rfl + +@[simp, grind =] theorem RAMState.writeFlag_flags (s : RAMState w k) + (op : CmpOp) (b : Bool) (op' : CmpOp) : + (s.writeFlag op b).Flags op' = if op' = op then b else s.Flags op' := by + simp [RAMState.writeFlag, Function.update_apply] + +@[simp, grind =] theorem RAMState.writeFlag_overwrite (s : RAMState w k) + (op : CmpOp) (a b : Bool) : + (s.writeFlag op a).writeFlag op b = s.writeFlag op b := by + cases s + simp [RAMState.writeFlag, Function.update_idem] + +@[simp, grind =] theorem RAMState.writeRegister_flags (s : RAMState w k) + (r : Register k) (v : Word w) : (s.writeRegister r v).Flags = s.Flags := rfl + +/-- Compile a `Unit` program to a finite block without consulting machine state. -/ +def instructions : Prog (WordRAM w k) Unit → List (WordRAM w k Unit) + | .pure _ => [] + | .liftBind q cont => + (result_type q ▸ q) :: instructions (cont ((result_type q).symm ▸ ())) + +@[simp] theorem instructions_pure : + instructions (pure () : Prog (WordRAM w k) Unit) = [] := rfl + +@[simp] theorem instructions_lift_bind (q : WordRAM w k Unit) + (cont : Unit → Prog (WordRAM w k) Unit) : + instructions (Cslib.FreeM.lift q >>= cont) = q :: instructions (cont ()) := rfl + +/-- Branch on the flag indexed by `op`, without exposing it as a Lean Boolean. -/ +def branch (op : CmpOp) (yes no : Prog (WordRAM w k) Unit) : Prog (WordRAM w k) Unit := + .liftBind (.branchCode op (instructions yes) (instructions no)) pure + +section ControlFlowConditions + +/-- Use an existing comparison flag as a condition, without running another comparison. -/ +def flag (op : CmpOp) : Prog.Condition (WordRAM w k) := branch op + +/-- Compare two registers anew whenever this condition is tested. -/ +def test (op : CmpOp) (x y : Register k) : Prog.Condition (WordRAM w k) := fun yes no => do + cmp (w := w) op x y + branch op yes no + +@[simp, grind =] theorem ifThenElse_flag (op : CmpOp) (yes no : Prog (WordRAM w k) Unit) : + Prog.ifThenElse (flag op) yes no = branch op yes no := rfl + +@[simp, grind =] theorem ifThenElse_test (op : CmpOp) (x y : Register k) + (yes no : Prog (WordRAM w k) Unit) : + Prog.ifThenElse (test op x y) yes no = (do cmp (w := w) op x y; branch op yes no) := rfl + +end ControlFlowConditions + /-- Time and the set of memory addresses accessed by an execution. -/ @[ext] -structure RAMCost (w : Nat) where - /-- Number of primitive queries executed. -/ +structure RAMCost (w k : Nat) where + /-- Number of primitive word and flag operations executed; branch selection is free. -/ time : Nat /-- Distinct addresses loaded from or stored to. -/ addresses : Finset (Word w) @@ -129,15 +291,15 @@ structure RAMCost (w : Nat) where namespace RAMCost @[simps] -instance : Zero (RAMCost w) := ⟨0, ∅⟩ +instance : Zero (RAMCost w k) := ⟨0, ∅⟩ @[simps] -instance : Add (RAMCost w) where +instance : Add (RAMCost w k) where add a b := ⟨a.time + b.time, a.addresses ∪ b.addresses⟩ attribute [grind =] zero_time zero_addresses add_time add_addresses -instance : AddCommMonoid (RAMCost w) where +instance : AddCommMonoid (RAMCost w k) where nsmul := nsmulRec zero_add a := by ext <;> simp add_zero a := by ext <;> simp @@ -145,37 +307,381 @@ instance : AddCommMonoid (RAMCost w) where add_comm a b := by ext <;> simp [Nat.add_comm, Finset.union_comm] /-- Normalize addition to the time sum and the union of accessed addresses. -/ -@[simp, grind =] theorem mk_add (time : Nat) (addresses : Finset (Word w)) (c : RAMCost w) : - (⟨time, addresses⟩ : RAMCost w) + c = ⟨time + c.time, addresses ∪ c.addresses⟩ := rfl +@[simp, grind =] theorem mk_add (time : Nat) (addresses : Finset (Word w)) (c : RAMCost w k) : + (⟨time, addresses⟩ : RAMCost w k) + c = ⟨time + c.time, addresses ∪ c.addresses⟩ := rfl -/-- Memory footprint in words: each accessed address is counted once. -/ -def space (c : RAMCost w) : Nat := c.addresses.card +/-- Distinct accessed memory cells, in words. -/ +def space (c : RAMCost w k) : Nat := c.addresses.card -/-- Accessed words outside the designated input region. -/ -def auxiliarySpace (c : RAMCost w) (inputRegion : Finset (Word w)) : Nat := +/-- Accessed memory outside the designated input region. -/ +def auxiliarySpace (c : RAMCost w k) (inputRegion : Finset (Word w)) : Nat := (c.addresses \ inputRegion).card -/-- Words in the footprint or the designated input region, including unread input cells. -/ -def totalSpace (c : RAMCost w) (inputRegion : Finset (Word w)) : Nat := +/-- All words in the footprint or input region, including unread input cells. -/ +def totalSpace (c : RAMCost w k) (inputRegion : Finset (Word w)) : Nat := (c.addresses ∪ inputRegion).card end RAMCost -/-- The unit-time model augmented with the set of addresses accessed by each query. -/ -@[simps] -def timeAndSpaceCost : ModelM (WordRAM w) (StateM (Memory w)) (RAMCost w) where - evalQuery := natCost.evalQuery - cost - | .load addr => ⟨1, {addr}⟩ - | .store addr _ => ⟨1, {addr}⟩ - | .binop _ _ _ => ⟨1, ∅⟩ - | .bnot _ => ⟨1, ∅⟩ - | .cmp _ _ _ => ⟨1, ∅⟩ - -/-- Tracking the memory footprint does not change a program's evaluation or final memory. -/ -@[simp] -theorem evalM_timeAndSpaceCost (P : Prog (WordRAM w) α) : - P.evalM timeAndSpaceCost = P.evalM natCost := rfl +/-- Interpreter fuel is separate from the machine state and its resource cost. -/ +@[ext] +structure ExecutionState (w k : Nat) where + /-- The physical memory, registers, and comparison flags. -/ + ram : RAMState w k + /-- Remaining interpreter steps, excluded from RAM resource costs. -/ + fuel : Nat + +/-- Exhaustion returns `none`, never a successful partial execution. -/ +abbrev ExecutionM (w k : Nat) := StateT (ExecutionState w k) Option + +/-- Sequence fuelled actions, threading both the RAM state and the remaining budget. -/ +@[simp] theorem run_bind_execution + (action : AddWriterT (RAMCost w k) (ExecutionM w k) α) + (next : α → AddWriterT (RAMCost w k) (ExecutionM w k) β) (s : ExecutionState w k) : + (action >>= next).run s = (do + let (a, t) ← action.run s + let (b, u) ← (next a.ret).run t + pure (⟨b.ret, a.tell + b.tell⟩, u)) := rfl + +/-- Repeat while the designated machine flag is true. Only instructions in the body can +update the flag. The test is free control flow, and each test consumes interpreter fuel. -/ +def whileLoop (op : CmpOp) (body : Prog (WordRAM w k) Unit) : Prog (WordRAM w k) Unit := + Cslib.FreeM.lift (.whileCode op (instructions body)) + +/-- Recompute a charged register comparison before each iteration and on exit. -/ +def whileCompare (op : CmpOp) (x y : Register k) (body : Prog (WordRAM w k) Unit) : + Prog (WordRAM w k) Unit := do + cmp (w := w) op x y + whileLoop op (do body; cmp (w := w) op x y) + +/-- One interpreter step, including pending code. -/ +structure Step (w k : Nat) where + /-- Charged primitive cost; branch and loop selection have zero cost. -/ + cost : RAMCost w k + /-- Physical machine state. -/ + ram : RAMState w k + /-- Remaining code, inaccessible to the machine. -/ + code : List (WordRAM w k Unit) + +/-- Primitive instructions execute directly; structured control schedules its selected code. -/ +def step (q : WordRAM w k Unit) (rest : List (WordRAM w k Unit)) + (s : RAMState w k) : Step w k := + match q with + | .nop => ⟨⟨1, ∅⟩, s, rest⟩ + | .set dst value => ⟨⟨1, ∅⟩, s.writeRegister dst value, rest⟩ + | .copy dst src => ⟨⟨1, ∅⟩, s.writeRegister dst (s.Registers src), rest⟩ + | .load dst addr => + ⟨⟨1, {s.Registers addr}⟩, s.writeRegister dst (s.Memory (s.Registers addr)), rest⟩ + | .store addr src => + ⟨⟨1, {s.Registers addr}⟩, + {s with Memory := Function.update s.Memory (s.Registers addr) (s.Registers src)}, rest⟩ + | .binop op dst x y => + ⟨⟨1, ∅⟩, s.writeRegister dst (op.eval (s.Registers x) (s.Registers y)), rest⟩ + | .bnot dst src => ⟨⟨1, ∅⟩, s.writeRegister dst (~~~s.Registers src), rest⟩ + | .cmp op x y => ⟨⟨1, ∅⟩, s.writeFlag op (op.eval (s.Registers x) (s.Registers y)), rest⟩ + | .clearFlag op => ⟨⟨1, ∅⟩, s.writeFlag op false, rest⟩ + | .branchCode op yes no => ⟨0, s, (if s.Flags op then yes else no) ++ rest⟩ + | .whileCode op body => ⟨0, s, if s.Flags op then body ++ q :: rest else rest⟩ + +/-- Execute pending code with one shared budget. Even an empty body consumes fuel on each test. -/ +def runCode : Nat → List (WordRAM w k Unit) → RAMState w k → + Option (AddWriter (RAMCost w k) Unit × ExecutionState w k) + | fuel, [], s => some (⟨(), 0⟩, ⟨s, fuel⟩) + | 0, _ :: _, _ => none + | fuel + 1, q :: rest, s => do + let next := step q rest s + let (result, final) ← runCode fuel next.code next.ram + pure (⟨(), next.cost + result.tell⟩, final) + +/-- Interpret a block with shared fuel and exact joint resource costs. -/ +def runBlock (code : List (WordRAM w k Unit)) : + AddWriterT (RAMCost w k) (ExecutionM w k) Unit := + AddWriterT.mk fun s => runCode s.fuel code s.ram + +/-- Interpret all WordRAM instructions through the existing joint model interface. -/ +def timeAndSpaceCost : ModelStateM (WordRAM w k) (ExecutionM w k) (RAMCost w k) where + runQuery q := (result_type q).symm ▸ runBlock [result_type q ▸ q] + +theorem timeAndSpaceCost_runQuery (q : WordRAM w k Unit) : + timeAndSpaceCost.runQuery q = runBlock [q] := rfl + +/-- Execute a program containing machine-controlled loops. -/ +def execute (fuel : Nat) (p : Prog (WordRAM w k) α) (s : RAMState w k) : + Option (AddWriter (RAMCost w k) α × ExecutionState w k) := + (p.runStateM timeAndSpaceCost).run ⟨s, fuel⟩ + +@[simp, grind =] theorem runCode_nil (fuel : Nat) (s : RAMState w k) : + runCode fuel [] s = some (⟨(), 0⟩, ⟨s, fuel⟩) := by + cases fuel <;> rfl + +@[simp, grind =] theorem runCode_zero_cons (q : WordRAM w k Unit) + (rest : List (WordRAM w k Unit)) (s : RAMState w k) : runCode 0 (q :: rest) s = none := rfl + +@[simp, grind =] theorem execute_pure (fuel : Nat) (a : α) (s : RAMState w k) : + execute fuel (pure a) s = some (⟨a, 0⟩, ⟨s, fuel⟩) := rfl + +/-- Appending code preserves the next physical step. -/ +@[simp] theorem step_append (q : WordRAM w k Unit) (rest tail : List (WordRAM w k Unit)) + (s : RAMState w k) : + step q (rest ++ tail) s = {step q rest s with code := (step q rest s).code ++ tail} := by + cases q with + | whileCode => simp only [step]; split <;> simp [List.append_assoc] + | _ => simp [step, List.append_assoc] + +private theorem unit_ret (a : AddWriter (RAMCost w k) Unit) : a.ret = () := + Subsingleton.elim _ _ + +@[simp] private theorem unit_result (a : AddWriter (RAMCost w k) Unit) : + (⟨(), a.tell⟩ : AddWriter (RAMCost w k) Unit) = a := by + cases a with | mk ret tell => cases ret; rfl + +/-- Executing concatenated code shares the budget and adds exactly the two execution costs. -/ +theorem runCode_append (fuel : Nat) (code tail : List (WordRAM w k Unit)) (s : RAMState w k) : + runCode fuel (code ++ tail) s = (do + let (a, t) ← runCode fuel code s + let (b, u) ← runCode t.fuel tail t.ram + pure (⟨(), a.tell + b.tell⟩, u)) := by + induction fuel generalizing code s with + | zero => + cases code <;> simp [runCode] + | succ fuel ih => + cases code with + | nil => simp + | cons q code => + simp only [List.cons_append, runCode, step_append, ih, bind_assoc] + congr 1 + funext result + obtain ⟨a, t⟩ := result + simp [add_assoc] + +@[simp] theorem runBlock_nil : runBlock ([] : List (WordRAM w k Unit)) = pure () := by + funext s + exact runCode_nil s.fuel s.ram + +@[simp] theorem runBlock_cons (q : WordRAM w k Unit) (rest : List (WordRAM w k Unit)) : + runBlock (q :: rest) = (timeAndSpaceCost.runQuery q >>= fun _ => runBlock rest) := by + apply AddWriterT.ext + funext s + simpa only [timeAndSpaceCost_runQuery, run_bind_execution, runBlock, AddWriterT.run_mk, + unit_ret, List.singleton_append] using + runCode_append s.fuel [q] rest s.ram + +@[simp] theorem runBlock_instructions (p : Prog (WordRAM w k) Unit) : + runBlock (instructions p) = p.runStateM timeAndSpaceCost := by + induction p with + | pure a => cases a; simp + | liftBind q cont ih => + cases q <;> simp [instructions, Prog.runStateM, Cslib.FreeM.liftM, ih] + +/-- Additional fuel preserves a completed code execution, including its exact RAM cost. -/ +theorem runCode_add_fuel (fuel extra : Nat) (code : List (WordRAM w k Unit)) (s : RAMState w k) + (result : AddWriter (RAMCost w k) Unit) (final : ExecutionState w k) + (h : runCode fuel code s = some (result, final)) : + runCode (fuel + extra) code s = some (result, { final with fuel := final.fuel + extra }) := by + induction fuel generalizing code s result final with + | zero => + cases code with + | nil => cases h; simp + | cons => simp at h + | succ fuel ih => + cases code with + | nil => + simp only [runCode_nil, Option.some.injEq, Prod.mk.injEq] at h + rcases h with ⟨rfl, rfl⟩ + simp + | cons q code => + simp only [Nat.succ_add, runCode] at h ⊢ + cases hr : runCode fuel (step q code s).code (step q code s).ram with + | none => simp [hr] at h + | some pair => + obtain ⟨a, t⟩ := pair + simp only [hr, Option.bind_eq_bind, Option.bind_some, Option.pure_def, + Option.some.injEq, Prod.mk.injEq] at h + obtain ⟨rfl, rfl⟩ := h + rw [ih _ _ _ _ hr] + rfl + +/-- Once a loop-containing program completes, extra fuel cannot change its outcome or cost. -/ +theorem execute_add_fuel (fuel extra : Nat) (p : Prog (WordRAM w k) Unit) (s : RAMState w k) + (result : AddWriter (RAMCost w k) Unit) (final : ExecutionState w k) + (h : execute fuel p s = some (result, final)) : + execute (fuel + extra) p s = some (result, { final with fuel := final.fuel + extra }) := by + simp only [execute, ← runBlock_instructions, runBlock, AddWriterT.run_mk] at h ⊢ + exact runCode_add_fuel fuel extra _ s result final h + +/-- A completed block execution, with its exact cost and final RAM state. The witness is +interpreter fuel, not data available to the program. -/ +def Completes (code : List (WordRAM w k Unit)) (s : RAMState w k) + (cost : RAMCost w k) (final : RAMState w k) : Prop := + ∃ fuel, runCode fuel code s = some (⟨(), cost⟩, ⟨final, 0⟩) + +@[simp] theorem completes_nil (s : RAMState w k) : Completes [] s 0 s := ⟨0, rfl⟩ + +@[simp, grind ←] theorem completes_nop (s : RAMState w k) : + Completes [.nop] s ⟨1, ∅⟩ s := ⟨1, rfl⟩ + +theorem Completes.step {q : WordRAM w k Unit} {rest : List (WordRAM w k Unit)} + {s t : RAMState w k} {cost : RAMCost w k} + (h : Completes (step q rest s).code (step q rest s).ram cost t) : + Completes (q :: rest) s ((step q rest s).cost + cost) t := by + obtain ⟨fuel, h⟩ := h + exact ⟨fuel + 1, by simp only [runCode, h]; rfl⟩ + +theorem Completes.append {code tail : List (WordRAM w k Unit)} {s t u : RAMState w k} + {a b : RAMCost w k} (h : Completes code s a t) (ht : Completes tail t b u) : + Completes (code ++ tail) s (a + b) u := by + obtain ⟨fuel, h⟩ := h + obtain ⟨extra, ht⟩ := ht + refine ⟨fuel + extra, ?_⟩ + rw [runCode_append, runCode_add_fuel fuel extra _ _ _ _ h] + simp [ht] +/-- Any completed execution agrees with the cost and RAM state of a completion witness. -/ +theorem Completes.unique {code : List (WordRAM w k Unit)} {s t : RAMState w k} + {cost : RAMCost w k} (h : Completes code s cost t) {fuel : Nat} + {result : AddWriter (RAMCost w k) Unit} {final : ExecutionState w k} + (hr : runCode fuel code s = some (result, final)) : result.tell = cost ∧ final.ram = t := by + obtain ⟨used, h⟩ := h + have h₁ := runCode_add_fuel used fuel code s _ _ h + have h₂ := runCode_add_fuel fuel used code s _ _ hr + rw [Nat.add_comm fuel used, h₁] at h₂ + simpa using congrArg (fun pair => (pair.fst.tell, pair.snd.ram)) (Option.some.inj h₂).symm + +@[simp] theorem instructions_bind (p : Prog (WordRAM w k) Unit) + (next : Unit → Prog (WordRAM w k) Unit) : + instructions (p >>= next) = instructions p ++ instructions (next ()) := by + induction p with + | pure a => cases a; rfl + | liftBind q cont ih => cases q <;> simp [instructions, ih] + +/-- At the execution boundary, compilation and `ModelStateM.runStateM` coincide. -/ +theorem execute_eq_runCode (fuel : Nat) (p : Prog (WordRAM w k) Unit) (s : RAMState w k) : + execute fuel p s = runCode fuel (instructions p) s := by + simp [execute, ← runBlock_instructions, runBlock] + +@[simp] theorem instructions_lift (q : WordRAM w k Unit) : + instructions (Cslib.FreeM.lift q) = [q] := rfl + +/-- A no-op uses one time unit and one fuel unit, and preserves the machine state. -/ +@[simp, grind =] theorem execute_nop_succ (fuel : Nat) (s : RAMState w k) : + execute (fuel + 1) (Cslib.FreeM.lift (.nop : WordRAM w k Unit)) s = + some (⟨(), ⟨1, ∅⟩⟩, ⟨s, fuel⟩) := by + simp [execute_eq_runCode, runCode, step] + +@[simp, grind =] theorem execute_nop_zero (s : RAMState w k) : + execute 0 (Cslib.FreeM.lift (.nop : WordRAM w k Unit)) s = none := rfl + +theorem completes_branch {op : CmpOp} {yes no : Prog (WordRAM w k) Unit} + {s t : RAMState w k} {cost : RAMCost w k} + (h : Completes (instructions (if s.Flags op then yes else no)) s cost t) : + Completes (instructions (branch op yes no)) s cost t := by + have hs : Completes (step (.branchCode op (instructions yes) (instructions no)) [] s).code + (step (.branchCode op (instructions yes) (instructions no)) [] s).ram cost t := by + simpa [step, apply_ite] using h + simpa [branch, instructions, step] using hs.step + +@[simp] theorem completes_while_false (op : CmpOp) (body : Prog (WordRAM w k) Unit) + (s : RAMState w k) (h : s.Flags op = false) : + Completes (instructions (whileLoop op body)) s 0 s := + ⟨1, by simp [whileLoop, runCode, step, h]⟩ + +/-- A loop iteration composes the body's exact execution with the remaining iterations. -/ +theorem completes_while_true (op : CmpOp) (body : Prog (WordRAM w k) Unit) + {s t u : RAMState w k} {a b : RAMCost w k} (h : s.Flags op = true) + (hb : Completes (instructions body) s a t) + (hr : Completes (instructions (whileLoop op body)) t b u) : + Completes (instructions (whileLoop op body)) s (a + b) u := by + have joined := hb.append hr + have hs : Completes (step (.whileCode op (instructions body)) [] s).code + (step (.whileCode op (instructions body)) [] s).ram (a + b) u := by + simpa [step, whileLoop, h] using joined + simpa [step, whileLoop] using hs.step + +/-- A body that clears its loop flag is the final iteration; exiting adds no cost. -/ +theorem Completes.while_stop {op : CmpOp} {body : Prog (WordRAM w k) Unit} + {s t : RAMState w k} {cost : RAMCost w k} + (hb : Completes (instructions body) s cost t) + (hs : s.Flags op = true) (ht : t.Flags op = false) : + Completes (instructions (whileLoop op body)) s cost t := by + simpa only [add_zero] using + completes_while_true op body hs hb (completes_while_false op body t ht) + +/-- Completion supplies sufficient interpreter fuel. -/ +theorem Completes.execute {p : Prog (WordRAM w k) Unit} {s t : RAMState w k} + {cost : RAMCost w k} (h : Completes (instructions p) s cost t) : + ∃ fuel, execute fuel p s = some (⟨(), cost⟩, ⟨t, 0⟩) := by + simpa only [execute_eq_runCode, Completes] using h + +/-- Branch selection consumes fuel, but no primitive-operation time. -/ +@[simp, grind =] theorem execute_branch_succ (fuel : Nat) (op : CmpOp) + (yes no : Prog (WordRAM w k) Unit) (s : RAMState w k) : + execute (fuel + 1) (branch op yes no) s = + if s.Flags op then execute fuel yes s else execute fuel no s := by + simp only [execute_eq_runCode, branch, instructions, runCode, step] + split <;> simp + +@[simp, grind =] theorem execute_while_zero (op : CmpOp) (body : Prog (WordRAM w k) Unit) + (s : RAMState w k) : execute 0 (whileLoop op body) s = none := by + simp [execute_eq_runCode, whileLoop] + +/-- A loop test reads its flag without modifying registers, memory, or RAM cost. -/ +theorem execute_while_succ (fuel : Nat) (op : CmpOp) (body : Prog (WordRAM w k) Unit) + (s : RAMState w k) : + execute (fuel + 1) (whileLoop op body) s = + if s.Flags op then execute fuel (do body; whileLoop op body) s + else some (⟨(), 0⟩, ⟨s, fuel⟩) := by + simp only [execute_eq_runCode, whileLoop, instructions_lift, instructions_bind, runCode, step] + split <;> simp + +@[simp] theorem execute_while_false (fuel : Nat) (op : CmpOp) + (body : Prog (WordRAM w k) Unit) (s : RAMState w k) (h : s.Flags op = false) : + execute (fuel + 1) (whileLoop op body) s = some (⟨(), 0⟩, ⟨s, fuel⟩) := by + simp [execute_while_succ, h] + +@[simp] theorem execute_while_true (fuel : Nat) (op : CmpOp) + (body : Prog (WordRAM w k) Unit) (s : RAMState w k) (h : s.Flags op = true) : + execute (fuel + 1) (whileLoop op body) s = + execute fuel (do body; whileLoop op body) s := by + simp [execute_while_succ, h] + +/-- Host-language return values are fixed by syntax; queries return only `Unit`. -/ +def returnValue : Prog (WordRAM w k) α → α + | .pure a => a + | .liftBind q next => returnValue (next ((result_type q).symm ▸ ())) + +@[simp] theorem returnValue_unit (p : Prog (WordRAM w k) Unit) : returnValue p = () := + Subsingleton.elim _ _ + +/-- Replacing the return value by its syntactically fixed value preserves the program. -/ +theorem eq_bind_return (p : Prog (WordRAM w k) α) : + p = (p >>= fun _ => pure (returnValue p)) := by + induction p with + | pure a => rfl + | liftBind q next ih => + cases q <;> apply congrArg (Cslib.FreeM.liftBind _) + all_goals + funext u + cases u + exact ih () + +/-- Completed execution cannot reveal a register, flag, or memory word through a Lean result. -/ +theorem execute_ret (p : Prog (WordRAM w k) α) (s : RAMState w k) (fuel : Nat) + (result : AddWriter (RAMCost w k) α) (final : ExecutionState w k) + (h : execute fuel p s = some (result, final)) : result.ret = returnValue p := by + have hr := h + rw [eq_bind_return p] at hr + simp only [execute] at h hr + simp only [Prog.runStateM_bind, run_bind_execution, h, Option.bind_eq_bind, + Option.bind_some, Prog.runStateM_pure, AddWriterT.run_pure] at hr + have hout := congrArg (fun r => r.map (fun pair => pair.fst.ret)) hr + simpa [StateT.pure, Pure.pure, AddWriter.pure] using hout.symm + +/-- Two successful runs have the same Lean return value, regardless of their machine inputs. -/ +theorem execute_ret_independent (p : Prog (WordRAM w k) α) (s t : RAMState w k) + {fuel fuel' : Nat} {result result' : AddWriter (RAMCost w k) α} + {final final' : ExecutionState w k} + (h : execute fuel p s = some (result, final)) + (h' : execute fuel' p t = some (result', final')) : result.ret = result'.ret := + (execute_ret p s fuel result final h).trans (execute_ret p t fuel' result' final' h').symm end WordRAM diff --git a/Algolean/Models/WordRAMSyntax.lean b/Algolean/Models/WordRAMSyntax.lean new file mode 100644 index 0000000..325dd45 --- /dev/null +++ b/Algolean/Models/WordRAMSyntax.lean @@ -0,0 +1,314 @@ +/- +Copyright (c) 2026 Shreyas Srinivas. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Shreyas Srinivas +-/ + +module + +public import Algolean.Models.WordRAM + +/-! +# Notation for Word-RAM programs + +Use `open scoped WordRAM Prog` to enable the notation in this file. +Start a program with `do [WordRAM w k]` to specify its word width and register count +once for the whole block. + +## Instructions + +The names below refer to registers. In `mem[addr]`, the address is held in register `addr`. + +- `dst ←ᵣ x + y`: add two registers and store the result in `dst`. + Subtraction and bitwise operations use the same form. +- `dst ←ᵣ ~~~src`: flip every bit of `src` and store the result in `dst`. +- `dst ←ᵣ src`: copy a register. +- `dst ←ᵣ imm[value]`: set a register to a constant. +- `dst ←ᵣ mem[addr]`: load a memory cell into a register. +- `mem[addr] ←ᵣ src`: store a register in a memory cell. +- `reset op`: set the selected comparison flag to false. +- `nop`: leave the machine state unchanged and charge one time unit. + +Write each word operation as a separate instruction. Parenthesize compound Lean +expressions used as register arguments. Assignment has precedence 10. + +## Branches and loops + +- `ifₚ condition then ... else ...`: run the selected body. + Use `flag op` to check an existing flag, or `test op x y` to compare two registers. +- `whileₚ op do ...`: repeat while the selected flag is true. + The body must update the flag if the loop is to stop. +- `whileₚ op x y do ...`: compare registers before each iteration and stop when + the comparison is false. +- `repeat [n]`: run an indented body `n` times. + +Branch and loop bodies return `Unit`. Comparisons cost one time unit; checking an +existing flag costs no time. The notation expands to the definitions in `WordRAM.lean` +and adds no operations of its own. + +The examples swap two memory cells and sum the even words in an input array. +-/ + +@[expose] public section + +namespace Algolean.Algorithms.Prog + +section ControlFlowNotation + +/-- Model-controlled `if` inside a `do` block; enable with `open scoped Prog`. -/ +scoped syntax "ifₚ " term " then " doSeq " else " doSeq : doElem + +scoped macro_rules + | `(doElem| ifₚ $condition then $yes else $no) => + `(doElem| Prog.ifThenElse $condition (do $yes) (do $no)) + +/-- Repeat an indented `Unit` body a fixed number of times; enable with `open scoped Prog`. -/ +scoped macro "repeat " "[" fuel:term "]" ppLine body:doSeq : doElem => + `(doElem| Prog.repeatLoop (fun yes _ => yes) (do $body) $fuel) + +end ControlFlowNotation + +end Algolean.Algorithms.Prog + +namespace Algolean.Algorithms.WordRAM + +/-- Compare the contents of two registers for equality. -/ +scoped infix:50 " =ᵣ " => WordRAM.test CmpOp.eq + +/-- Compare the contents of two registers as unsigned words. -/ +scoped infix:50 " <ᵣ " => WordRAM.test CmpOp.ult + +/-- Indented looping syntax over an existing machine comparison flag. -/ +scoped macro "whileₚ " op:term:max " do " body:doSeq : doElem => + `(doElem| WordRAM.whileLoop $op (do $body)) + +/-- Indented looping syntax that performs a fresh register comparison each time. -/ +scoped macro "whileₚ " op:term:max x:term:max y:term:max " do " body:doSeq : doElem => + `(doElem| WordRAM.whileCompare $op $x $y (do $body)) + + +/-- Add two source registers into the destination. -/ +scoped notation:10 (name := ramAdd) dst:max " ←ᵣ " x:max " + " y:max => + WordRAM.binop BinOp.add dst x y + +/-- Subtract the second source register from the first into the destination. -/ +scoped notation:10 (name := ramSub) dst:max " ←ᵣ " x:max " - " y:max => + WordRAM.binop BinOp.sub dst x y + +/-- Bitwise AND of two source registers into the destination. -/ +scoped notation:10 (name := ramAnd) dst:max " ←ᵣ " x:max " &&& " y:max => + WordRAM.binop BinOp.band dst x y + +/-- Bitwise OR of two source registers into the destination. -/ +scoped notation:10 (name := ramOr) dst:max " ←ᵣ " x:max " ||| " y:max => + WordRAM.binop BinOp.bor dst x y + +/-- Bitwise XOR of two source registers into the destination. -/ +scoped notation:10 (name := ramXor) dst:max " ←ᵣ " x:max " ^^^ " y:max => + WordRAM.binop BinOp.bxor dst x y + +/-- Shift left by the word held in the second source register. -/ +scoped notation:10 (name := ramShl) dst:max " ←ᵣ " x:max " <<< " y:max => + WordRAM.binop BinOp.shl dst x y + +/-- Shift right by the word held in the second source register. -/ +scoped notation:10 (name := ramShr) dst:max " ←ᵣ " x:max " >>> " y:max => + WordRAM.binop BinOp.shr dst x y + +/-- Complement the source register into the destination. -/ +scoped notation:10 (name := ramNot) dst:max " ←ᵣ " "~~~" src:max => + WordRAM.bnot dst src + +/-- Copy the source register into the destination. -/ +scoped notation:10 (name := ramCopy) dst:max " ←ᵣ " src:max => + WordRAM.copy dst src + +/-- Set the destination register to an immediate word. -/ +scoped notation:10 (name := ramSet) dst:max " ←ᵣ " "imm[" value "]" => + WordRAM.set dst value + +/-- Load memory at the address held in a register into the destination. -/ +scoped notation:10 (name := ramLoad) dst:max " ←ᵣ " "mem[" addr "]" => + WordRAM.load dst addr + +/-- Store a source register at the address held in another register. -/ +scoped notation:10 (name := ramStore) "mem[" addr "]" " ←ᵣ " src:max => + WordRAM.store addr src + +/-- Do nothing for one time unit. -/ +scoped notation (name := ramNop) "nop" => WordRAM.nop + +/-- Reset the selected comparison flag to false, leaving other flags unchanged. -/ +scoped notation (name := ramReset) "reset " op:max => WordRAM.clearFlag op + +/-- Fix word width and register count for all instruction notation inside a `do` block. -/ +scoped syntax (name := ramBlock) "do " "[" term "]" doSeq : term + +open Lean in +private meta partial def annotateInstructions (queryType : Term) + (stx : Syntax) : MacroM Syntax := do + -- A nested quotation supplies its own width and register count. + if stx.isOfKind ``ramBlock then + return stx + let stx ← match stx with + | .node info kind args => do + let args ← args.mapM (annotateInstructions queryType) + pure (.node info kind args) + | other => pure other + if [``ramAdd, ``ramSub, ``ramAnd, ``ramOr, ``ramXor, ``ramShl, ``ramShr, + ``ramNop, ``ramNot, ``ramCopy, ``ramSet, ``ramLoad, ``ramStore, + ``ramReset].contains stx.getKind then + let instruction : Term := ⟨stx⟩ + return ← `(($instruction : $queryType Unit)) + return stx + +macro_rules (kind := ramBlock) + | `(do [$queryType:term] $body:doSeq) => do + let body : Lean.TSyntax ``Lean.Parser.Term.doSeq := + ⟨← annotateInstructions queryType body⟩ + `((do $body : Prog $queryType Unit)) + +section Examples + +open scoped WordRAM + +example (dst x y : Register k) : + (dst ←ᵣ x + y : WordRAM w k Unit) = .binop .add dst x y := rfl + +example (dst src : Register k) : + (dst ←ᵣ ~~~src : WordRAM w k Unit) = .bnot dst src := rfl + +example (dst addr : Register k) : + (dst ←ᵣ mem[addr] : WordRAM w k Unit) = .load dst addr := rfl + +section SillySwapExample + +private abbrev swapAddr : Register 3 := 0 + +private abbrev swapA : Register 3 := 1 + +private abbrev swapB : Register 3 := 2 + +/-- Swap memory cells 0 and 1 using one address register and two value registers. +The three arithmetic operations need no additional temporary register. +For the record this example need not be so complicated. We can swap +with a single register. But then I wouldn't get to test drive the notation +for arithmetic for example -/ +private def arithmeticSwap (w : Nat) : Prog (WordRAM w 3) Unit := do [WordRAM w 3] + swapAddr ←ᵣ imm[0] + swapA ←ᵣ mem[swapAddr] + swapAddr ←ᵣ imm[1] + swapB ←ᵣ mem[swapAddr] + swapA ←ᵣ swapA + swapB + swapB ←ᵣ swapA - swapB + swapA ←ᵣ swapA - swapB + mem[swapAddr] ←ᵣ swapB + swapAddr ←ᵣ imm[0] + mem[swapAddr] ←ᵣ swapA + +/-- Input cells contain 250 and 17; all other memory cells contain 99. -/ +private def swapInputMemory : Memory 8 := + fun addr => if addr = 0 then 250 else if addr = 1 then 17 else 99 + +/-- Start with the input memory, zeroed registers, and cleared flags. -/ +private def swapInitialState : RAMState 8 3 where + Memory := swapInputMemory + Registers := fun _ => 0 + +/-- The two input cells are swapped, with the results also remaining in the value registers. -/ +private def swapFinalState : RAMState 8 3 where + Memory := fun addr => if addr = 0 then 17 else if addr = 1 then 250 else 99 + Registers := fun r => if r = swapAddr then 0 else if r = swapA then 17 else 250 + +-- The addition wraps around: 250 + 17 = 11 in an eight-bit word. +example : (execute 10 (arithmeticSwap 8) swapInitialState).map + (fun result => result.snd.ram) = some swapFinalState := by + apply congrArg some + apply (RAMState.mk.injEq ..).mpr + refine ⟨?_, ?_, rfl⟩ + · funext addr + by_cases h0 : addr = 0#8 <;> by_cases h1 : addr = 1#8 <;> + simp [step, RAMState.writeRegister, BinOp.eval, swapInitialState, + swapAddr, swapA, swapB, swapInputMemory, h0, h1] + · funext r + fin_cases r <;> decide + +-- Ten primitive operations, with no memory probes outside the two input cells. +example : (execute 10 (arithmeticSwap 8) swapInitialState).map + (fun result => (result.fst.tell.time, result.fst.tell.auxiliarySpace {0, 1})) = + some (10, 0) := by decide + +end SillySwapExample + +section EvenSumExample + +open scoped Prog + +private abbrev evenSum : Register 7 := 0 + +private abbrev inputIndex : Register 7 := 1 + +private abbrev inputSize : Register 7 := 2 + +private abbrev inputValue : Register 7 := 3 + +private abbrev lowBit : Register 7 := 4 + +private abbrev zero : Register 7 := 5 + +private abbrev one : Register 7 := 6 + +/-- Cell 0 contains `n`; sum the even words in cells 1 through `n`, modulo `2^w`. +Incrementing the index before the load supports `n = 2^w - 1` without wrapping the index. +At width 8, the header and input cells are bytes. -/ +private def sumEvenWords (w : Nat) : Prog (WordRAM w 7) Unit := do [WordRAM w 7] + evenSum ←ᵣ imm[0] + inputIndex ←ᵣ imm[0] + inputSize ←ᵣ mem[inputIndex] + zero ←ᵣ imm[0] + one ←ᵣ imm[1] + whileₚ .ult inputIndex inputSize do + inputIndex ←ᵣ inputIndex + one + inputValue ←ᵣ mem[inputIndex] + lowBit ←ᵣ inputValue &&& one + ifₚ test .eq lowBit zero then + evenSum ←ᵣ evenSum + inputValue + else + nop + +/-- Five input bytes: the even ones sum to `250 + 8 + 4 = 262`, or 6 modulo 256. -/ +private def evenSumInputMemory : Memory 8 := + fun addr => #[5, 250, 3, 8, 7, 4][addr.toNat]?.getD 99 + +private def evenSumInitialState : RAMState 8 7 where + Memory := evenSumInputMemory + Registers := fun _ => 0 + +example : (execute 100 (sumEvenWords 8) evenSumInitialState).map + (fun result => result.snd.ram.Registers evenSum) = some 6 := by decide + +-- The header and input cells are the entire memory footprint. +example : (execute 100 (sumEvenWords 8) evenSumInitialState).map + (fun result => (result.fst.tell.time, result.fst.tell.auxiliarySpace {0, 1, 2, 3, 4, 5})) = + some (36, 0) := by decide + +-- An empty input clears a stale result and does not read any payload cells. +example : + let s : RAMState 8 7 := + { Memory := fun addr => if addr = 0 then 0 else 42, Registers := fun _ => 255 } + (execute 7 (sumEvenWords 8) s).map + (fun result => (result.snd.ram.Registers evenSum, result.fst.tell.addresses)) = + some (0, {0}) := by decide + +-- The header plus three elements fills the entire two-bit address space. +example : + let s : RAMState 2 7 := + { Memory := fun addr => #[3, 2, 1, 2][addr.toNat]?.getD 0, Registers := fun _ => 0 } + (execute 40 (sumEvenWords 2) s).map + (fun result => result.snd.ram.Registers evenSum) = some 0 := by decide + +end EvenSumExample + +end Examples + +end Algolean.Algorithms.WordRAM diff --git a/Algolean/Problems/Basic.lean b/Algolean/Problems/Basic.lean new file mode 100644 index 0000000..b848547 --- /dev/null +++ b/Algolean/Problems/Basic.lean @@ -0,0 +1,89 @@ +/- +Copyright (c) 2026 Shreyas Srinivas. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Shreyas Srinivas +-/ + +module + +public import Mathlib.Logic.Basic + +/-! +# Problems and program guarantees + +`Problem Input Output` specifies which inputs are allowed and which outputs are +correct for each input. An input may have several correct outputs. + +- `Problem.Solves`: a given program terminates on every allowed input state, + and every completed execution produces a correct output. +- `Problem.RunsWithin`: a given program terminates on every allowed input state, + and every completed execution meets the supplied cost bound. +- `Problem.RunsWithin.mono`: a cost guarantee also implies any weaker bound. +- `Problem.restrict`: adds an input condition without changing which outputs + are correct. + +`Solves` and `RunsWithin` take the execution rules and the way inputs are stored +in states as arguments. `Solves` also takes the way outputs are stored. +-/ + +@[expose] public section + +namespace Algolean + +/-- An input/output specification independent of any computational model. -/ +structure Problem (Input : Type u) (Output : Type v) where + /-- Inputs on which an implementation must satisfy the specification. -/ + admissible : Input → Prop + /-- The valid outputs for each admissible input. -/ + spec : Input → Output → Prop + +namespace Problem + +/-- Total correctness of a fixed program, relative to an execution relation and input/output +representations. Every representing initial state must terminate, and every completed execution +must represent a valid output. Inputs outside the representation's domain are not covered. -/ +structure Solves (P : Problem Input Output) (program : Program) + (run : Program → State → Cost → State → Prop) + (repInput : Input → State → Prop) (repOutput : Output → State → Prop) : Prop where + /-- Every represented admissible input has a completed execution. -/ + terminates : ∀ input s, P.admissible input → repInput input s → ∃ cost t, run program s cost t + /-- All completed executions produce a represented answer satisfying the problem. -/ + correct : ∀ input s, P.admissible input → repInput input s → + ∀ cost t, run program s cost t → ∃ output, repOutput output t ∧ P.spec input output + +/-- A terminating resource guarantee for a fixed program. The execution relation determines +what costs mean; the bound may depend on the abstract input. -/ +structure RunsWithin (P : Problem Input Output) (program : Program) + (run : Program → State → Cost → State → Prop) + (repInput : Input → State → Prop) (bound : Input → Cost → Prop) : Prop where + /-- Divergence cannot satisfy a resource guarantee vacuously. -/ + terminates : ∀ input s, P.admissible input → repInput input s → ∃ cost t, run program s cost t + /-- Every completed execution satisfies the resource bound. -/ + bounded : ∀ input s, P.admissible input → repInput input s → + ∀ cost t, run program s cost t → bound input cost + +/-- Weaken a resource guarantee without changing the program or execution model. -/ +theorem RunsWithin.mono {P : Problem Input Output} + {run : Program → State → Cost → State → Prop} {repInput : Input → State → Prop} + {bound bound' : Input → Cost → Prop} + (h : P.RunsWithin program run repInput bound) + (hle : ∀ input cost, bound input cost → bound' input cost) : + P.RunsWithin program run repInput bound' := + ⟨h.terminates, fun input s ha hi cost t hr => hle input cost (h.bounded input s ha hi cost t hr)⟩ + +/-- Restrict a problem to inputs satisfying an additional precondition. -/ +def restrict (P : Problem Input Output) (precondition : Input → Prop) : Problem Input Output where + admissible input := P.admissible input ∧ precondition input + spec := P.spec + +@[simp, grind =] theorem restrict_admissible (P : Problem Input Output) + (precondition : Input → Prop) (input : Input) : + (P.restrict precondition).admissible input ↔ P.admissible input ∧ precondition input := Iff.rfl + +@[simp, grind =] theorem restrict_spec (P : Problem Input Output) + (precondition : Input → Prop) (input : Input) (output : Output) : + (P.restrict precondition).spec input output ↔ P.spec input output := Iff.rfl + +end Problem + +end Algolean diff --git a/Algolean/Problems/Search.lean b/Algolean/Problems/Search.lean new file mode 100644 index 0000000..caf4118 --- /dev/null +++ b/Algolean/Problems/Search.lean @@ -0,0 +1,343 @@ +/- +Copyright (c) 2026 Shreyas Srinivas. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Shreyas Srinivas +-/ + +module + +public import Algolean.Problems.Basic +public import Algolean.Models.WordRAM + +/-! +# Array search problems + +The input is an array and a key. The output is `some i` for a matching index, +or `none` when the key is absent. + +- `search`: accepts any matching index. +- `linearSearch`: requires the first matching index. +- `binarySearch`: requires an array sorted by the supplied relation and accepts + any matching index. +- `RunsWithin`: requires termination and a cost bound for every input state + storing the array and key as specified, including unsorted arrays. + +The `WordRAMLinearSearch` section collects the concrete input layout, representation +predicates, initial-state constructor and its proof, output decoding, and memory footprint. + +The main lemmas describe correct answers: + +- `IsFirstMatch.unique`: two first matches have the same index. +- `linearSearch_spec_search`: a correct first-match answer is a correct search answer. +- `search_none_iff`: a correct answer is `none` exactly when the key is absent. +- `linearSearch_some_iff`: a correct first-match answer is `some i` exactly when + `i` is the first matching index. +-/ + +@[expose] public section + +namespace Algolean.Search + +/-- The data and key supplied to a search problem. -/ +structure Input (α : Type u) where + /-- Array to search. -/ + data : Array α + /-- Value to find. -/ + key : α + +/-- An in-bounds index containing the search key. -/ +def IsMatch (data : Array α) (key : α) (i : Nat) : Prop := + i < data.size ∧ data[i]? = some key + +/-- A matching index with no earlier occurrence of the key. -/ +def IsFirstMatch (data : Array α) (key : α) (i : Nat) : Prop := + i < data.size ∧ data[i]? = some key ∧ ∀ j, j < i → data[j]? ≠ some key + +/-- Nondecreasing array order for the supplied relation, allowing duplicate elements. -/ +def SortedBy (le : α → α → Prop) (data : Array α) : Prop := + ∀ i j, (hi : i < data.size) → (hj : j < data.size) → i ≤ j → le data[i] data[j] + +/-- An arbitrary matching index, or an absence certificate. -/ +def search : Problem (Input α) (Option Nat) where + admissible _ := True + spec input + | none => input.key ∉ input.data + | some i => IsMatch input.data input.key i + +/-- The first matching index, or an absence certificate. -/ +def linearSearch : Problem (Input α) (Option Nat) where + admissible _ := True + spec input + | none => input.key ∉ input.data + | some i => IsFirstMatch input.data input.key i + +/-- Search in a sorted array; any matching index is acceptable. -/ +def binarySearch (le : α → α → Prop) : Problem (Input α) (Option Nat) := + search.restrict (fun input => SortedBy le input.data) + +/-- Resource guarantees for search on all represented arrays, including unsorted arrays. +Correctness can separately use the more restrictive binary-search problem. -/ +abbrev RunsWithin (program : Program) (run : Program → State → Cost → State → Prop) + (repInput : Input α → State → Prop) (bound : Input α → Cost → Prop) : Prop := + search.RunsWithin program run repInput bound + +@[simp] theorem search_admissible (input : Input α) : search.admissible input := trivial + +@[simp] theorem linearSearch_admissible (input : Input α) : + linearSearch.admissible input := trivial + +@[simp, grind =] theorem binarySearch_admissible (le : α → α → Prop) (input : Input α) : + (binarySearch le).admissible input ↔ SortedBy le input.data := by + simp [binarySearch] + +@[simp, grind =] theorem search_spec_none (input : Input α) : + search.spec input none ↔ input.key ∉ input.data := Iff.rfl + +@[simp, grind =] theorem search_spec_some (input : Input α) (i : Nat) : + search.spec input (some i) ↔ IsMatch input.data input.key i := Iff.rfl + +@[simp, grind =] theorem linearSearch_spec_none (input : Input α) : + linearSearch.spec input none ↔ input.key ∉ input.data := Iff.rfl + +@[simp, grind =] theorem linearSearch_spec_some (input : Input α) (i : Nat) : + linearSearch.spec input (some i) ↔ IsFirstMatch input.data input.key i := Iff.rfl + +@[simp, grind =] theorem binarySearch_spec (le : α → α → Prop) (input : Input α) + (output : Option Nat) : + (binarySearch le).spec input output ↔ search.spec input output := Iff.rfl + +/-- First-match search refines ordinary search. -/ +theorem IsFirstMatch.isMatch (h : IsFirstMatch data key i) : IsMatch data key i := + ⟨h.left, h.right.left⟩ + +/-- A successful match is a membership witness, independently of how it was found. -/ +theorem IsMatch.mem (h : IsMatch data key i) : key ∈ data := + Array.mem_iff_getElem?.mpr ⟨i, h.right⟩ + +/-- Two first-match witnesses for the same input must identify the same index. -/ +theorem IsFirstMatch.unique (hi : IsFirstMatch data key i) (hj : IsFirstMatch data key j) : + i = j := by + rcases hi with ⟨_, hi, hbeforeI⟩ + rcases hj with ⟨_, hj, hbeforeJ⟩ + rcases Nat.lt_trichotomy i j with hlt | heq | hgt + · exact (hbeforeJ i hlt hi).elim + · exact heq + · exact (hbeforeI j hgt hj).elim + +/-- Every answer satisfying first-match search also satisfies ordinary search. -/ +theorem linearSearch_spec_search (input : Input α) (output : Option Nat) + (h : linearSearch.spec input output) : search.spec input output := by + cases output with + | none => exact h + | some i => exact IsFirstMatch.isMatch h + +/-- For a correct search answer, `none` is equivalent to absence of the key. -/ +theorem search_none_iff (h : search.spec input output) : + output = none ↔ input.key ∉ input.data := by + cases output with + | none => exact ⟨fun _ => h, fun _ => rfl⟩ + | some i => + constructor + · intro h; cases h + · intro hnot + exact (hnot (IsMatch.mem h)).elim + +/-- A correct first-match answer identifies precisely the unique first matching index. -/ +theorem linearSearch_some_iff (h : linearSearch.spec input output) (i : Nat) : + output = some i ↔ IsFirstMatch input.data input.key i := by + cases output with + | none => + constructor + · intro h; cases h + · intro hfirst + exact (h hfirst.isMatch.mem).elim + | some j => + constructor + · intro heq + cases heq + exact h + · intro hfirst + exact congrArg some (IsFirstMatch.unique h hfirst) + +end Algolean.Search + +namespace Algolean.Algorithms.WordRAM + +section WordRAMLinearSearch + +/-! +## WordRAM linear-search representation + +The abstract problem above accepts any array and key. Its WordRAM representation stores +`input.data.size` in cell `0` and `input.data[i]` in cell `i + 1`. The header and payload +must fit in memory, so `input.data.size < 2 ^ w`. The key register is a parameter of the +representation and initial-state constructor, independent of the algorithm's register choices. + +`RepresentsArray` describes a generic array starting at zero. Applying it to `withSize` +represents the complete header-plus-payload layout. The array and output predicates are +also used by other WordRAM search algorithms. +-/ + +/-- An array occupies cells `0` through `size - 1`. Other cells are unconstrained. -/ +structure RepresentsArray (input : Array (Word w)) (memory : Memory w) : Prop where + /-- Every element has a distinct representable address, including a full address space. -/ + fits : input.size ≤ 2 ^ w + /-- Only input cells have prescribed contents. -/ + read : ∀ i (hi : i < input.size), memory (BitVec.ofNat w i) = input[i] + +attribute [grind →] RepresentsArray.read + +/-- The size in cell zero, followed by the array elements. -/ +def withSize (input : Array (Word w)) : Array (Word w) := + #[BitVec.ofNat w input.size] ++ input + +/-- The input size and elements are in memory; the key is in its register. +Other registers and flags may initially contain any values. -/ +structure RepresentsSizedSearchInput (input : Search.Input (Word w)) (key : Register k) + (s : RAMState w k) : Prop extends RepresentsArray (withSize input.data) s.Memory where + key_eq : s.Registers key = input.key + +/-- Reading an input cell from any representing RAM state returns the corresponding element. -/ +theorem RepresentsArray.read_state {s : RAMState w k} + (h : RepresentsArray input s.Memory) + (i : Nat) (hi : i < input.size) : s.Memory (BitVec.ofNat w i) = input[i] := h.read i hi + +/-- Every input index fits in a machine word. -/ +@[grind →] theorem RepresentsArray.index_lt (h : RepresentsArray input (w := w) memory) + (hi : i < input.size) : i < 2 ^ w := lt_of_lt_of_le hi h.fits + +/-- Converting a valid input index to a word and back preserves it. +Use this lemma with a representation argument; `simp` cannot infer that argument from the LHS. -/ +@[grind →] theorem RepresentsArray.address_toNat (h : RepresentsArray input (w := w) memory) + (hi : i < input.size) : (BitVec.ofNat w i).toNat = i := Nat.mod_eq_of_lt (h.index_lt hi) + +/-- Decode a word known to address an input element, without repeating the range proof. -/ +theorem RepresentsArray.toNat_of_eq (h : RepresentsArray input (w := w) memory) + (hi : i < input.size) {addr : Word w} (ha : addr = BitVec.ofNat w i) : addr.toNat = i := + ha ▸ h.address_toNat hi + +/-- Read an input element through any word known to contain its index. +This is an explicit rewrite helper: `grind` uses `RepresentsArray.read` and congruence instead. -/ +theorem RepresentsArray.read_of_eq (h : RepresentsArray input (w := w) memory) + (hi : i < input.size) {addr : Word w} (ha : addr = BitVec.ofNat w i) : memory addr = input[i] := + ha ▸ h.read i hi + +@[simp] theorem withSize_size (input : Array (Word w)) : + (withSize input).size = input.size + 1 := by + simp [withSize, Nat.add_comm] + +@[simp] theorem withSize_getElem_zero (input : Array (Word w)) : + (withSize input)[0] = BitVec.ofNat w input.size := by simp [withSize] + +@[simp] theorem withSize_getElem_succ (input : Array (Word w)) (i : Nat) (hi : i < input.size) : + (withSize input)[i + 1]' (by simp; lia) = input[i] := by simp [withSize] + +@[simp] theorem withSize_getElem?_succ (input : Array (Word w)) (i : Nat) : + (withSize input)[i + 1]? = input[i]? := by + simp [withSize, Array.getElem?_append] + +variable {input : Search.Input (Word w)} {key : Register k} {s : RAMState w k} + +theorem RepresentsSizedSearchInput.header + (h : RepresentsSizedSearchInput input key s) : + s.Memory (BitVec.ofNat w 0) = BitVec.ofNat w input.data.size := by + simpa using h.read 0 (by simp) + +@[grind →] theorem RepresentsSizedSearchInput.size_lt + (h : RepresentsSizedSearchInput input key s) : input.data.size < 2 ^ w := by + have := h.fits + simpa using this + +theorem RepresentsSizedSearchInput.header_toNat + (h : RepresentsSizedSearchInput input key s) : + (s.Memory (BitVec.ofNat w 0)).toNat = input.data.size := by + simpa [Word, BitVec.toNat_ofNat, Nat.mod_eq_of_lt h.size_lt] using + congrArg BitVec.toNat h.header + +/-- Array layout used by the initial machine state. -/ +def sizedArrayMemory (input : Array (BitVec w)) : Memory w := + fun addr => (withSize input)[addr.toNat]?.getD 0 + +@[grind =] theorem sizedArrayMemory_ofNat (input : Array (Word w)) + (hfits : input.size < 2 ^ w) (i : Nat) (hi : i < (withSize input).size) : + sizedArrayMemory input (BitVec.ofNat w i) = (withSize input)[i] := by + have h : i < 2 ^ w := by simp only [withSize_size] at hi; lia + simp [sizedArrayMemory, BitVec.toNat_ofNat, Nat.mod_eq_of_lt h, Array.getElem?_eq_getElem hi] + +/-- The memory builder stores the size header followed by every array element. -/ +@[simp] theorem sizedArrayMemory_represents (input : Array (Word w)) (hfits : input.size < 2 ^ w) : + RepresentsArray (withSize input) (sizedArrayMemory input) := + ⟨by simpa using hfits, fun i hi => sizedArrayMemory_ofNat input hfits i hi⟩ + +/-- Store the size header, array, and search key in the designated register. +Other registers and flags start at zero; the algorithm initializes its working state. -/ +def linearSearchState (input : Array (Word w)) (target : Word w) + (key : Register k) : RAMState w k := + ⟨sizedArrayMemory input, fun r => if r = key then target else 0, fun _ => false⟩ + +/-- The constructed state represents the input whenever the header and payload fit in memory. -/ +@[simp] theorem linearSearchState_represents (input : Array (Word w)) (target : Word w) + (key : Register k) (hfits : input.size < 2 ^ w) : + RepresentsSizedSearchInput ⟨input, target⟩ key (linearSearchState input target key) := + ⟨sizedArrayMemory_represents input hfits, by simp [linearSearchState]⟩ + +/-- Read the search result outside the program, for specifications and tests. -/ +def searchOutput (index : Register k) (s : RAMState w k) : Option Nat := + if s.Flags .eq then some (s.Registers index).toNat else none + +@[simp] theorem searchOutput_of_found (index : Register k) (s : RAMState w k) + (h : s.Flags .eq = true) : searchOutput index s = some (s.Registers index).toNat := by + simp [searchOutput, h] + +@[simp] theorem searchOutput_of_not_found (index : Register k) (s : RAMState w k) + (h : s.Flags .eq = false) : searchOutput index s = none := by + simp [searchOutput, h] + +/-- The result flag represents absence or a successful address. An absent result places no +constraint on the address register. -/ +def RepresentsSearchOutput (index : Register k) (output : Option Nat) (s : RAMState w k) : Prop := + match output with + | none => s.Flags .eq = false + | some i => s.Flags .eq = true ∧ (s.Registers index).toNat = i + +@[simp, grind =] theorem representsSearchOutput_iff (index : Register k) + (output : Option Nat) (s : RAMState w k) : + RepresentsSearchOutput index output s ↔ searchOutput index s = output := by + cases output <;> simp [RepresentsSearchOutput, searchOutput] + +/-- The external decoder always supplies a represented output. -/ +theorem representsSearchOutput_searchOutput (index : Register k) (s : RAMState w k) : + RepresentsSearchOutput index (searchOutput index s) s := by simp + +/-- Memory cells occupied by the input array. -/ +def inputRegion (input : Array (BitVec w)) : Finset (Word w) := + (Finset.range input.size).image (BitVec.ofNat w) + +@[simp, grind ←] theorem ofNat_mem_inputRegion (input : Array (BitVec w)) + (i : Nat) (hi : i < input.size) : BitVec.ofNat w i ∈ inputRegion input := + Finset.mem_image.mpr ⟨i, Finset.mem_range.mpr hi, rfl⟩ + +/-- A fitting array occupies exactly one distinct cell per element. -/ +theorem inputRegion_card (input : Array (BitVec w)) (hfits : input.size ≤ 2 ^ w) : + (inputRegion input).card = input.size := by + unfold inputRegion + rw [Finset.card_image_of_injOn (by + intro i hi j hj heq + have := congrArg BitVec.toNat heq + grind), Finset.card_range] + +/-- All input cells, including the size header. -/ +def sizedInputRegion (input : Array (Word w)) : Finset (Word w) := inputRegion (withSize input) + +@[simp] theorem zero_mem_sizedInputRegion (input : Array (Word w)) : + BitVec.ofNat w 0 ∈ sizedInputRegion input := by + simp only [sizedInputRegion, inputRegion, Finset.mem_image] + exact ⟨0, by simp, rfl⟩ + +@[simp] theorem sizedInputRegion_card (input : Array (Word w)) (hfits : input.size < 2 ^ w) : + (sizedInputRegion input).card = input.size + 1 := by + simpa [sizedInputRegion] using inputRegion_card (withSize input) (by simpa using hfits) + +end WordRAMLinearSearch + +end Algolean.Algorithms.WordRAM diff --git a/AlgoleanTests.lean b/AlgoleanTests.lean index 8ab44ac..5e09ab6 100644 --- a/AlgoleanTests.lean +++ b/AlgoleanTests.lean @@ -5,8 +5,12 @@ public import AlgoleanTests.FreeMonadWP public import AlgoleanTests.KMPExamples public import AlgoleanTests.ModelM public import AlgoleanTests.ModelMWP +public import AlgoleanTests.ModelStateM +public import AlgoleanTests.ModelStateMWP public import AlgoleanTests.NaivePatternSearchExamples +public import AlgoleanTests.Problems public import AlgoleanTests.ProgExamples public import AlgoleanTests.QueryExamples public import AlgoleanTests.RandomSampleExamples +public import AlgoleanTests.WordRAMBinarySearchExamples public import AlgoleanTests.WordRAMExamples diff --git a/AlgoleanTests/ModelStateM.lean b/AlgoleanTests/ModelStateM.lean new file mode 100644 index 0000000..fcd5a92 --- /dev/null +++ b/AlgoleanTests/ModelStateM.lean @@ -0,0 +1,83 @@ +/- +Copyright (c) 2026 Tanner Duve. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Tanner Duve +-/ + +module + +public import Algolean.ModelStateM + +/-! +# Tests for monadic query models + +This file tests branch-dependent cost accumulation and cost-preserving query reductions. +-/ + +@[expose] public section + +namespace AlgoleanTests.ModelStateM + +open Algolean Algolean.Algorithms Cslib + +/-- Queries for a binary choice and a unit-cost step. -/ +inductive ChoiceQ : Type → Type where + | choose : ChoiceQ Bool + | tick : ChoiceQ Unit + +/-- Interpret `ChoiceQ` in the list monad. -/ +def choiceModel : ModelStateM ChoiceQ List Nat := + ModelStateM.ofCost (fun | .choose => [false, true] | .tick => [()]) (fun _ => 1) + +/-- Perform an additional query on the `true` branch. -/ +def branch : Prog ChoiceQ Unit := do + if ← FreeM.lift .choose then + FreeM.lift .tick + +example : (branch.runStateM choiceModel).run = [⟨(), 1⟩, ⟨(), 2⟩] := rfl + +example : branch.costStateM choiceModel = [1, 2] := rfl + +/-- The cost of a choice can depend on that very choice's result. -/ +def correlatedChoice : ModelStateM ChoiceQ List Nat where + runQuery + | .choose => AddWriterT.mk [⟨false, 3⟩, ⟨true, 7⟩] + | .tick => AddWriterT.mk [⟨(), 1⟩] + +example : (branch.runStateM correlatedChoice).run = [⟨(), 3⟩, ⟨(), 8⟩] := rfl + +example : branch.costStateM correlatedChoice = [3, 8] := rfl + +example : branch.evalStateM correlatedChoice = [(), ()] := rfl + +/-- A unit-cost state increment. -/ +inductive TickQ : Type → Type where + | tick : TickQ Unit + +/-- A state increment of two. -/ +inductive DoubleTickQ : Type → Type where + | tickTwice : DoubleTickQ Unit + +/-- Interpret `TickQ` as a state increment. -/ +def tickModel : ModelStateM TickQ (StateM Nat) Nat := + ModelStateM.ofCost (fun | .tick => modify (· + 1)) (fun _ => 1) + +/-- Interpret `DoubleTickQ` as a state increment of two. -/ +def doubleTickModel : ModelStateM DoubleTickQ (StateM Nat) Nat := + ModelStateM.ofCost (fun | .tickTwice => modify (· + 2)) (fun _ => 2) + +/-- Implement one double increment using two unit increments. -/ +def doubleTickReduction : Reduction DoubleTickQ TickQ where + reduce + | .tickTwice => do + FreeM.lift .tick + FreeM.lift .tick + +example (P : Prog DoubleTickQ α) : + (P.reduceProg doubleTickReduction).runStateM tickModel = P.runStateM doubleTickModel := by + apply Prog.reduceProg_runStateM + intro _ q + cases q + rfl + +end AlgoleanTests.ModelStateM diff --git a/AlgoleanTests/ModelStateMWP.lean b/AlgoleanTests/ModelStateMWP.lean new file mode 100644 index 0000000..776ec56 --- /dev/null +++ b/AlgoleanTests/ModelStateMWP.lean @@ -0,0 +1,109 @@ +/- +Copyright (c) 2026 Tanner Duve. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Tanner Duve +-/ + +module + +public import Algolean.ModelStateM +public import Std.Tactic.Do + +/-! +# Weakest-precondition reasoning for `ModelStateM` + +This file exercises weakest-precondition reasoning and `mvcgen` for a `StateM` query model. +-/ + +@[expose] public section + +set_option mvcgen.warning false + +namespace AlgoleanTests.ModelStateMWP + +open Algolean Algolean.Algorithms Cslib Cslib.FreeM Std.Do + +/-- Queries for incrementing and reading a counter. -/ +inductive CounterQ : Type → Type where + | tick : CounterQ Unit + | read : CounterQ Nat + +/-- Interpret counter queries in `StateM Nat`, with unit cost for each query. -/ +def counterModel : ModelStateM CounterQ (StateM Nat) Nat := + ModelStateM.ofCost (fun | .tick => modify (· + 1) | .read => get) (fun _ => 1) + +section Evaluation + +local instance : HasHandler CounterQ (.arg Nat .pure) := counterModel.hasHandler + +/-- Increment the counter. -/ +def tick : Prog CounterQ Unit := FreeM.lift .tick + +/-- Read the counter. -/ +def read : Prog CounterQ Nat := FreeM.lift .read + +/-- Increment the counter and return its new value. -/ +def tickThenRead : Prog CounterQ Nat := do + tick + read + +example (P : Prog CounterQ α) : + wpH counterModel.handler P = wp (P.evalStateM counterModel) := + counterModel.wp_eq_wp_evalStateM P + +example {Q : PostCond Nat (.arg Nat .pure)} : + let _ : HasHandler CounterQ (.arg Nat .pure) := counterModel.hasHandler + Triple (FreeM.lift CounterQ.read : Prog CounterQ Nat) + (wp⟦counterModel.evalQuery .read⟧ Q) Q := by + mvcgen [counterModel, ModelStateM.handler] + +example (n : Nat) : + ⦃fun s => ⌜s = n⌝⦄ tickThenRead + ⦃⇓ value s => ⌜value = n + 1 ∧ s = n + 1⌝⦄ := by + mvcgen [tickThenRead, tick, read, counterModel, ModelStateM.handler] + subst_vars + exact ⟨rfl, rfl⟩ + +end Evaluation + +section Costs + +local instance counterCostHandler : HasHandler CounterQ (.arg Nat (.arg Nat .pure)) := + counterModel.hasCostHandler + +example (P : Prog CounterQ α) : + wpH counterModel.costHandler P = wp (P.runStateM counterModel) := + counterModel.wp_eq_wp_runStateM P + +-- Both queries are charged, and an existing cost is retained. +example (n c : Nat) : + ⦃fun cost s => ⌜cost = c ∧ s = n⌝⦄ tickThenRead + ⦃⇓ value cost s => ⌜value = n + 1 ∧ s = n + 1 ∧ cost = c + 2⌝⦄ := by + mvcgen [tickThenRead, tick, read] + simp_all only [HasHandler.handler, counterModel, wp_lift, ModelStateM.costHandler_apply_state, + ModelStateM.ofCost_runQuery_state, Nat.add_assoc, Nat.reduceAdd, + and_true, SPred.down_pure_nil] + exact ⟨rfl, rfl⟩ + +/-- A query whose cost is determined by the incoming machine state. -/ +def stateCostModel : ModelStateM CounterQ (StateM Nat) Nat where + runQuery + | .tick => AddWriterT.mk fun s => (⟨(), s + 1⟩, s + 1) + | .read => AddWriterT.mk fun s => (⟨s, 1⟩, s) + +end Costs + +section StateCosts + +local instance : HasHandler CounterQ (.arg Nat (.arg Nat .pure)) := + stateCostModel.hasCostHandler + +example (n c : Nat) : + ⦃fun cost s => ⌜cost = c ∧ s = n⌝⦄ tickThenRead + ⦃⇓ value cost s => ⌜value = n + 1 ∧ s = n + 1 ∧ cost = c + n + 2⌝⦄ := by + mvcgen [tickThenRead, tick, read] + simp_all [HasHandler.handler, stateCostModel, Nat.add_assoc] + +end StateCosts + +end AlgoleanTests.ModelStateMWP diff --git a/AlgoleanTests/Problems.lean b/AlgoleanTests/Problems.lean new file mode 100644 index 0000000..f1ada99 --- /dev/null +++ b/AlgoleanTests/Problems.lean @@ -0,0 +1,120 @@ +/- +Copyright (c) 2026 Shreyas Srinivas. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Shreyas Srinivas +-/ + +module + +public import Algolean.Problems.Search + +/-! +# Problem specification and resource contract tests + +Examples for abstract search specifications and the termination, correctness, and resource +guarantees required by `Problem.Solves` and `Problem.RunsWithin`. +-/ + +@[expose] public section + +namespace AlgoleanTests.Problems + +open Algolean + +/-- Any positive number at most the input is an acceptable witness. -/ +def positiveWitness : Problem Nat Nat where + admissible n := 0 < n + spec n output := 0 < output ∧ output ≤ n + +example : positiveWitness.admissible 3 := by simp [positiveWitness] + +example : ¬positiveWitness.admissible 0 := by simp [positiveWitness] + +-- The output relation permits multiple valid answers for the same input. +example : positiveWitness.spec 3 1 ∧ positiveWitness.spec 3 2 := by simp [positiveWitness] + +example : ¬positiveWitness.spec 3 4 := by simp [positiveWitness] + +-- Restriction retains the original precondition and adds the new one. +example : ¬(positiveWitness.restrict (· ≤ 10)).admissible 0 := by simp [positiveWitness] + +example : ¬(positiveWitness.restrict (· ≤ 10)).admissible 11 := by simp [positiveWitness] + +example (P : Problem Input Output) (precondition : Input → Prop) (input : Input) : + (P.restrict precondition).admissible input ↔ P.admissible input ∧ precondition input := by + simp + +example (P : Problem Input Output) (p q : Input → Prop) (input : Input) (output : Output) : + ((P.restrict p).restrict q).spec input output ↔ P.spec input output := by + simp + +-- First-match and arbitrary-match search differ on duplicate keys. +example : Search.linearSearch.spec ⟨#[4, 1, 4], 4⟩ (some 0) := by + simp [Search.IsFirstMatch] + +example : ¬Search.linearSearch.spec ⟨#[4, 1, 4], 4⟩ (some 2) := by + intro h + exact h.right.right 0 (by decide) rfl + +example : Search.search.spec ⟨#[4, 1, 4], 4⟩ (some 2) := by + simp [Search.IsMatch] + +example : Search.linearSearch.spec ⟨#[], (7 : Nat)⟩ none := by simp + +example : ¬Search.search.spec ⟨#[4, 1, 4], 4⟩ none := by simp + +example : ¬Search.search.spec ⟨#[4], 4⟩ (some 1) := by + simp [Search.IsMatch] + +-- An arbitrary-match answer alone does not certify the binary-search precondition. +example : ¬(Search.binarySearch Nat.le).admissible ⟨#[2, 1], 1⟩ := by + intro h + have hs := (Search.binarySearch_admissible _ _).mp h + exact (by decide : ¬2 ≤ 1) (hs 0 1 (by decide) (by decide) (by decide)) + +example (data : Array α) (key : α) (i j : Nat) + (hi : Search.IsFirstMatch data key i) (hj : Search.IsFirstMatch data key j) : i = j := + hi.unique hj + +-- A fixed program is verified directly; the input is supplied only to its execution relation. +private def identityRun (_ : Unit) (s cost t : Nat) : Prop := cost = 1 ∧ t = s + +private theorem identity_solves : + positiveWitness.Solves () identityRun Eq Eq := by + constructor + · intro input s _ _ + exact ⟨1, s, rfl, rfl⟩ + · intro input s ha hi cost t hr + obtain ⟨_, rfl⟩ := hr + exact ⟨t, rfl, hi ▸ ha, Nat.le_of_eq hi.symm⟩ + +example : positiveWitness.RunsWithin () identityRun Eq (fun _ cost => cost ≤ 1) := by + refine ⟨identity_solves.terminates, ?_⟩ + intro input s _ _ cost t hr + exact hr.left ▸ Nat.le_refl 1 + +-- A relation with no completed executions satisfies neither predicate. +example : ¬positiveWitness.Solves () (fun _ _ (_ : Nat) _ => False) Eq Eq := by + intro h + obtain ⟨cost, t, hr⟩ := h.terminates 1 1 (by simp [positiveWitness]) rfl + exact hr + +example : ¬positiveWitness.RunsWithin () (fun _ _ (_ : Nat) _ => False) Eq + (fun _ _ => True) := by + intro h + obtain ⟨cost, t, hr⟩ := h.terminates 1 1 (by simp [positiveWitness]) rfl + exact hr + +-- One good outcome does not excuse another execution with an invalid answer. +example : ¬positiveWitness.Solves () (fun _ (_ : Nat) (_ : Nat) (_ : Nat) => True) Eq Eq := by + intro h + obtain ⟨output, rfl, hs⟩ := h.correct 1 1 (by simp [positiveWitness]) rfl 1 0 trivial + exact Nat.lt_irrefl 0 hs.left + +-- Resource bounds cover every completed execution, not just a cheap witness. +example : ¬positiveWitness.RunsWithin () + (fun _ (s : Nat) (_ : Nat) t => t = s) Eq (fun _ cost => cost ≤ 1) := by + intro h + exact (by decide : ¬2 ≤ 1) (h.bounded 1 1 (by simp [positiveWitness]) rfl 2 1 rfl) + +end AlgoleanTests.Problems diff --git a/AlgoleanTests/RandomSampleExamples.lean b/AlgoleanTests/RandomSampleExamples.lean index 750b1e7..66b282a 100644 --- a/AlgoleanTests/RandomSampleExamples.lean +++ b/AlgoleanTests/RandomSampleExamples.lean @@ -22,7 +22,7 @@ noncomputable section namespace AlgoleanTests.RandomSampleExamples -open Algolean.Algorithms Cslib RandomSample Std.Do +open Algolean Algolean.Algorithms Cslib RandomSample Std.Do example (dist : PMF ℕ) : (draw dist).evalM (free (Cost := ℕ)) = dist := by simp @@ -77,7 +77,8 @@ example {α : Type} (dist : PMF α) : letI := (free (Cost := ℕ)).hasHandler ⦃⌜True⌝⦄ draw dist ⦃⇓ a => ⌜a ∈ dist.support⌝⦄ := by let _inst := (free (Cost := ℕ)).hasHandler - mvcgen [draw] - exact fun a ha => ha + mvcgen [draw, ModelM.handler, ModelM.hasHandler] + simp [FreeM.HasHandler.handler, ModelM.handler, + FreeM.LHandler.ofInterp, WP.wp, PredTrans.apply] end AlgoleanTests.RandomSampleExamples diff --git a/AlgoleanTests/WordRAMBinarySearchExamples.lean b/AlgoleanTests/WordRAMBinarySearchExamples.lean new file mode 100644 index 0000000..8fb6d65 --- /dev/null +++ b/AlgoleanTests/WordRAMBinarySearchExamples.lean @@ -0,0 +1,126 @@ +/- +Copyright (c) 2026 Shreyas Srinivas. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Shreyas Srinivas +-/ + +module + +public import Algolean.Algorithms.WordRAM.BinarySearch.Correctness +public import Algolean.Algorithms.WordRAM.BinarySearch.Complexity + +/-! # Uniform binary search on runtime-represented arrays -/ + +@[expose] public section + +namespace AlgoleanTests.WordRAMBinarySearchExamples + +open Algolean Algolean.Algorithms Algolean.Algorithms.WordRAM + +def input : Array (Word 8) := #[1, 3, 5, 7, 9, 11, 13] + +private theorem input_sorted : SortedWords input := by + intro i j hi hj hij + have hi' : i < 7 := hi + have hj' : j < 7 := hj + interval_cases i <;> interval_cases j <;> simp_all [input] + +def searchExample : Prog (WordRAM 8 6) Unit := binarySearch 8 + +example : (execute 50 searchExample (binarySearchState input 7)).map (fun r => + (searchOutput BinarySearch.middle r.snd.ram, r.fst.tell.time, r.fst.tell.addresses)) = + some (some 3, 9, {3}) := by decide + +example : (execute 50 searchExample (binarySearchState input 13)).map (fun r => + (searchOutput BinarySearch.middle r.snd.ram, r.fst.tell.time, r.fst.tell.addresses)) = + some (some 6, 25, {3, 5, 6}) := by decide + +example : (execute 50 searchExample (binarySearchState input 0)).map (fun r => + (searchOutput BinarySearch.middle r.snd.ram, r.fst.tell.time, r.fst.tell.addresses)) = + some (none, 27, {0, 1, 3}) := by decide + +example : (execute 50 searchExample (binarySearchState input 20)).map (fun r => + (searchOutput BinarySearch.middle r.snd.ram, r.fst.tell.time, + r.fst.tell.auxiliarySpace (inputRegion input), r.fst.tell.totalSpace (inputRegion input))) = + some (none, 27, 0, 7) := by decide + +-- Every address is available: no sentinel cell is reserved. +example : (execute 50 (binarySearch 2) (binarySearchState #[0, 1, 2, 3] 3)).map + (fun r => searchOutput BinarySearch.middle r.snd.ram) = some (some 3) := by decide + +example : (execute 50 (binarySearch 2) (binarySearchState (Array.replicate 4 0) 1)).map + (fun r => (searchOutput BinarySearch.middle r.snd.ram, r.fst.tell.time)) = + some (none, binarySearchTime 4) := by decide + +-- The nonempty flag distinguishes the two possible input lengths at word width zero. +example : (execute 13 (binarySearch 0) (binarySearchState #[0] 0)).map + (fun r => (searchOutput BinarySearch.middle r.snd.ram, r.fst.tell.time)) = + some (some 0, 9) := by decide + +example : (execute 3 (binarySearch 0) ((binarySearchState #[] 0).writeFlag .eq true)).map + (fun r => (searchOutput BinarySearch.middle r.snd.ram, r.fst.tell.time)) = + some (none, 2) := by decide + +example : execute 12 (binarySearch 0) (binarySearchState #[0] 0) = none := rfl + +def representingState (target junk : Word 8) : RAMState 8 6 := + ⟨fun addr => if addr.toNat < input.size then arrayMemory input addr else junk, + fun r => if r = BinarySearch.key then target + else if r = BinarySearch.upper then 6 else 255, fun _ => true⟩ + +private theorem representingState_input (target junk : Word 8) : + RepresentsBoundedSearchInput ⟨input, target⟩ BinarySearch.key BinarySearch.upper + (representingState target junk) := by + have hfits : input.size ≤ 2 ^ 8 := by decide + refine ⟨⟨⟨hfits, ?_⟩, by simp [representingState]⟩, + by simp [representingState, BinarySearch.upper, BinarySearch.key, input], + by simp [representingState, input]⟩ + intro i hi + have hiw : i < 2 ^ 8 := by have : input.size = 7 := rfl; lia + simpa only [representingState, wordAddress_toNat i hiw, if_pos hi] using + arrayMemory_ofNat input (by decide) i hi + +example (target junk : Word 8) : + ∃ fuel cost t, execute fuel searchExample (representingState target junk) = + some (⟨(), cost⟩, ⟨t, 0⟩) := + binarySearch_terminates ⟨input, target⟩ _ (representingState_input target junk) + +example (target junk : Word 8) (fuel : Nat) (result : AddWriter (RAMCost 8 6) Unit) + (final : ExecutionState 8 6) + (hr : execute fuel searchExample (representingState target junk) = some (result, final)) : + Search.search.spec ⟨input, target⟩ (searchOutput BinarySearch.middle final.ram) ∧ + result.tell.time ≤ binarySearchTime input.size ∧ + result.tell.auxiliarySpace (inputRegion input) = 0 := + ⟨binarySearch_correct_of_execute _ _ (representingState_input target junk) hr + (by simpa using input_sorted), + binarySearch_time_le _ _ (representingState_input target junk) hr, + binarySearch_auxiliarySpace _ _ (representingState_input target junk) hr⟩ + +example : (execute 50 searchExample (representingState 7 173)).map + (fun r => (searchOutput BinarySearch.middle r.snd.ram, r.snd.ram.Memory 200)) = + some (some 3, 173) := by decide + +example (n : Nat) (hn : n ≤ 2 ^ 8) : + ∃ (data : Array (Word 8)) (target : Word 8), + data.size = n ∧ data.size ≤ 2 ^ 8 ∧ SortedWords data ∧ target ∉ data ∧ + ∃ fuel cost t, execute fuel searchExample (binarySearchState data target) = + some (⟨(), cost⟩, ⟨t, 0⟩) ∧ cost.time = binarySearchTime n := + binarySearch_exists_worstCase 8 n (by decide) hn + +-- The contracts provide termination, correctness and both resource guarantees together. +example (target junk : Word 8) : + ∃ cost t output, Executes searchExample (representingState target junk) cost t ∧ + RepresentsSearchOutput BinarySearch.middle output t ∧ + (Search.binarySearch (fun a b : Word 8 => a.toNat ≤ b.toNat)).spec + ⟨input, target⟩ output ∧ + cost.time ≤ binarySearchTime input.size ∧ cost.auxiliarySpace (inputRegion input) = 0 := by + have hi := representingState_input target junk + have ha : (Search.binarySearch (fun a b : Word 8 => a.toNat ≤ b.toNat)).admissible + ⟨input, target⟩ := by + simpa using input_sorted + obtain ⟨cost, t, hr⟩ := (binarySearch_correct 8).terminates _ _ ha hi + obtain ⟨output, ho, hs⟩ := (binarySearch_correct 8).correct _ _ ha hi cost t hr + exact ⟨cost, t, output, hr, ho, hs, + (binarySearch_runsWithin 8).bounded _ _ trivial hi cost t hr⟩ + +end AlgoleanTests.WordRAMBinarySearchExamples diff --git a/AlgoleanTests/WordRAMExamples.lean b/AlgoleanTests/WordRAMExamples.lean index d0c8aa2..8f5bbce 100644 --- a/AlgoleanTests/WordRAMExamples.lean +++ b/AlgoleanTests/WordRAMExamples.lean @@ -6,229 +6,481 @@ Authors: Shreyas Srinivas module -public import Algolean.Algorithms.WordRAMLinearSearch +public import Algolean.Algorithms.WordRAM.LinearSearch.Correctness +public import Algolean.Algorithms.WordRAM.LinearSearch.Complexity +public import Algolean.Models.WordRAMSyntax -/-! -# Word-RAM examples - -Programs demonstrating mutable memory, indirect addressing, arithmetic overflow, bitwise operations, -and branch-dependent query costs. Every runtime word operation in these examples is a query. -Queries use Algolean's existing coercion into `Prog`; typed bindings fix the result type, and -explicit widths disambiguate queries whose operands are all literals. --/ +/-! # Register operations, structured control, and uniform linear search -/ @[expose] public section namespace AlgoleanTests.WordRAMExamples -open Algolean.Algorithms Algolean.Algorithms.WordRAM - -/-- Increment a memory cell using a load, a word addition, and a store. -/ -def increment (addr : Word w) : Prog (WordRAM w) Unit := do - let x : Word w ← load addr - let y : Word w ← binop .add x 1 - store addr y - --- The increment works for arbitrary initial memory and preserves every other cell. -example (mem : Memory w) (addr : Word w) : - ((increment addr).evalM natCost mem).2 addr = mem addr + 1 := by - change Function.update mem addr (mem addr + 1) addr = _ - simp - -example (mem : Memory w) (addr other : Word w) (h : other ≠ addr) : - ((increment addr).evalM natCost mem).2 other = mem other := by - change Function.update mem addr (mem addr + 1) other = _ - simp [h] - -example (mem : Memory w) (addr : Word w) : - ((increment addr).costM natCost mem).1 = 3 := rfl - -/-- Write the largest byte, increment it, and read the wrapped result. -/ -def overflow : Prog (WordRAM 8) (Word 8) := do - store (w := 8) 7 255 - increment 7 - load (w := 8) 7 - --- Evaluation returns the word and final memory; cost evaluation counts the queries. -example : (overflow.evalM natCost Memory.zero).1 = 0 := by decide -example : (overflow.costM natCost Memory.zero).1 = 5 := rfl -example : (overflow.evalM natCost Memory.zero).2 7 = 0 := by decide - -/-- A pointer stored in one cell selects the cell to increment. -/ -def indirectIncrement : Prog (WordRAM 8) (Word 8) := do - store (w := 8) 0 42 - store (w := 8) 42 9 - let addr : Word 8 ← load (w := 8) 0 - increment addr - load addr - -example : (indirectIncrement.evalM natCost Memory.zero).1 = 10 := by decide -example : (indirectIncrement.costM natCost Memory.zero).1 = 7 := rfl -example : (indirectIncrement.evalM natCost Memory.zero).2 0 = 42 := by decide - -/-- Replace a cell only if its unsigned value is below a threshold; return whether it changed. -The load and comparison cost two queries, with one additional query if the store is executed. -/ -def raiseTo (addr threshold : Word w) : Prog (WordRAM w) Bool := do - let x : Word w ← load addr - let below : Bool ← cmp .ult x threshold - if below then - store addr threshold - return true +open Algolean Algolean.Algorithms Algolean.Algorithms.WordRAM + +open scoped Prog WordRAM + +abbrev r0 : Register 4 := 0 +abbrev r1 : Register 4 := 1 +abbrev r2 : Register 4 := 2 +abbrev r3 : Register 4 := 3 + +-- Trigger the canonical read lemma, then transport it across an address equality. +example (input : Array (Word w)) (memory : Memory w) (addr : Word w) (i : Nat) + (hmem : RepresentsArray input memory) (hi : i < input.size) + (ha : addr = BitVec.ofNat w i) : memory addr = input[i] := by + grind only [RepresentsArray.read] + +section InstructionNotation + +variable (dst x y : Register k) + +example : (x =ᵣ y : Prog.Condition (WordRAM w k)) = test .eq x y := rfl + +example : (x <ᵣ y : Prog.Condition (WordRAM w k)) = test .ult x y := rfl + +example : (do [WordRAM w k] + ifₚ x =ᵣ y then + dst ←ᵣ x + else + ifₚ x <ᵣ y then + dst ←ᵣ y + else + nop) = + (do + cmp (w := w) .eq x y + branch .eq (do [WordRAM w k] dst ←ᵣ x) (do + cmp (w := w) .ult x y + branch .ult (do [WordRAM w k] dst ←ᵣ y) (do [WordRAM w k] nop))) := rfl + +example : (nop : WordRAM w k Unit) = .nop := rfl + +example (fuel : Nat) (s : RAMState w k) : + execute (fuel + 1) (do [WordRAM w k] nop) s = + some (⟨(), ⟨1, ∅⟩⟩, ⟨s, fuel⟩) := by simp + +example (s : RAMState w k) : execute 0 (do [WordRAM w k] nop) s = none := by simp + +example : (dst ←ᵣ x + y : WordRAM w k Unit) = .binop .add dst x y := rfl + +example : (dst ←ᵣ x - y : WordRAM w k Unit) = .binop .sub dst x y := rfl + +example : (dst ←ᵣ x &&& y : WordRAM w k Unit) = .binop .band dst x y := rfl + +example : (dst ←ᵣ x ||| y : WordRAM w k Unit) = .binop .bor dst x y := rfl + +example : (dst ←ᵣ x ^^^ y : WordRAM w k Unit) = .binop .bxor dst x y := rfl + +example : (dst ←ᵣ x <<< y : WordRAM w k Unit) = .binop .shl dst x y := rfl + +example : (dst ←ᵣ x >>> y : WordRAM w k Unit) = .binop .shr dst x y := rfl + +example : (dst ←ᵣ ~~~x : WordRAM w k Unit) = .bnot dst x := rfl + +example : (dst ←ᵣ x : WordRAM w k Unit) = .copy dst x := rfl + +example (value : Word w) : (dst ←ᵣ imm[value] : WordRAM w k Unit) = .set dst value := rfl + +example : (dst ←ᵣ mem[x] : WordRAM w k Unit) = .load dst x := rfl + +example : (mem[dst] ←ᵣ x : WordRAM w k Unit) = .store dst x := rfl + +-- Queries use the existing coercion into programs, with one instruction per statement. +example : instructions (do [WordRAM 8 4] + r0 ←ᵣ imm[7] + r1 ←ᵣ mem[r0] + r2 ←ᵣ r0 + r1 + r3 ←ᵣ ~~~r2 + mem[r0] ←ᵣ r3) = + [.set r0 7, .load r1 r0, .binop .add r2 r0 r1, .bnot r3 r2, .store r0 r3] := rfl + +-- Local bindings and nested control still use ordinary Lean syntax. +example : (do [WordRAM 8 4] + let dst := r0 + ifₚ flag .eq then + dst ←ᵣ r1 + r2 + else + whileₚ .ult do + dst ←ᵣ ~~~r1) = + branch .eq (.binop .add r0 r1 r2 : WordRAM 8 4 Unit) + (whileLoop .ult (.bnot r0 r1 : WordRAM 8 4 Unit)) := rfl + +-- A nested quotation supplies its own query type. +example : (do [WordRAM 8 4] + let q := do [WordRAM 2 1] + (0 : Register 1) ←ᵣ imm[1] + let _ := q + r0 ←ᵣ imm[7]) = ((.set r0 7 : WordRAM 8 4 Unit) : Prog (WordRAM 8 4) Unit) := rfl + +example (op : CmpOp) : (reset op : WordRAM w k Unit) = .clearFlag op := rfl + +example : (do [WordRAM 8 4] + reset .eq) = ((.clearFlag .eq : WordRAM 8 4 Unit) : Prog (WordRAM 8 4) Unit) := rfl + +-- Reset clears only its selected flag and costs one primitive operation. +example : + let s : RAMState 8 4 := { RAMState.zero with Flags := fun _ => true } + (execute 1 (do [WordRAM 8 4] reset .ult) s).map (fun result => + (result.snd.ram.Flags .ult, result.snd.ram.Flags .eq, result.fst.tell.time)) = + some (false, true, 1) := by decide + +/-- info: fun op ↦ reset op : CmpOp → WordRAM 8 4 Unit -/ +#guard_msgs in +#check fun (op : CmpOp) => WordRAM.clearFlag (w := 8) (k := 4) op + +-- Standard notation declarations reconstruct the instruction when pretty-printing. +/-- info: fun dst x y ↦ dst ←ᵣ x + y : Register 4 → Register 4 → Register 4 → WordRAM 8 4 Unit -/ +#guard_msgs in +#check fun (dst x y : Register 4) => WordRAM.binop (w := 8) .add dst x y + +/-- info: fun dst x ↦ dst ←ᵣ ~~~x : Register 4 → Register 4 → WordRAM 8 4 Unit -/ +#guard_msgs in +#check fun (dst x : Register 4) => WordRAM.bnot (w := 8) dst x + +end InstructionNotation + +def increment (w : Nat) : Prog (WordRAM w 4) Unit := do + load (w := w) r1 r0 + binop (w := w) .add r1 r1 r3 + store (w := w) r0 r1 + +def overflow : Prog (WordRAM 8 4) Unit := do + set (w := 8) r0 7 + set (w := 8) r1 255 + set (w := 8) r3 1 + store (w := 8) r0 r1 + increment 8 + +example : (execute 7 overflow RAMState.zero).map (fun r => + (r.snd.ram.Memory 7, r.snd.ram.Registers r1, r.fst.tell.time, r.fst.tell.addresses)) = + some (0, 0, 7, {7}) := by decide + +example : execute 6 overflow RAMState.zero = none := rfl + +def copyExample : Prog (WordRAM 8 4) Unit := do + set (w := 8) r0 42 + copy (w := 8) r1 r0 + set (w := 8) r0 7 + +example : (execute 3 copyExample RAMState.zero).map + (fun r => (r.snd.ram.Registers r1, r.fst.tell.time)) = some (42, 3) := by decide + +def followPointer : Prog (WordRAM 8 4) Unit := do + load (w := 8) r0 r0 + load (w := 8) r1 r0 + +def pointerState (ptr : Word 8) : RAMState 8 4 := + ⟨fun addr => if addr = 0 then ptr else 42, fun _ => 0, fun _ => false⟩ + +example : (execute 2 followPointer (pointerState 9)).map (fun r => + (r.snd.ram.Registers r1, r.fst.tell.time, r.fst.tell.addresses, r.fst.tell.space)) = + some (42, 2, {0, 9}, 2) := by decide + +example : (execute 2 followPointer (pointerState 0)).map + (fun r => r.fst.tell.addresses) = some {0} := by decide + +example : (execute 4 (followPointer *> followPointer) (pointerState 0)).map + (fun r => r.fst.tell) = some ⟨4, {0}⟩ := by decide + +example : (execute 2 followPointer (pointerState 9)).map (fun r => + (r.fst.tell.auxiliarySpace {0}, r.fst.tell.totalSpace {0, 1})) = some (1, 3) := by decide + +def storeThroughPointer : Prog (WordRAM 8 4) Unit := do + load (w := 8) r0 r0 + store (w := 8) r0 r0 + +example : (execute 2 storeThroughPointer (pointerState 9)).map + (fun r => (r.snd.ram.Memory 9, r.fst.tell.addresses)) = some (9, {0, 9}) := by decide + +def byteBinop (op : BinOp) (x y : Word 8) : Option (Word 8) := + (execute 1 (do binop (w := 8) op r2 r0 r1 : Prog (WordRAM 8 4) Unit) + ⟨fun _ => 0, fun r => if r = r0 then x else y, fun _ => false⟩).map + (fun r => r.snd.ram.Registers r2) + +example : byteBinop .sub 0 1 = some 255 := by decide + +example : byteBinop .band 170 204 = some 136 := by decide + +example : byteBinop .bor 170 204 = some 238 := by decide + +example : byteBinop .bxor 170 204 = some 102 := by decide + +example : byteBinop .shl 129 1 = some 2 := by decide + +example : byteBinop .shr 128 1 = some 64 := by decide + +example : byteBinop .shl 255 8 = some 0 := by decide + +example : byteBinop .shr 255 8 = some 0 := by decide + +example : byteBinop .shl 255 9 = some 0 := by decide + +example : byteBinop .shr 255 255 = some 0 := by decide + +def wordOnly : Prog (WordRAM 8 4) Unit := do + set (w := 8) r0 170 + bnot (w := 8) r1 r0 + cmp (w := 8) .eq r0 r1 + +example : (execute 3 wordOnly RAMState.zero).map (fun r => + (r.snd.ram.Registers r1, r.snd.ram.Flags .eq, r.fst.tell.time, r.fst.tell.space)) = + some (85, false, 3, 0) := by decide + +namespace Branches + +def initial (x y : Word 8) : RAMState 8 4 := + ⟨fun _ => 0, fun r => if r = r0 then x else if r = r1 then y else if r = r3 then 9 else 0, + fun _ => false⟩ + +def choose : Prog (WordRAM 8 4) Unit := do + ifₚ test .ult r0 r1 then + set (w := 8) r2 42 + store (w := 8) r3 r2 else - return false + set (w := 8) r2 99 + +example : (execute 4 choose (initial 3 7)).map (fun r => + (r.snd.ram.Memory 9, r.fst.tell.time, r.fst.tell.addresses, r.snd.ram.Flags .ult)) = + some (42, 3, {9}, true) := by decide + +example : (execute 3 choose (initial 7 3)).map (fun r => + (r.snd.ram.Memory 9, r.snd.ram.Registers r2, r.fst.tell.time, r.fst.tell.addresses)) = + some (0, 99, 2, ∅) := by decide + +def independentFlags : Prog (WordRAM 8 4) Unit := do + cmp (w := 8) .eq r0 r0 + cmp (w := 8) .ult r0 r1 + +example : (execute 2 independentFlags (initial 3 7)).map + (fun r => (r.snd.ram.Flags .eq, r.snd.ram.Flags .ult)) = some (true, true) := by decide + +def nested : Prog (WordRAM 8 4) Unit := do + cmp (w := 8) .ult r0 r1 + branch .ult + (do branch .ult (do set (w := 8) r2 42) (do [WordRAM 8 4] nop)) + (do [WordRAM 8 4] nop) + store (w := 8) r3 r2 -example : ((raiseTo (w := 8) 4 10).evalM natCost Memory.zero).1 = true := by - decide +example : execute 4 nested (initial 3 7) = none := rfl -example : ((raiseTo (w := 8) 4 10).costM natCost Memory.zero).1 = 3 := rfl +example : (execute 5 nested (initial 3 7)).map + (fun r => (r.fst.tell.time, r.snd.ram.Memory 9, r.snd.fuel)) = some (3, 42, 0) := by decide -example : ((raiseTo (w := 8) 4 10).evalM natCost Memory.zero).2 4 = 10 := by - decide +example : (execute 8 nested (initial 3 7)).map + (fun r => (r.fst.tell.time, r.snd.ram.Memory 9, r.snd.fuel)) = some (3, 42, 3) := by decide --- 255 is larger than 10 in the unsigned ordering, so this execution skips the store. -example : ((raiseTo (w := 8) 4 10).evalM natCost (fun _ => 255)).1 = false := by - decide +end Branches -example : ((raiseTo (w := 8) 4 10).costM natCost (fun _ => 255)).1 = 2 := rfl +namespace Loops -example : ((raiseTo (w := 8) 4 10).evalM natCost (fun _ => 255)).2 4 = 255 := by - decide +def repeated (fuel : Nat) : Prog (WordRAM 8 4) Unit := do + set (w := 8) r2 1 + repeat [fuel] + binop (w := 8) .add r0 r0 r2 -/-- Evaluate one byte operation through the query interpreter. -/ -def byteBinop (op : BinOp) (x y : Word 8) : Word 8 := - (Prog.evalM (binop op x y : Prog (WordRAM 8) (Word 8)) natCost Memory.zero).1 +example : (execute 4 (repeated 3) RAMState.zero).map + (fun r => (r.snd.ram.Registers r0, r.fst.tell.time)) = some (3, 4) := by decide -example : byteBinop .sub 0 1 = 255 := by decide -example : byteBinop .band 170 204 = 136 := by decide -example : byteBinop .bor 170 204 = 238 := by decide -example : byteBinop .bxor 170 204 = 102 := by decide -example : byteBinop .shl 129 1 = 2 := by decide -example : byteBinop .shr 128 1 = 64 := by decide +example : (execute 1 (repeated 0) RAMState.zero).map + (fun r => (r.snd.ram.Registers r0, r.fst.tell.time)) = some (0, 1) := by decide --- Shift counts are not masked modulo the word width, and right shifts do not extend the sign bit. -example : byteBinop .shl 255 8 = 0 := by decide -example : byteBinop .shr 255 8 = 0 := by decide -example : byteBinop .shl 255 9 = 0 := by decide -example : byteBinop .shr 255 255 = 0 := by decide +-- The indented flag loop and comparison loop use the same WordRAM query type as branches. +def count : Prog (WordRAM 8 4) Unit := do + set (w := 8) r2 1 + whileₚ .ult r0 r1 do + binop (w := 8) .add r0 r0 r2 + store (w := 8) r3 r0 +example : execute 12 count (Branches.initial 0 3) = none := rfl + +example : (execute 13 count (Branches.initial 0 3)).map + (fun r => (r.fst.tell.time, r.snd.ram.Memory 9, r.snd.fuel)) = some (9, 3, 0) := by decide + +example : (execute 4 count (Branches.initial 3 3)).map + (fun r => (r.fst.tell.time, r.snd.ram.Memory 9)) = some (3, 3) := by decide + +def flagLoop : Prog (WordRAM 8 4) Unit := do + whileₚ .ult do + clearFlag (w := 8) (k := 4) .ult + +example : (execute 3 flagLoop (RAMState.zero.writeFlag .ult true)).map + (fun r => (r.fst.tell.time, r.snd.ram.Flags .ult, r.snd.fuel)) = some (1, false, 0) := by decide + +example : (execute 1 flagLoop RAMState.zero).map + (fun r => r.fst.tell.time) = some 0 := by decide + +def forever : Prog (WordRAM 8 4) Unit := do [WordRAM 8 4] + cmp (w := 8) .eq r0 r0 + whileₚ .eq do + nop + +example (fuel : Nat) (s : RAMState 8 4) : execute fuel forever s = none := by + have loops : ∀ fuel (s : RAMState 8 4), s.Flags .eq = true → + runCode fuel [.whileCode .eq [.nop]] s = none := by + intro fuel + induction fuel using Nat.strong_induction_on with + | h fuel ih => + intro s h + cases fuel with + | zero => rfl + | succ fuel => + cases fuel with + | zero => simp [runCode, step, h] + | succ fuel => simp [runCode, step, h, ih fuel (by lia) s h] + cases fuel <;> simp [execute_eq_runCode, forever, whileLoop, runCode, step, CmpOp.eval, loops] + +def nested : Prog (WordRAM 8 4) Unit := do + set (w := 8) r2 1 + whileₚ .ult r0 r1 do + whileₚ .ult r0 r1 do + binop (w := 8) .add r0 r0 r2 + store (w := 8) r3 r0 + +example : execute 16 nested (Branches.initial 0 3) = none := rfl + +example : (execute 17 nested (Branches.initial 0 3)).map + (fun r => (r.fst.tell.time, r.snd.ram.Memory 9)) = some (11, 3) := by decide + +def skipped : Prog (WordRAM 8 4) Unit := do + cmp (w := 8) .ult r0 r1 + branch .ult (do set (w := 8) r2 42) forever + +example : (execute 3 skipped (Branches.initial 0 3)).map + (fun r => (r.fst.tell.time, r.snd.ram.Registers r2)) = some (2, 42) := by decide + +end Loops + +example : execute 0 (pure () : Prog (WordRAM 8 4) Unit) RAMState.zero = + some (⟨(), 0⟩, ⟨RAMState.zero, 0⟩) := rfl + +example : execute 0 (set (w := 8) r0 1 : Prog (WordRAM 8 4) Unit) RAMState.zero = none := rfl + +section WeakestPreconditions + +open Cslib.FreeM Std.Do + +local instance : HasHandler (WordRAM 8 4) + (.arg (RAMCost 8 4) (.arg (ExecutionState 8 4) (.except PUnit .pure))) := + timeAndSpaceCost.hasCostHandler + +set_option mvcgen.warning false in example : - (Prog.evalM (bnot (w := 8) 170 : Prog (WordRAM 8) (Word 8)) natCost Memory.zero).1 = 85 := by - decide + ⦃fun cost s => ⌜cost = 0 ∧ s = ⟨pointerState 9, 2⟩⌝⦄ followPointer + ⦃⇓ _ cost s => ⌜cost.time = 2 ∧ cost.addresses = {0, 9} ∧ s.ram.Registers r1 = 42⌝⦄ := by + mvcgen [followPointer] + simp_all [HasHandler.handler, ModelStateM.costHandler, timeAndSpaceCost, + runBlock, runCode, step, pointerState, r0, r1, Finset.pair_comm] +set_option mvcgen.warning false in example : - (Prog.evalM (cmp .eq (w := 8) 42 42 : Prog (WordRAM 8) Bool) natCost Memory.zero).1 = true := by - decide + ⦃fun cost s => ⌜cost = 0 ∧ s = ⟨Branches.initial 3 7, 4⟩⌝⦄ Branches.choose + ⦃⇓ _ cost s => ⌜cost.time = 3 ∧ cost.addresses = {9} ∧ s.ram.Memory 9 = 42⌝⦄ := by + mvcgen [Branches.choose, Prog.ifThenElse, test, branch] + simp_all [HasHandler.handler, ModelStateM.costHandler, timeAndSpaceCost, + runBlock, runCode, step, Branches.initial, CmpOp.eval, r0, r1, r2, r3] +set_option mvcgen.warning false in example : - (Prog.evalM (cmp .eq (w := 8) 42 43 : Prog (WordRAM 8) Bool) natCost Memory.zero).1 = - false := by - decide - --- Word-only operations leave arbitrary memory unchanged. -example (mem : Memory w) (op : BinOp) (x y : Word w) : - (Prog.evalM (binop op x y : Prog (WordRAM w) (Word w)) natCost mem).2 = mem := rfl - --- The same programs can track time and footprint without changing their definitions. -example (mem : Memory w) (addr : Word w) : - ((increment addr).costM timeAndSpaceCost mem).1 = ⟨3, {addr}⟩ := by - change (⟨1, {addr}⟩ : RAMCost w) + (⟨1, ∅⟩ + (⟨1, {addr}⟩ + 0)) = ⟨3, {addr}⟩ - ext <;> simp - -/-- Reuse a cell across several increments. -/ -def repeatIncrement (addr : Word w) : Nat → Prog (WordRAM w) Unit - | 0 => pure () - | n + 1 => do - increment addr - repeatIncrement addr n - -example : ((repeatIncrement (w := 8) 7 0).costM timeAndSpaceCost Memory.zero).1 = 0 := rfl - --- Twelve operations still access just one cell, even though it is read and written repeatedly. -example : ((repeatIncrement (w := 8) 7 4).costM timeAndSpaceCost Memory.zero).1.time = 12 := rfl -example : ((repeatIncrement (w := 8) 7 4).costM timeAndSpaceCost Memory.zero).1.space = 1 := by - decide - -example : (indirectIncrement.costM timeAndSpaceCost Memory.zero).1.addresses = {0, 42} := by - decide -example : (indirectIncrement.costM timeAndSpaceCost Memory.zero).1.time = 7 := rfl -example : (indirectIncrement.costM timeAndSpaceCost Memory.zero).1.space = 2 := by decide - --- Exclude the input cell at address 0; include an unread input cell at address 1 for total space. -example : (indirectIncrement.costM timeAndSpaceCost Memory.zero).1.auxiliarySpace {0, 1} = 1 := by - decide -example : (indirectIncrement.costM timeAndSpaceCost Memory.zero).1.totalSpace {0, 1} = 3 := by - decide - --- Both branches access the same cell, but only one branch writes it. -example : ((raiseTo (w := 8) 4 10).costM timeAndSpaceCost Memory.zero).1 = ⟨3, {4}⟩ := by - decide -example : ((raiseTo (w := 8) 4 10).costM timeAndSpaceCost (fun _ => 255)).1 = ⟨2, {4}⟩ := by - decide - -/-- Load a pointer from a cell and then read the pointed-to cell. -/ -def followPointer (slot : Word w) : Prog (WordRAM w) (Word w) := do - let addr : Word w ← load slot - load addr - --- The footprint depends on the address actually loaded, including when the pointer aliases itself. -example : ((followPointer (w := 8) 0).costM timeAndSpaceCost Memory.zero).1 = ⟨2, {0}⟩ := by - decide -example : ((followPointer (w := 8) 0).costM timeAndSpaceCost (fun _ => 9)).1 = ⟨2, {0, 9}⟩ := by - decide - -/-- Word arithmetic, complement, and comparison require no memory queries. -/ -def wordOnly (x y : Word w) : Prog (WordRAM w) Bool := do - let sum : Word w ← binop .add x y - let inverted : Word w ← bnot sum - cmp .eq inverted x - -example (mem : Memory w) (x y : Word w) : - ((wordOnly x y).costM timeAndSpaceCost mem).1 = ⟨3, ∅⟩ := by - change (⟨1, ∅⟩ : RAMCost w) + (⟨1, ∅⟩ + (⟨1, ∅⟩ + 0)) = ⟨3, ∅⟩ - ext <;> simp + ⦃fun cost s => ⌜cost = 0 ∧ s = ⟨RAMState.zero.writeFlag .ult true, 3⟩⌝⦄ Loops.flagLoop + ⦃⇓ _ cost s => ⌜cost.time = 1 ∧ s.ram.Flags .ult = false ∧ s.fuel = 0⌝⦄ := by + mvcgen [Loops.flagLoop, whileLoop] + simp_all [HasHandler.handler, ModelStateM.costHandler, timeAndSpaceCost, + runBlock, runCode, step, RAMState.zero] + +end WeakestPreconditions + +example (p : Prog (WordRAM w k) (List Bool)) (s t : RAMState w k) + (fuel fuel' : Nat) (result result' : AddWriter (RAMCost w k) (List Bool)) + (final final' : ExecutionState w k) + (h : execute fuel p s = some (result, final)) + (h' : execute fuel' p t = some (result', final')) : result.ret = result'.ret := + execute_ret_independent p s t h h' section LinearSearch -/-- Example input, including a duplicate key to demonstrate returning the first match. -/ -def searchInput : Array (BitVec 8) := #[12, 7, 42, 7, 99] - -/-- Choose a byte-sized key to search for in `searchInput`. -/ -def searchExample (key : BitVec 8) : Prog (WordRAM 8) (Option (Word 8)) := - linearSearch searchInput key (by decide) - --- The first 7 is at address 1: one failed comparison followed by a successful comparison. -example : (searchExample 7 |>.evalM timeAndSpaceCost (arrayMemory searchInput)).1 = some 1 := by - decide -example : (searchExample 7 |>.costM timeAndSpaceCost (arrayMemory searchInput)).1 = - ⟨5, {0, 1}⟩ := by decide - --- Finding the first element stops immediately; finding the last reads the entire array. -example : (searchExample 12 |>.costM timeAndSpaceCost (arrayMemory searchInput)).1 = - ⟨2, {0}⟩ := by decide -example : (searchExample 99 |>.evalM timeAndSpaceCost (arrayMemory searchInput)).1 = some 4 := by - decide -example : (searchExample 99 |>.costM timeAndSpaceCost (arrayMemory searchInput)).1 = - ⟨14, {0, 1, 2, 3, 4}⟩ := by decide - --- A missing key returns none after five loads, five comparisons, and five address increments. -example : (searchExample 18 |>.evalM timeAndSpaceCost (arrayMemory searchInput)).1 = none := by - decide -example : (searchExample 18 |>.costM timeAndSpaceCost (arrayMemory searchInput)).1 = - ⟨15, {0, 1, 2, 3, 4}⟩ := by decide - --- Early termination touches only two input cells and uses no auxiliary RAM cells. -example : (searchExample 7 |>.costM timeAndSpaceCost (arrayMemory searchInput)).1.space = 2 := by - decide -example : (searchExample 7 |>.costM timeAndSpaceCost (arrayMemory searchInput)).1.auxiliarySpace - {0, 1, 2, 3, 4} = 0 := by decide -example : (searchExample 7 |>.costM timeAndSpaceCost (arrayMemory searchInput)).1.totalSpace - {0, 1, 2, 3, 4} = 5 := by decide - --- The empty array performs no queries and returns none. -example : ((linearSearch (#[] : Array (BitVec 8)) 7 (by decide)).evalM timeAndSpaceCost - (arrayMemory #[])).1 = none := by decide -example : ((linearSearch (#[] : Array (BitVec 8)) 7 (by decide)).costM timeAndSpaceCost - (arrayMemory #[])).1 = 0 := by decide +def searchInput : Array (Word 8) := #[12, 7, 42, 7, 99] + +def searchExample : Prog (WordRAM 8 5) Unit := linearSearch 8 + +example : (execute 50 searchExample (linearSearchState searchInput 7 LinearSearch.key)).map + (fun r => + (searchOutput LinearSearch.index r.snd.ram, r.fst.tell.time, r.fst.tell.addresses, + r.fst.tell.auxiliarySpace (sizedInputRegion searchInput))) = + some (some 1, 14, {0, 1, 2}, 0) := by decide + +example : (execute 50 searchExample (linearSearchState searchInput 2 LinearSearch.key)).map + (fun r => + (searchOutput LinearSearch.index r.snd.ram, r.fst.tell.time, r.fst.tell.totalSpace + (sizedInputRegion searchInput))) = some (none, 27, 6) := by decide + +example : (execute 30 (linearSearch 2) (linearSearchState #[0, 1, 2] 2 LinearSearch.key)).map + (fun r => (searchOutput LinearSearch.index r.snd.ram, r.fst.tell.time)) = + some (some 2, 18) := by decide + +-- The key equals the size header, but no array element matches it. +example : (execute 30 (linearSearch 2) (linearSearchState #[1, 2, 1] 3 LinearSearch.key)).map + (fun r => (searchOutput LinearSearch.index r.snd.ram, r.fst.tell.time, + r.fst.tell.addresses)) = some (none, 19, {0, 1, 2, 3}) := by decide + +example : (execute 14 (linearSearch 1) (linearSearchState #[0] 0 LinearSearch.key)).map + (fun r => (searchOutput LinearSearch.index r.snd.ram, r.fst.tell.time)) = + some (some 0, 10) := by decide + +example : (execute 9 (linearSearch 0) + ((linearSearchState #[] 0 LinearSearch.key).writeFlag .eq true)).map + (fun r => (searchOutput LinearSearch.index r.snd.ram, r.fst.tell.time)) = + some (none, 7) := by decide + +def representingState (target junk : Word 8) : RAMState 8 5 := + ⟨fun addr => if addr.toNat < searchInput.size + 1 + then sizedArrayMemory searchInput addr else junk, + fun r => if r = LinearSearch.key then target else 255, fun _ => true⟩ + +private theorem representingState_input (target junk : Word 8) : + RepresentsSizedSearchInput ⟨searchInput, target⟩ LinearSearch.key + (representingState target junk) := by + refine ⟨⟨by simp [withSize, searchInput], ?_⟩, by simp [representingState]⟩ + intro i hi + have hiw : i < 2 ^ 8 := by simp [withSize, searchInput] at hi; lia + simpa only [representingState, wordAddress_toNat i hiw, withSize_size] using + (show (if i < searchInput.size + 1 then sizedArrayMemory searchInput (BitVec.ofNat 8 i) + else junk) = (withSize searchInput)[i] from + by + rw [if_pos (by simpa using hi)] + exact sizedArrayMemory_ofNat searchInput (by decide) i hi) + +example (target junk : Word 8) : + ∃ fuel cost t, execute fuel searchExample (representingState target junk) = + some (⟨(), cost⟩, ⟨t, 0⟩) := + linearSearch_terminates ⟨searchInput, target⟩ _ (representingState_input target junk) + +example (target junk : Word 8) (fuel : Nat) (result : AddWriter (RAMCost 8 5) Unit) + (final : ExecutionState 8 5) + (hr : execute fuel searchExample (representingState target junk) = some (result, final)) : + Search.linearSearch.spec ⟨searchInput, target⟩ (searchOutput LinearSearch.index final.ram) ∧ + result.tell.auxiliarySpace (sizedInputRegion searchInput) = 0 := + ⟨linearSearch_correct_of_execute _ _ (representingState_input target junk) hr, + linearSearch_auxiliarySpace _ _ (representingState_input target junk) hr⟩ + +example : (execute 50 searchExample (representingState 7 173)).map + (fun r => (searchOutput LinearSearch.index r.snd.ram, r.snd.ram.Memory 200)) = + some (some 1, 173) := by decide + end LinearSearch +-- The contracts provide termination, correctness and both resource guarantees together. +example (target junk : Word 8) : + ∃ cost t output, Executes searchExample (representingState target junk) cost t ∧ + RepresentsSearchOutput LinearSearch.index output t ∧ + Search.linearSearch.spec ⟨searchInput, target⟩ output ∧ + cost.time ≤ linearSearchTime searchInput.size ∧ + cost.auxiliarySpace (sizedInputRegion searchInput) = 0 := by + have hi := representingState_input target junk + have ha : Search.linearSearch.admissible ⟨searchInput, target⟩ := by + trivial + obtain ⟨cost, t, hr⟩ := (linearSearch_correct 8).terminates _ _ ha hi + obtain ⟨output, ho, hs⟩ := (linearSearch_correct 8).correct _ _ ha hi cost t hr + exact ⟨cost, t, output, hr, ho, hs, + (linearSearch_runsWithin 8).bounded _ _ trivial hi cost t hr⟩ + end AlgoleanTests.WordRAMExamples