Lax58.WordArena

Distinguished immutable word arenas

concepts/Lax58/WordArena.lean · lax-58

proven

Loading review…

Concept map

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

Evidence

This concept declares 12 statements. Each proof establishes one of them relative to its assumptions.

Definition and theorem

Every universal structural value has a distinguished dense postorder arena using three natural-number words per node. Natural leaves store a tag, payload, and padding word; pairs store a tag and two addresses of previously stored children. The root address is supplied as one additional word.

The explicit encoder determines every stored word. Density separately says that it adds no unreachable auxiliary blocks. The semantic representation relation, exact footprint, and explicit payload and address-space hypotheses form the public interface. The distinguished Lax-13 input is the root word followed by the arena words on the machine's read-only input tape. No whole-memory decoder, uniqueness of arbitrary physical layouts, mutation semantics, or operation-cost model is imposed.

Lean source view on GitHub

1	import Lax58.StructuralPresentation
2
3	/-!
4	---
5	title: Distinguished immutable word arenas
6	type: definition and theorem
7	---
8
9	Every universal structural value has a distinguished dense postorder arena
10	using three natural-number words per node. Natural leaves store a tag, payload,
11	and padding word; pairs store a tag and two addresses of previously stored
12	children. The root address is supplied as one additional word.
13
14	The explicit encoder determines every stored word. Density separately says
15	that it adds no unreachable auxiliary blocks. The semantic representation
16	relation, exact footprint, and explicit payload and address-space hypotheses
17	form the public interface. The distinguished Lax-13 input is the root word
18	followed by the arena words on the machine's read-only input tape. No whole-memory
19	decoder, uniqueness of arbitrary physical layouts, mutation semantics, or
20	operation-cost model is imposed.
21	-/
22
23	namespace Lax58.WordArena
24
25	open Lax58.StructuralPresentation
26
27	universe u
28
29	/-- A finite array of unbounded natural-number words. -/
30	abbrev WordMemory := Array Nat
31
32	/-- A closed word array together with its distinguished root address. -/
33	structure WordImage where
34	memory : WordMemory
35	root : Nat
36	deriving DecidableEq
37
38	namespace WordImage
39
40	/-- Number of words in the memory array. -/
41	def memoryWords (I : WordImage) : Nat := I.memory.size
42
43	/-- Total supplied words, including the separately supplied root. -/
44	def totalWords (I : WordImage) : Nat := I.memoryWords + 1
45
46	/-- The distinguished Lax-13 input tape: root, followed by all arena words. -/
47	def toInput (I : WordImage) : List Nat := I.root :: I.memory.toList
48
49	/-- The memory array fits in the address space of `w`-bit words. -/
50	def AddressSpaceFits (I : WordImage) (w : Nat) : Prop :=
51	I.memoryWords ≤ 2 ^ w
52
53	/-- Every supplied word, including the root, fits in `w` bits. -/
54	def ValuesFitInWord (I : WordImage) (w : Nat) : Prop :=
55	∀ x ∈ I.toInput, x < 2 ^ w
56
57	/-- Both the address space and all supplied word values fit at width `w`. -/
58	def FitsInWord (I : WordImage) (w : Nat) : Prop :=
59	I.AddressSpaceFits w ∧ I.ValuesFitInWord w
60
61	/-- The word at an in-bounds arena address. -/
62	def wordAt? (I : WordImage) (address : Nat) : Option Nat :=
63	I.memory[address]?
64
65	/-- Start of a complete aligned three-word arena block. -/
66	def ValidAddress (I : WordImage) (address : Nat) : Prop :=
67	address % 3 = 0 ∧ address + 2 < I.memoryWords
68
69	/-- Tag of a natural-payload block. -/
70	def natTag : Nat := 0
71
72	/-- Tag of a binary-pair block. -/
73	def pairTag : Nat := 1
74
75	/-- A block rooted at an address semantically represents a structural value. -/
76	inductive Represents (I : WordImage) : Nat → Raw → Prop where
77	\| nat {address payload : Nat}
78	(address_valid : I.ValidAddress address)
79	(tag : I.wordAt? address = some natTag)
80	(value : I.wordAt? (address + 1) = some payload)
81	(padding : I.wordAt? (address + 2) = some 0) :
82	I.Represents address (.nat payload)
83	\| pair {address leftAddress rightAddress : Nat} {left right : Raw}
84	(address_valid : I.ValidAddress address)
85	(tag : I.wordAt? address = some pairTag)
86	(left_reference : I.wordAt? (address + 1) = some leftAddress)
87	(right_reference : I.wordAt? (address + 2) = some rightAddress)
88	(left_value : I.Represents leftAddress left)
89	(right_value : I.Represents rightAddress right) :
90	I.Represents address (.pair left right)
91
92	/-- A pair block directly refers to one valid child block. -/
93	inductive ChildAddress (I : WordImage) : Nat → Nat → Prop where
94	\| left {parent child : Nat}
95	(parent_valid : I.ValidAddress parent)
96	(child_valid : I.ValidAddress child)
97	(tag : I.wordAt? parent = some pairTag)
98	(reference : I.wordAt? (parent + 1) = some child) :
99	I.ChildAddress parent child
100	\| right {parent child : Nat}
101	(parent_valid : I.ValidAddress parent)
102	(child_valid : I.ValidAddress child)
103	(tag : I.wordAt? parent = some pairTag)
104	(reference : I.wordAt? (parent + 2) = some child) :
105	I.ChildAddress parent child
106
107	/-- Addresses reachable from a chosen root by following child references. -/
108	inductive ReachableFrom (I : WordImage) (root : Nat) : Nat → Prop where
109	\| root : I.ReachableFrom root root
110	\| child {parent child : Nat}
111	(parent_reachable : I.ReachableFrom root parent)
112	(child_address : I.ChildAddress parent child) :
113	I.ReachableFrom root child
114
115	/-- Every aligned block is meaningful and all child references are valid. -/
116	def BlocksWellFormed (I : WordImage) : Prop :=
117	I.memoryWords % 3 = 0 ∧
118	∀ address, I.ValidAddress address → ∃ raw, I.Represents address raw
119
120	/-- Every block is valid and the distinguished root represents a value. -/
121	def RootedWellFormed (I : WordImage) : Prop :=
122	I.BlocksWellFormed ∧ ∃ raw, I.Represents I.root raw
123
124	/-- Every complete block is reachable from the distinguished root. -/
125	def Dense (I : WordImage) : Prop :=
126	∀ address, I.ValidAddress address → I.ReachableFrom I.root address
127
128	end WordImage
129
130	/-- Append the postorder arena of a raw value and return its root address. -/
131	def encodeInto : Raw → WordMemory → WordMemory × Nat
132	\| .nat payload, memory =>
133	let address := memory.size
134	(memory.push WordImage.natTag \|>.push payload \|>.push 0, address)
135	\| .pair left right, memory =>
136	let (memory, leftAddress) := encodeInto left memory
137	let (memory, rightAddress) := encodeInto right memory
138	let address := memory.size
139	(memory.push WordImage.pairTag \|>.push leftAddress \|>.push rightAddress, address)
140
141	/-- Distinguished closed postorder arena of a structural value. -/
142	def encodeRaw (raw : Raw) : WordImage :=
143	let (memory, root) := encodeInto raw #[]
144	{ memory, root }
145
146	/-- Distinguished arena of a value through a named structural presentation. -/
147	def encode {α : Type u} (P : Presentation α) (x : α) : WordImage :=
148	encodeRaw (P.toRaw x)
149
150	/-- An input word is exactly the distinguished arena input of the presented
151	value; no extra prefix, suffix, or advice is permitted. -/
152	def ArenaInput {α : Type u} (P : Presentation α) (x : α)
153	(input : List Nat) : Prop :=
154	input = (encode P x).toInput
155
156	axiom encodeRaw_represents (raw : Raw) :
157	(encodeRaw raw).Represents (encodeRaw raw).root raw
158
159	axiom encodeRaw_wellFormed (raw : Raw) :
160	(encodeRaw raw).RootedWellFormed
161
162	axiom encodeRaw_dense (raw : Raw) :
163	(encodeRaw raw).Dense
164
165	axiom encodeRaw_memoryWords (raw : Raw) :
166	(encodeRaw raw).memoryWords = 3 * raw.nodes
167
168	axiom encodeRaw_totalWords (raw : Raw) :
169	(encodeRaw raw).totalWords = 3 * raw.nodes + 1
170
171	axiom encodeRaw_toInput_length (raw : Raw) :
172	(encodeRaw raw).toInput.length = 3 * raw.nodes + 1
173
174	axiom encodeRaw_fits (raw : Raw) (w : Nat) :
175	raw.PayloadsFitInWord w →
176	3 * raw.nodes ≤ 2 ^ w →
177	(encodeRaw raw).FitsInWord w
178
179	axiom encode_represents {α : Type u} (P : Presentation α) (x : α) :
180	(encode P x).Represents (encode P x).root (P.toRaw x)
181
182	axiom encode_memoryWords {α : Type u} (P : Presentation α) (x : α) :
183	(encode P x).memoryWords = 3 * P.structuralSize x
184
185	axiom encode_totalWords {α : Type u} (P : Presentation α) (x : α) :
186	(encode P x).totalWords = 3 * P.structuralSize x + 1
187
188	axiom encode_toInput_length {α : Type u} (P : Presentation α) (x : α) :
189	(encode P x).toInput.length = 3 * P.structuralSize x + 1
190
191	axiom encode_fits {α : Type u} (P : Presentation α) (x : α) (w : Nat) :
192	P.PayloadsFitInWord x w →
193	3 * P.structuralSize x ≤ 2 ^ w →
194	(encode P x).FitsInWord w
195
196	end Lax58.WordArena
197

Show ProofShow ProofShow ProofShow ProofShow ProofShow ProofShow ProofShow ProofShow ProofShow ProofShow ProofShow Proof

Builds on

Lax58.StructuralPresentation

Used by

From Mathlib

none

Community review

Discussion

Ask a question or add context. Endorsements and structured flags are kept in the review panel above; your ORCID profile must share a public name.

0 comments

Loading discussion…

Lax Lean Archive

Distinguished immutable word arenas

Flags

Flag this concept

Concept map

Evidence

1st statement `encode_fits` proven

2nd statement `encode_memoryWords` proven

3rd statement `encode_represents` proven

4th statement `encode_toInput_length` proven

5th statement `encode_totalWords` proven

6th statement `encodeRaw_dense` proven

7th statement `encodeRaw_fits` proven

8th statement `encodeRaw_memoryWords` proven

9th statement `encodeRaw_represents` proven

10th statement `encodeRaw_toInput_length` proven

11th statement `encodeRaw_totalWords` proven

12th statement `encodeRaw_wellFormed` proven

Definition and theorem

Lean source view on GitHub

Builds on

Used by

From Mathlib

Discussion

Settings