AdeAtlas
Invariants / CN-PLUTUS-02

CN-PLUTUS-02

CN derived declared

Budget exhaustion and script failure must have a single deterministic failure shape

Source

classification_table.md §E

Authority surface
Per-script declared-ex_units cap ENFORCED: a script that overruns the ex_units its redeemer declared is rejected, closing the under-declared false-accept (aiken's eval_phase_two_raw caps only at the tx-wide protocol max Ade passes as initial_budget). The CLOSED failure-shape CLASSIFICATION (BudgetExhausted vs ContextBuildFailed vs ExecutionFailed) is not yet wired through to the verdict -- stays declared.

Enforcement trace

Code

Tests 7

  • under_declared_ex_units_must_reject
  • failing_validator_must_reject
  • extraneous_redeemer_must_reject
  • declared_ex_units_array_form_parsed_by_pointer
  • declared_ex_units_conway_map_form_parsed_by_pointer
  • extract_redeemer_fields_reads_pointer_and_ex_units
  • aiken_fixture_tx_evaluates_end_to_end

CI 1

Attack rationale

Prevents runtime-dependent failure behavior.

Evidence notes

Cardano-specific: budget accounting is a Plutus mechanism.