theorem Proofs.Autograd.Algebra.Graph.backprop_correct
  {α : Type} [TorchLean.Storage α]
  [CommSemiring α] {Δ : Type}
  {Γ ss : List Spec.Shape}
  (g :
    Proofs.Autograd.Algebra.Graph Δ Γ ss)
  (x dx : TorchLean.TensorPack α Γ)
  (d : Δ)
  (seed :
    TorchLean.TensorPack α (Γ ++ ss)) :
  Proofs.Autograd.Algebra.TensorPack.dotList
      (g.jvpCtx x dx d) seed =
    Proofs.Autograd.Algebra.TensorPack.dotList
      dx (g.backpropCtx x d seed)

theorem Proofs.Autograd.Algebra.Graph.backwardDenseFrom_lowerGraphToTape_eq_backpropAllCtx
  {α Δ : Type} [TorchLean.Storage α]
  [CommSemiring α]
  {Γ ss : List Spec.Shape}
  (g :
    Proofs.Autograd.Algebra.Graph Δ Γ ss)
  (x : TorchLean.TensorPack α Γ) (d0 : Δ)
  (seed :
    TorchLean.TensorPack α (Γ ++ ss)) :
  (g.lowerGraphToTape x
            d0).1.backwardDenseFrom
      seed.toShapeErasedArray =
    Except.ok
      (g.backpropAllCtx x d0
          seed).toShapeErasedArray

theorem Proofs.Autograd.Graph.backprop_correct_inner
  {Γ ss : List Spec.Shape}
  (g : Proofs.Autograd.Graph Γ ss)
  (xV dxV : Proofs.Autograd.CtxVec Γ)
  (seedV :
    Proofs.Autograd.CtxVec (Γ ++ ss)) :
  inner ℝ (g.jvpVec xV dxV) seedV =
    inner ℝ dxV (g.backpropVec xV seedV)

theorem Proofs.Autograd.Graph.backpropVec_eq_adjoint_fderiv_at
  {Γ ss : List Spec.Shape}
  (g : Proofs.Autograd.Graph Γ ss)
  (xV : Proofs.Autograd.CtxVec Γ)
  (seedV :
    Proofs.Autograd.CtxVec (Γ ++ ss)) :
  ∀
    (a :
      Proofs.Autograd.GraphFDerivCorrectAt
        g xV),
    g.backpropVec xV seedV =
      (ContinuousLinearMap.adjoint
          (fderiv ℝ g.evalVec xV))
        seedV

theorem Proofs.Autograd.Algebra.Graph.backwardDenseFrom_lowerGraphToTape_adjoint_fderiv_at
  {Δ : Type} {Γ ss : List Spec.Shape}
  (g :
    Proofs.Autograd.Algebra.Graph Δ Γ ss)
  (x : TorchLean.TensorPack ℝ Γ) (d0 : Δ)
  (seed :
    TorchLean.TensorPack ℝ (Γ ++ ss))
  (hg :
    Proofs.Autograd.GraphFDerivCorrectAt
      (g.toReal d0)
      (Proofs.Autograd.flattenCtx x)) :
  (g.lowerGraphToTape x
              d0).1.backwardDenseFrom
        seed.toShapeErasedArray =
      Except.ok
        (g.backpropAllCtx x d0
            seed).toShapeErasedArray ∧
    Proofs.Autograd.flattenCtx
        (Proofs.Autograd.Algebra.TensorPack.takeLeft
          (g.backpropAllCtx x d0 seed)) =
      (ContinuousLinearMap.adjoint
          (fderiv ℝ (g.toReal d0).evalVec
            (Proofs.Autograd.flattenCtx
              x)))
        (Proofs.Autograd.flattenCtx seed)

theorem Proofs.Autograd.Algebra.Graph.lowerGraphToTape_zeroPreserving
  {α : Type} [TorchLean.Storage α]
  [CommSemiring α] {Δ : Type}
  {Γ ss : List Spec.Shape}
  (g :
    Proofs.Autograd.Algebra.Graph Δ Γ ss)
  (x : TorchLean.TensorPack α Γ)
  (d0 : Δ) :
  Proofs.Autograd.Algebra.Graph.ZeroPreserving
    (g.lowerGraphToTape x d0).1

theorem Proofs.Autograd.Algebra.Graph.backwardDenseAll_lowerGraphToTape_eq_backpropAllCtx
  {α : Type} [TorchLean.Storage α]
  [CommSemiring α] {Δ : Type}
  {Γ ss : List Spec.Shape}
  (g :
    Proofs.Autograd.Algebra.Graph Δ Γ ss)
  (x : TorchLean.TensorPack α Γ) (d0 : Δ)
  {τ : Spec.Shape}
  (output : Proofs.Idx (Γ ++ ss) τ)
  (seed : TorchLean.Tensor α τ) :
  (g.lowerGraphToTape x
            d0).1.backwardDenseAll
      (↑output.i)
      (Spec.SomeTensor.ofTensor seed) =
    Except.ok
      (g.backpropAllCtx x d0
          (Proofs.Autograd.Algebra.TensorPack.single
            output
            seed)).toShapeErasedArray

theorem Proofs.Autograd.Algebra.Graph.backwardDenseAll_lowerGraphToTape_adjoint_fderiv
  {Δ : Type} {Γ ss : List Spec.Shape}
  (g :
    Proofs.Autograd.Algebra.Graph Δ Γ ss)
  (x : TorchLean.TensorPack ℝ Γ) (d0 : Δ)
  {τ : Spec.Shape}
  (output : Proofs.Idx (Γ ++ ss) τ)
  (seed : TorchLean.Tensor ℝ τ)
  (hg :
    Proofs.Autograd.GraphFDerivCorrect
      (g.toReal d0)) :
  (g.lowerGraphToTape x
              d0).1.backwardDenseAll
        (↑output.i)
        (Spec.SomeTensor.ofTensor seed) =
      Except.ok
        (g.backpropAllCtx x d0
            (Proofs.Autograd.Algebra.TensorPack.single
              output
              seed)).toShapeErasedArray ∧
    Proofs.Autograd.flattenCtx
        (Proofs.Autograd.Algebra.TensorPack.takeLeft
          (g.backpropAllCtx x d0
            (Proofs.Autograd.Algebra.TensorPack.single
              output seed))) =
      (ContinuousLinearMap.adjoint
          (fderiv ℝ (g.toReal d0).evalVec
            (Proofs.Autograd.flattenCtx
              x)))
        (Proofs.Autograd.flattenCtx
          (Proofs.Autograd.Algebra.TensorPack.single
            output seed))

theorem NN.Verification.Builtin.Proved.Correctness.lowerForwardProgramToIR_wellFormed
  {α : Type} [TorchLean.Storage α]
  [Context α]
  {paramShapes : List Spec.Shape}
  {inShape outShape : Spec.Shape}
  (p :
    NN.Verification.Builtin.Proved.ForwardProgram
      α paramShapes inShape outShape)
  (params :
    TorchLean.TensorPack α paramShapes) :
  (NN.Verification.Builtin.Proved.lowerForwardProgramToIR
          p params).graph.wellFormed =
    true

theorem NN.Verification.Builtin.Proved.Correctness.runForwardIR_eq_evalForward
  {α : Type} [TorchLean.Storage α]
  [Context α]
  {paramShapes : List Spec.Shape}
  {inShape outShape : Spec.Shape}
  (p :
    NN.Verification.Builtin.Proved.ForwardProgram
      α paramShapes inShape outShape)
  (params :
    TorchLean.TensorPack α paramShapes)
  (x : TorchLean.Tensor α inShape) :
  NN.Verification.Builtin.runForwardIR
      (NN.Verification.Builtin.Proved.lowerForwardProgramToIR
        p params)
      x =
    NN.Verification.Builtin.Proved.evalForward
      p params x

theorem NN.MLTheory.CROWN.Graph.CertSoundness.cert_encloses_semantics
  (g : NN.MLTheory.CROWN.Graph)
  (ps :
    NN.MLTheory.CROWN.Graph.ParamStore ℝ)
  (cert :
    Array
      (Option
        (NN.MLTheory.CROWN.FlatBox ℝ)))
  (inputs :
    Std.HashMap ℕ
      NN.MLTheory.CROWN.Graph.CertSoundness.Val)
  (vals :
    Array
      (Option
        NN.MLTheory.CROWN.Graph.CertSoundness.Val))
  (htopo :
    NN.MLTheory.CROWN.Graph.CertSoundness.TopoSorted
      g)
  (hsupp :
    NN.MLTheory.CROWN.Graph.CertSoundness.Supported
      g)
  (hcert :
    NN.MLTheory.CROWN.Graph.CertSoundness.CertLocalOK
      g ps cert)
  (hsem :
    NN.MLTheory.CROWN.Graph.CertSoundness.SemLocalOK
      g ps inputs vals)
  (hinputs :
    NN.MLTheory.CROWN.Graph.CertSoundness.InputsEnclosed
      g ps inputs)
  (id : ℕ) :
  id < g.nodes.size →
    match cert[id]!, vals[id]! with
    | some B, some v =>
      NN.MLTheory.CROWN.Graph.CertSoundness.EnclosesBox
        B v
    | x, x_1 => True

theorem NN.MLTheory.CROWN.Graph.CertSoundness.runIBP?_encloses_evalGraphRec
  (g : NN.MLTheory.CROWN.Graph)
  (ps :
    NN.MLTheory.CROWN.Graph.ParamStore ℝ)
  (inputs :
    Std.HashMap ℕ
      NN.MLTheory.CROWN.Graph.CertSoundness.Val)
  (htopo :
    NN.MLTheory.CROWN.Graph.CertSoundness.TopoSorted
      g)
  (hsupp :
    NN.MLTheory.CROWN.Graph.CertSoundness.Supported
      g)
  (hinputs :
    NN.MLTheory.CROWN.Graph.CertSoundness.InputsEnclosed
      g ps inputs)
  (id : ℕ) :
  id < g.nodes.size →
    match
      (NN.MLTheory.CROWN.Graph.CertSoundness.runIBP?
          g ps)[id]!,
      (NN.MLTheory.CROWN.Graph.CertSoundness.evalGraphRec
          g ps inputs)[id]! with
    | some B, some v =>
      NN.MLTheory.CROWN.Graph.CertSoundness.EnclosesBox
        B v
    | x, x_1 => True

theorem NN.MLTheory.CROWN.Graph.CertSoundness.runIBP_eq_runIBP?
  (g : NN.MLTheory.CROWN.Graph)
  (ps :
    NN.MLTheory.CROWN.Graph.ParamStore ℝ)
  (htopo :
    NN.MLTheory.CROWN.Graph.CertSoundness.TopoSorted
      g)
  (hcore :
    NN.MLTheory.CROWN.Graph.CertSoundness.EngineCore
      g)
  (hguard :
    g.crownGraphSemanticsSupported ps =
      true)
  (hcov :
    NN.MLTheory.CROWN.Graph.CertSoundness.IBPCovers
      g
      (NN.MLTheory.CROWN.Graph.CertSoundness.runIBP?
        g ps)) :
  g.runIBP ps =
    NN.MLTheory.CROWN.Graph.CertSoundness.runIBP?
      g ps

theorem NN.MLTheory.CROWN.Graph.CertSoundness.runIBP_encloses_evalGraphRec
  (g : NN.MLTheory.CROWN.Graph)
  (ps :
    NN.MLTheory.CROWN.Graph.ParamStore ℝ)
  (inputs :
    Std.HashMap ℕ
      NN.MLTheory.CROWN.Graph.CertSoundness.Val)
  (htopo :
    NN.MLTheory.CROWN.Graph.CertSoundness.TopoSorted
      g)
  (hcore :
    NN.MLTheory.CROWN.Graph.CertSoundness.EngineCore
      g)
  (hcov :
    NN.MLTheory.CROWN.Graph.CertSoundness.IBPCovers
      g
      (NN.MLTheory.CROWN.Graph.CertSoundness.runIBP?
        g ps))
  (hinputs :
    NN.MLTheory.CROWN.Graph.CertSoundness.InputsEnclosed
      g ps inputs)
  (id : ℕ) :
  id < g.nodes.size →
    ∀ (B : NN.MLTheory.CROWN.FlatBox ℝ)
      (v :
        NN.MLTheory.CROWN.Graph.CertSoundness.Val),
      (g.runIBP ps)[id]! = some B →
        (NN.MLTheory.CROWN.Graph.CertSoundness.evalGraphRec
                g ps inputs)[id]! =
            some v →
          NN.MLTheory.CROWN.Graph.CertSoundness.EnclosesBox
            B v

theorem NN.MLTheory.CROWN.Graph.CertSoundness.evalNode_bridge
  (nodes :
    Array NN.MLTheory.CROWN.Graph.Node)
  (payload : NN.IR.Payload ℝ)
  (ps :
    NN.MLTheory.CROWN.Graph.ParamStore ℝ)
  (input : Spec.SomeTensor ℝ)
  (inputs :
    Std.HashMap ℕ
      NN.MLTheory.CROWN.Graph.CertSoundness.Val)
  (rvals : Array (Spec.SomeTensor ℝ))
  (i : ℕ)
  (n : NN.MLTheory.CROWN.Graph.Node)
  (t : Spec.SomeTensor ℝ)
  (hps :
    NN.MLTheory.CROWN.Graph.CertSoundness.PayloadMatches
      payload ps)
  (hin :
    NN.MLTheory.CROWN.Graph.CertSoundness.InputsLift
      nodes input inputs)
  (hi : i < nodes.size)
  (hn : nodes[i]! = n) (hid : n.id = i)
  (hkind :
    NN.MLTheory.CROWN.Graph.CertSoundness.Bridged
      n.kind)
  (hvec :
    n.kind = NN.IR.OpKind.linear →
      ∀ p ∈ n.parents,
        ∀ (r : Spec.SomeTensor ℝ),
          rvals[p]? = some r →
            NN.MLTheory.CROWN.Graph.CertSoundness.IsVector
              r)
  (heval :
    NN.IR.Graph.evalNode payload input
        rvals i n =
      Except.ok t) :
  NN.MLTheory.CROWN.Graph.CertSoundness.evalNode?
      nodes ps inputs
      (NN.MLTheory.CROWN.Graph.CertSoundness.liftVals
        rvals)
      i =
    some
      (NN.MLTheory.CROWN.Graph.CertSoundness.flatOfSome
        t)