Shared unweighted graph representation, paths, and call-cost specifications
DefinitionCLRS_Graph_InputThis shared module defines a finite directed graph by adjacency lists on vertices 0,…,n−1. Parallel arcs count separately in m, the sum of row lengths; self-loops are allowed. It connects that graph to an allocated UnweightedGraph object with arrays of adjacency arrays and degrees. It defines edge-counted walks, reachability, shortest distance, mutual reachability, root permutations, and transposition preserving arc multiplicity. Caller-storage preservation includes all initially allocated sequences, objects, and collections, monotone allocation counters, nondecreasing graph_work, and unchanged other clocks. Freshness and distinctness predicates specify result allocation. The generated constructor semantics and public field interfaces are included. These are definitions, not proofs of traversal correctness.
import Definitions.Def_Algo2LeanLib_Modules
import Mathlib.Data.List.Range
import Mathlib.Algebra.BigOperators.Group.Finset.Basic
set_option autoImplicit true
set_option backward.isDefEq.respectTransparency false
set_option backward.defeqAttrib.useBackward true
-- Generated by Algo2Lean 0.1.4 https://github.com/lunjiah/algo2lean
namespace Algo.«graph_input»
open _root_.Algo2LeanGenerated
-- Independently compiled module; imported algorithms keep their own transitions.
namespace Algo2LeanGenerated
abbrev Ref_UnweightedGraph := ObjectRef
-- Shallow class membership; fields and referenced objects are observed separately.
def is_UnweightedGraph (h : Heap) (ref : Ref_UnweightedGraph) : Prop :=
ref < h.nextObject ∧ h.objectClass ref = some "graph_input.UnweightedGraph"
instance (h : Heap) (ref : Ref_UnweightedGraph) : Decidable (is_UnweightedGraph h ref) :=
inferInstanceAs (Decidable (ref < h.nextObject ∧ h.objectClass ref = some "graph_input.UnweightedGraph"))
def field_UnweightedGraph_size (h : Heap) (ref : Ref_UnweightedGraph) : Option Int :=
if is_UnweightedGraph h ref then (h.readField ref "size").bind ObjectValue.asInt else none
def set_UnweightedGraph_size (h : Heap) (ref : Ref_UnweightedGraph) (value : Int) : Heap :=
h.writeField ref "size" (ObjectValue.intValue value)
@[simp] theorem field_UnweightedGraph_size_set (h : Heap) (ref : Ref_UnweightedGraph) (value : Int)
(valid : is_UnweightedGraph h ref) :
field_UnweightedGraph_size (set_UnweightedGraph_size h ref value) ref = some value := by
have valid' : is_UnweightedGraph (set_UnweightedGraph_size h ref value) ref := by
simpa [set_UnweightedGraph_size, is_UnweightedGraph] using valid
rw [field_UnweightedGraph_size, if_pos valid']
unfold set_UnweightedGraph_size
rw [Heap.readField_writeField_same h ref "size" _ "graph_input.UnweightedGraph" valid.2]
rfl
def field_UnweightedGraph_adj (h : Heap) (ref : Ref_UnweightedGraph) : Option CollectionRef :=
if is_UnweightedGraph h ref then (h.readField ref "adj").bind ObjectValue.asCollection else none
def set_UnweightedGraph_adj (h : Heap) (ref : Ref_UnweightedGraph) (value : CollectionRef) : Heap :=
h.writeField ref "adj" (ObjectValue.collectionValue value)
@[simp] theorem field_UnweightedGraph_adj_set (h : Heap) (ref : Ref_UnweightedGraph) (value : CollectionRef)
(valid : is_UnweightedGraph h ref) :
field_UnweightedGraph_adj (set_UnweightedGraph_adj h ref value) ref = some value := by
have valid' : is_UnweightedGraph (set_UnweightedGraph_adj h ref value) ref := by
simpa [set_UnweightedGraph_adj, is_UnweightedGraph] using valid
rw [field_UnweightedGraph_adj, if_pos valid']
unfold set_UnweightedGraph_adj
rw [Heap.readField_writeField_same h ref "adj" _ "graph_input.UnweightedGraph" valid.2]
rfl
def field_UnweightedGraph_degree (h : Heap) (ref : Ref_UnweightedGraph) : Option SeqRef :=
if is_UnweightedGraph h ref then (h.readField ref "degree").bind ObjectValue.asSeq else none
def set_UnweightedGraph_degree (h : Heap) (ref : Ref_UnweightedGraph) (value : SeqRef) : Heap :=
h.writeField ref "degree" (ObjectValue.seqValue value)
@[simp] theorem field_UnweightedGraph_degree_set (h : Heap) (ref : Ref_UnweightedGraph) (value : SeqRef)
(valid : is_UnweightedGraph h ref) :
field_UnweightedGraph_degree (set_UnweightedGraph_degree h ref value) ref = some value := by
have valid' : is_UnweightedGraph (set_UnweightedGraph_degree h ref value) ref := by
simpa [set_UnweightedGraph_degree, is_UnweightedGraph] using valid
rw [field_UnweightedGraph_degree, if_pos valid']
unfold set_UnweightedGraph_degree
rw [Heap.readField_writeField_same h ref "degree" _ "graph_input.UnweightedGraph" valid.2]
rfl
/-- Build input data directly; this helper does not execute `__init__`. -/
def create_UnweightedGraph (h : Heap) (value_size : Int) (value_adj : CollectionRef) (value_degree : SeqRef) : Heap × Ref_UnweightedGraph :=
let ref := h.nextObject
let h := h.allocateObject "graph_input.UnweightedGraph"
let h := set_UnweightedGraph_size h ref value_size
let h := set_UnweightedGraph_adj h ref value_adj
let h := set_UnweightedGraph_degree h ref value_degree
(h, ref)
def seq_Seq_Int : SequenceType SeqRef where
name := "Seq[Int]"
encode := fun value => (ObjectValue.seqValue value)
decode := ObjectValue.asSeq
decode_encode := by intro value; rfl
structure State_UnweightedGraph___init__ where
v0 : Ref_UnweightedGraph := 0 -- self
v1 : Int := 0 -- size
v2 : CollectionRef := 0 -- adj
v3 : SeqRef := 0 -- degree
t4 : Unit := () -- temporary
structure State_UnweightedGraph where
v0 : Int := 0 -- size
v1 : CollectionRef := 0 -- adj
v2 : SeqRef := 0 -- degree
v3 : Ref_UnweightedGraph := 0 -- _instance
t4 : Ref_UnweightedGraph := 0 -- temporary
t5 : Unit := () -- temporary
t6 : Ref_UnweightedGraph := 0 -- temporary
t7 : Int := 0 -- temporary
t8 : CollectionRef := 0 -- temporary
t9 : SeqRef := 0 -- temporary
t10 : Ref_UnweightedGraph := 0 -- temporary
inductive Frame where
| invalid
| fn_UnweightedGraph___init__ (pc : Nat) (state : State_UnweightedGraph___init__)
| fn_UnweightedGraph (pc : Nat) (state : State_UnweightedGraph)
inductive Result where
| fn_UnweightedGraph___init__ (value : Unit)
| fn_UnweightedGraph (value : Ref_UnweightedGraph)
abbrev Configuration := Algo2LeanCore.Config Heap (Frame) Result
abbrev Stack := Algo2LeanCore.Stack (Frame) Result
abbrev Transcript := List (Configuration)
inductive Step : Configuration → Configuration → Prop where
| UnweightedGraph___init___pc1 (h : Heap) (s : State_UnweightedGraph___init__) (stack : Stack) :
Step (.active h (Frame.fn_UnweightedGraph___init__ 1 s) stack) (Algo2LeanCore.resumeConfig h (Result.fn_UnweightedGraph___init__ (s.t4)) stack)
| UnweightedGraph___init___pc2 (h : Heap) (s : State_UnweightedGraph___init__) (stack : Stack) :
Step (.active h (Frame.fn_UnweightedGraph___init__ 2 s) stack) (.active h (Frame.fn_UnweightedGraph___init__ 1 { s with t4 := () }) stack)
| UnweightedGraph___init___pc3 (h : Heap) (s : State_UnweightedGraph___init__) (stack : Stack) (defined : (is_UnweightedGraph h (s.v0))) :
Step (.active h (Frame.fn_UnweightedGraph___init__ 3 s) stack) (.active (set_UnweightedGraph_degree h (s.v0) (s.v3)) (Frame.fn_UnweightedGraph___init__ 2 s) stack)
| UnweightedGraph___init___pc4 (h : Heap) (s : State_UnweightedGraph___init__) (stack : Stack) (defined : (is_UnweightedGraph h (s.v0))) :
Step (.active h (Frame.fn_UnweightedGraph___init__ 4 s) stack) (.active (set_UnweightedGraph_adj h (s.v0) (s.v2)) (Frame.fn_UnweightedGraph___init__ 3 s) stack)
| UnweightedGraph___init___pc5 (h : Heap) (s : State_UnweightedGraph___init__) (stack : Stack) (defined : (is_UnweightedGraph h (s.v0))) :
Step (.active h (Frame.fn_UnweightedGraph___init__ 5 s) stack) (.active (set_UnweightedGraph_size h (s.v0) (s.v1)) (Frame.fn_UnweightedGraph___init__ 4 s) stack)
| UnweightedGraph_pc1 (h : Heap) (s : State_UnweightedGraph) (stack : Stack) (defined : is_UnweightedGraph h s.t4) :
Step (.active h (Frame.fn_UnweightedGraph 1 s) stack) (Algo2LeanCore.resumeConfig h (Result.fn_UnweightedGraph (s.t4)) stack)
| UnweightedGraph_pc2 (h : Heap) (s : State_UnweightedGraph) (stack : Stack) :
Step (.active h (Frame.fn_UnweightedGraph 2 s) stack) (.active h (Frame.fn_UnweightedGraph 1 { s with t4 := s.v3 }) stack)
| UnweightedGraph_pc3 (h : Heap) (s : State_UnweightedGraph) (stack : Stack) :
Step (.active h (Frame.fn_UnweightedGraph 3 s) stack) (.active h (Frame.fn_UnweightedGraph___init__ 5 ({ v0 := s.t6, v1 := s.t7, v2 := s.t8, v3 := s.t9 } : State_UnweightedGraph___init__)) ((fun value => match value with | .fn_UnweightedGraph___init__ result => (Frame.fn_UnweightedGraph 2 { s with t5 := result }) | _ => .invalid) :: stack))
| UnweightedGraph_pc4 (h : Heap) (s : State_UnweightedGraph) (stack : Stack) :
Step (.active h (Frame.fn_UnweightedGraph 4 s) stack) (.active h (Frame.fn_UnweightedGraph 3 { s with t9 := s.v2 }) stack)
| UnweightedGraph_pc5 (h : Heap) (s : State_UnweightedGraph) (stack : Stack) :
Step (.active h (Frame.fn_UnweightedGraph 5 s) stack) (.active h (Frame.fn_UnweightedGraph 4 { s with t8 := s.v1 }) stack)
| UnweightedGraph_pc6 (h : Heap) (s : State_UnweightedGraph) (stack : Stack) :
Step (.active h (Frame.fn_UnweightedGraph 6 s) stack) (.active h (Frame.fn_UnweightedGraph 5 { s with t7 := s.v0 }) stack)
| UnweightedGraph_pc7 (h : Heap) (s : State_UnweightedGraph) (stack : Stack) :
Step (.active h (Frame.fn_UnweightedGraph 7 s) stack) (.active h (Frame.fn_UnweightedGraph 6 { s with t6 := s.v3 }) stack)
| UnweightedGraph_pc8 (h : Heap) (s : State_UnweightedGraph) (stack : Stack) :
Step (.active h (Frame.fn_UnweightedGraph 8 s) stack) (.active h (Frame.fn_UnweightedGraph 7 { s with v3 := s.t10 }) stack)
| UnweightedGraph_pc9 (h : Heap) (s : State_UnweightedGraph) (stack : Stack) :
Step (.active h (Frame.fn_UnweightedGraph 9 s) stack) (.active (h.allocateObject "graph_input.UnweightedGraph") (Frame.fn_UnweightedGraph 8 { s with t10 := h.nextObject }) stack)
theorem terminal (h : Heap) (result : Result) :
Algo2LeanCore.Terminal Step (.done h result) := by
intro next transition
cases transition
end Algo2LeanGenerated
open Algo2LeanGenerated
def entry_UnweightedGraph___init__ (input : Ref_UnweightedGraph × Int × CollectionRef × SeqRef) : Frame :=
(Frame.fn_UnweightedGraph___init__ 5 ({ v0 := input.1, v1 := input.2.1, v2 := input.2.2.1, v3 := input.2.2.2 } : State_UnweightedGraph___init__))
def UnweightedGraph.__init__.ValidInput (h : Heap) (input : Ref_UnweightedGraph × Int × CollectionRef × SeqRef) : Prop := is_UnweightedGraph h input.1 ∧ seq_Seq_Int.valid h input.2.2.1 ∧ input.2.2.2 < h.nextRef
def UnweightedGraph.__init__.initial (h : Heap) (input : Ref_UnweightedGraph × Int × CollectionRef × SeqRef) : Configuration :=
Algo2LeanCore.start h (Frame.fn_UnweightedGraph___init__ 5 ({ v0 := input.1, v1 := input.2.1, v2 := input.2.2.1, v3 := input.2.2.2 } : State_UnweightedGraph___init__))
def UnweightedGraph.__init__.Run (h : Heap) (input : Ref_UnweightedGraph × Int × CollectionRef × SeqRef) (h' : Heap) (output : Unit) : Prop :=
_root_.Algo.«graph_input».UnweightedGraph.__init__.ValidInput h input ∧ Algo2LeanCore.Reaches Step (_root_.Algo.«graph_input».UnweightedGraph.__init__.initial h input) (.done h' (Result.fn_UnweightedGraph___init__ output))
def UnweightedGraph.__init__.ValidHeapTranscript (h : Heap) (input : Ref_UnweightedGraph × Int × CollectionRef × SeqRef) (trace : Transcript) : Prop :=
_root_.Algo.«graph_input».UnweightedGraph.__init__.ValidInput h input ∧ ∃ final, Algo2LeanCore.Valid Step (_root_.Algo.«graph_input».UnweightedGraph.__init__.initial h input) trace final
def UnweightedGraph.__init__.Call (h : Heap) (input : Ref_UnweightedGraph × Int × CollectionRef × SeqRef) (h' : Heap) (output : Unit) : Prop :=
_root_.Algo.«graph_input».UnweightedGraph.__init__.ValidInput h input ∧ Algo2LeanCore.Summary Step h (Frame.fn_UnweightedGraph___init__ 5 ({ v0 := input.1, v1 := input.2.1, v2 := input.2.2.1, v3 := input.2.2.2 } : State_UnweightedGraph___init__)) h' (Result.fn_UnweightedGraph___init__ output)
-- Complete this function from the supplied local state, under any caller stack.
def UnweightedGraph.__init__.CallFrom (state : Configuration) (finalHeap : Heap) (output : Unit) : Prop :=
match state with
| .active heap (Frame.fn_UnweightedGraph___init__ pc locals) _ =>
Algo2LeanCore.Summary Step heap (Frame.fn_UnweightedGraph___init__ pc locals) finalHeap (Result.fn_UnweightedGraph___init__ output)
| _ => False
-- Object inputs carry their heap, preserving shared references and cycles.
def UnweightedGraph.__init__.load (input : Heap × (Ref_UnweightedGraph × Int × CollectionRef × SeqRef)) : Heap × (Ref_UnweightedGraph × Int × CollectionRef × SeqRef) := input
def UnweightedGraph.__init__.ValidTranscript (my_input : Heap × (Ref_UnweightedGraph × Int × CollectionRef × SeqRef)) (trace : Transcript) : Prop :=
let loaded := _root_.Algo.«graph_input».UnweightedGraph.__init__.load my_input
_root_.Algo.«graph_input».UnweightedGraph.__init__.ValidHeapTranscript loaded.1 loaded.2 trace
def UnweightedGraph.__init__.Returns (my_input : Heap × (Ref_UnweightedGraph × Int × CollectionRef × SeqRef)) (my_output : Unit) : Prop :=
let loaded := _root_.Algo.«graph_input».UnweightedGraph.__init__.load my_input
∃ finalHeap, _root_.Algo.«graph_input».UnweightedGraph.__init__.Run loaded.1 loaded.2 finalHeap my_output
theorem UnweightedGraph.__init__.Call.run {before input after output}
(call : _root_.Algo.«graph_input».UnweightedGraph.__init__.Call before input after output) :
_root_.Algo.«graph_input».UnweightedGraph.__init__.Run before input after output :=
⟨call.1, call.2.root⟩
def entry_UnweightedGraph (input : Int × CollectionRef × SeqRef) : Frame :=
(Frame.fn_UnweightedGraph 9 ({ v0 := input.1, v1 := input.2.1, v2 := input.2.2 } : State_UnweightedGraph))
def UnweightedGraph.ValidInput (h : Heap) (input : Int × CollectionRef × SeqRef) : Prop := seq_Seq_Int.valid h input.2.1 ∧ input.2.2 < h.nextRef
def UnweightedGraph.initial (h : Heap) (input : Int × CollectionRef × SeqRef) : Configuration :=
Algo2LeanCore.start h (Frame.fn_UnweightedGraph 9 ({ v0 := input.1, v1 := input.2.1, v2 := input.2.2 } : State_UnweightedGraph))
def UnweightedGraph.Run (h : Heap) (input : Int × CollectionRef × SeqRef) (h' : Heap) (output : Ref_UnweightedGraph) : Prop :=
_root_.Algo.«graph_input».UnweightedGraph.ValidInput h input ∧ Algo2LeanCore.Reaches Step (_root_.Algo.«graph_input».UnweightedGraph.initial h input) (.done h' (Result.fn_UnweightedGraph output))
def UnweightedGraph.ValidHeapTranscript (h : Heap) (input : Int × CollectionRef × SeqRef) (trace : Transcript) : Prop :=
_root_.Algo.«graph_input».UnweightedGraph.ValidInput h input ∧ ∃ final, Algo2LeanCore.Valid Step (_root_.Algo.«graph_input».UnweightedGraph.initial h input) trace final
def UnweightedGraph.Call (h : Heap) (input : Int × CollectionRef × SeqRef) (h' : Heap) (output : Ref_UnweightedGraph) : Prop :=
_root_.Algo.«graph_input».UnweightedGraph.ValidInput h input ∧ Algo2LeanCore.Summary Step h (Frame.fn_UnweightedGraph 9 ({ v0 := input.1, v1 := input.2.1, v2 := input.2.2 } : State_UnweightedGraph)) h' (Result.fn_UnweightedGraph output)
-- Complete this function from the supplied local state, under any caller stack.
def UnweightedGraph.CallFrom (state : Configuration) (finalHeap : Heap) (output : Ref_UnweightedGraph) : Prop :=
match state with
| .active heap (Frame.fn_UnweightedGraph pc locals) _ =>
Algo2LeanCore.Summary Step heap (Frame.fn_UnweightedGraph pc locals) finalHeap (Result.fn_UnweightedGraph output)
| _ => False
-- Object inputs carry their heap, preserving shared references and cycles.
def UnweightedGraph.load (input : Heap × (Int × CollectionRef × SeqRef)) : Heap × (Int × CollectionRef × SeqRef) := input
def UnweightedGraph.ValidTranscript (my_input : Heap × (Int × CollectionRef × SeqRef)) (trace : Transcript) : Prop :=
let loaded := _root_.Algo.«graph_input».UnweightedGraph.load my_input
_root_.Algo.«graph_input».UnweightedGraph.ValidHeapTranscript loaded.1 loaded.2 trace
def UnweightedGraph.Returns (my_input : Heap × (Int × CollectionRef × SeqRef)) (my_output : Heap × (Ref_UnweightedGraph)) : Prop :=
let loaded := _root_.Algo.«graph_input».UnweightedGraph.load my_input
_root_.Algo.«graph_input».UnweightedGraph.Run loaded.1 loaded.2 my_output.1 my_output.2
theorem UnweightedGraph.Call.run {before input after output}
(call : _root_.Algo.«graph_input».UnweightedGraph.Call before input after output) :
_root_.Algo.«graph_input».UnweightedGraph.Run before input after output :=
⟨call.1, call.2.root⟩
end Algo.«graph_input»
set_option autoImplicit false
open Algo2LeanGenerated
namespace CLRS.GraphTraversal
/-- A finite directed multigraph. Each list position is one adjacency occurrence;
parallel arcs and self-loops are allowed. Rows outside the vertex range are ignored. -/
structure Graph where
size : Nat
neighbors : Nat → List Nat
bounded : ∀ u, u < size → ∀ v ∈ neighbors u, v < size
def Vertex (g : Graph) (v : Int) : Prop := 0 ≤ v ∧ v < (g.size : Int)
def Edge (g : Graph) (u v : Int) : Prop :=
Vertex g u ∧ Vertex g v ∧ v.toNat ∈ g.neighbors u.toNat
/-- Input size counts adjacency occurrences, including parallel arcs. -/
def edgeCount (g : Graph) : Nat :=
((List.range g.size).map fun u => (g.neighbors u).length).sum
/-- A path of exactly the stated number of edges; vertices may repeat. -/
inductive Walk (g : Graph) : Nat → Int → Int → Prop where
| zero (v : Int) : Vertex g v → Walk g 0 v v
| cons {length : Nat} {u v w : Int} :
Edge g u v → Walk g length v w → Walk g (length + 1) u w
def Reachable (g : Graph) (u v : Int) : Prop := ∃ length, Walk g length u v
def Shortest (g : Graph) (u v : Int) (distance : Nat) : Prop :=
Walk g distance u v ∧ ∀ length, Walk g length u v → distance ≤ length
def StronglyConnected (g : Graph) (u v : Int) : Prop :=
Reachable g u v ∧ Reachable g v u
/-- The finite graph represented by allocated, read-only arrays of arrays.
Only each row's declared prefix is meaningful; rows are allowed to alias. -/
def GraphRep (heap : Heap) (ref : ObjectRef) (g : Graph) : Prop :=
Algo.graph_input.Algo2LeanGenerated.is_UnweightedGraph heap ref ∧
Algo.graph_input.Algo2LeanGenerated.field_UnweightedGraph_size heap ref = some (g.size : Int) ∧
∃ adj degree,
Algo.graph_input.Algo2LeanGenerated.field_UnweightedGraph_adj heap ref = some adj ∧
Algo.graph_input.Algo2LeanGenerated.field_UnweightedGraph_degree heap ref = some degree ∧
Algo.graph_input.Algo2LeanGenerated.seq_Seq_Int.valid heap adj ∧ degree < heap.nextRef ∧
∀ u : Nat, u < g.size →
heap.read degree (u : Int) = ((g.neighbors u).length : Int) ∧
∃ row,
Algo.graph_input.Algo2LeanGenerated.seq_Seq_Int.get heap adj (u : Int) = some row ∧
row < heap.nextRef ∧
∀ j : Nat, j < (g.neighbors u).length →
heap.read row (j : Int) = ((g.neighbors u)[j]! : Int)
/-- All initially allocated caller storage survives; new storage may be allocated.
Costs are increments from the caller's actual clocks, without resetting them. -/
structure Preserves (before after : Heap) : Prop where
sequences : ∀ ref, ref < before.nextRef → after.read ref = before.read ref
objects : ∀ ref, ref < before.nextObject → after.objects ref = before.objects ref
collections : ∀ ref, ref < before.nextCollection → after.collections ref = before.collections ref
sequenceAllocation : before.nextRef ≤ after.nextRef
objectAllocation : before.nextObject ≤ after.nextObject
collectionAllocation : before.nextCollection ≤ after.nextCollection
workMonotone : before.clocks "graph_work" ≤ after.clocks "graph_work"
otherClocks : ∀ name, name ≠ "graph_work" → after.clocks name = before.clocks name
def work (before after : Heap) : Nat := Heap.cost before after "graph_work"
def FreshObject (before after : Heap) (result : ObjectRef) : Prop :=
before.nextObject ≤ result ∧ result < after.nextObject
def FreshArrays (before after : Heap) (refs : List SeqRef) : Prop :=
refs.Pairwise (fun a b => a ≠ b) ∧
∀ ref ∈ refs, before.nextRef ≤ ref ∧ ref < after.nextRef
/-- Every vertex occurs exactly once in the finite sequence prefix. -/
def VertexOrder (g : Graph) (order : Seq) : Prop :=
∃ values : List Int,
values.Perm ((List.range g.size).map Int.ofNat) ∧
∀ j : Nat, j < g.size → order (j : Int) = values[j]!
/-- Reverse every edge while retaining its multiplicity. Adjacency row order may change. -/
def IsTranspose (g transpose : Graph) : Prop :=
transpose.size = g.size ∧
∀ u v : Nat, u < g.size → v < g.size →
(transpose.neighbors u).count v = (g.neighbors v).count u
end CLRS.GraphTraversal
Read-back
What the Lean code literally says, in plain math · GPT-6 (Codex, independent fresh-context agent)
This bundle defines both a heap representation and a mathematical directed graph. A mathematical graph consists of a natural number and, for every natural number , a finite list of natural-number neighbors; whenever , every entry in that list must also be less than . Its vertices are precisely the integers with . An edge from to means that both are vertices and occurs in the neighbor list of ; repeated entries give repeated adjacency occurrences, although the edge proposition only records membership. The quantity is the sum of the lengths of the lists for . Lists at other indices do not affect the graph predicates or this sum. A walk of natural-number length zero stays at a valid vertex; a walk of length consists of an edge followed by a walk of length . Vertices may repeat. Reachability means existence of such a walk, shortest distance means that a walk of length exists and for every walk length with the same endpoints, and strong connectivity of two integers means reachability in both directions. A heap uses separate natural-number reference spaces for integer sequences, objects, and typed collections; an integer sequence is a total function from integers to integers, with no finite capacity. An unweighted-graph object is considered to have the correct class exactly when its reference lies below the heap's object-allocation counter and its stored class name is graph_input.UnweightedGraph; its size, adjacency, and degree readers additionally require fields of the appropriate tagged kinds. The direct creation helper allocates one such object and writes the three supplied fields without executing the initializer or checking their values. The generated initializer writes the supplied integer size, adjacency-collection reference, and degree-sequence reference into an existing object; its input condition requires the object to have the indicated class, the adjacency collection to be allocated with the Seq[Int] type tag, and the degree sequence to have an allocated reference. The generated constructor allocates an object and invokes that initializer; its input condition checks the adjacency tag and allocated degree reference, but imposes no nonnegativity or graph-consistency condition on the integer size. These operations do not add clock ticks. The generated transition system records local variables, program positions, heap snapshots, results, and suspended caller continuations. A run is a valid-input finite transition sequence from the initial state to a completed state; a call requires such a completion to the same final heap and result under every caller stack; a valid transcript may stop before completion. The corresponding load operations retain the supplied heap and references; return predicates expose the final heap for the constructor and existentially hide it for the unit-valued initializer. Calls from a local state require completion under every caller stack only when that state has the relevant active function frame, and are false otherwise. The bundle proves the stated same-field setter facts, absence of transitions from completed states, and that a call gives a top-level run. For any heap, object reference, and mathematical graph, the graph-representation predicate further requires an allocated graph-class object with size field exactly , an allocated adjacency collection with the indicated type tag, and an allocated degree sequence; for every , the degree entry at must equal the neighbor-list length, the adjacency entry at must decode to an allocated integer-sequence reference, and that row's entries in the declared prefix must equal the neighbor list in order. Rows, including their sequence references, need not be distinct and may share storage with the degree sequence if these equations hold; entries outside the specified prefixes are unrestricted. Representation allows , when the row requirements are empty but the object, collection, and degree allocation requirements remain. For any before and after heaps, preservation means equality of the complete contents of every initially allocated integer sequence, object, and collection, nondecrease of all three allocation counters and of the graph_work clock, and equality of every other named clock. Work is the final graph_work clock minus the initial clock using natural-number subtraction, which is truncated at zero without a monotonicity assumption. A fresh object reference lies at least at the old object counter and strictly below the new one; a list of fresh sequence references must be pairwise distinct and every reference must lie between the corresponding old and new sequence counters in the same way. Neither freshness predicate alone specifies an exact allocation count. A vertex order is a total integer sequence whose first entries equal some permutation of ; all other entries are unrestricted, and the condition is vacuous on entries when . A transpose is another mathematical graph of the same size whose number of occurrences of in row equals the original number of occurrences of in row for all ; row order is unrestricted.
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.