Dispatch.lean

/-
  Compiler.CompilationModel.Dispatch: Contract assembly and entrypoint wiring

  This module builds IR functions, constructor code, and whole contracts from
  the lower-level statement/expression compilation helpers.
-/
import Compiler.CompilationModel.Compile
import Compiler.CompilationModel.InternalArgs
import Compiler.CompilationModel.ParamLoading
import Compiler.CompilationModel.ScopeValidation
import Compiler.CompilationModel.TrustSurface
import Verity.Core.Intrinsics

namespace Compiler.CompilationModel

open Compiler
open Compiler.Yul
open Verity.Core.Intrinsics (HardFork)

/-- Pick a fresh internal return variable name for the given index. -/
def pickFreshInternalRetName (usedNames : List String) (idx : Nat) : String :=
  pickFreshName s!"__ret{idx}" usedNames

/-- Generate fresh internal return variable names for an internal function. -/
def freshInternalRetNames (returns : List ParamType) (usedNames : List String) : List String :=
  let retIndices :=
    returns.zipIdx.flatMap fun (retTy, idx) =>
      match retTy with
      | ParamType.array _ => [idx, idx]
      | _ => [idx]
  let (_, namesRev) := retIndices.foldl
    (fun (acc : List String × List String) idx =>
      let (used, names) := acc
      let fresh := pickFreshInternalRetName used idx
      (fresh :: used, fresh :: names))
    (usedNames, [])
  namesRev.reverse

-- Compile internal function to a Yul function definition (#181)
def compileInternalFunction (fields : List Field) (events : List EventDef) (errors : List ErrorDef)
    (adtTypes : List AdtTypeDef := []) (spec : FunctionSpec)
    (internalFunctions : List FunctionSpec := []) :
    Except String YulStmt := do
  validateFunctionSpec spec
  let returns ← functionReturns spec
  let paramNames := internalFunctionYulParamNames spec.params
  let usedNames := paramNames ++ collectStmtListBindNames spec.body
  let retNames := freshInternalRetNames returns usedNames
  let bodyStmts ← compileStmtList fields events errors .calldata retNames true
    (paramNames ++ retNames) adtTypes spec.body internalFunctions
  pure (YulStmt.funcDef (internalFunctionYulName spec.name) paramNames retNames bodyStmts)

theorem compileInternalFunction_ok_components
    (fields : List Field) (events : List EventDef) (errors : List ErrorDef)
    (spec : FunctionSpec) (stmt : YulStmt)
    (hcompile : compileInternalFunction fields events errors [] spec = Except.ok stmt) :
    ∃ returns retNames bodyStmts,
      validateFunctionSpec spec = Except.ok () ∧
      functionReturns spec = Except.ok returns ∧
      compileStmtList fields events errors .calldata retNames true
        (internalFunctionYulParamNames spec.params ++ retNames) [] spec.body = Except.ok bodyStmts ∧
      stmt = YulStmt.funcDef
        (internalFunctionYulName spec.name)
        (internalFunctionYulParamNames spec.params)
        retNames
        bodyStmts := by
  unfold compileInternalFunction at hcompile
  cases hvalidate : validateFunctionSpec spec
  · rw [hvalidate] at hcompile
    cases hcompile
  case ok _ =>
    cases hreturns : functionReturns spec
    · rw [hvalidate, hreturns] at hcompile
      cases hcompile
    case ok returns =>
      rw [hvalidate, hreturns] at hcompile
      simp only [bind, Except.bind] at hcompile
      cases hbody :
          compileStmtList fields events errors .calldata
            (freshInternalRetNames returns
              (internalFunctionYulParamNames spec.params ++ collectStmtListBindNames spec.body))
            true
            (internalFunctionYulParamNames spec.params ++
              freshInternalRetNames returns
                (internalFunctionYulParamNames spec.params ++ collectStmtListBindNames spec.body))
            []
            spec.body
      · rw [hbody] at hcompile
        cases hcompile
      case ok bodyStmts =>
        rw [hbody] at hcompile
        simp only [pure, Except.pure, Except.ok.injEq] at hcompile
        refine
          ⟨returns,
            freshInternalRetNames returns
              (internalFunctionYulParamNames spec.params ++ collectStmtListBindNames spec.body),
            bodyStmts,
            ?_⟩
        exact ⟨by simp, by simp,
          by simpa using hbody, by simpa using hcompile.symm⟩

theorem compileInternalFunction_some_ok_of_components
    (fields : List Field) (events : List EventDef) (errors : List ErrorDef)
    (spec : FunctionSpec) (returns : List ParamType) (retNames : List String)
    (bodyStmts : List YulStmt)
    (hvalidate : validateFunctionSpec spec = Except.ok ())
    (hreturns : functionReturns spec = Except.ok returns)
    (hretNames :
      retNames =
        freshInternalRetNames returns
          (internalFunctionYulParamNames spec.params ++ collectStmtListBindNames spec.body))
    (hbody :
      compileStmtList fields events errors .calldata retNames true
        (internalFunctionYulParamNames spec.params ++ retNames) [] spec.body = Except.ok bodyStmts) :
    compileInternalFunction fields events errors [] spec =
      Except.ok
        (YulStmt.funcDef
          (internalFunctionYulName spec.name)
          (internalFunctionYulParamNames spec.params)
          retNames
          bodyStmts) := by
  have hbody' :
      compileStmtList fields events errors .calldata
        (freshInternalRetNames returns
          (internalFunctionYulParamNames spec.params ++ collectStmtListBindNames spec.body))
        true
        (internalFunctionYulParamNames spec.params ++
          freshInternalRetNames returns
            (internalFunctionYulParamNames spec.params ++ collectStmtListBindNames spec.body))
        []
        spec.body = Except.ok bodyStmts := by
    simpa [hretNames] using hbody
  let paramNames := internalFunctionYulParamNames spec.params
  let compiledName := internalFunctionYulName spec.name
  have hmap :
      (YulStmt.funcDef
          compiledName
          paramNames
          (freshInternalRetNames returns (paramNames ++ collectStmtListBindNames spec.body))) <$>
        compileStmtList fields events errors .calldata
          (freshInternalRetNames returns (paramNames ++ collectStmtListBindNames spec.body))
          true
          (paramNames ++ freshInternalRetNames returns (paramNames ++ collectStmtListBindNames spec.body))
          []
          spec.body =
      Except.ok
        (YulStmt.funcDef
          compiledName
          paramNames
          (freshInternalRetNames returns (paramNames ++ collectStmtListBindNames spec.body))
          bodyStmts) := by
    simpa [paramNames, compiledName] using
      congrArg
        (fun compiledBody =>
          Except.map
            (fun compiledStmts =>
              YulStmt.funcDef
                compiledName
                paramNames
                (freshInternalRetNames returns (paramNames ++ collectStmtListBindNames spec.body))
                compiledStmts)
            compiledBody)
        hbody'
  unfold compileInternalFunction
  simp [hvalidate, hreturns]
  simpa [paramNames, compiledName, hretNames] using hmap

-- Compile function spec to IR function
def compileFunctionSpec (fields : List Field) (events : List EventDef) (errors : List ErrorDef)
    (adtTypes : List AdtTypeDef := []) (selector : Nat) (spec : FunctionSpec)
    (internalFunctions : List FunctionSpec := []) :
    Except String IRFunction := do
  validateFunctionSpec spec
  let returns ← functionReturns spec
  let paramLoads := genParamLoads spec.params
  let bodyStmts ← compileStmtList fields events errors .calldata [] false
    (spec.params.map (·.name)) adtTypes spec.body internalFunctions
  let allStmts := paramLoads ++ bodyStmts
  let retType := match returns with
    | [single] => single.toIRType
    | _ => IRType.unit
  return {
    name := spec.name
    selector := selector
    params := spec.params.map Param.toIRParam
    ret := retType
    payable := spec.isPayable
    body := allStmts
  }

/-- Build the Yul prologue for a `nonreentrant(lockField)` function (#1893).

    Uses **transient storage** (TLOAD / TSTORE introduced in Cancun) so the
    guard auto-clears at end-of-transaction and no exit-side cleanup is
    needed — even on early `return`, `revert`, or panic the lock cannot
    leak across transactions.

    The emitted Yul is:
    ```yul
    if eq(tload(<lockSlot>), 1) { revert(0, 0) }
    tstore(<lockSlot>, 1)
    ```

    `lockSlot` is the canonical slot resolved from the lock field name. The
    field is required to be a scalar `uint256` storage field by the macro
    validator (`Verity/Macro/Translate.lean` enforces this). Persistent
    storage at that slot is left untouched — only the transient mirror at
    the same numeric slot is used as the active lock, so legacy callers
    that initialise the field to zero need no migration. -/
def nonReentrantGuardPrologue (fields : List Field) (lockField : String) :
    Except String (List YulStmt) := do
  match findFieldWithResolvedSlot fields lockField with
  | none =>
      throw s!"Compilation error: nonreentrant lock '{lockField}' is not a declared storage field; declare it as a scalar uint256 field before annotating any function"
  | some (_field, slot) =>
      let lockSlot := YulExpr.lit slot
      let revertOnReentry :=
        YulStmt.if_
          (YulExpr.call "eq" [YulExpr.call "tload" [lockSlot], YulExpr.lit 1])
          [YulStmt.expr (YulExpr.call "revert" [YulExpr.lit 0, YulExpr.lit 0])]
      let acquire :=
        YulStmt.expr (YulExpr.call "tstore" [lockSlot, YulExpr.lit 1])
      pure [revertOnReentry, acquire]

/-- Wrap an already-compiled `IRFunction` with the `nonreentrant(lockField)`
    guard prologue (#1893) when the source `FunctionSpec` carries the
    annotation. The prologue is inserted **after** parameter loading and
    **before** the user-authored body so the lock check runs on every
    entry path before any user Yul can execute. Returns the input
    function unchanged when there is no `nonReentrantLock`.

    Kept separate from `compileFunctionSpec` so the IR-generation proof
    modules (which prove `compileFunctionSpec` produces a specific
    parameter-loads + body shape) are unaffected: the guard is a
    post-compilation transformation only applied to externals at the
    contract-assembly layer. -/
def attachNonReentrantGuard (fields : List Field) (spec : FunctionSpec)
    (irFn : IRFunction) : Except String IRFunction :=
  match spec.nonReentrantLock with
  | none => pure irFn
  | some lockField => do
      let guardStmts ← nonReentrantGuardPrologue fields lockField
      let paramLoadCount := (genParamLoads spec.params).length
      let (prefixLoads, suffix) := irFn.body.splitAt paramLoadCount
      -- Release the transient lock on normal exit so that a second top-level
      -- call to the same nonreentrant function in the same tx is allowed
      -- (the guard only protects against reentrancy *during* execution).
      -- Early returns/reverts inside the body may leave the lock set until
      -- tx end (transient), but this fixes the "never clears" case for the
      -- common fall-through path.
      let releaseSlot := match findFieldWithResolvedSlot fields lockField with
        | some (_, s) => s
        | none => 0   -- unreachable after prologue validation
      let release := YulStmt.expr (YulExpr.call "tstore" [YulExpr.lit releaseSlot, YulExpr.lit 0])
      pure { irFn with body := prefixLoads ++ guardStmts ++ suffix ++ [release] }

private def compileSpecialEntrypoint (fields : List Field) (events : List EventDef)
    (errors : List ErrorDef) (adtTypes : List AdtTypeDef := [])
    (internalFunctions : List FunctionSpec := []) (spec : FunctionSpec) :
    Except String IREntrypoint := do
  let bodyChunks ← compileStmtList fields events errors .calldata [] false [] adtTypes spec.body internalFunctions
  -- Apply nonreentrant guard for fallback/receive if annotated (high-severity
  -- Bugbot: previously these special entrypoints were compiled without the
  -- transient lock even when `nonreentrant(lock)` was declared).
  let guardedBody ← match spec.nonReentrantLock with
    | none => pure bodyChunks
    | some lockField =>
        let guardStmts ← nonReentrantGuardPrologue fields lockField
        let releaseSlot := match findFieldWithResolvedSlot fields lockField with
          | some (_, s) => s
          | none => 0
        let release := YulStmt.expr (YulExpr.call "tstore" [YulExpr.lit releaseSlot, YulExpr.lit 0])
        pure (guardStmts ++ bodyChunks ++ [release])
  pure {
    payable := spec.isPayable
    body := guardedBody
  }

def pickUniqueFunctionByName (name : String) (funcs : List FunctionSpec) :
    Except String (Option FunctionSpec) :=
  match funcs.filter (·.name == name) with
  | [] => pure none
  | [single] => pure (some single)
  | _ => throw s!"Compilation error: multiple '{name}' entrypoints are not allowed ({issue586Ref})"

-- Check if contract uses mappings
def usesMapping (fields : List Field) : Bool :=
  fields.any fun f => isMapping fields f.name

-- Compile deploy code (constructor)
-- Note: Don't append datacopy/return here - Codegen.deployCode does that
def compileConstructor (fields : List Field) (events : List EventDef) (errors : List ErrorDef)
    (adtTypes : List AdtTypeDef := []) (ctor : Option ConstructorSpec)
    (internalFunctions : List FunctionSpec := []) :
    Except String (List YulStmt) := do
  match ctor with
  | none => return []
  | some spec =>
    let argLoads := genConstructorArgLoads spec.params
    let bodyChunks ← compileStmtList fields events errors .memory [] false
      (spec.params.map (·.name)) adtTypes spec.body internalFunctions
    return argLoads ++ bodyChunks

-- Main compilation function
-- NOTE: this is the pure core compiler and does *not* verify canonical
-- selector/signature correspondence (it only checks count/duplicates).
-- Use `Compiler.Selector.compileChecked` on caller-provided selector lists.
-- WARNING: Order matters! If selector list is reordered but function list isn't,
-- functions will be mapped to wrong selectors with no runtime error.

/-- Reject specs that use the `nonreentrant(lockField)` annotation on a target
    fork that does not expose transient storage (EIP-1153, Cancun+).

    `attachNonReentrantGuard` synthesises a `TLOAD`/`TSTORE` guard and the CEI
    exemption for `nonreentrant` externals assumes that guard runs; emitting
    transient-storage opcodes on a pre-Cancun target (or evaluating the CEI
    exemption as if the guard existed) leaves the post-external-call write
    window open (Bugbot high-severity reentrancy thread). Fail closed at the
    compiler-model boundary so the bug cannot be expressed in a successful
    build (#1893 follow-up, also tracked under #1968). -/
def validateNonReentrantForkCompatibility
    (targetFork : HardFork) (spec : CompilationModel) : Except String Unit := do
  if HardFork.allows targetFork .cancun then
    pure ()
  else
    match spec.functions.find? (fun fn => fn.nonReentrantLock.isSome) with
    | some fn =>
        throw s!"Compilation error: function '{fn.name}' is annotated nonreentrant({fn.nonReentrantLock.getD ""}) but the targeted EVM fork {targetFork} does not expose transient storage (EIP-1153, Cancun+). The synthesised tload/tstore guard cannot run on pre-Cancun chains, so the post-external-call reentry window would be left unguarded. Either raise targetFork to at least Cancun, drop the annotation, or add an explicit pre-Cancun reentrancy guard ({issue1728Ref})."
    | none =>
        pure ()

private def validateCompileInputsBeforeFieldWriteConflict
    (spec : CompilationModel) : Except String Unit := do
  validateIdentifierShapes spec
  match (collectUsedExternalAssumptions spec).find? (fun ext => ext.linkMode == .external) with
  | some ext =>
      throw s!"Compilation error: {spec.name} uses raw linked-helper lowering for external ABI dependency '{ext.name}'. `linked_as := external` dependencies must lower through an ABI-call ECM such as Compiler.Modules.Calls.withReturn so returndata and revert data are preserved."
  | none =>
      pure ()
  match firstInvalidSlotAliasRange spec.slotAliasRanges with
  | some (idx, range) =>
      throw s!"Compilation error: slotAliasRanges[{idx}] has invalid source interval {range.sourceStart}..{range.sourceEnd} in {spec.name} ({issue623Ref}). slotAliasRanges require sourceStart <= sourceEnd."
  | none =>
      pure ()
  match firstSlotAliasSourceOverlap spec.slotAliasRanges with
  | some (idxA, a, idxB, b) =>
      throw s!"Compilation error: slotAliasRanges[{idxA}]={a.sourceStart}..{a.sourceEnd} and slotAliasRanges[{idxB}]={b.sourceStart}..{b.sourceEnd} overlap in source slots in {spec.name} ({issue623Ref}). Ensure slotAliasRanges source intervals are disjoint."
  | none =>
      pure ()
  match firstUnsupportedInternalDynamicParam spec.functions with
  | some (fnName, paramName, ty) =>
      throw s!"Compilation error: internal function '{fnName}' parameter '{paramName}' has unsupported dynamic type {repr ty} ({issue753Ref}). Internal dynamic ABI lowering currently supports only dynamic arrays with single-word static elements."
  | none =>
      pure ()
  match firstDuplicateFunctionParamName spec.functions with
  | some (fnName, dup) =>
      throw s!"Compilation error: duplicate parameter name '{dup}' in function '{fnName}'"
  | none =>
      pure ()
  for fn in spec.functions do
    match firstDuplicateName (fn.params.flatMap paramBindingNames) with
    | some dup =>
        throw s!"Compilation error: function parameter binding name '{dup}' collides with a compiler-generated parameter local in function '{fn.name}'"
    | none =>
        pure ()
  match firstDuplicateConstructorParamName spec.constructor with
  | some dup =>
      throw s!"Compilation error: duplicate parameter name '{dup}' in constructor"
  | none =>
      pure ()
  match spec.constructor with
  | some ctor =>
      match firstDuplicateName (ctor.params.flatMap paramBindingNames) with
      | some dup =>
          throw s!"Compilation error: constructor parameter binding name '{dup}' collides with a compiler-generated parameter local"
      | none =>
          pure ()
  | none =>
      pure ()
  for fn in spec.functions do
    validateFunctionSpec fn
    validateInteropFunctionSpec fn
    validateSpecialEntrypointSpec fn
    validateEventArgShapesInFunction fn spec.events
    validateCustomErrorArgShapesInFunction fn spec.errors
    validateInternalCallShapesInFunction spec.functions fn
    validateExternalCallTargetsInFunction spec.externals fn
  validateConstructorSpec spec.constructor
  validateInteropConstructorSpec spec.constructor
  validateExternalCallTargetsInConstructor spec.externals spec.constructor
  match spec.constructor with
  | none => pure ()
  | some ctor => do
      ctor.body.forM (validateEventArgShapesInStmt "constructor" ctor.params spec.events)
      ctor.body.forM (validateCustomErrorArgShapesInStmt "constructor" ctor.params spec.errors)
      ctor.body.forM (validateInternalCallShapesInStmt spec.functions "constructor" ctor.params)
  for ext in spec.externals do
    let _ ← externalFunctionReturns ext
    validateInteropExternalSpec ext
  match firstDuplicateName ((spec.functions.filter (fun fn => !fn.isInternal)).map functionSignature) with
  | some dup =>
      throw s!"Compilation error: duplicate function signature '{dup}' in {spec.name}"
  | none =>
      pure ()
  match firstDuplicateName ((spec.functions.filter (·.isInternal)).map (·.name)) with
  | some dup =>
      throw s!"Compilation error: duplicate internal function name '{dup}' in {spec.name}; internal function Yul definitions are keyed by name"
  | none =>
      pure ()
  let externalFunctionNames := (spec.functions.filter (fun fn => !fn.isInternal)).map (·.name)
  match (spec.functions.filter (·.isInternal)).find? (fun fn => externalFunctionNames.contains fn.name) with
  | some fn =>
      throw s!"Compilation error: internal function name '{fn.name}' collides with an external function name in {spec.name}; internal function Yul definitions are keyed by name"
  | none =>
      pure ()
  let functionEffects := inferFunctionEffects spec.functions
  for fn in spec.functions do
    validateFunctionSpecMutability functionEffects fn
  match firstDuplicateName (spec.errors.map (·.name)) with
  | some dup =>
      throw s!"Compilation error: duplicate custom error declaration '{dup}'"
  | none =>
      pure ()
  match firstDuplicateName (spec.fields.map (·.name)) with
  | some dup =>
      throw s!"Compilation error: duplicate field name '{dup}' in {spec.name}"
  | none =>
      pure ()
  match firstInvalidPackedBits spec.fields with
  | some (fieldName, packed) =>
      throw s!"Compilation error: field '{fieldName}' has invalid packedBits offset={packed.offset} width={packed.width} in {spec.name} ({issue623Ref}). Require 0 < width <= 256, offset < 256, and offset + width <= 256."
  | none =>
      pure ()
  match firstMappingPackedBits spec.fields with
  | some fieldName =>
      throw s!"Compilation error: field '{fieldName}' is a mapping and cannot declare packedBits in {spec.name} ({issue623Ref}). Packed subfields are only supported for value-word fields."
  | none =>
      pure ()
  match firstUnsupportedStorageArrayElemType spec.fields with
  | some (fieldName, elemType) =>
      throw s!"Compilation error: field '{fieldName}' uses unsupported storage dynamic array element type {repr elemType} in {spec.name} ({issue1571Ref}). This incremental lowering currently supports only one-storage-word elements (uint256, address, bool, bytes32)."
  | none =>
      pure ()
  firstInvalidStructField spec.fields

/-- Validate a `CompilationModel` end-to-end, including the
    `nonreentrant(<lock>)` ↔ `targetFork` pre-check (#1968).

    The default `targetFork := .cancun` preserves the historical single-arg
    call shape for tests, proofs, and `lake exe`-style executables that
    don't have a fork in scope. The compile driver in
    `Compiler.CompileDriverCommon.compileSpecsWithOptions` always passes
    the actual `options.targetFork` so transient-storage guards cannot
    be silently emitted against a pre-Cancun chain. -/
def validateCompileInputs (spec : CompilationModel) (selectors : List Nat)
    (targetFork : HardFork := .cancun) : Except String Unit := do
  validateNonReentrantForkCompatibility targetFork spec
  validateCompileInputsBeforeFieldWriteConflict spec
  let fields := applySlotAliasRanges spec.fields spec.slotAliasRanges
  let externalFns := spec.functions.filter (fun fn => !fn.isInternal && !isInteropEntrypointName fn.name)
  match firstFieldWriteSlotConflict fields with
  | some (slot, existingField, conflictingField) =>
      throw s!"Compilation error: storage slot {slot} has overlapping write ranges for '{existingField}' and '{conflictingField}' in {spec.name} ({issue623Ref}). Ensure full-slot writes are unique and packed bit ranges are disjoint per slot."
  | none =>
      pure ()
  match firstInvalidReservedRange spec.reservedSlotRanges with
  | some (idx, range) =>
      throw s!"Compilation error: reservedSlotRanges[{idx}] has invalid interval {range.start}..{range.end_} in {spec.name} ({issue623Ref}). Reserved slot range start must be <= end."
  | none =>
      pure ()
  match firstReservedRangeOverlap spec.reservedSlotRanges with
  | some (idxA, a, idxB, b) =>
      throw s!"Compilation error: reserved slot ranges reservedSlotRanges[{idxA}]={a.start}..{a.end_} and reservedSlotRanges[{idxB}]={b.start}..{b.end_} overlap in {spec.name} ({issue623Ref}). Ensure reserved ranges are disjoint."
  | none =>
      pure ()
  match firstReservedSlotWriteConflict fields spec.reservedSlotRanges with
  | some (slot, ownerName, rangeIdx, range) =>
      throw s!"Compilation error: field write slot {slot} ('{ownerName}') overlaps reservedSlotRanges[{rangeIdx}]={range.start}..{range.end_} in {spec.name} ({issue623Ref}). Adjust field slot/aliasSlots or reservedSlotRanges."
  | none =>
      pure ()
  match firstDuplicateName (spec.events.map (·.name)) with
  | some dup =>
      throw s!"Compilation error: duplicate event name '{dup}' in {spec.name}"
  | none =>
      pure ()
  for eventDef in spec.events do
    validateEventDef eventDef
  match firstDuplicateEventParamName spec.events with
  | some (evName, dup) =>
      throw s!"Compilation error: duplicate parameter name '{dup}' in event '{evName}'"
  | none =>
      pure ()
  match firstDuplicateName (spec.externals.map (·.name)) with
  | some dup =>
      throw s!"Compilation error: duplicate external declaration '{dup}' in {spec.name}"
  | none =>
      pure ()
  let mappingHelpersRequired := usesMapping fields
  let arrayHelpersRequired := contractUsesPlainArrayElement spec
  let arrayElementWordHelpersRequired := contractUsesArrayElementWord spec
  let paramDynamicHeadWordHelpersRequired := contractUsesParamDynamicHeadWord spec
  let mulDiv512HelpersRequired := contractUsesMulDiv512 spec
  let storageArrayHelpersRequired := contractUsesStorageArrayElement spec
  let dynamicBytesEqHelpersRequired := contractUsesDynamicBytesEq spec
  match firstReservedExternalCollision
      spec mappingHelpersRequired arrayHelpersRequired arrayElementWordHelpersRequired
        paramDynamicHeadWordHelpersRequired
        mulDiv512HelpersRequired
        storageArrayHelpersRequired dynamicBytesEqHelpersRequired with
  | some name =>
      if name.startsWith internalFunctionPrefix then
        throw s!"Compilation error: external declaration '{name}' uses reserved prefix '{internalFunctionPrefix}' ({issue756Ref})."
      else
        throw s!"Compilation error: external declaration '{name}' collides with compiler-generated/reserved symbol '{name}' ({issue756Ref}). Rename the external wrapper."
  | none =>
      pure ()
  for err in spec.errors do
    validateErrorDef err
  if externalFns.length != selectors.length then
    throw s!"Selector count mismatch for {spec.name}: {selectors.length} selectors for {externalFns.length} external functions"
  match firstDuplicateSelector selectors with
  | some dup =>
      let names := selectorNames spec selectors dup
      let nameStr := if names.isEmpty then "<unknown>" else String.intercalate ", " names
      throw s!"Selector collision in {spec.name}: {dup} assigned to {nameStr}"
  | none => pure ()

/-- Compile one selector-dispatched external and inject the transient-storage
    reentrancy guard prologue for `nonreentrant(lockField)` externals (#1893).
    Kept outside `compileFunctionSpec` so the IR-generation proof modules
    continue to characterise the underlying body shape without a
    nonReentrantLock case split; for lock-free functions this is exactly
    `compileFunctionSpec` (see `attachNonReentrantGuard`). -/
def compileGuardedFunctionSpec (fields : List Field) (events : List EventDef)
    (errors : List ErrorDef) (adtTypes : List AdtTypeDef)
    (internalFunctions : List FunctionSpec)
    (sel : Nat) (fnSpec : FunctionSpec) : Except String IRFunction := do
  let irFn ← compileFunctionSpec fields events errors adtTypes sel fnSpec internalFunctions
  attachNonReentrantGuard fields fnSpec irFn

def compileValidatedCore (spec : CompilationModel) (selectors : List Nat) : Except String IRContract := do
  let fields := applySlotAliasRanges spec.fields spec.slotAliasRanges
  let externalFns := spec.functions.filter (fun fn => !fn.isInternal && !isInteropEntrypointName fn.name)
  let internalFns := spec.functions.filter (·.isInternal)
  let mappingHelpersRequired := usesMapping fields
  let arrayHelpersRequired := contractUsesPlainArrayElement spec
  let arrayElementWordHelpersRequired := contractUsesArrayElementWord spec
  let paramDynamicHeadWordHelpersRequired := contractUsesParamDynamicHeadWord spec
  let mulDiv512HelpersRequired := contractUsesMulDiv512 spec
  let storageArrayHelpersRequired := contractUsesStorageArrayElement spec
  let dynamicBytesEqHelpersRequired := contractUsesDynamicBytesEq spec
  let fallbackSpec ← pickUniqueFunctionByName "fallback" spec.functions
  let receiveSpec ← pickUniqueFunctionByName "receive" spec.functions
  let functions ← (externalFns.zip selectors).mapM fun entry =>
    compileGuardedFunctionSpec fields spec.events spec.errors spec.adtTypes internalFns entry.2 entry.1
  let internalFuncDefs ← internalFns.mapM fun fn =>
    compileInternalFunction fields spec.events spec.errors spec.adtTypes fn internalFns
  let arrayElementHelpers :=
    (if arrayHelpersRequired then
      [ checkedArrayElementCalldataHelper
      , checkedArrayElementMemoryHelper
      ]
    else
      []) ++
    (if arrayElementWordHelpersRequired then
      [ checkedArrayElementWordCalldataHelper
      , checkedArrayElementWordMemoryHelper
      , checkedArrayElementDynamicWordCalldataHelper
      , checkedArrayElementDynamicWordMemoryHelper
      , checkedArrayElementDynamicDataOffsetCalldataHelper
      , checkedArrayElementDynamicDataOffsetMemoryHelper
      -- verity#1849 G1: dynamic-member length helpers share the
      -- `arrayElementWord` gate because they read the same struct-array
      -- elements and have negligible code size; conservative emission is
      -- correct and avoids a separate predicate.
      , checkedArrayElementDynamicMemberLengthCalldataHelper
      , checkedArrayElementDynamicMemberLengthMemoryHelper
      , checkedArrayElementDynamicMemberDataOffsetCalldataHelper
      , checkedArrayElementDynamicMemberDataOffsetMemoryHelper
      -- verity#1849 G2: dynamic-member element helpers gated the same way.
      , checkedArrayElementDynamicMemberElementCalldataHelper
      , checkedArrayElementDynamicMemberElementMemoryHelper
      ]
    else
      []) ++
    (if paramDynamicHeadWordHelpersRequired then
      [ checkedParamDynamicHeadWordCalldataHelper
      , checkedParamDynamicHeadWordMemoryHelper
      , checkedParamDynamicMemberLengthCalldataHelper
      , checkedParamDynamicMemberLengthMemoryHelper
      , checkedParamDynamicMemberDataOffsetCalldataHelper
      , checkedParamDynamicMemberDataOffsetMemoryHelper
      , checkedParamDynamicMemberElementCalldataHelper
      , checkedParamDynamicMemberElementMemoryHelper
      ]
    else
      []) ++
    -- verity#1761: full-precision multiply-divide. `fullMulDivUpHelper`
    -- calls `fullMulDivHelperName`, so emit the down helper unconditionally
    -- when either is used.
    (if mulDiv512HelpersRequired then
      [ fullMulDivHelper
      , fullMulDivUpHelper
      ]
    else
      [])
  let storageArrayElementHelpers :=
    if storageArrayHelpersRequired then
      [checkedStorageArrayElementHelper]
    else
      []
  let dynamicBytesEqHelpers :=
    if dynamicBytesEqHelpersRequired then
      [dynamicBytesEqCalldataHelper, dynamicBytesEqMemoryHelper]
    else
      []
  let fallbackEntrypoint ← fallbackSpec.mapM (compileSpecialEntrypoint fields spec.events spec.errors spec.adtTypes internalFns)
  let receiveEntrypoint ← receiveSpec.mapM (compileSpecialEntrypoint fields spec.events spec.errors spec.adtTypes internalFns)
  return {
    name := spec.name
    deploy := (← compileConstructor fields spec.events spec.errors spec.adtTypes spec.constructor internalFns)
    constructorPayable := spec.constructor.map (·.isPayable) |>.getD false
    functions := functions
    fallbackEntrypoint := fallbackEntrypoint
    receiveEntrypoint := receiveEntrypoint
    usesMapping := mappingHelpersRequired
    internalFunctions := arrayElementHelpers ++ storageArrayElementHelpers ++ dynamicBytesEqHelpers ++ internalFuncDefs
  }

/-- Compile a `CompilationModel` to an `IRContract`.

    The optional `targetFork` parameter is threaded through to
    `validateCompileInputs` so the `nonreentrant(<lock>)` ↔
    `HardFork.allows targetFork .cancun` pre-check (#1968) runs against
    the actual target chain. The default `.cancun` preserves the
    historical two-arg call shape for tests, proofs, and executables
    that don't model the fork; the compile driver always passes
    `options.targetFork`. -/
def compile (spec : CompilationModel) (selectors : List Nat)
    (targetFork : HardFork := .cancun) : Except String IRContract := do
  validateCompileInputs spec selectors targetFork
  compileValidatedCore spec selectors

theorem validateCompileInputs_identifierShapes_ok
    {spec : CompilationModel}
    {selectors : List Nat}
    (hvalidate : validateCompileInputs spec selectors = Except.ok ()) :
    validateIdentifierShapes spec = Except.ok () := by
  unfold validateCompileInputs validateCompileInputsBeforeFieldWriteConflict at hvalidate
  cases hshapes : validateIdentifierShapes spec with
  | error err =>
      simp [hshapes] at hvalidate
      cases hvalidate
  | ok _ =>
      simp

theorem validateCompileInputs_firstFieldWriteSlotConflict_eq_none
    {spec : CompilationModel}
    {selectors : List Nat}
    (hvalidate : validateCompileInputs spec selectors = Except.ok ()) :
    firstFieldWriteSlotConflict
        (applySlotAliasRanges spec.fields spec.slotAliasRanges) = none := by
  unfold validateCompileInputs at hvalidate
  cases hprefix : validateCompileInputsBeforeFieldWriteConflict spec with
  | error err =>
      simp [hprefix] at hvalidate
      cases hvalidate
  | ok _ =>
      cases hconflict : firstFieldWriteSlotConflict
          (applySlotAliasRanges spec.fields spec.slotAliasRanges) with
      | some conflict =>
          simp [hprefix, hconflict] at hvalidate
          cases hvalidate
      | none =>
          simp

end Compiler.CompilationModel