Exact-real IR semantics for the finite artifact fragment

The payload below reads the same binary32 parameter store as the fragment decoder. Successful tensor decoding retains each finite word's exact real value. The node equations use the ordinary IR evaluator, including its shape and parent checks.

noncomputable def NN.Verification.Cert.FiniteArtifact.exactPayload (ps : MLTheory.CROWN.Graph.ParamStore (FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) exactPayload._proof_1 exactPayload._proof_2 exactPayload._proof_3 exactPayload._proof_4)) : IR.Payload ℝ

Decode finite linear parameters into the payload consumed by the real IR evaluator.

theorem NN.Verification.Cert.FiniteArtifact.exactPayload_linear (ps : MLTheory.CROWN.Graph.ParamStore (FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) exactPayload._proof_1 exactPayload._proof_2 exactPayload._proof_3 exactPayload._proof_4)) (id : ℕ) (p : MLTheory.CROWN.Graph.LinParams (FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) exactPayload._proof_1 exactPayload._proof_2 exactPayload._proof_3 exactPayload._proof_4)) (weights : TorchLean.Tensor ℚ [p.m, p.n]) (bias : TorchLean.Tensor ℚ [p.m]) (hp : ps.linearWB[id]? = some p) (hw : decodeTensor p.w = some weights) (hb : decodeTensor p.b = some bias) : (exactPayload ps).linear? id = some { outDim := p.m, inDim := p.n, W := RationalReflection.realTensor weights, b := RationalReflection.realTensor bias }

A successful parameter read gives precisely the weights used by the real IR evaluator.

theorem NN.Verification.Cert.FiniteArtifact.decodeGraph_wellFormed (g : MLTheory.CROWN.Graph) (ps : MLTheory.CROWN.Graph.ParamStore (FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) exactPayload._proof_1 exactPayload._proof_2 exactPayload._proof_3 exactPayload._proof_4)) (decoded : DecodedGraph) (h : decodeGraph g ps = some decoded) : IR.Graph.wellFormed g = true

Successful decoding supplies the ordinary IR evaluator's structural guard.

theorem NN.Verification.Cert.FiniteArtifact.decodeGraph_denote (g : MLTheory.CROWN.Graph) (ps : MLTheory.CROWN.Graph.ParamStore (FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) exactPayload._proof_1 exactPayload._proof_2 exactPayload._proof_3 exactPayload._proof_4)) (decoded : DecodedGraph) (h : decodeGraph g ps = some decoded) (x : TorchLean.Tensor ℝ [decoded.inputDim]) : IR.Graph.denote g (exactPayload ps) { shape := [decoded.inputDim], tensor := x } (g.nodes.size - 1) = Except.ok { shape := [decoded.outputDim], tensor := decoded.program.eval x }

Successful decoding determines the ordinary graph evaluator's exact-real output.

theorem NN.Verification.Cert.FiniteArtifact.accepts_graph_sound (g : MLTheory.CROWN.Graph) (ps : MLTheory.CROWN.Graph.ParamStore (FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) exactPayload._proof_1 exactPayload._proof_2 exactPayload._proof_3 exactPayload._proof_4)) (cert : NodeReplay.CROWNCertificate) (query : OutputQuery) (h : accepts g ps cert query = true) : ∃ (decoded : Decoded), decode g ps cert query = some decoded ∧ nodeBounds cert query.outputId decoded.graph.inputDim decoded.graph.outputDim = some decoded.artifact.chain.bounds ∧ 0 < decoded.graph.inputDim ∧ 0 < decoded.graph.outputDim ∧ 0 < decoded.numConstraints ∧ ∀ (x : TorchLean.Tensor ℝ [decoded.graph.inputDim]), MLTheory.CROWN.Graph.Theorems.Semantics.encloses { dim := decoded.graph.inputDim, lo := RationalReflection.realTensor decoded.graph.input.lo, hi := RationalReflection.realTensor decoded.graph.input.hi } x → ∃ (y : TorchLean.Tensor ℝ [decoded.graph.outputDim]), IR.Graph.denote g (exactPayload ps) { shape := [decoded.graph.inputDim], tensor := x } query.outputId = Except.ok { shape := [decoded.graph.outputDim], tensor := y } ∧ ∀ (i : Fin decoded.numConstraints), have margin := (Spec.matVecMulSpec (RationalReflection.realTensor decoded.inequalities.weights) y).addSpec (RationalReflection.realTensor decoded.inequalities.bias); if decoded.strict = true then margin.getScalar i < 0 else margin.getScalar i ≤ 0

The requested margins hold for the original graph under its exactly decoded payload.