One semantic universe

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

This tutorial is intentionally not part of the beginner training tutorials; it lives under NN/Examples/Advanced.

We build one medium IR graph:

x ↦ tanh(sum(Linear2(ReLU(Linear1(x)))))

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 sanity-check that evalIEEE(G,x) lies in the IBP output box for random x ∈ 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 sanity check.

Run: lake exe torchlean one_semantic_universe --samples 50

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

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

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

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

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

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

def NN.Examples.Advanced.OneSemanticUniverse.W1Shape : Spec.Shape

def NN.Examples.Advanced.OneSemanticUniverse.b1Shape : Spec.Shape

def NN.Examples.Advanced.OneSemanticUniverse.W2Shape : Spec.Shape

def NN.Examples.Advanced.OneSemanticUniverse.b2Shape : Spec.Shape

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

• W1 : Spec.Tensor α W1Shape

  Weight matrix for layer 1.

• b1 : Spec.Tensor α b1Shape

  Bias for layer 1.

• W2 : Spec.Tensor α W2Shape

  Weight matrix for layer 2.

• b2 : Spec.Tensor α b2Shape

  Bias for layer 2.

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

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

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

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

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

def NN.Examples.Advanced.OneSemanticUniverse.evalOut {α : Type} [Context α] [Inhabited α] [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.Advanced.OneSemanticUniverse.x0Float : Spec.Tensor Float xShape

def NN.Examples.Advanced.OneSemanticUniverse.xBoxOf (α : Type) [API.Semantics.Scalar α] [API.Runtime.Scalar α] (eps : Float) : MLTheory.CROWN.Box α xShape

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

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

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

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

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