From 41a2b657821e53133e38b112da51be2947926b85 Mon Sep 17 00:00:00 2001 From: Josh Liebow-Feeser Date: Thu, 15 Oct 2026 18:06:35 -0400 Subject: [PATCH] Compose byte decoders at explicit element metadata Byte length cannot recover an element count when elements are zero-sized. Keep the count in slice decoding, and retain each child's metadata when composing indexed decoders into a sequence. Prove initialization, realizability for admitted values, and completeness through physical and mathematical decoding. Check empty uninhabited slices, distinct zero-byte counts, rejected metadata, and nested indexed sequences. These are pure representation laws; they do not supply a Rust layout or pointer-access premise. gherrit-pr-id: Grpvcydhrmu5xhlrgdma3sjuwlvxdozc6 Agent-authored-by: AI agent acting on joshlf's behalf --- anneal/lean/Rust/ReferentTests.lean | 33 +++++ anneal/lean/Rust/Storage.lean | 195 ++++++++++++++++++++++++++++ anneal/lean/RustStorageTests.lean | 129 ++++++++++++++++++ 3 files changed, 357 insertions(+) diff --git a/anneal/lean/Rust/ReferentTests.lean b/anneal/lean/Rust/ReferentTests.lean index 6da6be6793..838069d3c0 100644 --- a/anneal/lean/Rust/ReferentTests.lean +++ b/anneal/lean/Rust/ReferentTests.lean @@ -96,6 +96,39 @@ theorem no_value_not_complete : ¬noValueDecoder.CompleteWith noValueModel := by obtain ⟨value, _⟩ := complete () [] rfl initialized_nil exact nomatch value +-- A slice can be empty even though no element can be decoded. +def emptyElementDecoder : BitDecoder Empty where + byteSize := 0 + decode _ := none + +example : Safe (sliceDecoder emptyElementDecoder) some 0 [] := + ⟨[], [], rfl, rfl⟩ + +example : ¬Safe (sliceDecoder emptyElementDecoder) some 1 [] := by + rintro ⟨raw, value, accepted, _⟩ + have rejected : (sliceDecoder emptyElementDecoder).run 1 [] = none := by decide + rw [rejected] at accepted + contradiction + +-- Language validity at a positive ZST count cannot replace mathematical decoding. +example : (sliceDecoder unitDecoder).run 2 [] = some [(), ()] := by decide +example : ¬Safe (sliceDecoder unitDecoder) (fun _ => (none : Option Unit)) 2 [] := by + rintro ⟨_, _, _, rejected⟩ + contradiction + +-- The shared completeness law supplies safe admission at every requested byte count. +theorem sliceByte_complete : (sliceDecoder byteDecoder).CompleteWith some := by + intro count bytes width initialized + obtain ⟨values, accepted⟩ := + sliceDecoder_complete byteDecoder byteDecoder_complete count bytes width initialized + exact ⟨values, by simp [StorageDecoder.runWith, accepted]⟩ + +example (count : Nat) : + Transfer count (fun _ => True) .initialized + ((sliceDecoder byteDecoder).byteSize count) + (Safe (sliceDecoder byteDecoder) some count) .safe := + initialized_to_safe (sliceDecoder byteDecoder) some sliceByte_complete count count (fun _ => True) + example : Initialized (([AMByte.init 0, AMByte.init 1, AMByte.init 2].drop 1).take 1) := initialized_subrange _ (by simp [Initialized]) 1 1 diff --git a/anneal/lean/Rust/Storage.lean b/anneal/lean/Rust/Storage.lean index 2994183b2e..faa200f33f 100644 --- a/anneal/lean/Rust/Storage.lean +++ b/anneal/lean/Rust/Storage.lean @@ -418,6 +418,36 @@ theorem arrayDecoder_complete (element : BitDecoder Raw) simp only [arrayDecode, acceptedHead, tailDecode] rfl⟩ +/-- Realizable elements compose into a representation of the exact list. +Only elements admitted by `valid` need representations; an empty list therefore +needs no value or representation of its element type. -/ +theorem arrayDecoder_realizable (element : BitDecoder Raw) (valid : Raw → Prop) + (realizable : ∀ raw, valid raw → ∃ bytes, element.run bytes = some raw) + (values : List Raw) (admitted : ∀ value ∈ values, valid value) : + ∃ bytes, (arrayDecoder element values.length).run bytes = some ⟨values, rfl⟩ := by + induction values with + | nil => exact ⟨[], by simp [BitDecoder.run, arrayDecoder, arrayDecode]⟩ + | cons value values ih => + obtain ⟨head, acceptedHead⟩ := realizable value (admitted value (by simp)) + obtain ⟨tail, acceptedTail⟩ := ih (fun raw member => admitted raw (by simp [member])) + have headWidth := element.run_length head value acceptedHead + have tailWidth := arrayDecoder_run_length element values.length tail _ acceptedTail + have tailDecode : arrayDecode element values.length tail = some ⟨values, rfl⟩ := by + simpa [BitDecoder.run, arrayDecoder, tailWidth] using acceptedTail + have width : (head ++ tail).length = (values.length + 1) * element.byteSize := by + simp only [List.length_append, headWidth, tailWidth, Nat.succ_mul] + omega + have takeHead : (head ++ tail).take element.byteSize = head := by + rw [← headWidth] + simp + have dropHead : (head ++ tail).drop element.byteSize = tail := by + rw [← headWidth] + simp + refine ⟨head ++ tail, ?_⟩ + simp only [BitDecoder.run, arrayDecoder, List.length_cons, width, ↓reduceIte] + simp only [arrayDecode, takeHead, dropHead, acceptedHead, tailDecode] + rfl + /-- A physical decoder at explicit metadata. `metadata` observes the decoded raw value; `run` checks that observation against the requested metadata. Size need not identify metadata: zero-sized slices and padded layouts may share a width. @@ -552,6 +582,142 @@ theorem map_initialized [DecidableEq Metadata] (decoder : StorageDecoder Metadat | none => simp [language] at accepted | some raw => exact initialized metadata bytes raw language +/-- Each metadata entry requests one element, including when its width is zero. +Every element run checks both its byte width and its returned metadata. -/ +def sequenceDecode [DecidableEq Metadata] (element : StorageDecoder Metadata Raw) : + List Metadata → List AMByte → Option (List Raw) + | [], bytes => if bytes = [] then some [] else none + | metadata :: rest, bytes => do + let raw ← element.run metadata (bytes.take (element.byteSize metadata)) + let raws ← sequenceDecode element rest (bytes.drop (element.byteSize metadata)) + return raw :: raws + +/-- Compose repeated uses of one storage decoder at explicit element metadata. +The metadata list retains element boundaries when widths coincide or are zero. +This is a pure byte-domain construction; a Rust layout needs a separate bridge. -/ +def sequence [DecidableEq Metadata] (element : StorageDecoder Metadata Raw) : + StorageDecoder (List Metadata) (List Raw) where + byteSize metadata := (metadata.map element.byteSize).sum + metadata raws := raws.map element.metadata + decode := sequenceDecode element + +/-- The metadata list retains the number of elements independently of byte width. -/ +theorem sequence_run_count [DecidableEq Metadata] (element : StorageDecoder Metadata Raw) + (metadata : List Metadata) (bytes : List AMByte) (raws : List Raw) + (accepted : element.sequence.run metadata bytes = some raws) : + raws.length = metadata.length := by + have sameMetadata := element.sequence.run_metadata metadata bytes raws accepted + simpa [sequence] using congrArg List.length sameMetadata + +theorem sequenceDecode_initialized [DecidableEq Metadata] (element : StorageDecoder Metadata Raw) + (initialized : element.Initialized) (metadata : List Metadata) (bytes : List AMByte) + (raws : List Raw) (accepted : sequenceDecode element metadata bytes = some raws) : + Rust.Storage.Initialized bytes := by + induction metadata generalizing bytes raws with + | nil => + simp only [sequenceDecode] at accepted + split at accepted + · rename_i empty + simp [empty] + · contradiction + | cons metadata rest ih => + simp only [sequenceDecode] at accepted + cases first : element.run metadata (bytes.take (element.byteSize metadata)) with + | none => simp [first] at accepted + | some raw => + cases tail : sequenceDecode element rest (bytes.drop (element.byteSize metadata)) with + | none => simp [first, tail] at accepted + | some raws => + have both := (initialized_append _ _).mpr + ⟨initialized metadata _ raw first, ih _ raws tail⟩ + simpa using both + +/-- Sequence initialization covers every accepted element representation. -/ +theorem sequence_initialized [DecidableEq Metadata] (element : StorageDecoder Metadata Raw) + (initialized : element.Initialized) : element.sequence.Initialized := by + intro metadata bytes raws accepted + exact sequenceDecode_initialized element initialized metadata bytes raws + ((element.sequence.run_eq_some_iff metadata bytes raws).mp accepted).2.1 + +/-- Realizable admitted elements compose at exactly the requested metadata list. +The empty list needs no element value or element representation. -/ +theorem sequence_realizable [DecidableEq Metadata] (element : StorageDecoder Metadata Raw) + (valid : Raw → Prop) + (realizable : ∀ raw, valid raw → ∃ bytes, element.run (element.metadata raw) bytes = some raw) + (metadata : List Metadata) (raws : List Raw) + (sameMetadata : raws.map element.metadata = metadata) + (admitted : ∀ raw ∈ raws, valid raw) : + ∃ bytes, element.sequence.run metadata bytes = some raws := by + subst metadata + induction raws with + | nil => exact ⟨[], by simp [run, sequence, sequenceDecode]⟩ + | cons raw raws ih => + obtain ⟨head, acceptedHead⟩ := realizable raw (admitted raw (by simp)) + obtain ⟨tail, acceptedTail⟩ := ih (fun raw member => admitted raw (by simp [member])) + have headWidth := element.run_length _ head raw acceptedHead + have tailFacts := (element.sequence.run_eq_some_iff _ tail raws).mp acceptedTail + have width : (head ++ tail).length = + (raw :: raws |>.map element.metadata |>.map element.byteSize).sum := by + simp only [List.length_append, List.map_cons, List.sum_cons] + rw [headWidth, tailFacts.1] + rfl + have takeHead : (head ++ tail).take (element.byteSize (element.metadata raw)) = head := by + rw [← headWidth] + simp + have dropHead : (head ++ tail).drop (element.byteSize (element.metadata raw)) = tail := by + rw [← headWidth] + simp + refine ⟨head ++ tail, (element.sequence.run_eq_some_iff _ _ _).mpr ?_⟩ + refine ⟨width, ?_, rfl⟩ + change sequenceDecode element (element.metadata raw :: raws.map element.metadata) + (head ++ tail) = some (raw :: raws) + simp [sequenceDecode, takeHead, dropHead, acceptedHead, + show sequenceDecode element (raws.map element.metadata) tail = some raws from tailFacts.2.1] + +/-- Completeness composes both language and mathematical decoding at every +element's requested metadata. Rejection in either stage remains rejection. -/ +theorem sequence_completeWith [DecidableEq Metadata] (element : StorageDecoder Metadata Raw) + (decodeModel : Raw → Option Model) (complete : element.CompleteWith decodeModel) : + element.sequence.CompleteWith (List.mapM decodeModel) := by + intro metadata bytes width initialized + induction metadata generalizing bytes with + | nil => + have empty : bytes = [] := List.length_eq_zero_iff.mp (by simpa [sequence] using width) + subst bytes + exact ⟨[], by simp [runWith, run, sequence, sequenceDecode]⟩ + | cons metadata rest ih => + have totalWidth : bytes.length = + element.byteSize metadata + (rest.map element.byteSize).sum := by + simpa [sequence] using width + have sizeBound : element.byteSize metadata ≤ bytes.length := by omega + have headWidth : (bytes.take (element.byteSize metadata)).length = element.byteSize metadata := by + simp [List.length_take, Nat.min_eq_left sizeBound] + have tailWidth : (bytes.drop (element.byteSize metadata)).length = + element.sequence.byteSize rest := by + simp only [List.length_drop, sequence] + omega + have both : Rust.Storage.Initialized + (bytes.take (element.byteSize metadata) ++ bytes.drop (element.byteSize metadata)) := by + simpa using initialized + obtain ⟨model, acceptedHead⟩ := complete metadata _ headWidth ((initialized_append _ _).mp both).1 + obtain ⟨models, acceptedTail⟩ := ih _ tailWidth ((initialized_append _ _).mp both).2 + obtain ⟨raw, headLanguage, headModel⟩ := (element.runWith_eq_some_iff _ _ _ _).mp acceptedHead + obtain ⟨raws, tailLanguage, tailModel⟩ := + (element.sequence.runWith_eq_some_iff _ _ _ _).mp acceptedTail + have headMetadata := element.run_metadata _ _ _ headLanguage + have tailFacts := (element.sequence.run_eq_some_iff _ _ _).mp tailLanguage + refine ⟨model :: models, (element.sequence.runWith_eq_some_iff _ _ _ _).mpr ?_⟩ + refine ⟨raw :: raws, (element.sequence.run_eq_some_iff _ _ _).mpr ?_, ?_⟩ + · refine ⟨width, ?_, ?_⟩ + · change sequenceDecode element (metadata :: rest) bytes = some (raw :: raws) + simp [sequenceDecode, headLanguage, + show sequenceDecode element rest (bytes.drop (element.byteSize metadata)) = some raws from + tailFacts.2.1] + · change (raw :: raws).map element.metadata = metadata :: rest + simp only [List.map_cons, headMetadata] + exact congrArg (metadata :: ·) tailFacts.2.2 + · simp [List.mapM_cons, headModel, tailModel] + end StorageDecoder /-- Fixed-width decoding is the Unit-metadata case, with no metadata inferred @@ -598,4 +764,33 @@ theorem sliceDecoder_initialized (element : BitDecoder Raw) (initialized : eleme | none => simp [language] at accepted | some values => exact arrayDecoder_initialized element initialized count bytes values language +/-- The requested count remains observable even when all elements have size zero. -/ +theorem sliceDecoder_run_count (element : BitDecoder Raw) (count : Nat) (bytes : List AMByte) + (values : List Raw) (accepted : (sliceDecoder element).run count bytes = some values) : + values.length = count := + StorageDecoder.run_metadata (sliceDecoder element) count bytes values accepted + +/-- Element realizability supplies bytes at this exact count. It does not create +an element of an uninhabited type, and imposes no element obligation at count zero. -/ +theorem sliceDecoder_realizable (element : BitDecoder Raw) (valid : Raw → Prop) + (realizable : ∀ raw, valid raw → ∃ bytes, element.run bytes = some raw) + (count : Nat) (values : List Raw) (sameCount : values.length = count) + (admitted : ∀ value ∈ values, valid value) : + ∃ bytes, (sliceDecoder element).run count bytes = some values := by + obtain ⟨bytes, accepted⟩ := arrayDecoder_realizable element valid realizable values admitted + refine ⟨bytes, ?_⟩ + rw [← sameCount, sliceDecoder_run, accepted] + rfl + +/-- Every initialized representation at the explicit count admits a slice when +each element decoder is complete. No count is reconstructed from byte width. -/ +theorem sliceDecoder_complete (element : BitDecoder Raw) + (complete : ∀ bytes, bytes.length = element.byteSize → Initialized bytes → + ∃ raw, element.run bytes = some raw) + (count : Nat) (bytes : List AMByte) (width : bytes.length = count * element.byteSize) + (initialized : Initialized bytes) : + ∃ values, (sliceDecoder element).run count bytes = some values := by + obtain ⟨values, accepted⟩ := arrayDecoder_complete element complete count bytes width initialized + exact ⟨values.val, by rw [sliceDecoder_run, accepted]; rfl⟩ + end Rust.Storage diff --git a/anneal/lean/RustStorageTests.lean b/anneal/lean/RustStorageTests.lean index 5baaa60d0e..d827939b84 100644 --- a/anneal/lean/RustStorageTests.lean +++ b/anneal/lean/RustStorageTests.lean @@ -187,6 +187,135 @@ example : (sliceDecoder (statefulZstDecoder false)).run 1 [] = none := by decide example : (sliceDecoder (statefulZstDecoder false)).run 0 [] = some [] := by decide example : (sliceDecoder boolDecoder).Initialized := sliceDecoder_initialized _ boolDecoder_initialized +-- Count remains metadata when the representation has no bytes. +example : (sliceDecoder unitDecoder).byteSize 1 = (sliceDecoder unitDecoder).byteSize 7 := rfl +example (count : Nat) (bytes : List AMByte) (values : List Unit) + (accepted : (sliceDecoder unitDecoder).run count bytes = some values) : + values.length = count := sliceDecoder_run_count unitDecoder count bytes values accepted + +def emptyElementDecoder : BitDecoder Empty where + byteSize := 0 + decode _ := none + +example : (sliceDecoder emptyElementDecoder).run 0 [] = some [] := rfl +example : (sliceDecoder emptyElementDecoder).run 1 [] = none := by decide + +-- Any decoder of an empty type must reject a positive count, independent of width. +example (element : BitDecoder Empty) (count : Nat) (bytes : List AMByte) : + (sliceDecoder element).run (count + 1) bytes = none := by + cases decoded : (sliceDecoder element).run (count + 1) bytes with + | none => rfl + | some values => + have length := sliceDecoder_run_count element (count + 1) bytes values decoded + cases values with + | nil => simp at length + | cons value _ => exact nomatch value + +-- Missing language semantics propagate failure; width and initialization do not supply them. +def unknownElementDecoder : BitDecoder Unit where + byteSize := 0 + decode _ := none + +example : (sliceDecoder unknownElementDecoder).run 1 [] = none := by decide +example : (sliceDecoder unknownElementDecoder).runWith some 1 [] = none := by decide +example : ¬ (sliceDecoder unknownElementDecoder).CompleteWith some := by + intro complete + obtain ⟨value, accepted⟩ := complete 1 [] rfl initialized_nil + simp [StorageDecoder.runWith, sliceDecoder_run, BitDecoder.run, arrayDecoder, + arrayDecode, unknownElementDecoder] at accepted + +-- Realizability accepts the empty slice without an inhabitant of its element type. +example : ∃ bytes, (sliceDecoder emptyElementDecoder).run 0 bytes = some [] := + sliceDecoder_realizable emptyElementDecoder (fun _ => True) + (fun value _ => nomatch value) 0 [] rfl (by simp) + +-- Restricted element validity need only realize the values it admits. +example (values : List Bool) (admitted : ∀ value ∈ values, value = true) : ∃ bytes, + (sliceDecoder (boolDecoder.filterMap (fun value => if value then some value else none))).run + values.length bytes = some values := by + apply sliceDecoder_realizable _ (fun value => value = true) ?_ _ values rfl + · exact admitted + · intro value valid + subst value + exact ⟨[AMByte.init 1], by decide⟩ + +example (count : Nat) (bytes : List AMByte) (width : bytes.length = count) + (initialized : Initialized bytes) : + ∃ values, (sliceDecoder byteDecoder).run count bytes = some values := + sliceDecoder_complete byteDecoder byteDecoder_complete count bytes (by simpa [byteDecoder] using width) initialized + +example (count : Nat) : ∃ values, (sliceDecoder unitDecoder).run count [] = some values := + sliceDecoder_complete unitDecoder + (fun bytes width _ => ⟨(), emptyDecoder_complete () bytes width⟩) + count [] (by simp [unitDecoder, emptyDecoder]) initialized_nil + +-- Returned list length is checked independently of its zero-byte width. +def wrongSliceCountDecoder : StorageDecoder Nat (List Unit) where + byteSize _ := 0 + metadata := List.length + decode _ _ := some [] + +example : wrongSliceCountDecoder.decode 1 [] = some [] := rfl +example : wrongSliceCountDecoder.run 0 [] = some [] := by decide +example : wrongSliceCountDecoder.run 1 [] = none := by decide + +-- Nested indexed decoders retain every element's own metadata and byte boundary. +example : (sliceDecoder boolDecoder).sequence.run [2, 0, 1] + [AMByte.init 1, AMByte.init 0, AMByte.init 1] = some [[true, false], [], [true]] := by decide +example : (sliceDecoder boolDecoder).sequence.run [2, 0, 1] + [AMByte.init 1, AMByte.init 0] = none := by decide +example : (sliceDecoder boolDecoder).sequence.run [2, 0, 1] + [AMByte.init 1, AMByte.init 0, AMByte.init 2] = none := by decide +example : (sliceDecoder boolDecoder).sequence.Initialized := + StorageDecoder.sequence_initialized _ (sliceDecoder_initialized _ boolDecoder_initialized) + +-- Equal zero-byte widths preserve both the outer count and each inner count. +example : (sliceDecoder unitDecoder).sequence.byteSize [0, 2] = + (sliceDecoder unitDecoder).sequence.byteSize [2, 0] := rfl +example : (sliceDecoder unitDecoder).sequence.run [0, 2] [] = some [[], [(), ()]] := by decide +example : (sliceDecoder unitDecoder).sequence.run [2, 0] [] = some [[(), ()], []] := by decide +example (metadata : List Nat) (bytes : List AMByte) (raws : List (List Unit)) + (accepted : (sliceDecoder unitDecoder).sequence.run metadata bytes = some raws) : + raws.length = metadata.length := StorageDecoder.sequence_run_count _ metadata bytes raws accepted + +-- Empty inner slices require no element; a positive inner count still fails closed. +example : (sliceDecoder emptyElementDecoder).sequence.run [0, 0] [] = some [[], []] := by decide +example : (sliceDecoder emptyElementDecoder).sequence.run [0, 1] [] = none := by decide +example : (sliceDecoder unknownElementDecoder).sequence.run [0, 1] [] = none := by decide +example : wrongSliceCountDecoder.sequence.run [0] [] = some [[]] := by decide +example : wrongSliceCountDecoder.sequence.run [1] [] = none := by decide + +example (values : List (List Unit)) : ∃ bytes, + (sliceDecoder unitDecoder).sequence.run (values.map List.length) bytes = some values := by + refine StorageDecoder.sequence_realizable _ (fun _ => True) ?_ _ values rfl (by simp) + intro value _ + refine sliceDecoder_realizable unitDecoder (fun _ => True) ?_ _ value rfl (by simp) + intro value _ + cases value + exact ⟨[], rfl⟩ + +-- Completeness retains both stages of nested decoding, including empty sublists. +example : (sliceDecoder byteDecoder).sequence.CompleteWith (List.mapM some) := + StorageDecoder.sequence_completeWith _ some (by + intro count bytes width initialized + obtain ⟨values, accepted⟩ := sliceDecoder_complete byteDecoder byteDecoder_complete count bytes width initialized + exact ⟨values, by simp [StorageDecoder.runWith, accepted]⟩) + +example : ¬ (sliceDecoder unknownElementDecoder).sequence.CompleteWith (List.mapM some) := by + intro complete + obtain ⟨value, accepted⟩ := complete [0, 1] [] rfl initialized_nil + have rejected : (sliceDecoder unknownElementDecoder).sequence.run [0, 1] [] = none := by decide + simp [StorageDecoder.runWith, rejected] at accepted + +#print axioms arrayDecoder_realizable +#print axioms sliceDecoder_realizable +#print axioms sliceDecoder_complete +#print axioms sliceDecoder_run_count +#print axioms StorageDecoder.sequence_run_count +#print axioms StorageDecoder.sequence_initialized +#print axioms StorageDecoder.sequence_realizable +#print axioms StorageDecoder.sequence_completeWith + -- These synthetic layouts share a padded width for multiple metadata values. -- The example establishes no Rust representation or ABI for a particular type. def plateauDecoder : StorageDecoder Nat Nat where