Finite binary32 affine artifacts

The additional checks in this module interpret the supplied binary32 coefficients exactly. Local rational dominance checks repair the gap between agreement with rounded affine replay and enclosure of the decoded program's real computation. The supported graph fragment is a nonempty vector input followed by unary linear and ReLU nodes. The decoder checks the graph's structure and parameters. FiniteArtifactSemantics proves agreement between Program.eval and NN.IR.Graph.denote under the payload decoded from the same parameters, then establishes the requested margins for the original graph.

def NN.Verification.Cert.FiniteArtifact.decodeTensor {s : Spec.Shape} : TorchLean.Tensor (FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) decodeTensor._proof_1 decodeTensor._proof_2 decodeTensor._proof_3 decodeTensor._proof_4) s → Option (TorchLean.Tensor ℚ s)

Decode every scalar exactly, rejecting both infinities and NaNs.

def NN.Verification.Cert.FiniteArtifact.decodeAffine {n m : ℕ} (a : MLTheory.CROWN.AffineVec (FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) decodeTensor._proof_1 decodeTensor._proof_2 decodeTensor._proof_3 decodeTensor._proof_4) n m) : Option (MLTheory.CROWN.AffineVec ℚ n m)

Decode the coefficients of one supplied affine form.

def NN.Verification.Cert.FiniteArtifact.decodeBounds (n m : ℕ) (b : MLTheory.CROWN.Graph.FlatAffineBounds (FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) decodeTensor._proof_1 decodeTensor._proof_2 decodeTensor._proof_3 decodeTensor._proof_4)) : Option (CROWNQuery.Bounds n m)

Require the artifact's input and output dimensions to match the decoded node.

def NN.Verification.Cert.FiniteArtifact.affineDifference {n m : ℕ} (left right : MLTheory.CROWN.AffineVec ℚ n m) : MLTheory.CROWN.AffineVec ℚ n m

The affine difference whose nonpositivity expresses pointwise domination.

def NN.Verification.Cert.FiniteArtifact.dominates {n m : ℕ} (supplied exact : CROWNQuery.Bounds n m) (input : MLTheory.CROWN.Box ℚ [n]) : Bool

The supplied lower form is no larger, and its upper form no smaller, than the exact transfer.

inductive NN.Verification.Cert.FiniteArtifact.Chain (n : ℕ) : ℕ → Type

A decoded vector graph, including the affine entry supplied for every node.

• input {n : ℕ} (bounds : CROWNQuery.Bounds n n) : Chain n n
• linear {n m k : ℕ} (parent : Chain n m) (layer : Spec.LinearSpec ℚ m k) (bounds : CROWNQuery.Bounds n k) : Chain n k
• relu {n m : ℕ} (parent : Chain n m) (alpha : TorchLean.Tensor ℚ [m]) (bounds : CROWNQuery.Bounds n m) : Chain n m

def NN.Verification.Cert.FiniteArtifact.Chain.bounds {n m : ℕ} : Chain n m → CROWNQuery.Bounds n m

The actual artifact entry at the final node.

def NN.Verification.Cert.FiniteArtifact.Chain.check {n m : ℕ} (chain : Chain n m) (input : MLTheory.CROWN.Box ℚ [n]) : Bool

Check every supplied node entry against a transfer from its already checked parent.

inductive NN.Verification.Cert.FiniteArtifact.Program (n : ℕ) : ℕ → Type

The graph computation after finite parameter decoding, independent of any certificate.

• input {n : ℕ} : Program n n
• linear {n m k : ℕ} (parent : Program n m) (layer : Spec.LinearSpec ℚ m k) : Program n k
• relu {n m : ℕ} (parent : Program n m) : Program n m

def NN.Verification.Cert.FiniteArtifact.Program.length {n m : ℕ} : Program n m → ℕ

Count every node of the decoded graph, including its input.

def NN.Verification.Cert.FiniteArtifact.Chain.program {n m : ℕ} : Chain n m → Program n m

Erase certificate entries and relaxation choices without changing the graph computation.

structure NN.Verification.Cert.FiniteArtifact.DecodedGraph : Type

Finite parameters and input domain decoded from the graph, without consulting an artifact.

• inputDim : ℕ
• outputDim : ℕ
• input : MLTheory.CROWN.Box ℚ [self.inputDim]
• program : Program self.inputDim self.outputDim

def NN.Verification.Cert.FiniteArtifact.decodeTail (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) decodeTensor._proof_1 decodeTensor._proof_2 decodeTensor._proof_3 decodeTensor._proof_4)) {n : ℕ} : List MLTheory.CROWN.Graph.Node → {m : ℕ} → Program n m → Option ((k : ℕ) × Program n k)

Decode the remaining graph nodes, requiring the immediately preceding node as sole parent.

def NN.Verification.Cert.FiniteArtifact.decodeGraph (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) decodeTensor._proof_1 decodeTensor._proof_2 decodeTensor._proof_3 decodeTensor._proof_4)) : Option DecodedGraph

Decode exactly one nonempty vector input and a unary linear/ReLU chain.

structure NN.Verification.Cert.FiniteArtifact.Attached {n m : ℕ} (program : Program n m) : Type

An artifact attached to a particular independently decoded graph.

• chain : Chain n m
• sameProgram : self.chain.program = program

def NN.Verification.Cert.FiniteArtifact.nodeBounds (cert : NodeReplay.CROWNCertificate) (id n m : ℕ) : Option (CROWNQuery.Bounds n m)

Read a mandatory finite affine entry for a covered graph node.

def NN.Verification.Cert.FiniteArtifact.attach (cert : NodeReplay.CROWNCertificate) {n : ℕ} (input : MLTheory.CROWN.Box ℚ [n]) {m : ℕ} (program : Program n m) : Option (Attached program)

Attach the actual per-node coefficients; a missing entry causes rejection.

structure NN.Verification.Cert.FiniteArtifact.OutputQuery : Type

Requested inequalities at an explicitly designated output, with binary32 coefficients.

• outputId : ℕ
• inequalities : 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) decodeTensor._proof_1 decodeTensor._proof_2 decodeTensor._proof_3 decodeTensor._proof_4)
• strict : Bool

structure NN.Verification.Cert.FiniteArtifact.Decoded : Type

The graph, its attached artifact, and the exact interpretation of the requested margins.

• graph : DecodedGraph
• artifact : Attached self.graph.program
• numConstraints : ℕ
• inequalities : Spec.LinearSpec ℚ self.graph.outputDim self.numConstraints
• strict : Bool

def NN.Verification.Cert.FiniteArtifact.decode (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) decodeTensor._proof_1 decodeTensor._proof_2 decodeTensor._proof_3 decodeTensor._proof_4)) (cert : NodeReplay.CROWNCertificate) (query : OutputQuery) : Option Decoded

Decode the same graph, parameters, domain, artifact, and output query that acceptance checks.

def NN.Verification.Cert.FiniteArtifact.Decoded.check (decoded : Decoded) : Bool

Check nonempty dimensions, the input box, local artifact dominance, and all output margins.

def NN.Verification.Cert.FiniteArtifact.replayAccepts (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) decodeTensor._proof_1 decodeTensor._proof_2 decodeTensor._proof_3 decodeTensor._proof_4)) (cert : NodeReplay.CROWNCertificate) : Bool

Exact binary32 local replay of the same artifact. This is a diagnostic: it holds only when the artifact is bit-identical to Lean's own transcript, and accepts does not use it.

def NN.Verification.Cert.FiniteArtifact.accepts (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) decodeTensor._proof_1 decodeTensor._proof_2 decodeTensor._proof_3 decodeTensor._proof_4)) (cert : NodeReplay.CROWNCertificate) (query : OutputQuery) : Bool

Decode the covered program and run the exact-real dominance and margin checks. Any producer whose bounds dominate the exact transfers is accepted, whether or not they match binary32 replay.