Real soundness of finite binary32 artifacts

Exact decoding, local dominance, and structural induction connect the supplied affine entries to Program.eval on real inputs. No transfer theorem or semantic evaluation trace is an input to the checker soundness theorem. decode_coverage proves node-count and final-entry coverage. FiniteArtifactSemantics proves agreement with NN.IR.Graph.denote in decodeGraph_denote and lifts acceptance to the original graph's exact-real semantics in accepts_graph_sound.

theorem NN.Verification.Cert.FiniteArtifact.decodeScalar_sound (value : FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) decodeScalar_sound._proof_1 decodeScalar_sound._proof_2 decodeScalar_sound._proof_3 decodeScalar_sound._proof_4) (q : ℚ) (h : value.toRat? = some q) : value.toModel.isFinite = true ∧ value.toModel.toReal = ↑q

Successful scalar decoding retains the exact real denotation of the binary32 word.

theorem NN.Verification.Cert.FiniteArtifact.decodeTensor_sound {s : Spec.Shape} (value : TorchLean.Tensor (FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) decodeScalar_sound._proof_1 decodeScalar_sound._proof_2 decodeScalar_sound._proof_3 decodeScalar_sound._proof_4) s) (q : TorchLean.Tensor ℚ s) (h : decodeTensor value = some q) : TorchLean.Tensor.Forall (fun (v : FloatLib.Floats.ExecFloat.Binary { expWidth := 8, expWidth_ge_two := decodeScalar_sound._proof_1, fracWidth := 23, fracWidth_pos := decodeScalar_sound._proof_2, exponentBias := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8, encoding := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee, exponentBias_pos := decodeScalar_sound._proof_3, exponentBias_le_maxFinite := decodeScalar_sound._proof_4 }.expWidth { expWidth := 8, expWidth_ge_two := decodeScalar_sound._proof_1, fracWidth := 23, fracWidth_pos := decodeScalar_sound._proof_2, exponentBias := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8, encoding := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee, exponentBias_pos := decodeScalar_sound._proof_3, exponentBias_le_maxFinite := decodeScalar_sound._proof_4 }.fracWidth { expWidth := 8, expWidth_ge_two := decodeScalar_sound._proof_1, fracWidth := 23, fracWidth_pos := decodeScalar_sound._proof_2, exponentBias := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8, encoding := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee, exponentBias_pos := decodeScalar_sound._proof_3, exponentBias_le_maxFinite := decodeScalar_sound._proof_4 }.encoding { expWidth := 8, expWidth_ge_two := decodeScalar_sound._proof_1, fracWidth := 23, fracWidth_pos := decodeScalar_sound._proof_2, exponentBias := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8, encoding := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee, exponentBias_pos := decodeScalar_sound._proof_3, exponentBias_le_maxFinite := decodeScalar_sound._proof_4 }.exponentBias ⋯ ⋯ ⋯ ⋯ (FloatLib.Floats.Formats.BinaryInterchange.Configured.StoragePlan.forKnownWidth (FloatLib.Floats.ExecFloat.Binary.descriptor 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) decodeScalar_sound._proof_1 decodeScalar_sound._proof_2 decodeScalar_sound._proof_3 decodeScalar_sound._proof_4) (1 + 8 + 23) ⋯) (FloatLib.Floats.Formats.BinaryInterchange.Configured.Code (FloatLib.Floats.Formats.BinaryInterchange.Configured.StoragePlan.forKnownWidth (FloatLib.Floats.ExecFloat.Binary.descriptor 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) decodeScalar_sound._proof_1 decodeScalar_sound._proof_2 decodeScalar_sound._proof_3 decodeScalar_sound._proof_4) (1 + 8 + 23) ⋯))) => v.toModel.isFinite = true) value ∧ RationalReflection.realTensor q = TorchLean.Tensor.map (fun (v : FloatLib.Floats.ExecFloat.Binary { expWidth := 8, expWidth_ge_two := decodeScalar_sound._proof_1, fracWidth := 23, fracWidth_pos := decodeScalar_sound._proof_2, exponentBias := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8, encoding := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee, exponentBias_pos := decodeScalar_sound._proof_3, exponentBias_le_maxFinite := decodeScalar_sound._proof_4 }.expWidth { expWidth := 8, expWidth_ge_two := decodeScalar_sound._proof_1, fracWidth := 23, fracWidth_pos := decodeScalar_sound._proof_2, exponentBias := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8, encoding := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee, exponentBias_pos := decodeScalar_sound._proof_3, exponentBias_le_maxFinite := decodeScalar_sound._proof_4 }.fracWidth { expWidth := 8, expWidth_ge_two := decodeScalar_sound._proof_1, fracWidth := 23, fracWidth_pos := decodeScalar_sound._proof_2, exponentBias := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8, encoding := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee, exponentBias_pos := decodeScalar_sound._proof_3, exponentBias_le_maxFinite := decodeScalar_sound._proof_4 }.encoding { expWidth := 8, expWidth_ge_two := decodeScalar_sound._proof_1, fracWidth := 23, fracWidth_pos := decodeScalar_sound._proof_2, exponentBias := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8, encoding := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee, exponentBias_pos := decodeScalar_sound._proof_3, exponentBias_le_maxFinite := decodeScalar_sound._proof_4 }.exponentBias ⋯ ⋯ ⋯ ⋯ (FloatLib.Floats.Formats.BinaryInterchange.Configured.StoragePlan.forKnownWidth (FloatLib.Floats.ExecFloat.Binary.descriptor 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) decodeScalar_sound._proof_1 decodeScalar_sound._proof_2 decodeScalar_sound._proof_3 decodeScalar_sound._proof_4) (1 + 8 + 23) ⋯) (FloatLib.Floats.Formats.BinaryInterchange.Configured.Code (FloatLib.Floats.Formats.BinaryInterchange.Configured.StoragePlan.forKnownWidth (FloatLib.Floats.ExecFloat.Binary.descriptor 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) decodeScalar_sound._proof_1 decodeScalar_sound._proof_2 decodeScalar_sound._proof_3 decodeScalar_sound._proof_4) (1 + 8 + 23) ⋯))) => v.toModel.toReal) value

Tensor decoding is the pointwise exact-real interpretation of finite binary32 words.

theorem NN.Verification.Cert.FiniteArtifact.affineDifference_eval {n m : ℕ} (left right : MLTheory.CROWN.AffineVec ℚ n m) (x : TorchLean.Tensor ℝ [n]) (i : Fin m) : (MLTheory.CROWN.Graph.CrownCertSoundness.affineEvalAt (RationalReflection.realAffine (affineDifference left right)) x).getScalar i = (MLTheory.CROWN.Graph.CrownCertSoundness.affineEvalAt (RationalReflection.realAffine left) x).getScalar i - (MLTheory.CROWN.Graph.CrownCertSoundness.affineEvalAt (RationalReflection.realAffine right) x).getScalar i

Evaluation of a difference of decoded affine forms is their exact real difference.

theorem NN.Verification.Cert.FiniteArtifact.dominates_sound {n m : ℕ} (supplied exact : CROWNQuery.Bounds n m) (input : MLTheory.CROWN.Box ℚ [n]) (h : dominates supplied exact input = true) (x : TorchLean.Tensor ℝ [n]) (y : TorchLean.Tensor ℝ [m]) (hx : MLTheory.CROWN.Graph.Theorems.Semantics.encloses { dim := n, lo := RationalReflection.realTensor input.lo, hi := RationalReflection.realTensor input.hi } x) (hy : exact.Encloses x y) : supplied.Encloses x y

Accepted dominance transfers an enclosure to the supplied artifact coefficients.

noncomputable def NN.Verification.Cert.FiniteArtifact.Program.eval {n m : ℕ} (program : Program n m) (x : TorchLean.Tensor ℝ [n]) : TorchLean.Tensor ℝ [m]

Exact-real semantics of the program decoded independently from the graph and parameters.

theorem NN.Verification.Cert.FiniteArtifact.Chain.check_sound {n m : ℕ} (chain : Chain n m) (input : MLTheory.CROWN.Box ℚ [n]) (h : chain.check input = true) (x : TorchLean.Tensor ℝ [n]) (hx : MLTheory.CROWN.Graph.Theorems.Semantics.encloses { dim := n, lo := RationalReflection.realTensor input.lo, hi := RationalReflection.realTensor input.hi } x) : chain.bounds.Encloses x (chain.program.eval x)

Local same-artifact checks enclose the exact-real computation at the covered output. The artifact's bounds and relaxation slopes do not alter the value, which is that of the erased program.

def NN.Verification.Cert.FiniteArtifact.Decoded.Safe (decoded : Decoded) : Prop

Every requested inequality holds at the exact-real output of the decoded program.

theorem NN.Verification.Cert.FiniteArtifact.Decoded.check_sound (decoded : Decoded) (h : decoded.check = true) : decoded.Safe

The local checks prove every output margin, including strict inequalities.

theorem NN.Verification.Cert.FiniteArtifact.Decoded.check_nonempty (decoded : Decoded) (h : decoded.check = true) : 0 < decoded.graph.inputDim ∧ 0 < decoded.graph.outputDim ∧ 0 < decoded.numConstraints

Accepted checks cannot discharge an empty family of input, output, or margin coordinates.

theorem NN.Verification.Cert.FiniteArtifact.attach_bounds (cert : NodeReplay.CROWNCertificate) {n m : ℕ} (input : MLTheory.CROWN.Box ℚ [n]) (program : Program n m) (attached : Attached program) (h : attach cert input program = some attached) : nodeBounds cert (program.length - 1) n m = some attached.chain.bounds

Attaching an artifact retains its final supplied entry.

theorem NN.Verification.Cert.FiniteArtifact.decode_coverage (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) decodeScalar_sound._proof_1 decodeScalar_sound._proof_2 decodeScalar_sound._proof_3 decodeScalar_sound._proof_4)) (cert : NodeReplay.CROWNCertificate) (query : OutputQuery) (decoded : Decoded) (h : decode g ps cert query = some decoded) : decodeGraph g ps = some decoded.graph ∧ query.outputId + 1 = g.nodes.size ∧ decoded.graph.program.length = g.nodes.size ∧ nodeBounds cert query.outputId decoded.graph.inputDim decoded.graph.outputDim = some decoded.artifact.chain.bounds

Node-count and final-entry coverage, without an assertion about Graph.denote.

theorem NN.Verification.Cert.FiniteArtifact.accepts_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) decodeScalar_sound._proof_1 decodeScalar_sound._proof_2 decodeScalar_sound._proof_3 decodeScalar_sound._proof_4)) (cert : NodeReplay.CROWNCertificate) (query : OutputQuery) (h : accepts g ps cert query = true) : ∃ (decoded : Decoded), decode g ps cert query = some decoded ∧ decodeGraph g ps = some decoded.graph ∧ query.outputId + 1 = g.nodes.size ∧ 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 ∧ decoded.Safe

Acceptance proves the decoded program's margins without caller-supplied semantic premises.