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.DirectedBackward.runIBP_encloses {α : Type}
  [TorchLean.Storage α] [Context α] [NN.MLTheory.CROWN.BoundOps α]
  [NN.MLTheory.CROWN.LawfulBoundOps α]
  [NN.MLTheory.CROWN.NonlinearBoundOps α]
  [NN.MLTheory.CROWN.LawfulNonlinearBoundOps α]
  (g : NN.MLTheory.CROWN.Graph)
  (ps : NN.MLTheory.CROWN.Graph.ParamStore α) {dims : ℕ → ℕ}
  {v : ℕ → ℕ → ℝ}
  (hparent : ∀ id < g.nodes.size, ∀ p ∈ g.nodes[id]!.parents, p < id)
  (hsupported :
    NN.MLTheory.CROWN.Graph.DirectedBackward.ibpForwardSupported
        g.nodes =
      true)
  (hinputs :
    NN.MLTheory.CROWN.Graph.DirectedBackward.InputsInBoxes g.nodes ps
      dims v)
  (hequation :
    ∀ id < g.nodes.size,
      NN.MLTheory.CROWN.Graph.DirectedBackward.NodeEquation g.nodes ps
        (g.runIBP ps) dims v id)
  (id : ℕ) :
  id < g.nodes.size →
    ∀ (box : NN.MLTheory.CROWN.FlatBox α),
      (g.runIBP ps)[id]! = some box →
        NN.MLTheory.CROWN.Graph.DirectedBackward.RowEncloses box
          (dims id) (v id)