From 04257d445609bac4dd763c69640b203e206b4c6b Mon Sep 17 00:00:00 2001 From: Josh Liebow-Feeser Date: Thu, 15 Oct 2026 14:42:14 -0400 Subject: [PATCH] Model referent validity as byte-domain inclusion Add a shared algebra for uninitialized, initialized, and safe referent contents at an explicit byte width. Safe contents must pass both physical and mathematical decoding. This permits empty valid domains without an inhabitedness premise or a preferred representation. Prove the basic weakening, completeness, wrapper-domain, and initialized subrange rules. Transfers are conditional on equal endpoint widths, so composition also requires equal source and intermediate widths. Add a counterexample protecting that premise, plus invalid-boolean and empty-type tests. These are content facts; memory access and resource obligations remain separate. gherrit-pr-id: Gkc7ajwbs2rni7qu5gz3sdcm7457o6iuf Agent-authored-by: AI agent acting on joshlf's behalf --- anneal/lean/Rust.lean | 1 + anneal/lean/Rust/Referent.lean | 197 ++++++++++++++++++++++++++++ anneal/lean/Rust/ReferentTests.lean | 132 +++++++++++++++++++ anneal/lean/RustStorageTests.lean | 1 + 4 files changed, 331 insertions(+) create mode 100644 anneal/lean/Rust/Referent.lean create mode 100644 anneal/lean/Rust/ReferentTests.lean diff --git a/anneal/lean/Rust.lean b/anneal/lean/Rust.lean index 8ad93c4955..9199e7b863 100644 --- a/anneal/lean/Rust.lean +++ b/anneal/lean/Rust.lean @@ -11,6 +11,7 @@ import Rust.Memory import Rust.Pointer import Rust.Bytes import Rust.Storage +import Rust.Referent import Rust.Arithmetic /-! diff --git a/anneal/lean/Rust/Referent.lean b/anneal/lean/Rust/Referent.lean new file mode 100644 index 0000000000..88d4920882 --- /dev/null +++ b/anneal/lean/Rust/Referent.lean @@ -0,0 +1,197 @@ +/- Copyright 2026 The Fuchsia Authors + +Licensed under a BSD-style license , Apache License, Version 2.0 +, or the MIT +license , at your option. +This file may not be copied, modified, or distributed except according to +those terms. -/ + +module +public import Rust.Storage +@[expose] public section + +/-! +A referent state admits a domain of byte lists at an explicit width. `safe` +requires an admitted value; `initialized` requires only initialized bytes; and +`uninit` places no restriction on byte contents. Width remains a requirement in +all three states. These are pure facts about numeric bytes. A consumer must +separately justify any Rust memory, ownership, or pointer interpretation. + +`Transfer` describes a directional inclusion of domains when widths agree. A +width mismatch makes that implication vacuous, so composition needs evidence +that the intermediate width agrees. `Safe` supplies a reusable domain from a +storage decoder and a mathematical decoder; neither must choose an encoding. +-/ + +namespace Rust.Referent + +open Rust.Storage + +/-- The byte-content promise attached to a referent. -/ +inductive State where + | uninit + | initialized + | safe + deriving DecidableEq, Repr + +/-- Both decoding stages must succeed on this particular representation. +The witnesses need not describe a canonical representation or an inhabited type. -/ +def Safe [DecidableEq Metadata] (decoder : StorageDecoder Metadata Raw) + (decodeModel : Raw → Option Model) (metadata : Metadata) (bytes : List AMByte) : Prop := + ∃ raw value, decoder.run metadata bytes = some raw ∧ decodeModel raw = some value + +theorem safe_iff_runWith [DecidableEq Metadata] (decoder : StorageDecoder Metadata Raw) + (decodeModel : Raw → Option Model) (metadata : Metadata) (bytes : List AMByte) : + Safe decoder decodeModel metadata bytes ↔ + ∃ value, decoder.runWith decodeModel metadata bytes = some value := by + simp only [StorageDecoder.runWith_eq_some_iff, Safe] + constructor + · rintro ⟨raw, value, language, model⟩ + exact ⟨value, raw, language, model⟩ + · rintro ⟨value, raw, language, model⟩ + exact ⟨raw, value, language, model⟩ + +theorem safe_length [DecidableEq Metadata] (decoder : StorageDecoder Metadata Raw) + (decodeModel : Raw → Option Model) (metadata : Metadata) (bytes : List AMByte) + (admitted : Safe decoder decodeModel metadata bytes) : + bytes.length = decoder.byteSize metadata := by + obtain ⟨raw, _, language, _⟩ := admitted + exact decoder.run_length metadata bytes raw language + +theorem safe_initialized [DecidableEq Metadata] (decoder : StorageDecoder Metadata Raw) + (decodeModel : Raw → Option Model) (initialized : decoder.Initialized) + (metadata : Metadata) (bytes : List AMByte) + (admitted : Safe decoder decodeModel metadata bytes) : Initialized bytes := by + obtain ⟨raw, _, language, _⟩ := admitted + exact initialized metadata bytes raw language + +/-- A state always describes exactly the requested number of bytes. +In particular, `uninit` permits initialized bytes as well as uninitialized bytes. -/ +def Allowed (width : Nat) (safe : List AMByte → Prop) (state : State) + (bytes : List AMByte) : Prop := + bytes.length = width ∧ match state with + | .uninit => True + | .initialized => Initialized bytes + | .safe => safe bytes + +/-- Transfer retains the bytes and changes only the promise they satisfy. +The width guard is conditional: this relation does not itself prove equal sizes. -/ +def Transfer (sourceWidth : Nat) (sourceSafe : List AMByte → Prop) (sourceState : State) + (destinationWidth : Nat) (destinationSafe : List AMByte → Prop) + (destinationState : State) : Prop := + sourceWidth = destinationWidth → ∀ bytes, + Allowed sourceWidth sourceSafe sourceState bytes → + Allowed destinationWidth destinationSafe destinationState bytes + +/-- A language decoder that requires initialization lets safe bytes be read as +initialized bytes. The mathematical decoder may still reject other bytes. -/ +theorem safe_to_initialized [DecidableEq Metadata] + (decoder : StorageDecoder Metadata Raw) (decodeModel : Raw → Option Model) + (initialized : decoder.Initialized) (metadata : Metadata) + (destinationWidth : Nat) (destinationSafe : List AMByte → Prop) : + Transfer (decoder.byteSize metadata) (Safe decoder decodeModel metadata) .safe + destinationWidth destinationSafe .initialized := by + intro sameWidth bytes admitted + exact ⟨admitted.1.trans sameWidth, + safe_initialized decoder decodeModel initialized metadata bytes admitted.2⟩ + +/-- Initialization suffices for safe admission only when both decoding stages +are complete for every initialized representation of the requested width. -/ +theorem initialized_to_safe [DecidableEq Metadata] + (decoder : StorageDecoder Metadata Raw) (decodeModel : Raw → Option Model) + (complete : decoder.CompleteWith decodeModel) (metadata : Metadata) + (sourceWidth : Nat) (sourceSafe : List AMByte → Prop) : + Transfer sourceWidth sourceSafe .initialized + (decoder.byteSize metadata) (Safe decoder decodeModel metadata) .safe := by + intro sameWidth bytes admitted + have width := admitted.1.trans sameWidth + exact ⟨width, (safe_iff_runWith decoder decodeModel metadata bytes).mpr + (complete metadata bytes width admitted.2)⟩ + +theorem initialized_identity (sourceWidth destinationWidth : Nat) + (sourceSafe destinationSafe : List AMByte → Prop) : + Transfer sourceWidth sourceSafe .initialized destinationWidth destinationSafe .initialized := by + intro sameWidth bytes admitted + exact ⟨admitted.1.trans sameWidth, admitted.2⟩ + +/-- Forgetting a byte-content promise leaves only the width requirement. -/ +theorem to_uninit (sourceWidth destinationWidth : Nat) + (sourceSafe destinationSafe : List AMByte → Prop) (sourceState : State) : + Transfer sourceWidth sourceSafe sourceState destinationWidth destinationSafe .uninit := by + intro sameWidth bytes admitted + exact ⟨admitted.1.trans sameWidth, trivial⟩ + +theorem transfer_refl (width : Nat) (safe : List AMByte → Prop) (state : State) : + Transfer width safe state width safe state := by + intro _ _ admitted + exact admitted + +/-- The intermediate width must agree with the source width. Otherwise either +input transfer can hold solely because its own width guard is false. -/ +theorem transfer_trans + (sourceWidth middleWidth destinationWidth : Nat) + (sourceSafe middleSafe destinationSafe : List AMByte → Prop) + (sourceState middleState destinationState : State) + (first : Transfer sourceWidth sourceSafe sourceState middleWidth middleSafe middleState) + (second : Transfer middleWidth middleSafe middleState + destinationWidth destinationSafe destinationState) + (middleWidthAgrees : sourceWidth = middleWidth) : + Transfer sourceWidth sourceSafe sourceState destinationWidth destinationSafe destinationState := by + intro sameWidth bytes admitted + exact second (middleWidthAgrees.symm.trans sameWidth) bytes + (first middleWidthAgrees bytes admitted) + +/-- Replacing either safe predicate by an equivalent domain preserves transfer. +This supports transparent mathematical wrappers without a registry of wrappers. -/ +theorem allowed_congr (width : Nat) (left right : List AMByte → Prop) + (equivalent : ∀ bytes, left bytes ↔ right bytes) (state : State) (bytes : List AMByte) : + Allowed width left state bytes ↔ Allowed width right state bytes := by + cases state <;> simp only [Allowed] + exact and_congr_right (fun _ => equivalent bytes) + +/-- Safe domains transfer by predicate inclusion at the actual source width. +Wrappers can establish this premise directly from their decoding definitions. -/ +theorem safe_transfer_of_implication (sourceWidth destinationWidth : Nat) + (sourceSafe destinationSafe : List AMByte → Prop) + (preserves : ∀ bytes, bytes.length = sourceWidth → sourceSafe bytes → destinationSafe bytes) : + Transfer sourceWidth sourceSafe .safe destinationWidth destinationSafe .safe := by + intro sameWidth bytes admitted + exact ⟨admitted.1.trans sameWidth, preserves bytes admitted.1 admitted.2⟩ + +/-- Initialization is inherited by any sublist, including a contiguous range. -/ +theorem initialized_sublist (bytes subrange : List AMByte) + (initialized : Initialized bytes) (contained : subrange.Sublist bytes) : Initialized subrange := by + intro byte member + exact initialized byte (contained.subset member) + +theorem initialized_take (bytes : List AMByte) (initialized : Initialized bytes) (count : Nat) : + Initialized (bytes.take count) := + initialized_sublist bytes _ initialized (List.take_sublist count bytes) + +theorem initialized_drop (bytes : List AMByte) (initialized : Initialized bytes) (count : Nat) : + Initialized (bytes.drop count) := + initialized_sublist bytes _ initialized (List.drop_sublist count bytes) + +/-- A range is the requested prefix after skipping its starting position. -/ +theorem initialized_subrange (bytes : List AMByte) (initialized : Initialized bytes) + (start count : Nat) : Initialized ((bytes.drop start).take count) := + initialized_take _ (initialized_drop bytes initialized start) count + +/-- Splicing initialized bytes into initialized storage preserves initialization. +The separate length premise in `initialized_replace_length` preserves the width. -/ +theorem initialized_replace (bytes replacement : List AMByte) + (initialized : Initialized bytes) (replacementInitialized : Initialized replacement) + (start count : Nat) : + Initialized (bytes.take start ++ replacement ++ bytes.drop (start + count)) := by + exact (initialized_append _ _).mpr + ⟨(initialized_append _ _).mpr + ⟨initialized_take bytes initialized start, replacementInitialized⟩, + initialized_drop bytes initialized (start + count)⟩ + +theorem initialized_replace_length (bytes replacement : List AMByte) (start count : Nat) + (within : start + count ≤ bytes.length) (sameLength : replacement.length = count) : + (bytes.take start ++ replacement ++ bytes.drop (start + count)).length = bytes.length := by + simp only [List.length_append, List.length_take, List.length_drop, sameLength] + omega + +end Rust.Referent diff --git a/anneal/lean/Rust/ReferentTests.lean b/anneal/lean/Rust/ReferentTests.lean new file mode 100644 index 0000000000..6da6be6793 --- /dev/null +++ b/anneal/lean/Rust/ReferentTests.lean @@ -0,0 +1,132 @@ +/- Copyright 2026 The Fuchsia Authors + +Licensed under a BSD-style license , Apache License, Version 2.0 +, or the MIT +license , at your option. +This file may not be copied, modified, or distributed except according to +those terms. -/ + +module +import Rust.Referent + +/-! +These examples check the boundary of the byte-domain rules. In particular, +neither initialization nor an empty safe domain supplies a mathematical value. +The final example explains why transfer composition requires equal intermediate +widths even though each individual transfer is conditional on equal widths. +-/ + +namespace Rust.Referent.Tests + +open Rust.Storage + +def safeBool : List AMByte → Prop := + Safe boolDecoder.asStorageDecoder (fun value => some value) () + +theorem two_initialized : Initialized [AMByte.init 2] := by + simp [Initialized] + +theorem two_not_safe_bool : ¬safeBool [AMByte.init 2] := by + rintro ⟨raw, _, accepted, _⟩ + rw [BitDecoder.run_asStorageDecoder, boolDecoder_run_two] at accepted + contradiction + +/-- A byte has an initialized value even when it is not a valid boolean. -/ +theorem initialization_does_not_imply_safety : + ¬Transfer 1 safeBool .initialized 1 safeBool .safe := by + intro transfer + exact two_not_safe_bool (transfer rfl [AMByte.init 2] ⟨rfl, two_initialized⟩).2 + +example : Transfer 1 safeBool .safe 1 safeBool .initialized := + safe_to_initialized boolDecoder.asStorageDecoder (fun value => some value) + (boolDecoder.asStorageDecoder_initialized boolDecoder_initialized) () 1 safeBool + +example : Transfer 1 safeBool .initialized 1 safeBool .initialized := + initialized_identity 1 1 safeBool safeBool + +example (state : State) : Transfer 1 safeBool state 1 safeBool .uninit := + to_uninit 1 1 safeBool safeBool state + +def safeByte : List AMByte → Prop := + Safe byteDecoder.asStorageDecoder (fun value => some value) () + +theorem byte_complete : + byteDecoder.asStorageDecoder.CompleteWith (fun value => some value) := by + intro metadata bytes width initialized + cases metadata + obtain ⟨value, accepted⟩ := byteDecoder_complete bytes width initialized + exact ⟨value, by simp [StorageDecoder.runWith, accepted]⟩ + +example : Transfer 1 safeBool .initialized 1 safeByte .safe := + initialized_to_safe byteDecoder.asStorageDecoder (fun value => some value) + byte_complete () 1 safeBool + +example : Transfer 1 safeBool .safe 1 safeByte .safe := + transfer_trans 1 1 1 safeBool safeBool safeByte .safe .initialized .safe + (safe_to_initialized boolDecoder.asStorageDecoder (fun value => some value) + (boolDecoder.asStorageDecoder_initialized boolDecoder_initialized) () 1 safeBool) + (initialized_to_safe byteDecoder.asStorageDecoder (fun value => some value) + byte_complete () 1 safeBool) rfl + +example : Transfer 1 safeBool .safe 1 (fun bytes => safeBool bytes ∨ safeByte bytes) .safe := + safe_transfer_of_implication 1 1 _ _ (fun _ _ admitted => Or.inl admitted) + +/-- A zero-byte layout does not create a value of an empty type. -/ +def noValueDecoder : StorageDecoder Unit Empty where + byteSize _ := 0 + metadata value := nomatch value + decode _ _ := none + +def noValueModel (value : Empty) : Option Empty := nomatch value + +theorem no_value_safe_empty (bytes : List AMByte) : + ¬Safe noValueDecoder noValueModel () bytes := by + rintro ⟨raw, _⟩ + exact nomatch raw + +/-- An empty source domain entails every destination predicate, vacuously. -/ +theorem no_value_safe_transfer (width : Nat) (destination : List AMByte → Prop) : + Transfer 0 (Safe noValueDecoder noValueModel ()) .safe width destination .safe := by + intro _ bytes admitted + exact False.elim (no_value_safe_empty bytes admitted.2) + +/-- Completeness still needs a decoded value for the initialized empty list. -/ +theorem no_value_not_complete : ¬noValueDecoder.CompleteWith noValueModel := by + intro complete + obtain ⟨value, _⟩ := complete () [] rfl initialized_nil + exact nomatch value + +example : Initialized + (([AMByte.init 0, AMByte.init 1, AMByte.init 2].drop 1).take 1) := + initialized_subrange _ (by simp [Initialized]) 1 1 + +example : Initialized + ([AMByte.init 0, AMByte.init 1].take 1 ++ [AMByte.init 2] ++ + [AMByte.init 0, AMByte.init 1].drop (1 + 1)) := + initialized_replace _ _ (by simp [Initialized]) (by simp [Initialized]) 1 1 + +/-- Both premises hold because their widths differ. The conclusion has equal +widths and fails on a one-byte list, so unconditional transitivity is false. -/ +theorem intermediate_width_is_necessary : + Transfer 1 (fun _ => True) .safe 0 (fun _ => False) .safe ∧ + Transfer 0 (fun _ => False) .safe 1 (fun _ => False) .safe ∧ + ¬Transfer 1 (fun _ => True) .safe 1 (fun _ => False) .safe := by + refine ⟨?_, ?_, ?_⟩ + · intro impossible + omega + · intro impossible + omega + · intro transfer + exact (transfer rfl [AMByte.init 2] ⟨rfl, trivial⟩).2 + +#print axioms safe_to_initialized +#print axioms initialized_to_safe +#print axioms initialized_identity +#print axioms to_uninit +#print axioms transfer_trans +#print axioms initialized_subrange +#print axioms initialized_replace +#print axioms intermediate_width_is_necessary +#print axioms no_value_not_complete + +end Rust.Referent.Tests diff --git a/anneal/lean/RustStorageTests.lean b/anneal/lean/RustStorageTests.lean index 43637a1c88..5baaa60d0e 100644 --- a/anneal/lean/RustStorageTests.lean +++ b/anneal/lean/RustStorageTests.lean @@ -7,6 +7,7 @@ This file may not be copied, modified, or distributed except according to those terms. -/ module +import Rust.ReferentTests import Rust.Storage namespace Rust.Storage.Tests