import Vickrey.SettlementGasful
import Vickrey.Bytecode

/-! The required frame-level guarantee fixes the committed runtime bytes.
Source interpreter fuel and EVM gas are separate quantities. Arbitrary gas
may cause OutOfGas; no sufficient-gas bound or deployment theorem is asserted.
-/
namespace Vickrey
open EvmCompiler Assembly Simulation

/-- Closed compiler prerequisites for the exact committed runtime. -/
def StructuredCompilerExact : Prop :=
  ∃ (frontend : Solidity.Frontend.Object)
      (artifact : Solidity.Frontend.VerifiedStackObjectArtifact)
      (cert : StackHeadroom.Cert),
    Generated.ast.elaboratePreservingOrder? .cancun = .ok frontend ∧
    frontend.compileVerifiedStackObjectArtifactWithLinkerSymbols? [] = some artifact ∧
    StackHeadroom.check? artifact.codeArtifact.compact cert = true ∧
    artifact.image.bytes = Generated.runtimeBytes

def ExactRuntimeGasfulSettlement : Prop :=
  ∀ (a b : Bid) (base : SourceState) (gas : EvmYul.UInt256),
    ∃ openFuel : Nat,
      let run := EvmYul.EVM.X (max openFuel (gas.toNat + 6))
        (EvmYul.EVM.D_J (Bytecode.ofList Generated.runtimeBytes)
          (EvmYul.UInt256.ofNat 0))
        (freshGasfulEntry Generated.runtimeBytes base a b gas)
      (∃ final, run = .ok (.success final (encodeOutcome (auction a.val b.val)))) ∨
        GasfulBridge.OutOfGasFrameSemantics run

end Vickrey