lean_try/GraphOptVerify/Core/GraphProgram.lean at main · Yuhx141/lean_try · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
import GraphOptVerify.Core.GraphEquiv

namespace GraphOptVerify.ONNX

universe u v

@[simp] theorem TensorValue.hasType_ofShape {R : Type u}
    (assignment : ShapeAssignment) (value : TensorValue R) :
    TensorValue.hasType assignment value
      (.denseTensor (.float .float32) (some (ShapeSpec.ofShape value.shape))) :=
  ShapeSpec.matches_ofShape assignment value.shape

@[simp] theorem TensorValue.hasType_mk {R : Type u}
    (assignment : ShapeAssignment) (shape : Shape) (data : Tensor R shape) :
    TensorValue.hasType assignment ⟨shape, data⟩
      (.denseTensor (.float .float32) (some (ShapeSpec.ofShape shape))) :=
  ShapeSpec.matches_ofShape assignment shape

theorem NodeEval.single_output {model : ValueModel.{u}} (context : EvalContext model)
    (assignment : ShapeAssignment) (node : Node) (environment : Environment model)
    (inputs : InputValues model) (outputName : String) (output : model.Carrier)
    (wellFormed : node.WellFormed)
    (resolved : resolveInputs environment node.inputNames = some inputs)
    (captures : node.captureNames = []) (outputNames : node.outputNames = [some outputName])
    (fresh : environment.lookup outputName = none)
    (relation : OpRel node.schema context (node.call context assignment inputs []) [some output]) :
    NodeEval context assignment node environment (environment ++ [(outputName, output)]) := by
  have step := NodeEval.step node environment inputs [] [some output] wellFormed resolved
    (by simp [captures, resolveNames])
    (by simpa [namesFresh, Node.liveOutputNames, outputNames] using fresh)
    (by simp [outputMask, outputNames]) relation
  simpa [bindOutputs, outputNames] using step

/-- A generated program supplies executions for every typed boundary value.
The mathematical equality concerns the whole result list; the final theorem
also retains registration, legality and existence of graph executions. -/
theorem GraphEquivOn.of_parameterized_execution {model : ValueModel.{u}}
    {context : EvalContext model} {left right : Graph model}
    {Parameters : Type v} (inhabited : Nonempty Parameters)
    (runtime : Parameters → Environment model)
    (leftOutput rightOutput : Parameters → List model.Carrier)
    (functional : context.Functional)
    (leftRegistered : left.Registered context) (rightRegistered : right.Registered context)
    (leftRuns : ∀ parameters, GraphEval context left (runtime parameters) (leftOutput parameters))
    (rightRuns : ∀ parameters, GraphEval context right (runtime parameters) (rightOutput parameters))
    (same : ∀ parameters, leftOutput parameters = rightOutput parameters) :
    GraphEquivOn context left right (fun inputs => ∃ parameters, inputs = runtime parameters) := by
  refine ⟨?_, leftRegistered, rightRegistered, ?_, ?_⟩
  · rcases inhabited with ⟨parameters⟩
    exact ⟨runtime parameters, parameters, rfl⟩
  · rintro inputs ⟨parameters, rfl⟩
    exact ⟨leftOutput parameters, leftRuns parameters⟩
  · rintro inputs ⟨parameters, rfl⟩ outputs
    constructor
    · intro execution
      have equality := GraphEval.functional functional execution (leftRuns parameters)
      rw [equality, same parameters]
      exact rightRuns parameters
    · intro execution
      have equality := GraphEval.functional functional execution (rightRuns parameters)
      rw [equality, ← same parameters]
      exact leftRuns parameters

/-- Positional ONNX boundary correspondence need not preserve textual names.
Both binding functions and the entire parameter domain are fixed in the
statement. Executions still use the original graph names, including captures.
This is the same joint GraphEval relation, with explicit boundary bindings. -/
structure GraphEquivOnBindings {model : ValueModel.{u}} (context : EvalContext model)
    (left right : Graph model) {Parameters : Type v}
    (leftInputs rightInputs : Parameters → Environment model) : Prop where
  domainInhabited : Nonempty Parameters
  leftRegistered : left.Registered context
  rightRegistered : right.Registered context
  leftExecutable : ∀ parameters, ∃ outputs,
    GraphEval context left (leftInputs parameters) outputs
  sameOutputs : ∀ parameters outputs,
    GraphEval context left (leftInputs parameters) outputs ↔
      GraphEval context right (rightInputs parameters) outputs

theorem GraphEquivOnBindings.of_execution {model : ValueModel.{u}}
    {context : EvalContext model} {left right : Graph model}
    {Parameters : Type v} (inhabited : Nonempty Parameters)
    (leftInputs rightInputs : Parameters → Environment model)
    (leftOutput rightOutput : Parameters → List model.Carrier)
    (functional : context.Functional)
    (leftRegistered : left.Registered context) (rightRegistered : right.Registered context)
    (leftRuns : ∀ parameters, GraphEval context left (leftInputs parameters) (leftOutput parameters))
    (rightRuns : ∀ parameters, GraphEval context right (rightInputs parameters) (rightOutput parameters))
    (same : ∀ parameters, leftOutput parameters = rightOutput parameters) :
    GraphEquivOnBindings context left right leftInputs rightInputs := by
  refine ⟨inhabited, leftRegistered, rightRegistered, ?_, ?_⟩
  · intro parameters
    exact ⟨leftOutput parameters, leftRuns parameters⟩
  · intro parameters outputs
    constructor
    · intro execution
      have equality := GraphEval.functional functional execution (leftRuns parameters)
      rw [equality, same parameters]
      exact rightRuns parameters
    · intro execution
      have equality := GraphEval.functional functional execution (rightRuns parameters)
      rw [equality, ← same parameters]
      exact leftRuns parameters

theorem GraphEquivOnBindings.toGraphEquivOn {model : ValueModel.{u}}
    {context : EvalContext model} {left right : Graph model} {Parameters : Type v}
    {runtime : Parameters → Environment model}
    (equivalence : GraphEquivOnBindings context left right runtime runtime) :
    GraphEquivOn context left right (fun inputs => ∃ parameters, inputs = runtime parameters) := by
  refine ⟨?_, equivalence.leftRegistered, equivalence.rightRegistered, ?_, ?_⟩
  · rcases equivalence.domainInhabited with ⟨parameters⟩
    exact ⟨runtime parameters, parameters, rfl⟩
  · rintro inputs ⟨parameters, rfl⟩
    exact equivalence.leftExecutable parameters
  · rintro inputs ⟨parameters, rfl⟩ outputs
    exact equivalence.sameOutputs parameters outputs

end GraphOptVerify.ONNX