One semantic universe

End-to-end “one semantic universe” tutorial (single graph, many semantics, one checker).

This tutorial lives under NN/Examples/DeepDives because it connects execution, interval semantics, and checker soundness in one graph.

We build one medium IR graph:

$$ x\mapsto\tanh\!\left(\operatorname{sum} \left(\operatorname{Linear}_2(\operatorname{ReLU}(\operatorname{Linear}_1(x)))\right)\right) $$

and then:

1. evaluate it under multiple scalar semantics (ℝ, FP32, IEEE32Exec);
2. run IBP under multiple interval semantics (endpoints in ℝ, FP32, IEEE32Exec with directed rounding);
3. empirically check that evalIEEE(G,x) lies in the IBP output box for random $x\in B$;
4. point to the Lean theorem that the Boolean checker is sound (Box.containsDecBool_sound).

Notes:

• ℝ and FP32 instantiations are proof-oriented and noncomputable (they typecheck, but do not run as an executable).
• IEEE32Exec is fully executable inside Lean, so we use it for the runnable consistency check.

Run: lake exe torchlean one_semantic_universe --samples 50

def NN.Examples.DeepDives.OneSemanticUniverse.usage : String

Command-line help for the one-semantics tutorial.

def NN.Examples.DeepDives.OneSemanticUniverse.inDim : ℕ

def NN.Examples.DeepDives.OneSemanticUniverse.hidDim : ℕ

def NN.Examples.DeepDives.OneSemanticUniverse.outDim : ℕ

def NN.Examples.DeepDives.OneSemanticUniverse.xShape : Spec.Shape

def NN.Examples.DeepDives.OneSemanticUniverse.hShape : Spec.Shape

def NN.Examples.DeepDives.OneSemanticUniverse.yShape : Spec.Shape

def NN.Examples.DeepDives.OneSemanticUniverse.hiddenWeightShape : Spec.Shape

def NN.Examples.DeepDives.OneSemanticUniverse.hiddenBiasShape : Spec.Shape

def NN.Examples.DeepDives.OneSemanticUniverse.outputWeightShape : Spec.Shape

def NN.Examples.DeepDives.OneSemanticUniverse.outputBiasShape : Spec.Shape

structure NN.Examples.DeepDives.OneSemanticUniverse.Params (α : Type) : Type

• hiddenWeight : Spec.Tensor α hiddenWeightShape

  Weight matrix for layer 1.

• hiddenBias : Spec.Tensor α hiddenBiasShape

  Bias for layer 1.

• outputWeight : Spec.Tensor α outputWeightShape

  Weight matrix for layer 2.

• outputBias : Spec.Tensor α outputBiasShape

  Bias for layer 2.

def NN.Examples.DeepDives.OneSemanticUniverse.Params.map {α β : Type} (f : α → β) (p : Params α) : Params β

def NN.Examples.DeepDives.OneSemanticUniverse.paramsFloat : Params Float

def NN.Examples.DeepDives.OneSemanticUniverse.g : IR.Graph

def NN.Examples.DeepDives.OneSemanticUniverse.mkPayload {α : Type} [Context α] (p : Params α) : IR.Payload α

def NN.Examples.DeepDives.OneSemanticUniverse.mkParamStore {α : Type} [Context α] (p : Params α) (xB : MLTheory.CROWN.FlatBox α) : MLTheory.CROWN.Graph.ParamStore α

def NN.Examples.DeepDives.OneSemanticUniverse.evalOut {α : Type} [Context α] [DecidableEq Spec.Shape] (p : Params α) (x : Spec.Tensor α xShape) : Except String (Spec.Tensor α Spec.Shape.scalar)

Proof-only instantiations (typechecks)

These have lines ensure we can interpret the same graph under:

• ℝ (reference semantics),
• FP32 (proof-oriented rounding-on-ℝ model),
• plus IBP over those endpoint types.

They live in a propositional example, so they do not affect the executable tutorial.

def NN.Examples.DeepDives.OneSemanticUniverse.referenceInputFloat : Spec.Tensor Float xShape

def NN.Examples.DeepDives.OneSemanticUniverse.xBoxOf (α : Type) [Context α] [TorchLean.Runtime.FromFloat α] (eps : Float) : MLTheory.CROWN.Box α xShape

def NN.Examples.DeepDives.OneSemanticUniverse.toFlatXBox {α : Type} [Context α] (B : MLTheory.CROWN.Box α xShape) : MLTheory.CROWN.FlatBox α

def NN.Examples.DeepDives.OneSemanticUniverse.scalarBoxOfFlat (B : MLTheory.CROWN.FlatBox TorchLean.Floats.IEEE32Exec) : Except String (MLTheory.CROWN.Box TorchLean.Floats.IEEE32Exec Spec.Shape.scalar)

def NN.Examples.DeepDives.OneSemanticUniverse.sampleInBoxIEEE (seed idx : ℕ) (B : MLTheory.CROWN.Box TorchLean.Floats.IEEE32Exec xShape) : Spec.Tensor TorchLean.Floats.IEEE32Exec xShape

def NN.Examples.DeepDives.OneSemanticUniverse.showIEEECheck (samples : ℕ) : IO Unit

def NN.Examples.DeepDives.OneSemanticUniverse.main (args : List String) : IO Unit