diff --git a/Makefile b/Makefile index 9dcb671c154..ecd0f6b18ba 100644 --- a/Makefile +++ b/Makefile @@ -18,6 +18,7 @@ ALL_EXECUTABLE_SPEC_NAMES = \ _sync \ build_docs \ clean \ + comptests \ help \ lint \ serve_docs \ @@ -106,15 +107,18 @@ help-verbose: @echo "" @echo "$(BOLD)make comptests$(NORM)" @echo "" - @echo " Generates compliance tests for fork choice. These tests verify that" - @echo " implementations correctly handle fork choice scenarios." + @echo " Generates compliance tests. These tests verify that implementations" + @echo " correctly handle fork choice and state transition scenarios." @echo " Uses pytest collection and xdist parallelism." @echo "" @echo " Parameters:" + @echo " kind= Test kind: fork_choice (default), state_transition" @echo " fc_gen_config= Configuration size (tiny, small, standard; default: tiny)" @echo " fork= Generate for specific fork (comma-separated)" @echo " preset= Generate for specific preset (comma-separated)" @echo " comptests_dir= Output directory for generated compliance tests" + @echo " handler= State-transition handler (default: all)" + @echo " profile= State-transition profile (smoke, standard, all; default: standard)" @echo " threads=N Number of threads to use" @echo " seed=N Override test seeds (fuzzing mode)" @echo " group_slice_index=N 0-based shard index for deterministic test-group slicing" @@ -127,6 +131,8 @@ help-verbose: @echo " make comptests comptests_dir=./compliance-spec-tests/tests" @echo " make comptests fc_gen_config=standard fork=deneb preset=mainnet threads=8" @echo " make comptests fc_gen_config=tiny fork=gloas group_slice_index=0 group_slice_count=4" + @echo " make comptests kind=state_transition" + @echo " make comptests kind=state_transition handler=withdrawals profile=smoke" @echo "" @echo "$(BOLD)DOCUMENTATION$(NORM)" @echo "$(BOLD)--------------------------------------------------------------------------------$(NORM)" @@ -289,6 +295,9 @@ lint: _pyspec COMMA:= , DEFAULT_COMPTESTS_DIR = $(CURDIR)/../compliance-spec-tests/tests COMPTESTS_DIR = $(if $(comptests_dir),$(comptests_dir),$(DEFAULT_COMPTESTS_DIR)) +COMPTESTS_KIND = $(if $(kind),$(kind),fork_choice) + +ifeq ($(COMPTESTS_KIND),fork_choice) # Generate compliance tests (fork choice). comptests: FC_GEN_CONFIG := $(if $(fc_gen_config),$(fc_gen_config),tiny) @@ -313,6 +322,29 @@ comptests: _pyspec $(MAYBE_GROUP_SLICE_COUNT) \ $(CURDIR)/tests/generators/compliance_runners/fork_choice/generate_comptests.py +else ifeq ($(COMPTESTS_KIND),state_transition) + +# Generate compliance tests (state transition). +comptests: MAYBE_HANDLER := $(if $(handler),--handler $(handler)) +comptests: MAYBE_PROFILE := $(if $(profile),--profile $(profile)) +comptests: MAYBE_PARALLEL := $(if $(filter 1,$(threads)),,$(if $(threads),-n $(threads) --dist=worksteal,-n logical --dist=worksteal)) +comptests: _pyspec + @$(UV_RUN) pytest \ + $(MAYBE_PARALLEL) \ + --capture=no \ + --comptests-output=$(COMPTESTS_DIR) \ + $(MAYBE_HANDLER) \ + $(MAYBE_PROFILE) \ + $(CURDIR)/tests/generators/compliance_runners/state_transition/generate_comptests.py + +else + +comptests: + @echo "Unsupported compliance test kind: $(COMPTESTS_KIND)" >&2 + @exit 1 + +endif + ############################################################################### # Cleaning ############################################################################### diff --git a/tests/formats/epoch_processing/README.md b/tests/formats/epoch_processing/README.md index 3c89fc2ce79..89a45727228 100644 --- a/tests/formats/epoch_processing/README.md +++ b/tests/formats/epoch_processing/README.md @@ -68,6 +68,8 @@ Sub-transitions: - `pending_consolidations` (>=Electra) - `pending_deposits` (>=Electra) - `pending_randao_commitments` (>=EIP-8321) +- `builder_pending_payments` (>=Gloas) +- `ptc_window` (>=Gloas) The resulting state should match the expected `post` state. diff --git a/tests/generators/compliance_runners/state_transition/README.md b/tests/generators/compliance_runners/state_transition/README.md new file mode 100644 index 00000000000..196376c62af --- /dev/null +++ b/tests/generators/compliance_runners/state_transition/README.md @@ -0,0 +1,113 @@ +# State-transition compliance test generator + +State-transition compliance test generator intended to produce reference tests +for individual state-transition handlers. Each handler models semantic coverage +conditions, materializes concrete SSZ test vectors, and validates the generated +vectors against the executable specification. + +The generator currently targets the `gloas` fork with the `minimal` preset. Its +test cases follow the standard +[operations test format](../../../formats/operations/README.md) or +[epoch processing test format](../../../formats/epoch_processing/README.md), +depending on the handler. + +## Handlers + +Operation handlers: + +- `attestation` +- `builder_deposit_request` +- `builder_exit_request` +- `consolidation_request` +- `deposit_request` +- `execution_payload_bid` +- `parent_execution_payload` +- `payload_attestation` +- `proposer_slashing` +- `withdrawal_request` +- `withdrawals` + +Epoch-processing handlers: + +- `builder_pending_payments` +- `pending_deposits` +- `ptc_window` + +## Generating tests + +From the repository root: + +```bash +make comptests kind=state_transition +``` + +The default profile is `standard`, and all handlers are generated. Select a +handler, profile, or output directory with Make variables: + +```bash +make comptests kind=state_transition handler=withdrawals profile=smoke +make comptests kind=state_transition profile=all +make comptests kind=state_transition comptests_dir=../compliance-spec-tests/tests +``` + +The supported profiles are: + +- `smoke` — one representative per terminal outcome +- `normal` — cases with no independently failed conditions +- `exceptional` — single-fault cases +- `standard` — `normal` plus `exceptional` +- `all` — every distinct model coverage signature + +`make comptests` is the supported generation path. The underlying module can +also be run directly: + +```bash +uv run python -m tests.generators.compliance_runners.state_transition.run +uv run python -m tests.generators.compliance_runners.state_transition.run \ + --handler withdrawals --profile smoke +uv run python -m tests.generators.compliance_runners.state_transition.run \ + --comptests-output /path/to/output +``` + +The direct command writes to each handler's local `reftests/` directory unless +`--comptests-output` is provided. It validates each handler immediately after +materialization. Handler-specific MiniZinc models, coverage definitions, +materializers, and validators are located in the corresponding provider +directory. + +A handler may have multiple provider directories. Their cases are appended to +the same handler output with distinct case numbers and validated independently; +the provider directory is an implementation detail, while the generated manifest +continues to use the protocol handler name. + +## Running generated tests + +From the repository root, run the compliance runner against a directory +containing generated `reftests`: + +```bash +uv run pytest \ + tests/generators/compliance_runners/state_transition/runner/test_run.py \ + --test-dir ${test_dir} +``` + +The `--test-dir` option can be repeated to run multiple test roots. Optional +`--start` and `--limit` arguments select a slice of the discovered cases. + +## Output + +Generated cases use this layout: + +```text +/minimal/gloas/ + operations//main/case_XXXX/ + epoch_processing//main/case_XXXX/ +``` + +Each case contains `pre.ssz_snappy`, the operation input when applicable, +`post.ssz_snappy` when the handler accepts the input, `meta.yaml`, +`manifest.yaml`, and `dimensions.yaml` with the claimed coverage dimensions. + +The modelling approach and the distinction between coverage dimensions, +materialization, and validation are documented in +[`TEST_METHODOLOGY.md`](TEST_METHODOLOGY.md). diff --git a/tests/generators/compliance_runners/state_transition/TEST_METHODOLOGY.md b/tests/generators/compliance_runners/state_transition/TEST_METHODOLOGY.md new file mode 100644 index 00000000000..2c7a6b44e50 --- /dev/null +++ b/tests/generators/compliance_runners/state_transition/TEST_METHODOLOGY.md @@ -0,0 +1,320 @@ +# Test modelling methodology + +This document describes a methodology for generating compliance tests by +modelling semantic situations, materializing them into concrete test vectors, +and validating that each vector realizes its model solution. It is general — the +same structure applies to state-transition, fork-choice, and execution-spec +tests. The running example is the `process_execution_payload_bid` handler on the +`gloas` `BeaconState` (the exploratory model in [`old/models/`](old/models) +illustrates its solution space). It and +[`builder_exit_request/`](builder_exit_request) are worked aspect-based +instances that **share** realization aspects from a common [`aspects/`](aspects) +directory; earlier single-model *smoke-profile* versions are archived under +[`old2/`](old2). + +Central design principle: + +> **Realization aspects** define reusable relations between coverage and +> materialization dimensions. **Handler aspects** bind those relations to a +> specific handler's state and operation. **Coverage aspects** select which +> projections and combinations become tests. + +Separating *what a situation means and how to build it* from *which situations +become tests* lets handlers share semantic models, and lets one model support +different coverage strengths without rewriting domain constraints. + +## Relational view + +Model the system under test as a relation: + +```text +DomainRelation ⊆ Input × Output × Outcome × Trace +``` + +- `Input` — the precondition plus the operation or event. +- `Output` — the resulting state or observable effect. +- `Outcome` — the terminal behavior (accept, reject, no-op, …). +- `Trace` — which semantic checks were reached. + +For a state transition, `Input` is a `PreState` plus an optional operation and +`Output` is a `PostState`. Sequences of operations fit the same shape. + +Predicate coverage is the minimum bar; combinations of predicates, boundary +relations, outcomes, effects, and traces expose more bugs. Source and branch +coverage are diagnostic feedback, not the coverage model itself. + +## Dimensions + +### Coverage dimensions + +A **coverage dimension** is an atomic semantic projection used in a coverage +formula. Input-side coverage dimensions usually correspond to predicates or +comparisons extracted from the specification (`builder_found`, `builder_active`, +`bid_parent_hash_matches`, …). + +- Boolean predicates should be exercised both true and false wherever they are + applicable. + +- Comparisons should keep their boundary structure rather than collapsing + immediately to a boolean. Model the comparison as `{LT, EQ, GT}` and derive + the boolean by choosing which outcomes count as true: + + ```text + available_balance_to_bid_amount ∈ {LT, EQ, GT} + can_builder_cover_bid := available_balance_to_bid_amount ∈ {EQ, GT} + ``` + + Mirror the specification's *exact* boundary — including any offsets and guards + (for `can_builder_cover_bid`, the pending-withdrawal term and the + minimum-balance guard) — rather than a simplified approximation. + +Coverage dimensions may also be **derived** from output, outcome, or trace: the +handler outcome, whether a check was reached, whether a state field changed. +Derived dimensions relate to inputs by constraints, so a coverage formula can +select a target outcome or effect and the solver solves back to an input that +produces it. + +### Materialization dimensions + +A **materialization dimension** is a concrete or symbolic value needed to build +the vector (builder balance, bid value, referenced index, queue length, slot, +signing key). The division of labor is: + +- the **solver** assigns coverage dimensions and *symbolic* comparison outcomes; +- the **materializer** chooses concrete operands that realize them. + +The solver assignment is authoritative: the materializer must not substitute a +different, easier-to-construct value for a requested comparison or predicate. +Concrete protocol values are often too large for a finite-domain solver — prefer +a `{LT, EQ, GT}` comparison dimension and let the materializer pick operands. + +Materialization dimensions need not appear in coverage formulas. Auxiliary +encoding variables are neither coverage obligations nor part of the materializer +contract unless explicitly exported. + +## Aspects + +An **aspect** is a reusable relation over dimensions, defined around semantic +functionality rather than the handler that first needs it (entity reference and +membership, builder/validator lifecycle, funds, withdrawal credentials and +authorization, queue capacity, slot/epoch relations, signed messages, …). Three +complementary layers: + +### Realization aspects + +A **realization aspect** connects coverage dimensions to materialization +dimensions and excludes incoherent assignments. It states what an assignment +means and how to realize it — not which assignments become tests. Each coverage +dimension it defines must carry: + +- a stable name and a finite domain; +- a semantic description and a specification reference; +- an applicability condition, if any; +- materialization dimensions or rules sufficient to realize it; +- an independent procedure for recovering it from a serialized vector. + +A dimension that must appear in solutions has to be a genuine solver output, not +an artifact the flattener can eliminate. In MiniZinc, *declare and constrain* it +(`var T: d; constraint d <-> …;`) rather than *define* it (`var T: d = …;`): +defined variables may be inlined away and then be absent from the solution — and +so from the materialized coverage fingerprint. Derived coverage dimensions +(outcome, effects, "check reached") in particular must be +declared-and-constrained. + +### Handler aspects + +A **handler aspect** assembles shared realization aspects, binds their abstract +roles to concrete state and operation fields, and adds genuinely +handler-specific dimensions. For `process_execution_payload_bid` it might bind +an entity-reference aspect to `bid.builder_index` / `state.builders`, a +builder-lifecycle and a funds aspect to the referenced builder, and a +signed-message aspect to the bid — plus local dimensions for self-build, KZG +count, slot, and parent fields. It also states inter-aspect applicability +(lifecycle and funds apply only to an external bid whose reference resolves). + +The same shared aspect bound by several handlers makes overlap explicit. +Realization aspects live in a common directory and are `include`d by each +handler model; a handler only binds their applicability to its own fields. For +example, `execution_payload_bid` and `builder_exit_request` include the *same* +`builder_lifecycle` (`is_active_builder`) and `builder_pending_balance` +(`get_pending_balance_to_withdraw_for_builder`) aspect files, binding +applicability to `builder_ref == EXISTING` and to `builder_pubkey_found` +respectively. Improving one domain model or recovery procedure then benefits +every handler that uses it. + +When a handler binds an aspect to **more than one role** (e.g. the source and +target validators of a consolidation), the aspect is written as a +*parameterized* predicate over its dimension vars — +`validator_lifecycle_ok(active, exiting, applicable)`, +`validator_credential_ok(kind, applicable)` — plus derived-value functions +(`cred_has_execution`, …). The handler declares role-prefixed vars +(`validator_active` / `target_active`, …) and applies the predicate once per +role, so both roles reuse the exact same relation. Single-role aspects may +remain plain flat declarations. + +### Coverage aspects + +A **coverage aspect** expresses a coverage criterion over the exposed +dimensions; it selects, it does not materialize. It can be input-side or derived +from output, outcome, or trace: + +```text +exhaustive(builder_active, builder_version_valid, available_balance_to_bid_amount) +cover_each(handler_outcome) +pairwise(handler_outcome, pending_payment_written) +``` + +Operators: `cover_each` (every applicable value of a dimension), `exhaustive` +(full cross product of the listed dimensions), `pairwise` / `three_way` (all 2- +or 3-tuples across dimensions), and single- vs multi-fault selection (for +diagnosis vs adversarial coverage). + +## Applicability, reachability, and decisiveness + +Guarded conditions need three distinct concepts; conflating them corrupts +coverage. + +**Applicability.** A dimension is *applicable* when its value can be recovered +from the input vector. If a builder reference does not resolve, predicates over +that builder's lifecycle, funds, or key are not applicable. Represent it +explicitly: + +```text +builder_active_applicable := external_bid and builder_found +``` + +When the guard is false the coverage value is `NA`; it must not be forced to an +arbitrary true or false merely to satisfy the solver. + +**Reachability.** A predicate is *reached* when execution evaluates its check; +this depends on gate order. A predicate can be applicable but not reached: an +existing builder may simultaneously be inactive, mis-versioned, underfunded, and +badly signed — all recoverable from the vector even though execution stops at +the activity check. Later applicable dimensions must **not** be set to `NA` +merely because an earlier gate rejected the operation; a trace dimension records +which checks were reached. + +**Decisiveness.** A predicate is *decisive* when it determines the terminal +outcome. First-failing-gate identifies the decisive predicate but does not erase +the other applicable assignments. + +Keeping these separate permits rich multi-predicate enumeration while preserving +accurate short-circuit semantics. + +## Coverage formulas and profiles + +A coverage formula states which projections and combinations should appear; it +is separate from the constraints that define valid situations. The default +favors richer solutions: enumerate combinations within a small active aspect, +retain `LT`/`EQ`/`GT` boundaries, enumerate applicable predicates even when only +the first failing one is reached, and include successful and exceptional +combinations (and effects present vs absent). Across several large aspects, use +an explicit interaction policy — exhaustive for selected high-risk relations, +pairwise or three-way otherwise, single- and multi-fault cases. + +The same handler relation supports multiple profiles. State-transition handler +profiles classify records by the number of independently applicable failed +conditions (`nfaults`), not by the first-failing terminal outcome: + +```text +smoke: one canonical case per outcome +normal: nfaults == 0 +exceptional: nfaults == 1 (the usual single-fault profile) +standard: normal ∪ exceptional +all: every unique solution by coverage signature +``` + +One-case-per-outcome frontiers are useful smoke tests, but they are not a +substitute for the richer fault-count profiles. A terminal outcome remains a +derived observation; it must not erase other applicable failures that were not +reached because of short-circuit evaluation. + +Quality is measured by satisfied obligations, not case count: every applicable +value of every dimension, every requested pair or tuple, every outcome, every +check reached and not reached where possible, every selected effect, every +comparison boundary. If satisfying assignments are too numerous, reduce them +with a deterministic set cover that preserves the declared obligations, and +report uncovered or unsatisfiable obligations explicitly. Deduplicate solutions +by a coverage fingerprint over applicable coverage values and `NA` markers — not +over auxiliary or concrete materialization choices. + +## Materialization + +A materializer converts one immutable solver solution into a concrete vector. It +must: + +- consume the solution's coverage and materialization dimensions; +- choose concrete operands for symbolic comparison dimensions; +- construct all input objects, preserving **every** applicable coverage + assignment; +- serialize the original solution alongside the vector; +- emit the expected outcome and effects when the test format requires them. + +The materializer must **not** re-derive a new set of claims from the object it +constructed — doing so can hide a failure to realize the solver assignment. It +may use the executable specification to build auxiliary state or a candidate +post-state, but that execution must not overwrite the authoritative solution. + +A per-case artifact retains at least the solution: + +```yaml +solution: + builder_found: true + builder_active: false + available_balance_to_bid_amount: LT + outcome: REJECT_EXTERNAL_INACTIVE +``` + +## Validation + +Validation has several independent responsibilities. + +**Materialization correctness.** Decode the vector and independently recover +every applicable coverage dimension via its aspect's recovery procedure, then +compare to the solver assignment. A divergence is a generator failure even if +the handler produces the expected outcome. + +```text +selected assignment → concrete vector → independently recovered assignment +``` + +Also check that every declared dimension is present, that `NA` agrees with its +applicability guard, that no undeclared dimensions appear, and that +materialization dimensions satisfy their declared constraints. + +**Outcome, trace, and effect correctness.** Recover or observe the derived +dimensions and compare them to their model assignments — expected vs observed +outcome, reached checks, and state changes. For a rejected operation, confirm no +forbidden mutation occurred and that `post` is omitted where the format requires +it; distinguish this from a no-op whose `post` is present but unchanged. + +**Global coverage audit.** After per-case checks, evaluate the whole suite +against its coverage aspects. The run must fail when a declared value or +requested combination is missing, an outcome/trace/effect obligation is +uncovered, duplicates displace a required assignment, or a supposedly +satisfiable obligation has no solution. Per-case correctness does not imply +suite coverage. + +**Implementation and code coverage.** Execute validated vectors against the +implementation and any independent oracles. Source and branch coverage are +diagnostic: gaps feed back into predicate extraction, aspect definitions, +bindings, or coverage formulas — they are not themselves the selection +criterion. + +## Pipeline + +1. **Predicate extraction** — identify predicates, comparisons, and hidden + boundary relations in the specification; record stable spec anchors. +2. **Aspect modelling** — define reusable realization relations between coverage + and materialization dimensions. +3. **Handler assembly** — bind shared aspects to a handler's state and + operation; add handler-local relations. +4. **Coverage selection** — apply input, outcome, trace, and effect coverage + aspects at the chosen profile. +5. **Solving** — enumerate satisfying coverage assignments. +6. **Materialization** — build vectors without changing their assignments. +7. **Validation** — independently recover dimensions, outcomes, traces, and + effects and compare them to the solutions. +8. **Coverage audit** — prove the suite satisfies its declared obligations. +9. **Implementation execution** — run the vectors and use code coverage and + external oracles as feedback. diff --git a/tests/generators/compliance_runners/state_transition/__init__.py b/tests/generators/compliance_runners/state_transition/__init__.py new file mode 100644 index 00000000000..92dcb838dd8 --- /dev/null +++ b/tests/generators/compliance_runners/state_transition/__init__.py @@ -0,0 +1 @@ +"""State-transition compliance-test generators and validators.""" diff --git a/tests/generators/compliance_runners/state_transition/aspect_coverage.py b/tests/generators/compliance_runners/state_transition/aspect_coverage.py new file mode 100644 index 00000000000..349b60fbe85 --- /dev/null +++ b/tests/generators/compliance_runners/state_transition/aspect_coverage.py @@ -0,0 +1,208 @@ +"""Handler-agnostic combinatorial-over-aspects coverage. + +A handler describes its coverage as a set of *aspects*, each a factor whose value +is the tuple of its coverage dimensions (`outcome` is usually one of them). This +module enumerates the handler model's feasible space once and provides t-wise +covering-set selection over any subset of aspects. Enumerated records also +retain the handler's fault count, allowing profiles to classify cases +independently of the terminal outcome. + +A provider's own `coverage.py` supplies: + - `model_path` : the handler MiniZinc model, + - `dims` : the solution variables to read (its coverage dimensions), + - `aspects` : {aspect_name: [dim, ...]} (include an `outcome` dimension), + - `rank(rec)` : lower = cleaner representative (e.g. fewer faults), +and then calls `enumerate_signatures(...)` + `build_profile(...)`. + +See `execution_payload_bid/coverage.py` for a worked instantiation. +""" + +from __future__ import annotations + +from collections.abc import Callable +from itertools import combinations +from typing import TYPE_CHECKING + +import minizinc + +if TYPE_CHECKING: + from pathlib import Path + +Aspects = dict[str, list[str]] +Rank = Callable[[dict], int] + + +def _state(rec: dict, dims: list[str]) -> tuple: + return tuple(rec[d] for d in dims) + + +def signature(rec: dict, aspects: Aspects) -> tuple: + return tuple(_state(rec, dims) for dims in aspects.values()) + + +def enumerate_signatures( + model_path: Path, dims: list[str], aspects: Aspects, rank: Rank | None = None +) -> list[dict]: + """Distinct aspect-state representatives over the model's feasible space. + + Dedups by the full aspect signature, keeping the lowest-`rank` representative. + """ + rank = rank or (lambda _r: 0) + model = minizinc.Model(str(model_path)) + result = minizinc.Instance(minizinc.Solver.lookup("gecode"), model).solve(all_solutions=True) + reps: dict[tuple, dict] = {} + for sol in result: + rec = {n: (bool(v) if isinstance(v := getattr(sol, n), bool) else str(v)) for n in dims} + rec["_rank"] = rank(rec) + # The handler rank is currently its fault count. Keep that value + # explicit so profile selection is independent of the terminal outcome. + rec["_nfaults"] = rec["_rank"] + sig = signature(rec, aspects) + if sig not in reps or rec["_rank"] < reps[sig]["_rank"]: + reps[sig] = rec + return list(reps.values()) + + +def filter_faults(recs: list[dict], nfaults: int) -> list[dict]: + """Return records with exactly ``nfaults`` independently counted faults.""" + return [rec for rec in recs if rec["_nfaults"] == nfaults] + + +def smoke(recs: list[dict], outcome_aspects: Aspects) -> tuple[int, list[dict]]: + """Select one representative for each terminal outcome, when present.""" + if not any("outcome" in dims for dims in outcome_aspects.values()): + return cover(recs, outcome_aspects, 1) + return cover(recs, {"outcome": ["outcome"]}, 1) + + +def build_profile( + recs: list[dict], + name: str, + all_aspects: Aspects, + input_aspects: Aspects, + outcome_aspect: Aspects, + *, + normal_outcome_aspect: Aspects | None = None, + exceptional_aspects: Aspects | None = None, + normal_t: int = 2, + exceptional_t: int = 1, +) -> tuple[int, list[dict]]: + """Build a standard set of fault-count coverage profiles. + + Handler modules provide their aspect groups and may override the normal + outcome coverage, exceptional aspects, or coverage strength when they have + a handler-specific policy. + """ + if name == "all": + return len(recs), recs + if name == "smoke": + return smoke(recs, all_aspects) + if name == "normal": + normal_records = filter_faults(recs, 0) + normal = cover(normal_records, input_aspects, normal_t) + if normal_outcome_aspect is None: + return normal + _, normal_inputs = cover(normal_records, input_aspects, normal_t) + _, normal_outcomes = cover(normal_records, normal_outcome_aspect, 1) + return -1, dedup(normal_inputs + normal_outcomes, all_aspects) + if name == "exceptional": + exceptional_coverage = ( + exceptional_aspects if exceptional_aspects is not None else outcome_aspect + ) + return cover(filter_faults(recs, 1), exceptional_coverage, exceptional_t) + if name == "standard": + _, normal = build_profile( + recs, + "normal", + all_aspects, + input_aspects, + outcome_aspect, + normal_outcome_aspect=normal_outcome_aspect, + exceptional_aspects=exceptional_aspects, + normal_t=normal_t, + exceptional_t=exceptional_t, + ) + _, exceptional = build_profile( + recs, + "exceptional", + all_aspects, + input_aspects, + outcome_aspect, + normal_outcome_aspect=normal_outcome_aspect, + exceptional_aspects=exceptional_aspects, + normal_t=normal_t, + exceptional_t=exceptional_t, + ) + return -1, dedup(normal + exceptional, all_aspects) + raise ValueError(f"unknown profile: {name}") + + +def _slice( + recs: list[dict], outcome_dim: str, outcome_filter: str | None, accept: set +) -> list[dict]: + if outcome_filter == "normal": + return [r for r in recs if r[outcome_dim] in accept] + if outcome_filter == "exceptional": + return [r for r in recs if r[outcome_dim] not in accept] + return recs + + +def cover( + recs: list[dict], + aspects: Aspects, + t: int, + outcome_filter: str | None = None, + outcome_dim: str = "outcome", + accept: str | set = "ACCEPT", +) -> tuple[int, list[dict]]: + """Greedy t-wise covering set over `aspects` (within an optional outcome slice). + + `accept` is the outcome value (or set of values) that count as "normal"; + everything else is "exceptional". Returns (number of feasible t-wise + obligations, chosen representatives). + """ + accept_set = {accept} if isinstance(accept, str) else set(accept) + names = list(aspects) + dims_of = [aspects[n] for n in names] + + # Candidates deduplicated by their projection onto the chosen aspects. + reps: dict[tuple, dict] = {} + for rec in _slice(recs, outcome_dim, outcome_filter, accept_set): + proj = tuple(_state(rec, d) for d in dims_of) + if proj not in reps or rec["_rank"] < reps[proj]["_rank"]: + reps[proj] = rec + + all_obl: set = set() + covered_by: dict[tuple, frozenset] = {} + for proj in reps: + combos = {(sub, tuple(proj[k] for k in sub)) for sub in combinations(range(len(names)), t)} + covered_by[proj] = frozenset(combos) + all_obl |= combos + + uncovered = set(all_obl) + chosen: list[dict] = [] + while uncovered: + best, best_gain, best_rank = None, 0, 1 << 30 + for proj, combos in covered_by.items(): + gain = len(combos & uncovered) + if gain > best_gain or ( + gain == best_gain and gain > 0 and reps[proj]["_rank"] < best_rank + ): + best, best_gain, best_rank = proj, gain, reps[proj]["_rank"] + if best is None or best_gain == 0: + break + chosen.append(reps[best]) + uncovered -= covered_by[best] + return len(all_obl), chosen + + +def dedup(recs: list[dict], aspects: Aspects) -> list[dict]: + """Deduplicate a list of representatives by their full aspect signature.""" + seen: set = set() + out: list[dict] = [] + for r in recs: + sig = signature(r, aspects) + if sig not in seen: + seen.add(sig) + out.append(r) + return out diff --git a/tests/generators/compliance_runners/state_transition/aspects/base.mzn b/tests/generators/compliance_runners/state_transition/aspects/base.mzn new file mode 100644 index 00000000000..5ea2bd9c1bf --- /dev/null +++ b/tests/generators/compliance_runners/state_transition/aspects/base.mzn @@ -0,0 +1,17 @@ +% Shared value domains for coverage dimensions. +% +% One enum carries every coverage value plus NA, so a not-applicable dimension +% can be marked NA regardless of whether it is a comparison or a boolean. +% Comparison dimensions range over CMP (or CMP_NA when guarded); boolean +% coverage dimensions over BOOLV (or BOOLV_NA when guarded). +% +% NA marks a dimension that is not applicable (its value cannot be recovered +% from the input vector). It is distinct from an applicable-but-unreached +% dimension, which keeps a real value. + +enum Dim = { LT, EQ, GT, F, T, NA }; + +set of Dim: CMP = { LT, EQ, GT }; +set of Dim: CMP_NA = { LT, EQ, GT, NA }; +set of Dim: BOOLV = { F, T }; +set of Dim: BOOLV_NA = { F, T, NA }; diff --git a/tests/generators/compliance_runners/state_transition/aspects/blob_kzg_capacity.mzn b/tests/generators/compliance_runners/state_transition/aspects/blob_kzg_capacity.mzn new file mode 100644 index 00000000000..b4b0f169128 --- /dev/null +++ b/tests/generators/compliance_runners/state_transition/aspects/blob_kzg_capacity.mzn @@ -0,0 +1,12 @@ +% Realization aspect: blob KZG commitment capacity. +% +% Spec: len(bid.blob_kzg_commitments) <= get_blob_parameters(...).max_blobs_per_block +% (specs/gloas/beacon-chain.md process_execution_payload_bid :1633). +% Always applicable (checked on both branches). + +include "base.mzn"; + +var CMP: bid_kzg_to_max; % compare(len(commitments), max_blobs_per_block) + +var bool: bid_kzg_under_limit; +constraint bid_kzg_under_limit <-> (bid_kzg_to_max in {LT, EQ}); diff --git a/tests/generators/compliance_runners/state_transition/aspects/block_context.mzn b/tests/generators/compliance_runners/state_transition/aspects/block_context.mzn new file mode 100644 index 00000000000..6ed55484bf7 --- /dev/null +++ b/tests/generators/compliance_runners/state_transition/aspects/block_context.mzn @@ -0,0 +1,18 @@ +% Realization aspect: block-context matching. +% +% Spec (specs/gloas/beacon-chain.md process_execution_payload_bid :1642-1644): +% bid.parent_block_hash == state.latest_block_hash +% bid.parent_block_root == get_block_root_at_slot(state, state.slot - 1) +% bid.prev_randao == get_randao_mix(state, get_current_epoch(state)) +% Always applicable. + +include "base.mzn"; + +var bool: bid_parent_block_hash_matches; +var bool: bid_prev_randao_matches; + +% parent_block_root compares against get_block_root_at_slot(state, slot - 1), +% which is only defined past genesis. NA at the genesis slot. +var bool: bid_parent_block_root_applicable; +var BOOLV_NA: bid_parent_block_root_matches; +constraint (bid_parent_block_root_matches == NA) <-> not bid_parent_block_root_applicable; diff --git a/tests/generators/compliance_runners/state_transition/aspects/builder_funds.mzn b/tests/generators/compliance_runners/state_transition/aspects/builder_funds.mzn new file mode 100644 index 00000000000..4b910c892c3 --- /dev/null +++ b/tests/generators/compliance_runners/state_transition/aspects/builder_funds.mzn @@ -0,0 +1,21 @@ +% Realization aspect: builder funds / coverage (parameterized). +% +% can_builder_cover_bid (specs/gloas/beacon-chain.md can_builder_cover_bid): +% min_balance = MIN_DEPOSIT_AMOUNT + get_pending_balance_to_withdraw_for_builder(...) +% if builder.balance < min_balance: return False # guard boundary +% return builder.balance - min_balance >= bid.value # coverage boundary +% Two comparison dimensions preserve both boundaries; the predicate carries the +% nested applicability and the balance==min coherence, and a function derives +% can_cover. min_balance must be realized including the pending offset. + +include "base.mzn"; + +predicate builder_funds_ok(var Dim: balance_to_min, var Dim: available_to_bid, var bool: applicable) = + (balance_to_min == NA <-> not applicable) + /\ (available_to_bid == NA <-> not (applicable /\ balance_to_min in {EQ, GT})) + % balance == min_balance means zero available, which cannot exceed a + % non-negative bid value, so the available/bid comparison is never GT there. + /\ (balance_to_min == EQ -> available_to_bid in {LT, EQ}); + +function var bool: builder_can_cover(var Dim: balance_to_min, var Dim: available_to_bid) = + balance_to_min in {EQ, GT} /\ available_to_bid in {EQ, GT}; diff --git a/tests/generators/compliance_runners/state_transition/aspects/builder_lifecycle.mzn b/tests/generators/compliance_runners/state_transition/aspects/builder_lifecycle.mzn new file mode 100644 index 00000000000..bdfab3d8d5c --- /dev/null +++ b/tests/generators/compliance_runners/state_transition/aspects/builder_lifecycle.mzn @@ -0,0 +1,18 @@ +% Realization aspect: builder lifecycle (parameterized). +% +% is_active_builder: deposit_epoch < finalized_checkpoint.epoch and +% withdrawable_epoch == FAR_FUTURE_EPOCH (specs/gloas/beacon-chain.md). +% Predicate + derived function over a builder's (deposit_to_finalized_epoch, +% withdrawable_epoch_set) dimensions, instantiable per role. Shared by +% execution_payload_bid and builder_exit_request. + +include "base.mzn"; + +predicate builder_lifecycle_ok(var Dim: deposit_to_finalized_epoch, + var Dim: withdrawable_epoch_set, var bool: applicable) = + (deposit_to_finalized_epoch == NA <-> not applicable) + /\ (withdrawable_epoch_set == NA <-> not applicable); + +function var bool: builder_is_active(var Dim: deposit_to_finalized_epoch, + var Dim: withdrawable_epoch_set) = + deposit_to_finalized_epoch == LT /\ withdrawable_epoch_set == F; diff --git a/tests/generators/compliance_runners/state_transition/aspects/builder_membership.mzn b/tests/generators/compliance_runners/state_transition/aspects/builder_membership.mzn new file mode 100644 index 00000000000..52adb9ff0d4 --- /dev/null +++ b/tests/generators/compliance_runners/state_transition/aspects/builder_membership.mzn @@ -0,0 +1,9 @@ +% Realization aspect: builder membership by public key. +% +% Whether request.pubkey resolves to an existing builder in state.builders +% (specs/gloas/beacon-chain.md process_builder_exit_request / process_builder_deposit_request). +% Shared by the pubkey-addressed builder handlers. + +include "base.mzn"; + +var bool: builder_pubkey_found; diff --git a/tests/generators/compliance_runners/state_transition/aspects/builder_payment_quorum.mzn b/tests/generators/compliance_runners/state_transition/aspects/builder_payment_quorum.mzn new file mode 100644 index 00000000000..b2f0ddcff8e --- /dev/null +++ b/tests/generators/compliance_runners/state_transition/aspects/builder_payment_quorum.mzn @@ -0,0 +1,8 @@ +% Reusable payment-weight / quorum comparison relation. +include "base.mzn"; + +predicate builder_payment_quorum_ok(var Dim: relation, var bool: applicable) = + (relation == NA <-> not applicable) /\ + (applicable -> relation in CMP); + +function var bool: meets_builder_payment_quorum(var Dim: relation) = relation in {EQ, GT}; diff --git a/tests/generators/compliance_runners/state_transition/aspects/builder_pending_balance.mzn b/tests/generators/compliance_runners/state_transition/aspects/builder_pending_balance.mzn new file mode 100644 index 00000000000..aa189fe2050 --- /dev/null +++ b/tests/generators/compliance_runners/state_transition/aspects/builder_pending_balance.mzn @@ -0,0 +1,15 @@ +% Realization aspect: builder pending balance / queues (parameterized). +% +% get_pending_balance_to_withdraw_for_builder over builder_pending_withdrawals +% and builder_pending_payments (specs/gloas/beacon-chain.md). Predicate + derived +% function, instantiable per role. Shared by execution_payload_bid and +% builder_exit_request. + +include "base.mzn"; + +predicate builder_pending_ok(var Dim: has_withdrawal, var Dim: has_payment, var bool: applicable) = + (has_withdrawal == NA <-> not applicable) + /\ (has_payment == NA <-> not applicable); + +function var bool: builder_has_pending(var Dim: has_withdrawal, var Dim: has_payment) = + has_withdrawal == T \/ has_payment == T; diff --git a/tests/generators/compliance_runners/state_transition/aspects/builder_reset.mzn b/tests/generators/compliance_runners/state_transition/aspects/builder_reset.mzn new file mode 100644 index 00000000000..91abeed37a0 --- /dev/null +++ b/tests/generators/compliance_runners/state_transition/aspects/builder_reset.mzn @@ -0,0 +1,21 @@ +% Realization aspect: swept-builder reset condition (builder_deposit_request). +% +% On a top-up to an exited, drained builder — withdrawable_epoch != FAR_FUTURE +% and balance == 0 — the withdrawable epoch is reset before crediting the +% deposit (specs/gloas/beacon-chain.md process_builder_deposit_request). +% +% Note: `builder_withdrawable_epoch_set` is the same predicate as in +% builder_lifecycle; a future refactor could factor it into a shared +% builder-exit-status aspect. Applicable only when a builder is resolved. + +include "base.mzn"; + +var bool: builder_reset_applicable; +var BOOLV_NA: builder_withdrawable_epoch_set; +var BOOLV_NA: builder_balance_zero; +constraint (builder_withdrawable_epoch_set == NA) <-> not builder_reset_applicable; +constraint (builder_balance_zero == NA) <-> not builder_reset_applicable; + +var bool: reset_applies; +constraint reset_applies <-> + (builder_withdrawable_epoch_set == T /\ builder_balance_zero == T); diff --git a/tests/generators/compliance_runners/state_transition/aspects/builder_version.mzn b/tests/generators/compliance_runners/state_transition/aspects/builder_version.mzn new file mode 100644 index 00000000000..21668e555cf --- /dev/null +++ b/tests/generators/compliance_runners/state_transition/aspects/builder_version.mzn @@ -0,0 +1,10 @@ +% Realization aspect: builder version (parameterized). +% +% state.builders[builder_index].version == PAYLOAD_BUILDER_VERSION +% (specs/gloas/beacon-chain.md process_execution_payload_bid). Single guarded +% boolean; the handler exposes the coverage dimension var and applies the guard. + +include "base.mzn"; + +predicate builder_version_ok(var Dim: valid, var bool: applicable) = + (valid == NA <-> not applicable); diff --git a/tests/generators/compliance_runners/state_transition/aspects/consolidation_churn.mzn b/tests/generators/compliance_runners/state_transition/aspects/consolidation_churn.mzn new file mode 100644 index 00000000000..ab48f1cb6b3 --- /dev/null +++ b/tests/generators/compliance_runners/state_transition/aspects/consolidation_churn.mzn @@ -0,0 +1,9 @@ +% Realization aspect: consolidation churn availability. +% +% sufficient_consolidation_churn <-> get_consolidation_churn_limit(state) > MIN_ACTIVATION_BALANCE +% (specs/electra/beacon-chain.md process_consolidation_request). The materializer +% realizes it by sizing the active validator set. Always applicable. + +include "base.mzn"; + +var bool: sufficient_consolidation_churn; diff --git a/tests/generators/compliance_runners/state_transition/aspects/consolidation_pair.mzn b/tests/generators/compliance_runners/state_transition/aspects/consolidation_pair.mzn new file mode 100644 index 00000000000..6530a630c3e --- /dev/null +++ b/tests/generators/compliance_runners/state_transition/aspects/consolidation_pair.mzn @@ -0,0 +1,9 @@ +% Realization aspect: consolidation source/target pairing. +% +% same_source_target <-> source_pubkey == target_pubkey. When true, only the +% switch-to-compounding path can apply; otherwise it is a consolidation +% (specs/electra/beacon-chain.md process_consolidation_request). + +include "base.mzn"; + +var bool: same_source_target; diff --git a/tests/generators/compliance_runners/state_transition/aspects/deposit_amount.mzn b/tests/generators/compliance_runners/state_transition/aspects/deposit_amount.mzn new file mode 100644 index 00000000000..f0af02ceccb --- /dev/null +++ b/tests/generators/compliance_runners/state_transition/aspects/deposit_amount.mzn @@ -0,0 +1,13 @@ +% Realization aspect: deposit-amount profile. +% +% Profiles used by deposit-like handlers: +% ZERO, MINIMUM, ACTIVATION, or ABOVE_ACTIVATION. `amount_nonzero` is the +% derived predicate shared by handlers that only need the zero/nonzero split. + +include "base.mzn"; + +enum AmountProfile = { ZERO, MINIMUM, ACTIVATION, ABOVE_ACTIVATION }; + +var AmountProfile: amount_profile; +var bool: amount_nonzero; +constraint amount_nonzero <-> amount_profile != ZERO; diff --git a/tests/generators/compliance_runners/state_transition/aspects/deposit_pubkey.mzn b/tests/generators/compliance_runners/state_transition/aspects/deposit_pubkey.mzn new file mode 100644 index 00000000000..169927e8b86 --- /dev/null +++ b/tests/generators/compliance_runners/state_transition/aspects/deposit_pubkey.mzn @@ -0,0 +1,9 @@ +% Realization aspect: deposit request pubkey membership. +% +% pubkey_is_existing_validator <-> request.pubkey matches some state.validators[i].pubkey. +% process_deposit_request copies the request verbatim into a PendingDeposit and +% does NOT branch on this — pure input/output coverage. Always applicable. + +include "base.mzn"; + +var bool: pubkey_is_existing_validator; diff --git a/tests/generators/compliance_runners/state_transition/aspects/entity_reference.mzn b/tests/generators/compliance_runners/state_transition/aspects/entity_reference.mzn new file mode 100644 index 00000000000..c6f4d431baa --- /dev/null +++ b/tests/generators/compliance_runners/state_transition/aspects/entity_reference.mzn @@ -0,0 +1,21 @@ +% Realization aspect: entity reference & membership. +% +% Resolve bid.builder_index against state.builders: +% builder_index == BUILDER_INDEX_SELF_BUILD -> SELF_BUILD +% index resolves to an existing builder -> EXISTING +% index past the registry (no builder) -> NON_EXISTING +% (specs/gloas/beacon-chain.md process_execution_payload_bid :1619; is_active_builder indexing) +% +% Shared with builder_exit_request / builder_deposit_request (all resolve a builder). + +include "base.mzn"; + +enum BuilderRef = { SELF_BUILD, EXISTING, NON_EXISTING }; +var BuilderRef: builder_ref; + +var bool: self_build; +var bool: external_bid; +var bool: builder_found; +constraint self_build <-> (builder_ref == SELF_BUILD); +constraint external_bid <-> (builder_ref != SELF_BUILD); +constraint builder_found <-> (builder_ref == EXISTING); diff --git a/tests/generators/compliance_runners/state_transition/aspects/partial_queue_capacity.mzn b/tests/generators/compliance_runners/state_transition/aspects/partial_queue_capacity.mzn new file mode 100644 index 00000000000..f0be2bcd54e --- /dev/null +++ b/tests/generators/compliance_runners/state_transition/aspects/partial_queue_capacity.mzn @@ -0,0 +1,9 @@ +% Realization aspect: pending-partial-withdrawals queue capacity. +% +% partial_queue_full <-> len(state.pending_partial_withdrawals) == PENDING_PARTIAL_WITHDRAWALS_LIMIT +% (specs/electra/beacon-chain.md process_withdrawal_request). A full queue blocks +% partial requests only (full exits still process). Always applicable. + +include "base.mzn"; + +var bool: partial_queue_full; diff --git a/tests/generators/compliance_runners/state_transition/aspects/pending_consolidations_capacity.mzn b/tests/generators/compliance_runners/state_transition/aspects/pending_consolidations_capacity.mzn new file mode 100644 index 00000000000..fcafd5f7ed2 --- /dev/null +++ b/tests/generators/compliance_runners/state_transition/aspects/pending_consolidations_capacity.mzn @@ -0,0 +1,8 @@ +% Realization aspect: pending-consolidations queue capacity. +% +% pending_consolidations_full <-> len(state.pending_consolidations) == PENDING_CONSOLIDATIONS_LIMIT +% (specs/electra/beacon-chain.md process_consolidation_request). Always applicable. + +include "base.mzn"; + +var bool: pending_consolidations_full; diff --git a/tests/generators/compliance_runners/state_transition/aspects/self_build_signature.mzn b/tests/generators/compliance_runners/state_transition/aspects/self_build_signature.mzn new file mode 100644 index 00000000000..bf5aec57c1e --- /dev/null +++ b/tests/generators/compliance_runners/state_transition/aspects/self_build_signature.mzn @@ -0,0 +1,9 @@ +% Realization aspect: self-build signature sentinel (parameterized). +% +% For self-builds the signature must equal bls.G2_POINT_AT_INFINITY rather than a +% real signature (specs/gloas/beacon-chain.md process_execution_payload_bid). + +include "base.mzn"; + +predicate self_build_signature_ok(var Dim: is_infinity, var bool: applicable) = + (is_infinity == NA <-> not applicable); diff --git a/tests/generators/compliance_runners/state_transition/aspects/signed_message.mzn b/tests/generators/compliance_runners/state_transition/aspects/signed_message.mzn new file mode 100644 index 00000000000..df6efbaed41 --- /dev/null +++ b/tests/generators/compliance_runners/state_transition/aspects/signed_message.mzn @@ -0,0 +1,12 @@ +% Realization aspect: builder message signature validity (parameterized). +% +% A boolean coverage dimension: does the message carry a valid builder signature? +% The handler binds which signature and its applicability — e.g. +% verify_execution_payload_bid_signature for a bid, +% is_valid_builder_deposit_signature for a builder deposit. Shared across signed +% builder handlers. + +include "base.mzn"; + +predicate signed_message_ok(var Dim: valid, var bool: applicable) = + (valid == NA <-> not applicable); diff --git a/tests/generators/compliance_runners/state_transition/aspects/slot_epoch.mzn b/tests/generators/compliance_runners/state_transition/aspects/slot_epoch.mzn new file mode 100644 index 00000000000..6569b2e16ff --- /dev/null +++ b/tests/generators/compliance_runners/state_transition/aspects/slot_epoch.mzn @@ -0,0 +1,17 @@ +% Realization aspect: slot / epoch relationship. +% +% Spec: bid.slot == state.slot ; state.slot > GENESIS_SLOT +% (specs/gloas/beacon-chain.md process_execution_payload_bid :1639-1640). +% Always applicable. + +include "base.mzn"; + +var CMP: bid_slot_to_state; % compare(bid.slot, state.slot) +var bool: state_slot_past_genesis; % state.slot > GENESIS_SLOT + +var bool: bid_slot_matches; +constraint bid_slot_matches <-> (bid_slot_to_state == EQ); + +% bid.slot < state.slot requires state.slot > GENESIS_SLOT (a bid slot cannot be +% below the genesis slot), so LT implies the state is past genesis. +constraint (bid_slot_to_state == LT) -> state_slot_past_genesis; diff --git a/tests/generators/compliance_runners/state_transition/aspects/source_authorization.mzn b/tests/generators/compliance_runners/state_transition/aspects/source_authorization.mzn new file mode 100644 index 00000000000..74ddeeba0b2 --- /dev/null +++ b/tests/generators/compliance_runners/state_transition/aspects/source_authorization.mzn @@ -0,0 +1,12 @@ +% Realization aspect: source-address authorization. +% +% Whether the request's source_address matches the referenced builder's +% execution_address, i.e. builder.execution_address == request.source_address +% (specs/gloas/beacon-chain.md process_builder_exit_request). Applicable only +% when a builder is resolved. + +include "base.mzn"; + +var bool: source_authorization_applicable; +var BOOLV_NA: source_address_matches; +constraint (source_address_matches == NA) <-> not source_authorization_applicable; diff --git a/tests/generators/compliance_runners/state_transition/aspects/validator_balance.mzn b/tests/generators/compliance_runners/state_transition/aspects/validator_balance.mzn new file mode 100644 index 00000000000..8a0e49e589b --- /dev/null +++ b/tests/generators/compliance_runners/state_transition/aspects/validator_balance.mzn @@ -0,0 +1,14 @@ +% Realization aspect: validator balance thresholds (partial withdrawal). +% +% sufficient_effective_balance <-> effective_balance >= MIN_ACTIVATION_BALANCE +% has_excess_balance <-> balance > MIN_ACTIVATION_BALANCE + pending_balance_to_withdraw +% (specs/electra/beacon-chain.md process_withdrawal_request). Applicable when a +% validator is resolved. + +include "base.mzn"; + +var bool: validator_balance_applicable; +var BOOLV_NA: sufficient_effective_balance; +var BOOLV_NA: has_excess_balance; +constraint (sufficient_effective_balance == NA) <-> not validator_balance_applicable; +constraint (has_excess_balance == NA) <-> not validator_balance_applicable; diff --git a/tests/generators/compliance_runners/state_transition/aspects/validator_credential.mzn b/tests/generators/compliance_runners/state_transition/aspects/validator_credential.mzn new file mode 100644 index 00000000000..bf99a9f5067 --- /dev/null +++ b/tests/generators/compliance_runners/state_transition/aspects/validator_credential.mzn @@ -0,0 +1,20 @@ +% Realization aspect: validator withdrawal-credential kind (parameterized). +% +% withdrawal_credentials[:1]: BLS (0x00), ETH1 (0x01), or COMPOUNDING (0x02). +% Parameterized as a predicate over a credential var + derived-value functions, +% instantiable per role (source, target). The handler declares a role-prefixed +% `var ValidatorCredentialKind` and exposes the derived booleans it needs. + +include "base.mzn"; + +enum ValidatorCredentialKind = { CRED_BLS, CRED_ETH1, CRED_COMPOUNDING, CRED_NA }; + +predicate validator_credential_ok(var ValidatorCredentialKind: c, var bool: applicable) = + (c == CRED_NA <-> not applicable); + +function var bool: cred_has_execution(var ValidatorCredentialKind: c) = + c in {CRED_ETH1, CRED_COMPOUNDING}; +function var bool: cred_has_compounding(var ValidatorCredentialKind: c) = + c == CRED_COMPOUNDING; +function var bool: cred_is_eth1(var ValidatorCredentialKind: c) = + c == CRED_ETH1; diff --git a/tests/generators/compliance_runners/state_transition/aspects/validator_lifecycle.mzn b/tests/generators/compliance_runners/state_transition/aspects/validator_lifecycle.mzn new file mode 100644 index 00000000000..54820e88d9e --- /dev/null +++ b/tests/generators/compliance_runners/state_transition/aspects/validator_lifecycle.mzn @@ -0,0 +1,15 @@ +% Realization aspect: validator lifecycle (parameterized). +% +% active <-> is_active_validator (activation_epoch <= epoch < exit_epoch) +% exiting <-> exit_epoch != FAR_FUTURE_EPOCH +% +% Parameterized as a predicate over a validator's (active, exiting) coverage +% dimensions, instantiable per role (source, target, or a single validator) — +% the handler declares role-prefixed vars and applies the predicate to each. +% `applicable` is true when the validator resolves. + +include "base.mzn"; + +predicate validator_lifecycle_ok(var Dim: active, var Dim: exiting, var bool: applicable) = + (active == NA <-> not applicable) + /\ (exiting == NA <-> not applicable); diff --git a/tests/generators/compliance_runners/state_transition/aspects/validator_membership.mzn b/tests/generators/compliance_runners/state_transition/aspects/validator_membership.mzn new file mode 100644 index 00000000000..5e40cb58f39 --- /dev/null +++ b/tests/generators/compliance_runners/state_transition/aspects/validator_membership.mzn @@ -0,0 +1,9 @@ +% Realization aspect: validator membership by public key. +% +% Whether request.validator_pubkey resolves to an existing validator in +% state.validators. Shared by the pubkey-addressed validator handlers +% (withdrawal_request, consolidation_request, voluntary_exit). + +include "base.mzn"; + +var bool: validator_pubkey_found; diff --git a/tests/generators/compliance_runners/state_transition/aspects/validator_pending_withdrawal.mzn b/tests/generators/compliance_runners/state_transition/aspects/validator_pending_withdrawal.mzn new file mode 100644 index 00000000000..67e7d4c9073 --- /dev/null +++ b/tests/generators/compliance_runners/state_transition/aspects/validator_pending_withdrawal.mzn @@ -0,0 +1,11 @@ +% Realization aspect: validator pending partial withdrawals. +% +% has_pending_partial_withdrawal <-> get_pending_balance_to_withdraw(state, index) > 0 +% (sum of pending_partial_withdrawals for the validator; specs/electra). Applicable +% when a validator is resolved. + +include "base.mzn"; + +var bool: validator_pending_applicable; +var BOOLV_NA: has_pending_partial_withdrawal; +constraint (has_pending_partial_withdrawal == NA) <-> not validator_pending_applicable; diff --git a/tests/generators/compliance_runners/state_transition/aspects/validator_seasoning.mzn b/tests/generators/compliance_runners/state_transition/aspects/validator_seasoning.mzn new file mode 100644 index 00000000000..3844ae902f1 --- /dev/null +++ b/tests/generators/compliance_runners/state_transition/aspects/validator_seasoning.mzn @@ -0,0 +1,11 @@ +% Realization aspect: validator seasoning (parameterized). +% +% old_enough <-> current_epoch >= activation_epoch + SHARD_COMMITTEE_PERIOD. +% Only source-role validators gate on this. Coherence with lifecycle +% (old_enough and not exiting implies active) is stated by the handler where +% both are instantiated for the same role. + +include "base.mzn"; + +predicate validator_seasoning_ok(var Dim: old_enough, var bool: applicable) = + (old_enough == NA <-> not applicable); diff --git a/tests/generators/compliance_runners/state_transition/aspects/withdrawal_amount.mzn b/tests/generators/compliance_runners/state_transition/aspects/withdrawal_amount.mzn new file mode 100644 index 00000000000..0a30f48834d --- /dev/null +++ b/tests/generators/compliance_runners/state_transition/aspects/withdrawal_amount.mzn @@ -0,0 +1,9 @@ +% Realization aspect: withdrawal request amount. +% +% is_full_exit_request <-> amount == FULL_EXIT_REQUEST_AMOUNT (0). A zero amount +% requests a full exit; any positive amount is a partial withdrawal +% (specs/electra/beacon-chain.md process_withdrawal_request). Always applicable. + +include "base.mzn"; + +var bool: is_full_exit_request; diff --git a/tests/generators/compliance_runners/state_transition/aspects/withdrawal_credential.mzn b/tests/generators/compliance_runners/state_transition/aspects/withdrawal_credential.mzn new file mode 100644 index 00000000000..c36fb196bd3 --- /dev/null +++ b/tests/generators/compliance_runners/state_transition/aspects/withdrawal_credential.mzn @@ -0,0 +1,13 @@ +% Realization aspect: withdrawal-credential profile. +% +% withdrawal_credentials[:1]: BLS (0x00), ETH1 (0x01), COMPOUNDING (0x02), or +% BUILDER (0xB0). The builder predicate is derived from this profile. +% (specs/gloas/beacon-chain.md withdrawal credential prefixes). + +include "base.mzn"; + +enum WithdrawalCredentialsProfile = { BLS, ETH1, COMPOUNDING, BUILDER }; + +var WithdrawalCredentialsProfile: withdrawal_credentials_profile; +var bool: wc_is_builder_prefix; +constraint wc_is_builder_prefix <-> withdrawal_credentials_profile == BUILDER; diff --git a/tests/generators/compliance_runners/state_transition/aspects_helpers/__init__.py b/tests/generators/compliance_runners/state_transition/aspects_helpers/__init__.py new file mode 100644 index 00000000000..e69de29bb2d diff --git a/tests/generators/compliance_runners/state_transition/aspects_helpers/deposit_amount.py b/tests/generators/compliance_runners/state_transition/aspects_helpers/deposit_amount.py new file mode 100644 index 00000000000..1fc16b447ad --- /dev/null +++ b/tests/generators/compliance_runners/state_transition/aspects_helpers/deposit_amount.py @@ -0,0 +1,27 @@ +"""Shared Python realization helpers for deposit-amount profiles.""" + +from __future__ import annotations + +from typing import Any + + +def deposit_amount_from_profile(spec: Any, profile: str) -> int: + return { + "ZERO": 0, + "MINIMUM": int(spec.MIN_DEPOSIT_AMOUNT), + "ACTIVATION": int(spec.MIN_ACTIVATION_BALANCE), + "ABOVE_ACTIVATION": int(spec.MIN_ACTIVATION_BALANCE + spec.EFFECTIVE_BALANCE_INCREMENT), + }[profile] + + +def deposit_amount_profile(spec: Any, amount: Any) -> str: + amount = int(amount) + if amount == 0: + return "ZERO" + if amount == int(spec.MIN_DEPOSIT_AMOUNT): + return "MINIMUM" + if amount == int(spec.MIN_ACTIVATION_BALANCE): + return "ACTIVATION" + if amount > int(spec.MIN_ACTIVATION_BALANCE): + return "ABOVE_ACTIVATION" + return "UNKNOWN" diff --git a/tests/generators/compliance_runners/state_transition/aspects_helpers/withdrawal_credential.py b/tests/generators/compliance_runners/state_transition/aspects_helpers/withdrawal_credential.py new file mode 100644 index 00000000000..70dfef471a4 --- /dev/null +++ b/tests/generators/compliance_runners/state_transition/aspects_helpers/withdrawal_credential.py @@ -0,0 +1,25 @@ +"""Shared Python realization helpers for withdrawal-credential profiles.""" + +from __future__ import annotations + +from typing import Any + + +def _withdrawal_credential_prefixes(spec: Any) -> dict[str, bytes]: + return { + "BLS": bytes(spec.BLS_WITHDRAWAL_PREFIX), + "ETH1": bytes(spec.ETH1_ADDRESS_WITHDRAWAL_PREFIX), + "COMPOUNDING": bytes(spec.COMPOUNDING_WITHDRAWAL_PREFIX), + "BUILDER": bytes(spec.BUILDER_WITHDRAWAL_PREFIX), + } + + +def withdrawal_credentials_from_profile(spec: Any, profile: str, address_tail: bytes) -> bytes: + return _withdrawal_credential_prefixes(spec)[profile] + b"\x00" * 11 + address_tail + + +def withdrawal_credentials_profile(spec: Any, credentials: Any) -> str: + profiles = { + prefix: profile for profile, prefix in _withdrawal_credential_prefixes(spec).items() + } + return profiles.get(bytes(credentials[:1]), "UNKNOWN") diff --git a/tests/generators/compliance_runners/state_transition/attestation/__init__.py b/tests/generators/compliance_runners/state_transition/attestation/__init__.py new file mode 100644 index 00000000000..3a3b52b20ea --- /dev/null +++ b/tests/generators/compliance_runners/state_transition/attestation/__init__.py @@ -0,0 +1,9 @@ +"""Aspect-based compliance runner for Gloas attestations.""" + +from .coverage import build_profile +from .materializer import AttestationMaterializer +from .validation import validate_case + +MATERIALIZER = AttestationMaterializer + +__all__ = ("MATERIALIZER", "build_profile", "validate_case") diff --git a/tests/generators/compliance_runners/state_transition/attestation/coverage.py b/tests/generators/compliance_runners/state_transition/attestation/coverage.py new file mode 100644 index 00000000000..c4fdc8ed228 --- /dev/null +++ b/tests/generators/compliance_runners/state_transition/attestation/coverage.py @@ -0,0 +1,66 @@ +"""Coverage profiles for Gloas ``process_attestation``.""" + +from __future__ import annotations + +from pathlib import Path + +from tests.generators.compliance_runners.state_transition.aspect_coverage import ( + build_profile as _build_profile, + enumerate_signatures, +) + +from .materializer import _DIMS + +INPUT_ASPECTS = { + "data": [ + "target_epoch_in_window", + "target_epoch_matches_slot", + "inclusion_delay_ok", + "index_valid", + ], + "committees": ["committee_indices_valid", "committee_nonempty", "aggregation_length_valid"], + "signature": ["signature_valid"], + "builder_payment": [ + "attestation_is_same_slot", + "pending_payment_amount_positive", + "sets_new_participation_flag", + ], +} +OUTCOME_ASPECT = {"outcome": ["target_is_current", "payment_weight_increased", "outcome"]} +ALL_ASPECTS = {**INPUT_ASPECTS, **OUTCOME_ASPECT} +MODEL = Path(__file__).parent / "models" / "handler_attestation.mzn" + + +def _nfaults(r: dict) -> int: + # Count independent failing checks. Structural checks are a dependency + # chain: later checks are not applicable when an earlier check already + # prevents the attestation from being indexed and processed. + faults = int(not r["target_epoch_in_window"]) + if r["target_epoch_in_window"]: + faults += int(not r["target_epoch_matches_slot"]) + faults += int(not r["inclusion_delay_ok"]) + faults += int(not r["index_valid"]) + if r["index_valid"]: + faults += int(not r["committee_indices_valid"]) + if r["committee_indices_valid"]: + faults += int(not r["committee_nonempty"]) + if r["committee_nonempty"]: + faults += int(not r["aggregation_length_valid"]) + if r["aggregation_length_valid"]: + faults += int(not r["signature_valid"]) + return faults + + +def _recs(): + return enumerate_signatures(MODEL, _DIMS, ALL_ASPECTS, _nfaults) + + +def build_profile(name): + return _build_profile( + _recs(), + name, + ALL_ASPECTS, + INPUT_ASPECTS, + OUTCOME_ASPECT, + normal_outcome_aspect=OUTCOME_ASPECT, + ) diff --git a/tests/generators/compliance_runners/state_transition/attestation/materializer.py b/tests/generators/compliance_runners/state_transition/attestation/materializer.py new file mode 100644 index 00000000000..fc0f0890550 --- /dev/null +++ b/tests/generators/compliance_runners/state_transition/attestation/materializer.py @@ -0,0 +1,166 @@ +"""Materialize canonical Gloas ``process_attestation`` gate cases.""" + +from __future__ import annotations + +from typing import Any, TYPE_CHECKING + +from eth_consensus_specs.test.helpers.attestations import get_valid_attestation, sign_attestation +from eth_consensus_specs.test.helpers.genesis import create_genesis_state +from eth_consensus_specs.test.helpers.state import transition_to +from tests.generators.compliance_runners.state_transition.materializer import Materializer + +if TYPE_CHECKING: + from tests.generators.compliance_runners.gen_base.gen_typing import TestCasePart + +EPOCHS_PAST_GENESIS = 10 +_DIMS = [ + "target_epoch_in_window", + "target_epoch_matches_slot", + "inclusion_delay_ok", + "index_valid", + "committee_indices_valid", + "committee_nonempty", + "aggregation_length_valid", + "signature_valid", + "target_is_current", + "attestation_is_same_slot", + "pending_payment_amount_positive", + "sets_new_participation_flag", + "payment_weight_increased", + "outcome", +] +_GATES = _DIMS[:8] +_REJECTS = { + "REJECT_TARGET_EPOCH_OUT_OF_WINDOW": 0, + "REJECT_TARGET_EPOCH_SLOT_MISMATCH": 1, + "REJECT_INCLUSION_DELAY": 2, + "REJECT_INDEX": 3, + "REJECT_COMMITTEE_INDEX": 4, + "REJECT_COMMITTEE_EMPTY": 5, + "REJECT_AGGREGATION_LENGTH": 6, + "REJECT_SIGNATURE": 7, +} + + +def _b(sol: Any, name: str) -> bool: + return bool(getattr(sol, name)) + + +class AttestationMaterializer(Materializer): + runner_name = "operations" + handler_name = "attestation" + + def _base_state(self) -> Any: + state = create_genesis_state( + self.spec, + validator_balances=[self.spec.MAX_EFFECTIVE_BALANCE] * 64, + activation_threshold=self.spec.MAX_EFFECTIVE_BALANCE, + ) + state.slot = self.spec.Slot(EPOCHS_PAST_GENESIS * self.spec.SLOTS_PER_EPOCH + 2) + return state + + def materialize_solution(self, sol: Any) -> tuple[dict, list[TestCasePart]]: + spec, pre = self.spec, self._base_state() + same_slot = _b(sol, "attestation_is_same_slot") + if same_slot: + pre = create_genesis_state( + spec, + validator_balances=[spec.MAX_EFFECTIVE_BALANCE] * 64, + activation_threshold=spec.MAX_EFFECTIVE_BALANCE, + ) + transition_to(spec, pre, spec.Slot(spec.MIN_ATTESTATION_INCLUSION_DELAY)) + current = int(spec.get_current_epoch(pre)) + target_current = _b(sol, "target_is_current") + target_matches_slot = _b(sol, "target_epoch_matches_slot") + # For a mismatch, choose a slot from the opposite epoch first. This + # preserves target_is_current while making the target/slot comparison + # false; changing only the target epoch would invert that dimension. + slot_target_current = target_current if target_matches_slot else not target_current + slot = ( + 0 + if same_slot + else ( + int(pre.slot) - 1 + if slot_target_current + else int(spec.compute_start_slot_at_epoch(current)) - 1 + ) + ) + committee = spec.get_beacon_committee(pre, spec.Slot(slot), 0) + attestation = get_valid_attestation( + spec, + pre, + slot=slot, + index=0, + signed=False, + filter_participant_set=lambda _: {committee[0]}, + ) + data = attestation.data + if not _b(sol, "target_epoch_in_window"): + data.target.epoch = spec.Epoch(current + 1) + elif not target_matches_slot: + data.target.epoch = spec.Epoch(current if target_current else current - 1) + if not _b(sol, "inclusion_delay_ok"): + data.slot = pre.slot + if _b(sol, "target_epoch_matches_slot"): + data.target.epoch = spec.compute_epoch_at_slot(pre.slot) + if not _b(sol, "index_valid"): + data.index = spec.CommitteeIndex(2) + if not _b(sol, "committee_indices_valid"): + invalid = int(spec.get_committee_count_per_slot(pre, data.target.epoch)) + attestation.committee_bits[0] = False + attestation.committee_bits[invalid] = True + if not _b(sol, "committee_nonempty"): + for i in range(len(attestation.aggregation_bits)): + attestation.aggregation_bits[i] = False + if not _b(sol, "aggregation_length_valid"): + # Add an unused bit rather than removing one. A short bitfield can + # make the preceding committee-attester access fail, changing this + # intended length-only failure into an earlier failure. + aggregation_bits = list(attestation.aggregation_bits) + [False] + attestation.aggregation_bits = spec.AggregationBits(data=aggregation_bits) + # These are pre-state properties. Materialize them independently of + # whether a later gate permits the handler to consume the attestation. + if same_slot and not _b(sol, "sets_new_participation_flag"): + flags = pre.current_epoch_participation[committee[0]] + for flag in range(len(spec.PARTICIPATION_FLAG_WEIGHTS)): + flags = spec.add_flag(flags, flag) + pre.current_epoch_participation[committee[0]] = flags + if same_slot and _b(sol, "pending_payment_amount_positive"): + payment_index = int(spec.SLOTS_PER_EPOCH) + slot % int(spec.SLOTS_PER_EPOCH) + pre.builder_pending_payments[payment_index] = spec.BuilderPendingPayment( + weight=spec.Gwei(0), + withdrawal=spec.BuilderPendingWithdrawal( + fee_recipient=spec.ExecutionAddress(), + amount=spec.Gwei(1), + builder_index=spec.BuilderIndex(0), + ), + ) + if ( + _b(sol, "signature_valid") + and _b(sol, "committee_indices_valid") + and _b(sol, "committee_nonempty") + and _b(sol, "aggregation_length_valid") + ): + sign_attestation(spec, pre, attestation) + post = pre.copy() + parent_slot = pre.latest_block_header.slot + try: + spec.process_attestation(post, attestation, parent_slot) + except (AssertionError, IndexError): + post = None + claimed = { + name: (_b(sol, name) if name != "outcome" else str(sol.outcome)) for name in _DIMS + } + meta = { + "description": f"process_attestation: {claimed['outcome']}", + "bls_setting": 1, + "parent_slot": int(parent_slot), + "claimed": claimed, + } + parts: list[TestCasePart] = [ + ("pre", "ssz", pre.encode_bytes()), + ("attestation", "ssz", attestation.encode_bytes()), + ] + if post is not None: + parts.append(("post", "ssz", post.encode_bytes())) + return meta, parts diff --git a/tests/generators/compliance_runners/state_transition/attestation/models/handler_attestation.mzn b/tests/generators/compliance_runners/state_transition/attestation/models/handler_attestation.mzn new file mode 100644 index 00000000000..9592965a6e7 --- /dev/null +++ b/tests/generators/compliance_runners/state_transition/attestation/models/handler_attestation.mzn @@ -0,0 +1,48 @@ +% Relational model: process_attestation (Gloas). Gate values are deliberately +% free: coverage profiles, not a first-failing frontier, select representatives. +enum Outcome = { REJECT_TARGET_EPOCH_OUT_OF_WINDOW, REJECT_TARGET_EPOCH_SLOT_MISMATCH, + REJECT_INCLUSION_DELAY, REJECT_INDEX, REJECT_COMMITTEE_INDEX, REJECT_COMMITTEE_EMPTY, + REJECT_AGGREGATION_LENGTH, REJECT_SIGNATURE, ACCEPT_CURRENT, ACCEPT_PREVIOUS }; +var bool: target_epoch_in_window; var bool: target_epoch_matches_slot; +var bool: inclusion_delay_ok; var bool: index_valid; var bool: committee_indices_valid; +var bool: committee_nonempty; var bool: aggregation_length_valid; var bool: signature_valid; +var bool: target_is_current; var bool: attestation_is_same_slot; +var bool: pending_payment_amount_positive; var bool: sets_new_participation_flag; +var bool: payment_weight_increased; var Outcome: outcome; +constraint attestation_is_same_slot -> target_is_current; +constraint attestation_is_same_slot -> target_epoch_matches_slot; +constraint attestation_is_same_slot -> inclusion_delay_ok; +% An inclusion-delay failure is materialized at state.slot. If its target still +% matches that slot, it is necessarily a current-epoch target. +constraint not inclusion_delay_ok /\ target_epoch_matches_slot -> target_is_current; +constraint not inclusion_delay_ok /\ not target_epoch_matches_slot -> not target_is_current; +% Payment weight is a same-slot effect. The materializer's flag-preparation +% dimension is likewise meaningful only for a same-slot attestation. +constraint not attestation_is_same_slot -> + (not pending_payment_amount_positive /\ not sets_new_participation_flag); +% An out-of-window target is materialized in the future. It is neither the +% current target nor consistent with the (current/previous) attestation slot. +constraint not target_epoch_in_window -> + (not target_is_current /\ not target_epoch_matches_slot); +% The materializer signs only structurally valid attestations. Once committee +% processing cannot reach a later structural/signature check, its value is +% deterministically false in the concrete vector. +constraint not committee_indices_valid -> + (not committee_nonempty /\ not aggregation_length_valid /\ not signature_valid); +constraint not committee_nonempty -> not signature_valid; +constraint not aggregation_length_valid -> not signature_valid; +% The materializer can only prepare same-slot participation/payment state once +% the signed attestation is structurally valid. These dimensions therefore +% cannot be true when a structural or signature gate blocks that preparation. +constraint (not signature_valid \/ not committee_indices_valid \/ + not committee_nonempty \/ not aggregation_length_valid) -> + (not pending_payment_amount_positive /\ not sets_new_participation_flag); +constraint not index_valid -> + (not pending_payment_amount_positive /\ not sets_new_participation_flag); +constraint outcome = if not target_epoch_in_window then REJECT_TARGET_EPOCH_OUT_OF_WINDOW + elseif not target_epoch_matches_slot then REJECT_TARGET_EPOCH_SLOT_MISMATCH + elseif not inclusion_delay_ok then REJECT_INCLUSION_DELAY elseif not index_valid then REJECT_INDEX + elseif not committee_indices_valid then REJECT_COMMITTEE_INDEX elseif not committee_nonempty then REJECT_COMMITTEE_EMPTY + elseif not aggregation_length_valid then REJECT_AGGREGATION_LENGTH elseif not signature_valid then REJECT_SIGNATURE + elseif target_is_current then ACCEPT_CURRENT else ACCEPT_PREVIOUS endif; +constraint payment_weight_increased <-> outcome in {ACCEPT_CURRENT, ACCEPT_PREVIOUS} /\ attestation_is_same_slot /\ pending_payment_amount_positive /\ sets_new_participation_flag; diff --git a/tests/generators/compliance_runners/state_transition/attestation/validation.py b/tests/generators/compliance_runners/state_transition/attestation/validation.py new file mode 100644 index 00000000000..4c388654866 --- /dev/null +++ b/tests/generators/compliance_runners/state_transition/attestation/validation.py @@ -0,0 +1,153 @@ +"""Recover and validate Gloas attestation coverage dimensions.""" + +from __future__ import annotations + +from typing import Any, TYPE_CHECKING + +from ruamel.yaml import YAML + +from eth_consensus_specs.gloas import minimal as spec +from tests.generators.compliance_runners.state_transition.validation import check_dimensions, decode + +if TYPE_CHECKING: + from pathlib import Path + + from tests.generators.compliance_runners.state_transition.validation import Check + +_YAML = YAML(typ="safe") + + +def _committee_dimensions(pre: Any, attestation: Any) -> tuple[bool, bool, bool]: + """Recover independent committee-index, nonempty, and length predicates.""" + try: + indices = spec.get_committee_indices(attestation.committee_bits) + count = spec.get_committee_count_per_slot(pre, attestation.data.target.epoch) + except (AssertionError, IndexError): + return False, False, False + indices_valid = all(index < count for index in indices) + if not indices_valid: + return False, False, False + offset = 0 + nonempty = True + try: + for index in indices: + committee = spec.get_beacon_committee(pre, attestation.data.slot, index) + end = min(offset + len(committee), len(attestation.aggregation_bits)) + bits = attestation.aggregation_bits[offset:end] + if len(bits) != len(committee) or not any(bits): + nonempty = False + offset += len(committee) + return indices_valid, nonempty, len(attestation.aggregation_bits) == offset + except (AssertionError, IndexError): + return False, False, False + + +def _signature_valid(pre: Any, attestation: Any) -> bool: + try: + return bool( + spec.is_valid_indexed_attestation(pre, spec.get_indexed_attestation(pre, attestation)) + ) + except (AssertionError, IndexError): + return False + + +def _is_attestation_same_slot(pre: Any, data: Any) -> bool: + try: + return bool(spec.is_attestation_same_slot(pre, data)) + except AssertionError: + return False + + +def _sets_new_participation_flag(pre: Any, attestation: Any, same_slot: bool) -> bool: + if not same_slot: + return False + try: + flag_indices = spec.get_attestation_participation_flag_indices( + pre, + attestation.data, + pre.slot - attestation.data.slot, + pre.latest_block_header.slot, + ) + participation = ( + pre.current_epoch_participation + if attestation.data.target.epoch == spec.get_current_epoch(pre) + else pre.previous_epoch_participation + ) + return any( + any(not spec.has_flag(participation[index], flag) for flag in flag_indices) + for index in spec.get_attesting_indices(pre, attestation) + ) + except (AssertionError, IndexError): + return False + + +def recover(pre: Any, attestation: Any) -> dict[str, Any]: + data = attestation.data + current = spec.get_current_epoch(pre) + target_in_window = data.target.epoch in (spec.get_previous_epoch(pre), current) + target_matches_slot = data.target.epoch == spec.compute_epoch_at_slot(data.slot) + inclusion_delay_ok = data.slot + spec.MIN_ATTESTATION_INCLUSION_DELAY <= pre.slot + committee_indices_valid, committee_nonempty, aggregation_length_valid = _committee_dimensions( + pre, attestation + ) + signature_valid = _signature_valid(pre, attestation) + target_is_current = data.target.epoch == current + same_slot = _is_attestation_same_slot(pre, data) + payment_index = ( + int(spec.SLOTS_PER_EPOCH) + int(data.slot) % int(spec.SLOTS_PER_EPOCH) + if target_is_current + else int(data.slot) % int(spec.SLOTS_PER_EPOCH) + ) + pending_payment_amount_positive = ( + pre.builder_pending_payments[payment_index].withdrawal.amount > 0 + ) + sets_new_participation_flag = _sets_new_participation_flag(pre, attestation, same_slot) + + if not target_in_window: + handler_outcome = "REJECT_TARGET_EPOCH_OUT_OF_WINDOW" + elif not target_matches_slot: + handler_outcome = "REJECT_TARGET_EPOCH_SLOT_MISMATCH" + elif not inclusion_delay_ok: + handler_outcome = "REJECT_INCLUSION_DELAY" + elif data.index >= 2: + handler_outcome = "REJECT_INDEX" + elif not committee_indices_valid: + handler_outcome = "REJECT_COMMITTEE_INDEX" + elif not committee_nonempty: + handler_outcome = "REJECT_COMMITTEE_EMPTY" + elif not aggregation_length_valid: + handler_outcome = "REJECT_AGGREGATION_LENGTH" + elif not signature_valid: + handler_outcome = "REJECT_SIGNATURE" + else: + handler_outcome = "ACCEPT_CURRENT" if target_is_current else "ACCEPT_PREVIOUS" + + payment_weight_increased = ( + handler_outcome.startswith("ACCEPT_") + and sets_new_participation_flag + and pending_payment_amount_positive + ) + return { + "target_epoch_in_window": target_in_window, + "target_epoch_matches_slot": target_matches_slot, + "inclusion_delay_ok": inclusion_delay_ok, + "index_valid": data.index < 2, + "committee_indices_valid": committee_indices_valid, + "committee_nonempty": committee_nonempty, + "aggregation_length_valid": aggregation_length_valid, + "signature_valid": signature_valid, + "target_is_current": target_is_current, + "attestation_is_same_slot": same_slot, + "pending_payment_amount_positive": pending_payment_amount_positive, + "sets_new_participation_flag": sets_new_participation_flag, + "payment_weight_increased": payment_weight_increased, + "outcome": handler_outcome, + } + + +def validate_case(case_dir: Path) -> list[Check]: + pre = decode(case_dir / "pre.ssz_snappy", spec.BeaconState) + attestation = decode(case_dir / "attestation.ssz_snappy", spec.Attestation) + claimed = _YAML.load((case_dir / "dimensions.yaml").read_text())["claimed"] + actual = recover(pre, attestation) + return check_dimensions(claimed, actual) diff --git a/tests/generators/compliance_runners/state_transition/builder_deposit_request/__init__.py b/tests/generators/compliance_runners/state_transition/builder_deposit_request/__init__.py new file mode 100644 index 00000000000..6e6f359a254 --- /dev/null +++ b/tests/generators/compliance_runners/state_transition/builder_deposit_request/__init__.py @@ -0,0 +1,7 @@ +from .coverage import build_profile +from .materializer import BuilderDepositRequestMaterializer +from .validation import validate_case + +MATERIALIZER = BuilderDepositRequestMaterializer + +__all__ = ("MATERIALIZER", "build_profile", "validate_case") diff --git a/tests/generators/compliance_runners/state_transition/builder_deposit_request/coverage.py b/tests/generators/compliance_runners/state_transition/builder_deposit_request/coverage.py new file mode 100644 index 00000000000..5f9210b9db5 --- /dev/null +++ b/tests/generators/compliance_runners/state_transition/builder_deposit_request/coverage.py @@ -0,0 +1,49 @@ +"""Coverage profiles for process_builder_deposit_request. + +Handler-specific instantiation of the shared ``..aspect_coverage`` engine. +Reuses the shared aspects builder_membership and signed_message (the SAME +signature aspect execution_payload_bid binds). + +Run: + uv run python -m ...builder_deposit_request.coverage + uv run python -m ...builder_deposit_request.coverage standard --materialize +""" + +from __future__ import annotations + +from pathlib import Path + +from tests.generators.compliance_runners.state_transition.aspect_coverage import ( + build_profile as _build_profile, + enumerate_signatures, +) + +from .materializer import _DIMS + +INPUT_ASPECTS = { + "withdrawal_credential": ["withdrawal_credentials_profile"], + "builder_membership": ["builder_pubkey_found"], + "signed_message": ["builder_signature_valid"], + "deposit_amount": ["amount_profile", "amount_nonzero"], + "builder_reset": ["builder_withdrawable_epoch_set", "builder_balance_zero"], +} +OUTCOME_ASPECT = {"outcome": ["outcome"]} +ALL_ASPECTS = {**INPUT_ASPECTS, **OUTCOME_ASPECT} +MODEL = Path(__file__).parent / "models" / "handler_builder_deposit_request.mzn" + + +def _nfaults(r: dict) -> int: + is_builder = r["withdrawal_credentials_profile"] == "BUILDER" + faults = int(not is_builder) + # The signature is checked only for a new builder with the right prefix. + if is_builder and not r["builder_pubkey_found"]: + faults += int(r["builder_signature_valid"] != "T") + return faults + + +def build_profile(name): + return _build_profile(_recs(), name, ALL_ASPECTS, INPUT_ASPECTS, OUTCOME_ASPECT) + + +def _recs(): + return enumerate_signatures(MODEL, _DIMS, ALL_ASPECTS, _nfaults) diff --git a/tests/generators/compliance_runners/state_transition/builder_deposit_request/materializer.py b/tests/generators/compliance_runners/state_transition/builder_deposit_request/materializer.py new file mode 100644 index 00000000000..ad292507be3 --- /dev/null +++ b/tests/generators/compliance_runners/state_transition/builder_deposit_request/materializer.py @@ -0,0 +1,129 @@ +"""Materialize aspect-model solutions into process_builder_deposit_request cases. + +Realizes each applicable coverage dimension into a concrete pre / +BuilderDepositRequest / post vector (real BLS deposit signatures) and serializes +the solution. The operation never raises, so `post` is always present. + +Spec: specs/gloas/beacon-chain.md process_builder_deposit_request. +""" + +from __future__ import annotations + +from typing import Any, TYPE_CHECKING + +from eth_consensus_specs.test.helpers.genesis import create_genesis_state +from eth_consensus_specs.test.helpers.keys import builder_pubkey_to_privkey, builder_pubkeys +from eth_consensus_specs.utils import bls +from tests.generators.compliance_runners.state_transition.aspects_helpers.deposit_amount import ( + deposit_amount_from_profile, +) +from tests.generators.compliance_runners.state_transition.aspects_helpers.withdrawal_credential import ( + withdrawal_credentials_from_profile, +) +from tests.generators.compliance_runners.state_transition.materializer import Materializer + +if TYPE_CHECKING: + from tests.generators.compliance_runners.gen_base.gen_typing import TestCasePart + +REQUEST_PUBKEY = builder_pubkeys[0] +WRONG_PUBKEY = builder_pubkeys[1] +EPOCHS_PAST_GENESIS = 10 + +_DIMS = [ + "withdrawal_credentials_profile", + "wc_is_builder_prefix", + "builder_pubkey_found", + "builder_signature_valid", + "amount_profile", + "amount_nonzero", + "builder_withdrawable_epoch_set", + "builder_balance_zero", + "reset_applies", + "builder_credited", + "outcome", +] + + +def _s(sol: Any, n: str) -> str: + return str(getattr(sol, n)) + + +def _b(sol: Any, n: str) -> bool: + return bool(getattr(sol, n)) + + +class BuilderDepositRequestMaterializer(Materializer): + runner_name = "operations" + handler_name = "builder_deposit_request" + + def _sign(self, request: Any, privkey: int) -> Any: + spec = self.spec + message = spec.DepositMessage( + pubkey=request.pubkey, + withdrawal_credentials=request.withdrawal_credentials, + amount=request.amount, + ) + root = spec.compute_signing_root(message, spec.compute_domain(spec.DOMAIN_BUILDER_DEPOSIT)) + return bls.Sign(privkey, root) + + def _base_state(self) -> Any: + spec = self.spec + state = create_genesis_state( + spec, + validator_balances=[spec.MAX_EFFECTIVE_BALANCE] * 64, + activation_threshold=spec.MAX_EFFECTIVE_BALANCE, + ) + state.builders = type(state.builders)() + state.slot = spec.Slot(EPOCHS_PAST_GENESIS * spec.SLOTS_PER_EPOCH) + return state + + def materialize_solution(self, sol: Any) -> tuple[dict, list[TestCasePart]]: + spec = self.spec + found = _b(sol, "builder_pubkey_found") + pre = self._base_state() + current_epoch = int(spec.get_current_epoch(pre)) + address_tail = spec.sha256(REQUEST_PUBKEY)[12:] + + if found: + wset = _s(sol, "builder_withdrawable_epoch_set") == "T" + bzero = _s(sol, "builder_balance_zero") == "T" + pre.builders.append( + spec.Builder( + pubkey=spec.BLSPubkey(REQUEST_PUBKEY), + version=spec.PAYLOAD_BUILDER_VERSION, + execution_address=spec.ExecutionAddress(address_tail), + balance=spec.Gwei(0) if bzero else spec.Gwei(spec.MIN_ACTIVATION_BALANCE), + deposit_epoch=spec.Epoch(0), + withdrawable_epoch=spec.Epoch(current_epoch) if wset else spec.FAR_FUTURE_EPOCH, + ) + ) + + credentials_profile = _s(sol, "withdrawal_credentials_profile") + wc = withdrawal_credentials_from_profile(spec, credentials_profile, address_tail) + amount = deposit_amount_from_profile(spec, _s(sol, "amount_profile")) + + request = spec.BuilderDepositRequest( + pubkey=spec.BLSPubkey(REQUEST_PUBKEY), + withdrawal_credentials=spec.Bytes32(wc), + amount=spec.Gwei(amount), + ) + signer = REQUEST_PUBKEY if _s(sol, "builder_signature_valid") == "T" else WRONG_PUBKEY + request.signature = self._sign(request, builder_pubkey_to_privkey[signer]) + + post = pre.copy() + spec.process_builder_deposit_request(post, request) # never raises + + parts = [ + ("pre", "ssz", pre.encode_bytes()), + ("builder_deposit_request", "ssz", request.encode_bytes()), + ("post", "ssz", post.encode_bytes()), + ] + claimed = { + n: (_b(sol, n) if isinstance(getattr(sol, n), bool) else _s(sol, n)) for n in _DIMS + } + meta = { + "description": f"process_builder_deposit_request: {claimed['outcome']}", + "bls_setting": 1, + "claimed": claimed, + } + return meta, parts diff --git a/tests/generators/compliance_runners/state_transition/builder_deposit_request/models/handler_builder_deposit_request.mzn b/tests/generators/compliance_runners/state_transition/builder_deposit_request/models/handler_builder_deposit_request.mzn new file mode 100644 index 00000000000..69b9f793fe8 --- /dev/null +++ b/tests/generators/compliance_runners/state_transition/builder_deposit_request/models/handler_builder_deposit_request.mzn @@ -0,0 +1,47 @@ +% Handler model: process_builder_deposit_request. +% +% Reuses the SHARED aspects builder_membership and signed_message (the same +% signature aspect execution_payload_bid uses) plus withdrawal_credential, +% deposit_amount, and builder_reset. No solve item; a coverage driver solves. +% +% Spec: specs/gloas/beacon-chain.md process_builder_deposit_request. + +include "../../aspects/withdrawal_credential.mzn"; +include "../../aspects/builder_membership.mzn"; +include "../../aspects/signed_message.mzn"; % shared with execution_payload_bid +include "../../aspects/deposit_amount.mzn"; +include "../../aspects/builder_reset.mzn"; + +% ---- Signature instance (parameterized signed_message aspect) --------------- +% The deposit signature is a pure function of the request, so it is recoverable +% (applicable) regardless of path — reached only on the new-builder path. +var BOOLV_NA: builder_signature_valid; +constraint signed_message_ok(builder_signature_valid, true); + +% The reset-condition dimensions are recoverable when a builder is resolved. +constraint builder_reset_applicable <-> builder_pubkey_found; + +% ---- Outcome (spec branch order) -------------------------------------------- +enum Outcome = { + IGNORED_BAD_PREFIX, + IGNORED_BAD_SIGNATURE, + ADDED_NEW_BUILDER, + TOPPED_UP, + TOPPED_UP_AFTER_RESET +}; + +var Outcome: outcome; +constraint outcome = + if not wc_is_builder_prefix then + IGNORED_BAD_PREFIX + elseif not builder_pubkey_found then + (if builder_signature_valid == T then ADDED_NEW_BUILDER else IGNORED_BAD_SIGNATURE endif) + else + (if reset_applies then TOPPED_UP_AFTER_RESET else TOPPED_UP endif) + endif; + +% ---- Effect ----------------------------------------------------------------- +% Declared-and-constrained so the solver exposes it (see TEST_METHODOLOGY.md). +var bool: builder_credited; +constraint builder_credited <-> + (outcome in {ADDED_NEW_BUILDER, TOPPED_UP, TOPPED_UP_AFTER_RESET}); diff --git a/tests/generators/compliance_runners/state_transition/builder_deposit_request/validation.py b/tests/generators/compliance_runners/state_transition/builder_deposit_request/validation.py new file mode 100644 index 00000000000..b9312c6fbcd --- /dev/null +++ b/tests/generators/compliance_runners/state_transition/builder_deposit_request/validation.py @@ -0,0 +1,81 @@ +"""Independent validation of process_builder_deposit_request vectors. + +Recovers every applicable coverage dimension from the decoded pre state and +BuilderDepositRequest via the real spec predicates, recomputes the outcome, and +Imports neither the materializer nor the model. +""" + +from __future__ import annotations + +from typing import Any, TYPE_CHECKING + +from ruamel.yaml import YAML + +from eth_consensus_specs.gloas import minimal as spec +from tests.generators.compliance_runners.state_transition.aspects_helpers.deposit_amount import ( + deposit_amount_profile, +) +from tests.generators.compliance_runners.state_transition.aspects_helpers.withdrawal_credential import ( + withdrawal_credentials_profile, +) +from tests.generators.compliance_runners.state_transition.validation import check_dimensions, decode + +if TYPE_CHECKING: + from pathlib import Path + + from tests.generators.compliance_runners.state_transition.validation import Check + +_YAML = YAML(typ="safe") +_ACCEPT = {"ADDED_NEW_BUILDER", "TOPPED_UP", "TOPPED_UP_AFTER_RESET"} + + +def _tri(x: bool) -> str: + return "T" if x else "F" + + +def recover(pre: Any, request: Any) -> dict[str, Any]: + pubkeys = [b.pubkey for b in pre.builders] + found = request.pubkey in pubkeys + credential_profile = withdrawal_credentials_profile(spec, request.withdrawal_credentials) + r: dict[str, Any] = { + "withdrawal_credentials_profile": credential_profile, + "wc_is_builder_prefix": bool( + spec.is_builder_withdrawal_credential(request.withdrawal_credentials) + ), + "builder_pubkey_found": found, + "builder_signature_valid": _tri(bool(spec.is_valid_builder_deposit_signature(request))), + "amount_profile": deposit_amount_profile(spec, request.amount), + "amount_nonzero": int(request.amount) > 0, + } + + if found: + b = pre.builders[pubkeys.index(request.pubkey)] + wset = b.withdrawable_epoch != spec.FAR_FUTURE_EPOCH + bzero = int(b.balance) == 0 + r["builder_withdrawable_epoch_set"] = _tri(wset) + r["builder_balance_zero"] = _tri(bzero) + r["reset_applies"] = bool(wset and bzero) + else: + r["builder_withdrawable_epoch_set"] = "NA" + r["builder_balance_zero"] = "NA" + r["reset_applies"] = False + + if not r["wc_is_builder_prefix"]: + outcome = "IGNORED_BAD_PREFIX" + elif not found: + outcome = ( + "ADDED_NEW_BUILDER" if r["builder_signature_valid"] == "T" else "IGNORED_BAD_SIGNATURE" + ) + else: + outcome = "TOPPED_UP_AFTER_RESET" if r["reset_applies"] else "TOPPED_UP" + r["outcome"] = outcome + r["builder_credited"] = outcome in _ACCEPT + return r + + +def validate_case(case_dir: Path) -> list[Check]: + pre = decode(case_dir / "pre.ssz_snappy", spec.BeaconState) + request = decode(case_dir / "builder_deposit_request.ssz_snappy", spec.BuilderDepositRequest) + claimed = _YAML.load((case_dir / "dimensions.yaml").read_text())["claimed"] + actual = recover(pre, request) + return check_dimensions(claimed, actual) diff --git a/tests/generators/compliance_runners/state_transition/builder_exit_request/__init__.py b/tests/generators/compliance_runners/state_transition/builder_exit_request/__init__.py new file mode 100644 index 00000000000..fad1144dbdb --- /dev/null +++ b/tests/generators/compliance_runners/state_transition/builder_exit_request/__init__.py @@ -0,0 +1,7 @@ +from .coverage import build_profile +from .materializer import BuilderExitRequestMaterializer +from .validation import validate_case + +MATERIALIZER = BuilderExitRequestMaterializer + +__all__ = ("MATERIALIZER", "build_profile", "validate_case") diff --git a/tests/generators/compliance_runners/state_transition/builder_exit_request/coverage.py b/tests/generators/compliance_runners/state_transition/builder_exit_request/coverage.py new file mode 100644 index 00000000000..451675a097e --- /dev/null +++ b/tests/generators/compliance_runners/state_transition/builder_exit_request/coverage.py @@ -0,0 +1,50 @@ +"""Coverage profiles for process_builder_exit_request. + +Handler-specific instantiation of the shared ``..aspect_coverage`` engine — +the SAME engine execution_payload_bid uses. Two of the aspects +(builder_lifecycle, builder_pending_balance) are the shared aspect files bound +by both handlers. + +Run: + uv run python -m ...builder_exit_request.coverage # summary + uv run python -m ...builder_exit_request.coverage standard --materialize +""" + +from __future__ import annotations + +from pathlib import Path + +from tests.generators.compliance_runners.state_transition.aspect_coverage import ( + build_profile as _build_profile, + enumerate_signatures, +) + +from .materializer import _DIMS + +INPUT_ASPECTS = { + "builder_membership": ["builder_pubkey_found"], + "builder_lifecycle": ["builder_deposit_to_finalized_epoch", "builder_withdrawable_epoch_set"], + "builder_pending_balance": ["builder_has_pending_withdrawal", "builder_has_pending_payment"], + "source_authorization": ["source_address_matches"], +} +OUTCOME_ASPECT = {"outcome": ["outcome"]} +ALL_ASPECTS = {**INPUT_ASPECTS, **OUTCOME_ASPECT} +MODEL = Path(__file__).parent / "models" / "handler_builder_exit_request.mzn" + + +def _nfaults(r: dict) -> int: + if not r["builder_pubkey_found"]: + return 1 + f = 0 + f += not r["builder_active"] + f += r["source_address_matches"] != "T" + f += r["builder_has_pending_balance"] + return int(f) + + +def build_profile(name): + return _build_profile(_recs(), name, ALL_ASPECTS, INPUT_ASPECTS, OUTCOME_ASPECT) + + +def _recs(): + return enumerate_signatures(MODEL, _DIMS, ALL_ASPECTS, _nfaults) diff --git a/tests/generators/compliance_runners/state_transition/builder_exit_request/materializer.py b/tests/generators/compliance_runners/state_transition/builder_exit_request/materializer.py new file mode 100644 index 00000000000..8f64aa1d93b --- /dev/null +++ b/tests/generators/compliance_runners/state_transition/builder_exit_request/materializer.py @@ -0,0 +1,134 @@ +"""Materialize aspect-model solutions into process_builder_exit_request cases. + +Consumes solution-like objects (from `coverage.py`), realizes each applicable +coverage dimension into a concrete pre / BuilderExitRequest / post vector, and +serializes the solution to dimensions.yaml. This operation never raises, so +`post` is always present (a no-op leaves it unchanged). + +Spec: specs/gloas/beacon-chain.md process_builder_exit_request. +""" + +from __future__ import annotations + +from typing import Any, TYPE_CHECKING + +from eth_consensus_specs.test.helpers.genesis import create_genesis_state +from eth_consensus_specs.test.helpers.keys import builder_pubkeys +from tests.generators.compliance_runners.state_transition.materializer import Materializer + +if TYPE_CHECKING: + from tests.generators.compliance_runners.gen_base.gen_typing import TestCasePart + +REQUEST_PUBKEY = builder_pubkeys[0] +BUILDER_ADDRESS = b"\x22" * 20 +OTHER_ADDRESS = b"\x33" * 20 +FINALIZED_EPOCH = 5 +EPOCHS_PAST_GENESIS = 10 + +_DIMS = [ + "builder_pubkey_found", + "builder_deposit_to_finalized_epoch", + "builder_withdrawable_epoch_set", + "builder_has_pending_withdrawal", + "builder_has_pending_payment", + "source_address_matches", + "builder_active", + "builder_has_pending_balance", + "exit_initiated", + "outcome", +] + + +def _s(sol: Any, n: str) -> str: + return str(getattr(sol, n)) + + +def _b(sol: Any, n: str) -> bool: + return bool(getattr(sol, n)) + + +class BuilderExitRequestMaterializer(Materializer): + runner_name = "operations" + handler_name = "builder_exit_request" + + def _base_state(self) -> Any: + spec = self.spec + state = create_genesis_state( + spec, + validator_balances=[spec.MAX_EFFECTIVE_BALANCE] * 64, + activation_threshold=spec.MAX_EFFECTIVE_BALANCE, + ) + state.builders = type(state.builders)() + state.slot = spec.Slot(EPOCHS_PAST_GENESIS * spec.SLOTS_PER_EPOCH) + state.finalized_checkpoint = spec.Checkpoint( + epoch=spec.Epoch(FINALIZED_EPOCH), root=spec.Root(b"\x01" * 32) + ) + return state + + def materialize_solution(self, sol: Any) -> tuple[dict, list[TestCasePart]]: + spec = self.spec + found = _b(sol, "builder_pubkey_found") + pre = self._base_state() + current_epoch = int(spec.get_current_epoch(pre)) + + if found: + dep = _s(sol, "builder_deposit_to_finalized_epoch") + deposit_epoch = { + "LT": FINALIZED_EPOCH - 1, + "EQ": FINALIZED_EPOCH, + "GT": FINALIZED_EPOCH + 1, + }[dep] + wset = _s(sol, "builder_withdrawable_epoch_set") == "T" + pre.builders.append( + spec.Builder( + pubkey=spec.BLSPubkey(REQUEST_PUBKEY), + version=spec.PAYLOAD_BUILDER_VERSION, + execution_address=spec.ExecutionAddress(BUILDER_ADDRESS), + balance=spec.Gwei(spec.MIN_ACTIVATION_BALANCE), + deposit_epoch=spec.Epoch(deposit_epoch), + withdrawable_epoch=spec.Epoch(current_epoch) if wset else spec.FAR_FUTURE_EPOCH, + ) + ) + if _s(sol, "builder_has_pending_withdrawal") == "T": + pre.builder_pending_withdrawals.append( + spec.BuilderPendingWithdrawal( + fee_recipient=spec.ExecutionAddress(BUILDER_ADDRESS), + amount=spec.Gwei(1), + builder_index=spec.BuilderIndex(0), + ) + ) + if _s(sol, "builder_has_pending_payment") == "T": + pre.builder_pending_payments[0] = spec.BuilderPendingPayment( + weight=spec.Gwei(1), + withdrawal=spec.BuilderPendingWithdrawal( + fee_recipient=spec.ExecutionAddress(BUILDER_ADDRESS), + amount=spec.Gwei(1), + builder_index=spec.BuilderIndex(0), + ), + proposer_index=spec.ValidatorIndex(0), + ) + matches = _s(sol, "source_address_matches") == "T" + source_address = BUILDER_ADDRESS if matches else OTHER_ADDRESS + else: + source_address = BUILDER_ADDRESS # arbitrary; pubkey absent from registry + + request = spec.BuilderExitRequest( + source_address=spec.ExecutionAddress(source_address), + pubkey=spec.BLSPubkey(REQUEST_PUBKEY), + ) + post = pre.copy() + spec.process_builder_exit_request(post, request) # never raises + + claimed = { + n: (_b(sol, n) if isinstance(getattr(sol, n), bool) else _s(sol, n)) for n in _DIMS + } + meta = { + "description": f"process_builder_exit_request: {claimed['outcome']}", + "claimed": claimed, + } + parts = [ + ("pre", "ssz", pre.encode_bytes()), + ("builder_exit_request", "ssz", request.encode_bytes()), + ("post", "ssz", post.encode_bytes()), + ] + return meta, parts diff --git a/tests/generators/compliance_runners/state_transition/builder_exit_request/models/handler_builder_exit_request.mzn b/tests/generators/compliance_runners/state_transition/builder_exit_request/models/handler_builder_exit_request.mzn new file mode 100644 index 00000000000..ff602873fdd --- /dev/null +++ b/tests/generators/compliance_runners/state_transition/builder_exit_request/models/handler_builder_exit_request.mzn @@ -0,0 +1,73 @@ +% Handler model: process_builder_exit_request. +% +% Reuses the SHARED realization aspects builder_lifecycle (is_active_builder) and +% builder_pending_balance (get_pending_balance_to_withdraw_for_builder) — the +% same aspect files bound by execution_payload_bid — plus builder_membership and +% source_authorization. No solve item; a coverage driver solves. +% +% Spec: specs/gloas/beacon-chain.md process_builder_exit_request. + +include "../../aspects/builder_membership.mzn"; +include "../../aspects/builder_lifecycle.mzn"; % shared with execution_payload_bid +include "../../aspects/builder_pending_balance.mzn"; % shared with execution_payload_bid +include "../../aspects/source_authorization.mzn"; + +% ---- Builder instance (parameterized aspects applied to one builder) -------- +var CMP_NA: builder_deposit_to_finalized_epoch; +var BOOLV_NA: builder_withdrawable_epoch_set; +constraint builder_lifecycle_ok(builder_deposit_to_finalized_epoch, + builder_withdrawable_epoch_set, builder_pubkey_found); +var bool: builder_active; +constraint builder_active <-> + builder_is_active(builder_deposit_to_finalized_epoch, builder_withdrawable_epoch_set); + +var BOOLV_NA: builder_has_pending_withdrawal; +var BOOLV_NA: builder_has_pending_payment; +constraint builder_pending_ok(builder_has_pending_withdrawal, builder_has_pending_payment, + builder_pubkey_found); +var bool: builder_has_pending_balance; +constraint builder_has_pending_balance <-> + builder_has_pending(builder_has_pending_withdrawal, builder_has_pending_payment); + +constraint source_authorization_applicable <-> builder_pubkey_found; + +% Well-formedness: a builder holds pending balance only while active. +constraint builder_has_pending_balance -> builder_active; + +% ---- Gate passes (spec order) ----------------------------------------------- +var bool: g_found = builder_pubkey_found; +var bool: g_active = builder_active; +var bool: g_addr = source_address_matches == T; +var bool: g_no_pending = not builder_has_pending_balance; + +% ---- Outcome (first-failing gate) ------------------------------------------- +enum Outcome = { + EXIT_INITIATED, + IGNORED_PUBKEY_NOT_FOUND, + IGNORED_NOT_ACTIVE, + IGNORED_ADDRESS_MISMATCH, + IGNORED_PENDING_NONZERO +}; + +var Outcome: outcome; +constraint outcome = + if not g_found then IGNORED_PUBKEY_NOT_FOUND + elseif not g_active then IGNORED_NOT_ACTIVE + elseif not g_addr then IGNORED_ADDRESS_MISMATCH + elseif not g_no_pending then IGNORED_PENDING_NONZERO + else EXIT_INITIATED + endif; + +% ---- Faults (applicable gate in its failing state) -------------------------- +var bool: fault_found = not g_found; +var bool: fault_active = builder_pubkey_found /\ not g_active; +var bool: fault_addr = builder_pubkey_found /\ not g_addr; +var bool: fault_pending = builder_pubkey_found /\ not g_no_pending; +var int: n_faults = + bool2int(fault_found) + bool2int(fault_active) + + bool2int(fault_addr) + bool2int(fault_pending); + +% ---- Effect ----------------------------------------------------------------- +% Declared-and-constrained (not `= expr`) so the solver exposes it in solutions. +var bool: exit_initiated; +constraint exit_initiated <-> (outcome == EXIT_INITIATED); diff --git a/tests/generators/compliance_runners/state_transition/builder_exit_request/validation.py b/tests/generators/compliance_runners/state_transition/builder_exit_request/validation.py new file mode 100644 index 00000000000..e5b5ee67d8b --- /dev/null +++ b/tests/generators/compliance_runners/state_transition/builder_exit_request/validation.py @@ -0,0 +1,93 @@ +"""Independent validation of process_builder_exit_request vectors. + +Recovers every applicable coverage dimension from the decoded pre state and +BuilderExitRequest via the real spec predicates, compares to the serialized +solution and recomputes the outcome. Imports neither the materializer nor the +model. +""" + +from __future__ import annotations + +from typing import Any, TYPE_CHECKING + +from ruamel.yaml import YAML + +from eth_consensus_specs.gloas import minimal as spec +from tests.generators.compliance_runners.state_transition.validation import check_dimensions, decode + +if TYPE_CHECKING: + from pathlib import Path + + from tests.generators.compliance_runners.state_transition.validation import Check + +_YAML = YAML(typ="safe") + + +def _tri(x: bool) -> str: + return "T" if x else "F" + + +def _cmp(a: int, b: int) -> str: + return "LT" if a < b else ("EQ" if a == b else "GT") + + +def recover(pre: Any, request: Any) -> dict[str, Any]: + pubkeys = [b.pubkey for b in pre.builders] + found = request.pubkey in pubkeys + r: dict[str, Any] = {"builder_pubkey_found": found} + + if found: + idx = spec.BuilderIndex(pubkeys.index(request.pubkey)) + b = pre.builders[idx] + finalized = int(pre.finalized_checkpoint.epoch) + pending = int(spec.get_pending_balance_to_withdraw_for_builder(pre, idx)) + r["builder_deposit_to_finalized_epoch"] = _cmp(int(b.deposit_epoch), finalized) + r["builder_withdrawable_epoch_set"] = _tri(b.withdrawable_epoch != spec.FAR_FUTURE_EPOCH) + r["builder_has_pending_withdrawal"] = _tri( + any( + w.builder_index == idx and int(w.amount) > 0 + for w in pre.builder_pending_withdrawals + ) + ) + r["builder_has_pending_payment"] = _tri( + any( + p.withdrawal.builder_index == idx and int(p.withdrawal.amount) > 0 + for p in pre.builder_pending_payments + ) + ) + r["source_address_matches"] = _tri(b.execution_address == request.source_address) + r["builder_active"] = bool(spec.is_active_builder(pre, idx)) + r["builder_has_pending_balance"] = pending != 0 + else: + for n in ( + "builder_deposit_to_finalized_epoch", + "builder_withdrawable_epoch_set", + "builder_has_pending_withdrawal", + "builder_has_pending_payment", + "source_address_matches", + ): + r[n] = "NA" + r["builder_active"] = False + r["builder_has_pending_balance"] = False + + if not r["builder_pubkey_found"]: + outcome = "IGNORED_PUBKEY_NOT_FOUND" + elif not r["builder_active"]: + outcome = "IGNORED_NOT_ACTIVE" + elif r["source_address_matches"] != "T": + outcome = "IGNORED_ADDRESS_MISMATCH" + elif r["builder_has_pending_balance"]: + outcome = "IGNORED_PENDING_NONZERO" + else: + outcome = "EXIT_INITIATED" + r["outcome"] = outcome + r["exit_initiated"] = outcome == "EXIT_INITIATED" + return r + + +def validate_case(case_dir: Path) -> list[Check]: + pre = decode(case_dir / "pre.ssz_snappy", spec.BeaconState) + request = decode(case_dir / "builder_exit_request.ssz_snappy", spec.BuilderExitRequest) + claimed = _YAML.load((case_dir / "dimensions.yaml").read_text())["claimed"] + actual = recover(pre, request) + return check_dimensions(claimed, actual) diff --git a/tests/generators/compliance_runners/state_transition/builder_pending_payments/__init__.py b/tests/generators/compliance_runners/state_transition/builder_pending_payments/__init__.py new file mode 100644 index 00000000000..3e5bfa1532f --- /dev/null +++ b/tests/generators/compliance_runners/state_transition/builder_pending_payments/__init__.py @@ -0,0 +1,9 @@ +"""Compliance generator for ``process_builder_pending_payments``.""" + +from .coverage import build_profile +from .materializer import BuilderPendingPaymentsMaterializer +from .validation import validate_case + +MATERIALIZER = BuilderPendingPaymentsMaterializer + +__all__ = ("MATERIALIZER", "build_profile", "validate_case") diff --git a/tests/generators/compliance_runners/state_transition/builder_pending_payments/coverage.py b/tests/generators/compliance_runners/state_transition/builder_pending_payments/coverage.py new file mode 100644 index 00000000000..7e7ec92ca79 --- /dev/null +++ b/tests/generators/compliance_runners/state_transition/builder_pending_payments/coverage.py @@ -0,0 +1,32 @@ +from __future__ import annotations + +from pathlib import Path + +from tests.generators.compliance_runners.state_transition.aspect_coverage import ( + build_profile as _build_profile, + enumerate_signatures, +) + +from .materializer import _DIMS + +MODEL = Path(__file__).parent / "models" / "handler_builder_pending_payments.mzn" +ASPECTS = { + "previous_section": ["previous_epoch_occupancy", "mixed_quorum_relations"], + "quorum": ["target_weight_to_quorum", "qualifying_payment_count"], + "withdrawal": ["target_amount_nonzero"], + "retained_section": ["next_epoch_payments_nondefault"], + "existing_output": ["preexisting_withdrawals_nonempty"], + "effects": ["withdrawals_appended", "state_effected", "outcome"], +} + + +def _recs(): + return enumerate_signatures(MODEL, _DIMS, ASPECTS, _nfaults) + + +def _nfaults(_r: dict) -> int: + return 0 + + +def build_profile(name): + return _build_profile(_recs(), name, ASPECTS, ASPECTS, {"outcome": ["outcome"]}) diff --git a/tests/generators/compliance_runners/state_transition/builder_pending_payments/materializer.py b/tests/generators/compliance_runners/state_transition/builder_pending_payments/materializer.py new file mode 100644 index 00000000000..6f2467dd601 --- /dev/null +++ b/tests/generators/compliance_runners/state_transition/builder_pending_payments/materializer.py @@ -0,0 +1,91 @@ +from __future__ import annotations + +from typing import TYPE_CHECKING + +from eth_consensus_specs.test.helpers.genesis import create_genesis_state +from tests.generators.compliance_runners.state_transition.materializer import Materializer + +if TYPE_CHECKING: + from tests.generators.compliance_runners.gen_base.gen_typing import TestCasePart + +_DIMS = [ + "previous_epoch_occupancy", + "target_weight_to_quorum", + "target_amount_nonzero", + "qualifying_payment_count", + "mixed_quorum_relations", + "next_epoch_payments_nondefault", + "preexisting_withdrawals_nonempty", + "withdrawals_appended", + "previous_epoch_discarded", + "next_epoch_shifted_forward", + "new_tail_defaulted", + "outcome", + "state_effected", +] + + +class BuilderPendingPaymentsMaterializer(Materializer): + runner_name = "epoch_processing" + handler_name = "builder_pending_payments" + + def materialize_solution(self, sol) -> tuple[dict, list[TestCasePart]]: + s = self.spec + pre = create_genesis_state( + s, + validator_balances=[s.MAX_EFFECTIVE_BALANCE] * 64, + activation_threshold=s.MAX_EFFECTIVE_BALANCE, + ) + s.process_slots(pre, s.Slot(s.SLOTS_PER_EPOCH - 1)) + q = s.get_builder_payment_quorum_threshold(pre) + assert q > 0 + spe = int(s.SLOTS_PER_EPOCH) + + def payment(slot, weight, amount): + return s.BuilderPendingPayment( + weight=s.Gwei(weight), + withdrawal=s.BuilderPendingWithdrawal( + fee_recipient=s.ExecutionAddress(bytes([slot + 1]) * 20), + amount=s.Gwei(amount), + builder_index=s.BuilderIndex(slot + 10), + ), + proposer_index=s.ValidatorIndex(slot + 20), + ) + + rel = str(sol.target_weight_to_quorum) + weight = {"LT": q - 1, "EQ": q, "GT": q + 1}.get(rel, 0) + amount = 0 if str(sol.target_amount_nonzero) == "F" else 100 + occ = str(sol.previous_epoch_occupancy) + count = str(sol.qualifying_payment_count) + if occ == "SINGLE": + pre.builder_pending_payments[0] = payment(0, weight, amount) + elif occ == "MULTIPLE": + if bool(sol.mixed_quorum_relations): + for i, w in enumerate((q - 1, q, q + 1)): + pre.builder_pending_payments[i] = payment(i, w, amount + i) + else: + qualifiers = {"ZERO": 0, "ONE": 1, "MULTIPLE_COUNT": 2}[count] + ws = [weight] + ws.extend([q] * max(0, qualifiers - int(weight >= q))) + ws.extend([q if count == "MULTIPLE_COUNT" else q - 1] * (3 - len(ws))) + for i, w in enumerate(ws): + pre.builder_pending_payments[i] = payment(i, w, amount + i) + if bool(sol.next_epoch_payments_nondefault): + pre.builder_pending_payments[spe] = payment(7, q + 1, 77) + pre.builder_pending_payments[spe + 1] = payment(8, q - 1, 88) + if bool(sol.preexisting_withdrawals_nonempty): + pre.builder_pending_withdrawals.append( + s.BuilderPendingWithdrawal( + fee_recipient=s.ExecutionAddress(b"\xaa" * 20), + amount=s.Gwei(99), + builder_index=s.BuilderIndex(99), + ) + ) + post = pre.copy() + s.process_builder_pending_payments(post) + claimed = { + n: (bool(v) if isinstance(v := getattr(sol, n), bool) else str(v)) for n in _DIMS + } + meta = {"description": "process_builder_pending_payments", "claimed": claimed} + parts = [("pre", "ssz", pre.encode_bytes()), ("post", "ssz", post.encode_bytes())] + return meta, parts diff --git a/tests/generators/compliance_runners/state_transition/builder_pending_payments/models/handler_builder_pending_payments.mzn b/tests/generators/compliance_runners/state_transition/builder_pending_payments/models/handler_builder_pending_payments.mzn new file mode 100644 index 00000000000..27785b2ced3 --- /dev/null +++ b/tests/generators/compliance_runners/state_transition/builder_pending_payments/models/handler_builder_pending_payments.mzn @@ -0,0 +1,33 @@ +include "../../aspects/base.mzn"; +include "../../aspects/builder_payment_quorum.mzn"; +enum Occupancy = { EMPTY, SINGLE, MULTIPLE }; +enum Count = { ZERO, ONE, MULTIPLE_COUNT }; +enum Outcome = { NO_STATE_CHANGE, ROTATED_ONLY, APPENDED_ONE_AND_ROTATED, APPENDED_MULTIPLE_AND_ROTATED }; +var Occupancy: previous_epoch_occupancy; +var Dim: target_weight_to_quorum; +var BOOLV_NA: target_amount_nonzero; +var Count: qualifying_payment_count; +var bool: mixed_quorum_relations; +var bool: next_epoch_payments_nondefault; +var bool: preexisting_withdrawals_nonempty; +var Count: withdrawals_appended; +var bool: previous_epoch_discarded; +var bool: next_epoch_shifted_forward; +var bool: new_tail_defaulted; +var Outcome: outcome; +var bool: state_effected; +constraint builder_payment_quorum_ok(target_weight_to_quorum, previous_epoch_occupancy != EMPTY); +constraint (target_amount_nonzero == NA) <-> previous_epoch_occupancy == EMPTY; +constraint (previous_epoch_occupancy == EMPTY) -> (qualifying_payment_count == ZERO /\ mixed_quorum_relations == false); +constraint (previous_epoch_occupancy == SINGLE) -> (qualifying_payment_count in {ZERO, ONE} /\ mixed_quorum_relations == false); +constraint (previous_epoch_occupancy == SINGLE /\ target_weight_to_quorum == LT) -> qualifying_payment_count == ZERO; +constraint (previous_epoch_occupancy == SINGLE /\ target_weight_to_quorum in {EQ, GT}) -> qualifying_payment_count == ONE; +constraint mixed_quorum_relations -> (previous_epoch_occupancy == MULTIPLE /\ qualifying_payment_count == MULTIPLE_COUNT /\ target_weight_to_quorum == LT); +constraint (previous_epoch_occupancy == MULTIPLE /\ target_weight_to_quorum in {EQ, GT}) -> qualifying_payment_count in {ONE, MULTIPLE_COUNT}; +constraint (withdrawals_appended == qualifying_payment_count); +constraint previous_epoch_discarded /\ next_epoch_shifted_forward /\ new_tail_defaulted; +constraint (previous_epoch_occupancy == EMPTY /\ not next_epoch_payments_nondefault) -> outcome == NO_STATE_CHANGE; +constraint (qualifying_payment_count == ZERO /\ (previous_epoch_occupancy != EMPTY \/ next_epoch_payments_nondefault)) -> outcome == ROTATED_ONLY; +constraint qualifying_payment_count == ONE -> outcome == APPENDED_ONE_AND_ROTATED; +constraint qualifying_payment_count == MULTIPLE_COUNT -> outcome == APPENDED_MULTIPLE_AND_ROTATED; +constraint state_effected <-> outcome != NO_STATE_CHANGE; diff --git a/tests/generators/compliance_runners/state_transition/builder_pending_payments/validation.py b/tests/generators/compliance_runners/state_transition/builder_pending_payments/validation.py new file mode 100644 index 00000000000..829e70c404b --- /dev/null +++ b/tests/generators/compliance_runners/state_transition/builder_pending_payments/validation.py @@ -0,0 +1,124 @@ +from __future__ import annotations + +from typing import TYPE_CHECKING + +from ruamel.yaml import YAML + +from eth_consensus_specs.gloas import minimal as spec +from tests.generators.compliance_runners.state_transition.validation import check_dimensions, decode + +if TYPE_CHECKING: + from pathlib import Path + + from tests.generators.compliance_runners.state_transition.validation import Check + +Y = YAML(typ="safe") + + +def validate_case(case_dir: Path) -> list[Check]: + pre = decode(case_dir / "pre.ssz_snappy", spec.BeaconState) + spe = int(spec.SLOTS_PER_EPOCH) + q = spec.get_builder_payment_quorum_threshold(pre) + claimed = Y.load((case_dir / "dimensions.yaml").read_text())["claimed"] + + appended = [p.withdrawal for p in pre.builder_pending_payments[:spe] if p.weight >= q] + payments = list(pre.builder_pending_payments[spe:]) + [ + spec.BuilderPendingPayment() for _ in range(spe) + ] + withdrawals = list(pre.builder_pending_withdrawals) + appended + + expected = pre.copy() + expected.builder_pending_payments = spec.BuilderPendingPayments(data=payments) + expected.builder_pending_withdrawals = spec.BuilderPendingWithdrawals(data=withdrawals) + + first = list(pre.builder_pending_payments[:spe]) + occupied = [p for p in first if p != spec.BuilderPendingPayment()] + + relation = "NA" + if occupied: + if occupied[0].weight < q: + relation = "LT" + elif occupied[0].weight == q: + relation = "EQ" + else: + relation = "GT" + + if not occupied: + previous_epoch_occupancy = "EMPTY" + elif len(occupied) == 1: + previous_epoch_occupancy = "SINGLE" + else: + previous_epoch_occupancy = "MULTIPLE" + + if not occupied: + target_amount_nonzero = "NA" + elif occupied[0].withdrawal.amount: + target_amount_nonzero = "T" + else: + target_amount_nonzero = "F" + + if not appended: + qualifying_payment_count = "ZERO" + elif len(appended) == 1: + qualifying_payment_count = "ONE" + else: + qualifying_payment_count = "MULTIPLE_COUNT" + + quorum_relations = set() + for payment in occupied: + if payment.weight < q: + quorum_relations.add("LT") + elif payment.weight == q: + quorum_relations.add("EQ") + else: + quorum_relations.add("GT") + mixed_quorum_relations = {"LT", "EQ", "GT"}.issubset(quorum_relations) + + next_epoch_payments_nondefault = any( + p != spec.BuilderPendingPayment() for p in pre.builder_pending_payments[spe:] + ) + + preexisting_withdrawals_nonempty = bool(pre.builder_pending_withdrawals) + + if not appended: + withdrawals_appended = "ZERO" + elif len(appended) == 1: + withdrawals_appended = "ONE" + else: + withdrawals_appended = "MULTIPLE_COUNT" + + previous_epoch_discarded = all(p == spec.BuilderPendingPayment() for p in payments[spe:]) + + next_epoch_shifted_forward = list(payments[:spe]) == list(pre.builder_pending_payments[spe:]) + + new_tail_defaulted = all(p == spec.BuilderPendingPayment() for p in payments[spe:]) + + if not occupied and not any( + p != spec.BuilderPendingPayment() for p in pre.builder_pending_payments[spe:] + ): + outcome = "NO_STATE_CHANGE" + elif not appended: + outcome = "ROTATED_ONLY" + elif len(appended) == 1: + outcome = "APPENDED_ONE_AND_ROTATED" + else: + outcome = "APPENDED_MULTIPLE_AND_ROTATED" + + state_effected = expected.hash_tree_root() != pre.hash_tree_root() + + actual = { + "previous_epoch_occupancy": previous_epoch_occupancy, + "target_weight_to_quorum": relation, + "target_amount_nonzero": target_amount_nonzero, + "qualifying_payment_count": qualifying_payment_count, + "mixed_quorum_relations": mixed_quorum_relations, + "next_epoch_payments_nondefault": next_epoch_payments_nondefault, + "preexisting_withdrawals_nonempty": preexisting_withdrawals_nonempty, + "withdrawals_appended": withdrawals_appended, + "previous_epoch_discarded": previous_epoch_discarded, + "next_epoch_shifted_forward": next_epoch_shifted_forward, + "new_tail_defaulted": new_tail_defaulted, + "outcome": outcome, + "state_effected": state_effected, + } + return check_dimensions(claimed, actual) diff --git a/tests/generators/compliance_runners/state_transition/conftest.py b/tests/generators/compliance_runners/state_transition/conftest.py new file mode 100644 index 00000000000..fd8b615020f --- /dev/null +++ b/tests/generators/compliance_runners/state_transition/conftest.py @@ -0,0 +1,48 @@ +from __future__ import annotations + +from pathlib import Path + +import pytest +from tests.generators.compliance_runners.state_transition.catalog import HANDLERS + +from tests.generators.compliance_runners.state_transition.run import PROFILES + + +def pytest_addoption(parser): + parser.addoption( + "--comptests-output", + type=Path, + default=None, + help="Output directory for generated compliance tests", + ) + parser.addoption( + "--handler", + choices=(*HANDLERS, "all"), + default="all", + help="State-transition handler to generate", + ) + parser.addoption( + "--profile", + choices=PROFILES, + default="standard", + help="State-transition coverage profile", + ) + + +@pytest.fixture +def comptests_output(request) -> Path | None: + return request.config.getoption("--comptests-output") + + +def pytest_generate_tests(metafunc): + if "handler" not in metafunc.fixturenames: + return + + selected_handler = metafunc.config.getoption("--handler") + handlers = HANDLERS if selected_handler == "all" else (selected_handler,) + metafunc.parametrize("handler", handlers, ids=handlers) + + +@pytest.fixture +def profile(request) -> str: + return request.config.getoption("--profile") diff --git a/tests/generators/compliance_runners/state_transition/consolidation_request/__init__.py b/tests/generators/compliance_runners/state_transition/consolidation_request/__init__.py new file mode 100644 index 00000000000..db79eaf848b --- /dev/null +++ b/tests/generators/compliance_runners/state_transition/consolidation_request/__init__.py @@ -0,0 +1,7 @@ +from .coverage import build_profile +from .materializer import ConsolidationRequestMaterializer +from .validation import validate_case + +MATERIALIZER = ConsolidationRequestMaterializer + +__all__ = ("MATERIALIZER", "build_profile", "validate_case") diff --git a/tests/generators/compliance_runners/state_transition/consolidation_request/coverage.py b/tests/generators/compliance_runners/state_transition/consolidation_request/coverage.py new file mode 100644 index 00000000000..b370ff1aea3 --- /dev/null +++ b/tests/generators/compliance_runners/state_transition/consolidation_request/coverage.py @@ -0,0 +1,95 @@ +"""Coverage profiles for process_consolidation_request. + +Handler-specific instantiation of the shared ``..aspect_coverage`` engine. +Reuses the validator family for the SOURCE validator + source_authorization, and +a compact target_validator aspect for the target. + +Run: + uv run python -m ...consolidation_request.coverage + uv run python -m ...consolidation_request.coverage standard --materialize +""" + +from __future__ import annotations + +from pathlib import Path + +from tests.generators.compliance_runners.state_transition.aspect_coverage import ( + build_profile as _build_profile, + enumerate_signatures, +) + +from .materializer import _DIMS + +# Fine-grained input aspects remain part of the signature used by `all`; the +# normal/exceptional profiles use the composite validator_state factor. +FINE_INPUT_ASPECTS = { + "consolidation_pair": ["same_source_target"], + "pending_consolidations_capacity": ["pending_consolidations_full"], + "consolidation_churn": ["sufficient_consolidation_churn"], + "validator_membership": ["validator_pubkey_found"], + "validator_credential": ["validator_credential"], + "source_authorization": ["source_address_matches"], + "validator_lifecycle": ["validator_active", "validator_exiting", "validator_old_enough"], + "validator_pending_withdrawal": ["has_pending_partial_withdrawal"], + "target_validator": ["target_found", "target_credential", "target_active", "target_exiting"], +} +OUTCOME_ASPECT = {"outcome": ["outcome"]} +INPUT_ASPECTS = { + "consolidation_pair": ["same_source_target"], + "pending_consolidations_capacity": ["pending_consolidations_full"], + "consolidation_churn": ["sufficient_consolidation_churn"], + "validator_state": [ + "validator_pubkey_found", + "validator_credential", + "source_address_matches", + "validator_active", + "validator_exiting", + "validator_old_enough", + "has_pending_partial_withdrawal", + "target_found", + "target_credential", + "target_active", + "target_exiting", + ], +} +FINE_ALL_ASPECTS = {**FINE_INPUT_ASPECTS, **OUTCOME_ASPECT} +ALL_ASPECTS = {**INPUT_ASPECTS, **OUTCOME_ASPECT} +MODEL = Path(__file__).parent / "models" / "handler_consolidation_request.mzn" + + +def _nfaults(r: dict) -> int: + if r["same_source_target"]: + if not r["validator_pubkey_found"]: + return 1 + return sum( + ( + r["source_address_matches"] != "T", + r["validator_credential"] != "CRED_ETH1", + r["validator_active"] != "T", + r["validator_exiting"] == "T", + ) + ) + + faults = int(r["pending_consolidations_full"]) + int(not r["sufficient_consolidation_churn"]) + faults += int(not r["validator_pubkey_found"]) + faults += int(r["target_found"] != "T") + if r["validator_pubkey_found"]: + faults += int( + not (r["validator_has_execution_credential"] and r["source_address_matches"] == "T") + ) + faults += int(r["validator_active"] != "T") + faults += int(r["validator_exiting"] == "T") + faults += int(r["validator_old_enough"] != "T") + faults += int(r["has_pending_partial_withdrawal"] == "T") + faults += int(r["target_active"] != "T") if r["target_found"] == "T" else 0 + faults += int(r["target_exiting"] == "T") if r["target_found"] == "T" else 0 + faults += int(not r["target_has_compounding_credential"]) if r["target_found"] == "T" else 0 + return faults + + +def build_profile(name): + return _build_profile(_recs(), name, ALL_ASPECTS, INPUT_ASPECTS, OUTCOME_ASPECT) + + +def _recs(): + return enumerate_signatures(MODEL, _DIMS, FINE_ALL_ASPECTS, _nfaults) diff --git a/tests/generators/compliance_runners/state_transition/consolidation_request/materializer.py b/tests/generators/compliance_runners/state_transition/consolidation_request/materializer.py new file mode 100644 index 00000000000..9a80b2c4c44 --- /dev/null +++ b/tests/generators/compliance_runners/state_transition/consolidation_request/materializer.py @@ -0,0 +1,174 @@ +"""Materialize aspect-model solutions into process_consolidation_request cases. + +The most involved materializer: two validators (source + target), a churn gate +realized by sizing the active validator set (64 -> sufficient, 32 -> ==MIN, i.e. +insufficient), and two queue fills. No BLS. Never raises, so `post` is always +present. + +Spec: specs/electra/beacon-chain.md process_consolidation_request (inherited by gloas). +""" + +from __future__ import annotations + +from typing import Any, TYPE_CHECKING + +from eth_consensus_specs.test.helpers.genesis import create_genesis_state +from eth_consensus_specs.test.helpers.keys import pubkeys +from tests.generators.compliance_runners.state_transition.materializer import Materializer + +if TYPE_CHECKING: + from tests.generators.compliance_runners.gen_base.gen_typing import TestCasePart + +N_SUFFICIENT = 64 # get_consolidation_churn_limit > MIN_ACTIVATION_BALANCE +N_INSUFFICIENT = 32 # get_consolidation_churn_limit == MIN_ACTIVATION_BALANCE +SOURCE_INDEX = 0 +TARGET_INDEX = 1 +CURRENT_EPOCH = 70 +ADDRESS = b"\x22" * 20 +OTHER_ADDRESS = b"\x33" * 20 + +_SRC_PREFIX = {"CRED_BLS": b"\x00", "CRED_ETH1": b"\x01", "CRED_COMPOUNDING": b"\x02"} + +_DIMS = [ + "same_source_target", + "pending_consolidations_full", + "sufficient_consolidation_churn", + "validator_pubkey_found", + "validator_credential", + "source_address_matches", + "validator_active", + "validator_exiting", + "validator_old_enough", + "has_pending_partial_withdrawal", + "target_found", + "target_credential", + "target_active", + "target_exiting", + "validator_has_execution_credential", + "validator_has_compounding_credential", + "target_has_compounding_credential", + "outcome", + "state_effected", +] + + +def _s(sol: Any, n: str) -> str: + return str(getattr(sol, n)) + + +def _b(sol: Any, n: str) -> bool: + return bool(getattr(sol, n)) + + +class ConsolidationRequestMaterializer(Materializer): + runner_name = "operations" + handler_name = "consolidation_request" + + def _epochs(self, active: bool, exiting: bool, old_enough: bool) -> tuple[int, int]: + far = int(self.spec.FAR_FUTURE_EPOCH) + activation = 0 if old_enough else CURRENT_EPOCH - 10 + if active: + exit_epoch = (CURRENT_EPOCH + 10) if exiting else far + elif exiting: + exit_epoch = CURRENT_EPOCH - 1 + else: + activation, exit_epoch = CURRENT_EPOCH + 10, far + return activation, exit_epoch + + def _set_validator( + self, v: Any, prefix: bytes, active: bool, exiting: bool, old_enough: bool + ) -> None: + spec = self.spec + v.withdrawal_credentials = spec.Bytes32(prefix + b"\x00" * 11 + ADDRESS) + activation, exit_epoch = self._epochs(active, exiting, old_enough) + v.activation_epoch = spec.Epoch(activation) + v.exit_epoch = spec.Epoch(exit_epoch) + + def materialize_solution(self, sol: Any) -> tuple[dict, list[TestCasePart]]: + spec = self.spec + n = N_SUFFICIENT if _b(sol, "sufficient_consolidation_churn") else N_INSUFFICIENT + pre = create_genesis_state( + spec, + validator_balances=[spec.MAX_EFFECTIVE_BALANCE] * n, + activation_threshold=spec.MAX_EFFECTIVE_BALANCE, + ) + pre.slot = spec.Slot(CURRENT_EPOCH * spec.SLOTS_PER_EPOCH) + absent_source = pubkeys[n] + absent_target = pubkeys[n + 1] + + same = _b(sol, "same_source_target") + source_found = _b(sol, "validator_pubkey_found") + + # ---- source validator -------------------------------------------------- + if source_found: + self._set_validator( + pre.validators[SOURCE_INDEX], + _SRC_PREFIX[_s(sol, "validator_credential")], + _s(sol, "validator_active") == "T", + _s(sol, "validator_exiting") == "T", + _s(sol, "validator_old_enough") == "T", + ) + source_pubkey = pre.validators[SOURCE_INDEX].pubkey + source_address = ADDRESS if _s(sol, "source_address_matches") == "T" else OTHER_ADDRESS + else: + source_pubkey = absent_source + source_address = ADDRESS + + # ---- target validator (consolidation path only) ------------------------ + if same: + target_pubkey = source_pubkey + elif _s(sol, "target_found") == "T": + self._set_validator( + pre.validators[TARGET_INDEX], + _SRC_PREFIX[_s(sol, "target_credential")], + _s(sol, "target_active") == "T", + _s(sol, "target_exiting") == "T", + old_enough=True, + ) + target_pubkey = pre.validators[TARGET_INDEX].pubkey + else: + target_pubkey = absent_target + + # ---- source pending partial withdrawal --------------------------------- + if source_found and _s(sol, "has_pending_partial_withdrawal") == "T": + pre.pending_partial_withdrawals.append( + spec.PendingPartialWithdrawal( + validator_index=spec.ValidatorIndex(SOURCE_INDEX), + amount=spec.Gwei(1), + withdrawable_epoch=spec.Epoch(CURRENT_EPOCH), + ) + ) + + # ---- pending consolidations queue -------------------------------------- + if _b(sol, "pending_consolidations_full"): + pre.pending_consolidations = spec.PendingConsolidations( + data=[ + spec.PendingConsolidation( + source_index=spec.ValidatorIndex(2), + target_index=spec.ValidatorIndex(3), + ) + for _ in range(int(spec.PENDING_CONSOLIDATIONS_LIMIT)) + ] + ) + + request = spec.ConsolidationRequest( + source_address=spec.ExecutionAddress(source_address), + source_pubkey=spec.BLSPubkey(source_pubkey), + target_pubkey=spec.BLSPubkey(target_pubkey), + ) + post = pre.copy() + spec.process_consolidation_request(post, request) # never raises + + claimed = { + k: (_b(sol, k) if isinstance(getattr(sol, k), bool) else _s(sol, k)) for k in _DIMS + } + meta = { + "description": f"process_consolidation_request: {claimed['outcome']}", + "claimed": claimed, + } + parts = [ + ("pre", "ssz", pre.encode_bytes()), + ("consolidation_request", "ssz", request.encode_bytes()), + ("post", "ssz", post.encode_bytes()), + ] + return meta, parts diff --git a/tests/generators/compliance_runners/state_transition/consolidation_request/models/handler_consolidation_request.mzn b/tests/generators/compliance_runners/state_transition/consolidation_request/models/handler_consolidation_request.mzn new file mode 100644 index 00000000000..6bdfb94df4b --- /dev/null +++ b/tests/generators/compliance_runners/state_transition/consolidation_request/models/handler_consolidation_request.mzn @@ -0,0 +1,119 @@ +% Handler model: process_consolidation_request. +% +% Two paths: switch-to-compounding (source == target) and consolidation +% (source != target). The parameterized validator aspects (lifecycle / credential) +% are instantiated for BOTH the source and the target role — the same aspect +% predicates, applied twice. Seasoning + authorization + pending are source-only. +% +% Spec: specs/electra/beacon-chain.md process_consolidation_request (inherited by gloas). + +include "../../aspects/consolidation_pair.mzn"; +include "../../aspects/pending_consolidations_capacity.mzn"; +include "../../aspects/consolidation_churn.mzn"; +include "../../aspects/validator_membership.mzn"; % source membership (validator_pubkey_found) +include "../../aspects/validator_credential.mzn"; % parameterized (source + target) +include "../../aspects/validator_lifecycle.mzn"; % parameterized (source + target) +include "../../aspects/validator_seasoning.mzn"; % parameterized (source only) +include "../../aspects/source_authorization.mzn"; % shared with builder_exit / withdrawal +include "../../aspects/validator_pending_withdrawal.mzn"; % source + +% ---- Source validator instance ---------------------------------------------- +var ValidatorCredentialKind: validator_credential; +var BOOLV_NA: validator_active; +var BOOLV_NA: validator_exiting; +var BOOLV_NA: validator_old_enough; +constraint validator_credential_ok(validator_credential, validator_pubkey_found); +constraint validator_lifecycle_ok(validator_active, validator_exiting, validator_pubkey_found); +constraint validator_seasoning_ok(validator_old_enough, validator_pubkey_found); +constraint (validator_old_enough == T /\ validator_exiting == F) -> (validator_active == T); +constraint source_authorization_applicable <-> validator_pubkey_found; +constraint validator_pending_applicable <-> validator_pubkey_found; + +var bool: validator_has_execution_credential; +var bool: validator_has_compounding_credential; +constraint validator_has_execution_credential <-> cred_has_execution(validator_credential); +constraint validator_has_compounding_credential <-> cred_has_compounding(validator_credential); + +% ---- Target validator instance (consolidation path only) -------------------- +% The target role exists only when source != target; membership then decides the +% rest. Same lifecycle/credential predicates as the source, applied to target vars. +var BOOLV_NA: target_found; +constraint (target_found == NA) <-> same_source_target; +var bool: target_role_found = (not same_source_target) /\ target_found == T; + +var ValidatorCredentialKind: target_credential; +var BOOLV_NA: target_active; +var BOOLV_NA: target_exiting; +constraint validator_credential_ok(target_credential, target_role_found); +constraint validator_lifecycle_ok(target_active, target_exiting, target_role_found); + +var bool: target_has_compounding_credential; +constraint target_has_compounding_credential <-> cred_has_compounding(target_credential); + +% ---- Source predicates ------------------------------------------------------ +var bool: source_found = validator_pubkey_found; +var bool: source_authorized = source_address_matches == T; +var bool: source_is_eth1 = validator_credential == CRED_ETH1; +var bool: source_active = validator_active == T; +var bool: source_exiting = validator_exiting == T; +var bool: source_old_enough = validator_old_enough == T; +var bool: source_has_pending = has_pending_partial_withdrawal == T; + +var bool: switch_valid = + same_source_target /\ source_found /\ source_authorized /\ source_is_eth1 + /\ source_active /\ (not source_exiting); + +% ---- Outcome ---------------------------------------------------------------- +enum Outcome = { + SWITCHED_TO_COMPOUNDING, + SWITCH_REJECTED_SOURCE_NOT_FOUND, + SWITCH_REJECTED_NOT_AUTHORIZED, + SWITCH_REJECTED_NOT_ETH1, + SWITCH_REJECTED_INACTIVE, + SWITCH_REJECTED_EXITING, + REJECTED_QUEUE_FULL, + REJECTED_INSUFFICIENT_CHURN, + REJECTED_SOURCE_NOT_FOUND, + REJECTED_TARGET_NOT_FOUND, + REJECTED_SOURCE_CREDENTIALS, + REJECTED_TARGET_NOT_COMPOUNDING, + REJECTED_SOURCE_INACTIVE, + REJECTED_TARGET_INACTIVE, + REJECTED_SOURCE_EXITING, + REJECTED_TARGET_EXITING, + REJECTED_SOURCE_TOO_YOUNG, + REJECTED_SOURCE_PENDING_WITHDRAWAL, + CONSOLIDATED +}; + +var Outcome: outcome; +constraint outcome = + if switch_valid then + SWITCHED_TO_COMPOUNDING + elseif same_source_target then + (if not source_found then SWITCH_REJECTED_SOURCE_NOT_FOUND + elseif not source_authorized then SWITCH_REJECTED_NOT_AUTHORIZED + elseif not source_is_eth1 then SWITCH_REJECTED_NOT_ETH1 + elseif not source_active then SWITCH_REJECTED_INACTIVE + else SWITCH_REJECTED_EXITING endif) + else + (if pending_consolidations_full then REJECTED_QUEUE_FULL + elseif not sufficient_consolidation_churn then REJECTED_INSUFFICIENT_CHURN + elseif not source_found then REJECTED_SOURCE_NOT_FOUND + elseif not (target_found == T) then REJECTED_TARGET_NOT_FOUND + elseif not (source_execution_and_authorized) then REJECTED_SOURCE_CREDENTIALS + elseif not target_has_compounding_credential then REJECTED_TARGET_NOT_COMPOUNDING + elseif not source_active then REJECTED_SOURCE_INACTIVE + elseif not (target_active == T) then REJECTED_TARGET_INACTIVE + elseif source_exiting then REJECTED_SOURCE_EXITING + elseif target_exiting == T then REJECTED_TARGET_EXITING + elseif not source_old_enough then REJECTED_SOURCE_TOO_YOUNG + elseif source_has_pending then REJECTED_SOURCE_PENDING_WITHDRAWAL + else CONSOLIDATED endif) + endif; + +var bool: source_execution_and_authorized = validator_has_execution_credential /\ source_authorized; + +% ---- Effect ----------------------------------------------------------------- +var bool: state_effected; +constraint state_effected <-> (outcome in {SWITCHED_TO_COMPOUNDING, CONSOLIDATED}); diff --git a/tests/generators/compliance_runners/state_transition/consolidation_request/validation.py b/tests/generators/compliance_runners/state_transition/consolidation_request/validation.py new file mode 100644 index 00000000000..27701a1a683 --- /dev/null +++ b/tests/generators/compliance_runners/state_transition/consolidation_request/validation.py @@ -0,0 +1,167 @@ +"""Independent validation of process_consolidation_request vectors. + +Recovers every applicable coverage dimension from the decoded pre state and +ConsolidationRequest via the real spec predicates (source + target validators, +churn, both paths), and recomputes the 19-way outcome. Imports neither the +materializer nor the model. +""" + +from __future__ import annotations + +from typing import Any, TYPE_CHECKING + +from ruamel.yaml import YAML + +from eth_consensus_specs.gloas import minimal as spec +from tests.generators.compliance_runners.state_transition.validation import check_dimensions, decode + +if TYPE_CHECKING: + from pathlib import Path + + from tests.generators.compliance_runners.state_transition.validation import Check + +_YAML = YAML(typ="safe") +_ACCEPT = {"SWITCHED_TO_COMPOUNDING", "CONSOLIDATED"} + + +def _tri(x: bool) -> str: + return "T" if x else "F" + + +def _credential(v: Any) -> str: + prefix = bytes(v.withdrawal_credentials[:1]) + if prefix == bytes(spec.COMPOUNDING_WITHDRAWAL_PREFIX): + return "CRED_COMPOUNDING" + if prefix == bytes(spec.ETH1_ADDRESS_WITHDRAWAL_PREFIX): + return "CRED_ETH1" + return "CRED_BLS" + + +def recover(pre: Any, request: Any) -> dict[str, Any]: + cur = spec.get_current_epoch(pre) + scp = int(spec.config.SHARD_COMMITTEE_PERIOD) + val_pubkeys = [v.pubkey for v in pre.validators] + same = request.source_pubkey == request.target_pubkey + source_found = request.source_pubkey in val_pubkeys + + r: dict[str, Any] = { + "same_source_target": bool(same), + "pending_consolidations_full": len(pre.pending_consolidations) + == int(spec.PENDING_CONSOLIDATIONS_LIMIT), + "sufficient_consolidation_churn": int(spec.get_consolidation_churn_limit(pre)) + > int(spec.MIN_ACTIVATION_BALANCE), + "validator_pubkey_found": bool(source_found), + } + + if source_found: + sv = pre.validators[val_pubkeys.index(request.source_pubkey)] + sidx = spec.ValidatorIndex(val_pubkeys.index(request.source_pubkey)) + r["validator_credential"] = _credential(sv) + r["validator_has_execution_credential"] = bool(spec.has_execution_withdrawal_credential(sv)) + r["validator_has_compounding_credential"] = bool( + spec.has_compounding_withdrawal_credential(sv) + ) + r["source_address_matches"] = _tri(sv.withdrawal_credentials[12:] == request.source_address) + r["validator_active"] = _tri(bool(spec.is_active_validator(sv, cur))) + r["validator_exiting"] = _tri(sv.exit_epoch != spec.FAR_FUTURE_EPOCH) + r["validator_old_enough"] = _tri(int(cur) >= int(sv.activation_epoch) + scp) + r["has_pending_partial_withdrawal"] = _tri( + int(spec.get_pending_balance_to_withdraw(pre, sidx)) > 0 + ) + else: + r["validator_credential"] = "CRED_NA" + r["validator_has_execution_credential"] = False + r["validator_has_compounding_credential"] = False + for n in ( + "source_address_matches", + "validator_active", + "validator_exiting", + "validator_old_enough", + "has_pending_partial_withdrawal", + ): + r[n] = "NA" + + # target role only on the consolidation path + if same: + r["target_found"] = "NA" + r["target_credential"] = "CRED_NA" + r["target_has_compounding_credential"] = False + r["target_active"] = "NA" + r["target_exiting"] = "NA" + elif request.target_pubkey in val_pubkeys: + tv = pre.validators[val_pubkeys.index(request.target_pubkey)] + r["target_found"] = "T" + r["target_credential"] = _credential(tv) + r["target_has_compounding_credential"] = bool( + spec.has_compounding_withdrawal_credential(tv) + ) + r["target_active"] = _tri(bool(spec.is_active_validator(tv, cur))) + r["target_exiting"] = _tri(tv.exit_epoch != spec.FAR_FUTURE_EPOCH) + else: + r["target_found"] = "F" + r["target_credential"] = "CRED_NA" + r["target_has_compounding_credential"] = False + for n in ("target_active", "target_exiting"): + r[n] = "NA" + + r["outcome"] = _derive(r) + r["state_effected"] = r["outcome"] in _ACCEPT + return r + + +def _derive(r: dict) -> str: + same = r["same_source_target"] + src_found = r["validator_pubkey_found"] + src_auth = r["source_address_matches"] == "T" + src_eth1 = r["validator_credential"] == "CRED_ETH1" + src_exec = r["validator_has_execution_credential"] + src_active = r["validator_active"] == "T" + src_exiting = r["validator_exiting"] == "T" + src_old = r["validator_old_enough"] == "T" + src_pending = r["has_pending_partial_withdrawal"] == "T" + + if same and src_found and src_auth and src_eth1 and src_active and not src_exiting: + return "SWITCHED_TO_COMPOUNDING" + if same: + if not src_found: + return "SWITCH_REJECTED_SOURCE_NOT_FOUND" + if not src_auth: + return "SWITCH_REJECTED_NOT_AUTHORIZED" + if not src_eth1: + return "SWITCH_REJECTED_NOT_ETH1" + if not src_active: + return "SWITCH_REJECTED_INACTIVE" + return "SWITCH_REJECTED_EXITING" + if r["pending_consolidations_full"]: + return "REJECTED_QUEUE_FULL" + if not r["sufficient_consolidation_churn"]: + return "REJECTED_INSUFFICIENT_CHURN" + if not src_found: + return "REJECTED_SOURCE_NOT_FOUND" + if r["target_found"] != "T": + return "REJECTED_TARGET_NOT_FOUND" + if not (src_exec and src_auth): + return "REJECTED_SOURCE_CREDENTIALS" + if not r["target_has_compounding_credential"]: + return "REJECTED_TARGET_NOT_COMPOUNDING" + if not src_active: + return "REJECTED_SOURCE_INACTIVE" + if r["target_active"] != "T": + return "REJECTED_TARGET_INACTIVE" + if src_exiting: + return "REJECTED_SOURCE_EXITING" + if r["target_exiting"] == "T": + return "REJECTED_TARGET_EXITING" + if not src_old: + return "REJECTED_SOURCE_TOO_YOUNG" + if src_pending: + return "REJECTED_SOURCE_PENDING_WITHDRAWAL" + return "CONSOLIDATED" + + +def validate_case(case_dir: Path) -> list[Check]: + pre = decode(case_dir / "pre.ssz_snappy", spec.BeaconState) + request = decode(case_dir / "consolidation_request.ssz_snappy", spec.ConsolidationRequest) + claimed = _YAML.load((case_dir / "dimensions.yaml").read_text())["claimed"] + actual = recover(pre, request) + return check_dimensions(claimed, actual) diff --git a/tests/generators/compliance_runners/state_transition/deposit_request/__init__.py b/tests/generators/compliance_runners/state_transition/deposit_request/__init__.py new file mode 100644 index 00000000000..0207bac96f0 --- /dev/null +++ b/tests/generators/compliance_runners/state_transition/deposit_request/__init__.py @@ -0,0 +1,7 @@ +from .coverage import build_profile +from .materializer import DepositRequestMaterializer +from .validation import validate_case + +MATERIALIZER = DepositRequestMaterializer + +__all__ = ("MATERIALIZER", "build_profile", "validate_case") diff --git a/tests/generators/compliance_runners/state_transition/deposit_request/coverage.py b/tests/generators/compliance_runners/state_transition/deposit_request/coverage.py new file mode 100644 index 00000000000..5dc7606fed5 --- /dev/null +++ b/tests/generators/compliance_runners/state_transition/deposit_request/coverage.py @@ -0,0 +1,41 @@ +"""Coverage profiles for process_deposit_request. + +This handler has no faults, so its exceptional profile is empty. `normal` and +`standard` provide pairwise coverage over its input-shape dimensions. + +Run: + uv run python -m ...deposit_request.coverage + uv run python -m ...deposit_request.coverage standard --materialize +""" + +from __future__ import annotations + +from pathlib import Path + +from tests.generators.compliance_runners.state_transition.aspect_coverage import ( + build_profile as _build_profile, + enumerate_signatures, +) + +from .materializer import _DIMS + +INPUT_ASPECTS = { + "deposit_amount": ["amount_profile", "amount_nonzero"], + "withdrawal_credentials": ["withdrawal_credentials_profile"], + "signature": ["signature_profile"], + "deposit_pubkey": ["pubkey_is_existing_validator"], +} +ALL_ASPECTS = INPUT_ASPECTS +MODEL = Path(__file__).parent / "models" / "handler_deposit_request.mzn" + + +def _nfaults(_r: dict) -> int: + return 0 # no failing gates in this handler + + +def build_profile(name): + return _build_profile(_recs(), name, ALL_ASPECTS, ALL_ASPECTS, {"outcome": ["outcome"]}) + + +def _recs(): + return enumerate_signatures(MODEL, _DIMS, ALL_ASPECTS, _nfaults) diff --git a/tests/generators/compliance_runners/state_transition/deposit_request/materializer.py b/tests/generators/compliance_runners/state_transition/deposit_request/materializer.py new file mode 100644 index 00000000000..9a36dca5d09 --- /dev/null +++ b/tests/generators/compliance_runners/state_transition/deposit_request/materializer.py @@ -0,0 +1,100 @@ +"""Materialize aspect-model solutions into process_deposit_request cases. + +The simplest handler — no gates, no signature check; it always appends a +PendingDeposit and, if the start index is unset, sets it. The request fields are +copied verbatim, so validation's substantive check is output correctness. + +Spec: specs/electra/beacon-chain.md process_deposit_request (inherited by gloas). +""" + +from __future__ import annotations + +from typing import Any, TYPE_CHECKING + +from eth_consensus_specs.test.helpers.deposits import build_deposit_data +from eth_consensus_specs.test.helpers.genesis import create_genesis_state +from eth_consensus_specs.test.helpers.keys import privkeys, pubkeys +from tests.generators.compliance_runners.state_transition.aspects_helpers.deposit_amount import ( + deposit_amount_from_profile, +) +from tests.generators.compliance_runners.state_transition.aspects_helpers.withdrawal_credential import ( + withdrawal_credentials_from_profile, +) +from tests.generators.compliance_runners.state_transition.materializer import Materializer + +if TYPE_CHECKING: + from tests.generators.compliance_runners.gen_base.gen_typing import TestCasePart + +NUM_VALIDATORS = 64 +REQUEST_INDEX = 5 +INVALID_SIGNATURE = b"\x00" * 96 # not verified by this handler + +_DIMS = [ + "amount_profile", + "amount_nonzero", + "withdrawal_credentials_profile", + "signature_profile", + "pubkey_is_existing_validator", +] + + +def _b(sol: Any, n: str) -> bool: + return bool(getattr(sol, n)) + + +def _s(sol: Any, n: str) -> str: + return str(getattr(sol, n)) + + +class DepositRequestMaterializer(Materializer): + runner_name = "operations" + handler_name = "deposit_request" + + def materialize_solution(self, sol: Any) -> tuple[dict, list[TestCasePart]]: + spec = self.spec + pre = create_genesis_state( + spec, + validator_balances=[spec.MAX_EFFECTIVE_BALANCE] * NUM_VALIDATORS, + activation_threshold=spec.MAX_EFFECTIVE_BALANCE, + ) + key_index = 0 if _b(sol, "pubkey_is_existing_validator") else NUM_VALIDATORS + pubkey = pre.validators[key_index].pubkey if key_index == 0 else pubkeys[key_index] + amount_profile = _s(sol, "amount_profile") + credentials_profile = _s(sol, "withdrawal_credentials_profile") + signature_profile = _s(sol, "signature_profile") + amount = deposit_amount_from_profile(spec, amount_profile) + withdrawal_credentials = withdrawal_credentials_from_profile( + spec, credentials_profile, b"\x11" * 20 + ) + deposit_data = build_deposit_data( + spec, + pubkey, + privkeys[key_index], + amount, + withdrawal_credentials, + signed=signature_profile == "VALID", + ) + request = spec.DepositRequest( + pubkey=spec.BLSPubkey(pubkey), + withdrawal_credentials=spec.Bytes32(withdrawal_credentials), + amount=spec.Gwei(amount), + signature=( + deposit_data.signature + if signature_profile == "VALID" + else spec.BLSSignature(INVALID_SIGNATURE) + ), + index=spec.Uint64(REQUEST_INDEX), + ) + post = pre.copy() + spec.process_deposit_request(post, request) # never raises + + claimed = { + n: (_b(sol, n) if isinstance(getattr(sol, n), bool) else _s(sol, n)) for n in _DIMS + } + meta = {"description": "process_deposit_request", "claimed": claimed} + parts = [ + ("pre", "ssz", pre.encode_bytes()), + ("deposit_request", "ssz", request.encode_bytes()), + ("post", "ssz", post.encode_bytes()), + ] + return meta, parts diff --git a/tests/generators/compliance_runners/state_transition/deposit_request/models/handler_deposit_request.mzn b/tests/generators/compliance_runners/state_transition/deposit_request/models/handler_deposit_request.mzn new file mode 100644 index 00000000000..d3cff6dd202 --- /dev/null +++ b/tests/generators/compliance_runners/state_transition/deposit_request/models/handler_deposit_request.mzn @@ -0,0 +1,18 @@ +% Handler model: process_deposit_request (gloas). +% +% Modified in gloas: the Electra start-index logic is REMOVED — the handler +% unconditionally appends a PendingDeposit copied from the request (with +% slot = state.slot) and touches nothing else. So there is a single outcome and +% no gates; `amount_nonzero` and `pubkey_is_existing_validator` are pure +% input/output-shape dimensions. No solve item. +% +% Spec: specs/gloas/beacon-chain.md process_deposit_request (invoked via +% apply_parent_execution_payload). + +include "../../aspects/deposit_amount.mzn"; +include "../../aspects/deposit_pubkey.mzn"; +include "../../aspects/withdrawal_credential.mzn"; + +enum SignatureProfile = { VALID, INVALID }; + +var SignatureProfile: signature_profile; diff --git a/tests/generators/compliance_runners/state_transition/deposit_request/validation.py b/tests/generators/compliance_runners/state_transition/deposit_request/validation.py new file mode 100644 index 00000000000..f62063ba323 --- /dev/null +++ b/tests/generators/compliance_runners/state_transition/deposit_request/validation.py @@ -0,0 +1,59 @@ +"""Independent validation of process_deposit_request vectors. + +Since the handler has no predicates to re-derive beyond `start_index_unset`, the +substantive check is OUTPUT correctness: the appended PendingDeposit matches the +request (with slot = pre.slot), the queue grew by one, and the start index was +set iff it was unset. Imports neither the materializer nor the model. +""" + +from __future__ import annotations + +from typing import Any, TYPE_CHECKING + +from ruamel.yaml import YAML + +from eth_consensus_specs.gloas import minimal as spec +from tests.generators.compliance_runners.state_transition.aspects_helpers.deposit_amount import ( + deposit_amount_profile, +) +from tests.generators.compliance_runners.state_transition.aspects_helpers.withdrawal_credential import ( + withdrawal_credentials_profile, +) +from tests.generators.compliance_runners.state_transition.validation import check_dimensions, decode + +if TYPE_CHECKING: + from pathlib import Path + + from generators.compliance_runners.state_transition.validation import Check + +_YAML = YAML(typ="safe") + + +def recover(pre: Any, request: Any) -> dict[str, Any]: + amount = int(request.amount) + return { + "amount_profile": deposit_amount_profile(spec, amount), + "amount_nonzero": amount > 0, + "withdrawal_credentials_profile": withdrawal_credentials_profile( + spec, request.withdrawal_credentials + ), + "signature_profile": ( + "VALID" + if spec.is_valid_deposit_signature( + request.pubkey, + request.withdrawal_credentials, + request.amount, + request.signature, + ) + else "INVALID" + ), + "pubkey_is_existing_validator": request.pubkey in [v.pubkey for v in pre.validators], + } + + +def validate_case(case_dir: Path) -> list[Check]: + pre = decode(case_dir / "pre.ssz_snappy", spec.BeaconState) + request = decode(case_dir / "deposit_request.ssz_snappy", spec.DepositRequest) + claimed = _YAML.load((case_dir / "dimensions.yaml").read_text())["claimed"] + actual = recover(pre, request) + return check_dimensions(claimed, actual) diff --git a/tests/generators/compliance_runners/state_transition/execution_payload_bid/__init__.py b/tests/generators/compliance_runners/state_transition/execution_payload_bid/__init__.py new file mode 100644 index 00000000000..7c98837e28a --- /dev/null +++ b/tests/generators/compliance_runners/state_transition/execution_payload_bid/__init__.py @@ -0,0 +1,7 @@ +from .coverage import build_profile +from .materializer import ExecutionPayloadBidMaterializer +from .validation import validate_case + +MATERIALIZER = ExecutionPayloadBidMaterializer + +__all__ = ("MATERIALIZER", "build_profile", "validate_case") diff --git a/tests/generators/compliance_runners/state_transition/execution_payload_bid/coverage.py b/tests/generators/compliance_runners/state_transition/execution_payload_bid/coverage.py new file mode 100644 index 00000000000..0fc9b8a157f --- /dev/null +++ b/tests/generators/compliance_runners/state_transition/execution_payload_bid/coverage.py @@ -0,0 +1,114 @@ +"""Coverage profiles for process_execution_payload_bid. + +Handler-specific instantiation of the generic combinatorial-over-aspects engine +in ``..aspect_coverage``: it declares this handler's aspects, coverage +dimensions, model, and a fault-count rank, then exposes named profiles. + +Run: + uv run python -m ...execution_payload_bid.coverage # profile summary + uv run python -m ...execution_payload_bid.coverage standard --materialize +""" + +from __future__ import annotations + +from pathlib import Path + +from tests.generators.compliance_runners.state_transition.aspect_coverage import ( + build_profile as _build_profile, + enumerate_signatures, +) + +from .materializer import _DIMS + +# Fine-grained input aspects (realization + the handler-local bid amount). +# The dimensions remain part of the signature used by `all`. The normal and +# exceptional profiles use coarser logical groups, where dimensions in each +# group form one composite factor for coverage. +FINE_INPUT_ASPECTS = { + "entity_reference": ["builder_ref"], + "builder_lifecycle": ["builder_deposit_to_finalized_epoch", "builder_withdrawable_epoch_set"], + "builder_version": ["builder_version_valid"], + "builder_pending_balance": ["builder_has_pending_withdrawal", "builder_has_pending_payment"], + "builder_funds": ["builder_balance_to_min_balance", "builder_available_to_bid"], + "signed_message": ["builder_signature_valid"], + "self_build_signature": ["self_build_signature_is_infinity"], + "bid_amount": ["amount_positive"], + "blob_kzg_capacity": ["bid_kzg_to_max"], + "slot_epoch": ["bid_slot_to_state", "state_slot_past_genesis"], + "block_context": [ + "bid_parent_block_hash_matches", + "bid_parent_block_root_matches", + "bid_prev_randao_matches", + ], +} +OUTCOME_ASPECT = {"outcome": ["outcome"]} + +# A complete builder/state tuple participates in pairwise joins with every +# other aspect. This is intentionally a tuple-valued aspect rather than a +# new MiniZinc predicate: the handler still constrains each realization +# dimension independently and aspect_coverage.py joins their feasible values. +INPUT_ASPECTS = { + "builder_state": [ + "builder_ref", + "builder_deposit_to_finalized_epoch", + "builder_withdrawable_epoch_set", + "builder_version_valid", + "builder_has_pending_withdrawal", + "builder_has_pending_payment", + "builder_balance_to_min_balance", + "builder_available_to_bid", + ], + "signed_message": ["builder_signature_valid"], + "self_build_signature": ["self_build_signature_is_infinity"], + "bid_amount": ["amount_positive"], + "beacon_context": [ + "bid_kzg_to_max", + "bid_slot_to_state", + "state_slot_past_genesis", + "bid_parent_block_hash_matches", + "bid_parent_block_root_matches", + "bid_prev_randao_matches", + ], +} + +FINE_ALL_ASPECTS = {**FINE_INPUT_ASPECTS, **OUTCOME_ASPECT} +ALL_ASPECTS = {**INPUT_ASPECTS, **OUTCOME_ASPECT} +MODEL = Path(__file__).parent / "models" / "handler_execution_payload_bid.mzn" + + +def _recs(): + return enumerate_signatures(MODEL, _DIMS, FINE_ALL_ASPECTS, _nfaults) + + +def _nfaults(r: dict) -> int: + """Failing applicable gates (mirrors the handler), for clean-rep tie-breaking.""" + f = 0 + if r["self_build"]: + f += r["amount_positive"] + f += r["self_build_signature_is_infinity"] != "T" + elif r["builder_ref"] == "NON_EXISTING": + f += 1 + elif r["builder_ref"] == "EXISTING": + f += not r["builder_active"] + f += r["builder_version_valid"] != "T" + f += not r["builder_can_cover_bid"] + f += r["builder_signature_valid"] != "T" + f += r["bid_kzg_to_max"] not in ("LT", "EQ") + f += r["bid_slot_to_state"] != "EQ" + f += not r["state_slot_past_genesis"] + f += not r["bid_parent_block_hash_matches"] + f += r["bid_parent_block_root_matches"] == "F" + f += not r["bid_prev_randao_matches"] + return int(f) + + +def build_profile(name): + return _build_profile( + _recs(), + name, + ALL_ASPECTS, + INPUT_ASPECTS, + OUTCOME_ASPECT, + exceptional_aspects={"builder_state": INPUT_ASPECTS["builder_state"], **OUTCOME_ASPECT}, + exceptional_t=2, + ) diff --git a/tests/generators/compliance_runners/state_transition/execution_payload_bid/materializer.py b/tests/generators/compliance_runners/state_transition/execution_payload_bid/materializer.py new file mode 100644 index 00000000000..a3546ddba8f --- /dev/null +++ b/tests/generators/compliance_runners/state_transition/execution_payload_bid/materializer.py @@ -0,0 +1,261 @@ +"""Materialize aspect-model solutions into process_execution_payload_bid cases. + +Solves models/coverage_smoke.mzn, reduces the solutions to the declared +obligation cover_each((outcome, self_build)) — the "both branches for the shared +tail" set — and materializes each representative into a concrete +pre / SignedExecutionPayloadBid / post vector, realizing every applicable +coverage dimension of its solution. The immutable solution is serialized to +dimensions.yaml (the contract validation.py checks against). + +Spec: specs/gloas/beacon-chain.md process_execution_payload_bid. + +Usage: + uv run python -m tests.generators.compliance_runners.state_transition.execution_payload_bid.materializer +""" + +from __future__ import annotations + +from typing import Any, TYPE_CHECKING + +from eth_consensus_specs.test.helpers.genesis import create_genesis_state +from eth_consensus_specs.test.helpers.keys import builder_pubkey_to_privkey, builder_pubkeys +from eth_consensus_specs.utils import bls +from tests.generators.compliance_runners.state_transition.materializer import Materializer + +if TYPE_CHECKING: + from tests.generators.compliance_runners.gen_base.gen_typing import TestCasePart + +BUILDER_PUBKEY = builder_pubkeys[0] # the referenced builder +WRONG_PUBKEY = builder_pubkeys[1] # a different signer, for invalid signatures +FINALIZED_EPOCH = 5 # fabricated, with headroom for LT/EQ/GT deposits +EPOCHS_PAST_GENESIS = 10 +BIG = 10**10 # comfortable balance headroom above min_balance + +# Coverage dimensions serialized to dimensions.yaml (the authoritative solution). +_DIMS = [ + "builder_ref", + "builder_deposit_to_finalized_epoch", + "builder_withdrawable_epoch_set", + "builder_version_valid", + "builder_has_pending_withdrawal", + "builder_has_pending_payment", + "builder_balance_to_min_balance", + "builder_available_to_bid", + "builder_signature_valid", + "self_build_signature_is_infinity", + "amount_positive", + "bid_kzg_to_max", + "bid_slot_to_state", + "state_slot_past_genesis", + "bid_parent_block_hash_matches", + "bid_parent_block_root_matches", + "bid_prev_randao_matches", + # derived, recorded for validation convenience + "builder_active", + "builder_can_cover_bid", + "self_build", + "outcome", +] + + +def _s(sol: Any, name: str) -> str: + return str(getattr(sol, name)) + + +def _b(sol: Any, name: str) -> bool: + return bool(getattr(sol, name)) + + +class ExecutionPayloadBidMaterializer(Materializer): + runner_name = "operations" + handler_name = "execution_payload_bid" + + def _sign(self, state: Any, bid: Any, privkey: int) -> Any: + spec = self.spec + domain = spec.get_domain(state, spec.DOMAIN_BEACON_BUILDER) + root = spec.compute_signing_root(bid, domain) + return bls.Sign(privkey, root) + + def _base_state(self, past_genesis: bool) -> Any: + spec = self.spec + state = create_genesis_state( + spec, + validator_balances=[spec.MAX_EFFECTIVE_BALANCE] * 256, + activation_threshold=spec.MAX_EFFECTIVE_BALANCE, + ) + state.builders = type(state.builders)() + state.slot = ( + spec.Slot(EPOCHS_PAST_GENESIS * spec.SLOTS_PER_EPOCH) if past_genesis else spec.Slot(0) + ) + # Fabricate a finalized checkpoint with headroom so deposit vs finalized + # can be LT/EQ/GT (even at the genesis slot, where it is pathological but + # spec-accepted — is_active_builder reads finalized_checkpoint, not slot). + state.finalized_checkpoint = spec.Checkpoint( + epoch=spec.Epoch(FINALIZED_EPOCH), root=spec.Root(b"\x01" * 32) + ) + return state + + def materialize_solution(self, sol: Any) -> tuple[dict, list[TestCasePart]]: + spec = self.spec + ref = _s(sol, "builder_ref") + self_build = _b(sol, "self_build") + past_genesis = _b(sol, "state_slot_past_genesis") + + pre = self._base_state(past_genesis) + current_epoch = int(spec.get_current_epoch(pre)) + + # ---- Builder registry (EXISTING only) ------------------------------- + if ref == "EXISTING": + pw = _s(sol, "builder_has_pending_withdrawal") == "T" + pp = _s(sol, "builder_has_pending_payment") == "T" + pending_total = (1 if pw else 0) + (1 if pp else 0) + min_balance = int(spec.MIN_DEPOSIT_AMOUNT) + pending_total + + dep = _s(sol, "builder_deposit_to_finalized_epoch") + deposit_epoch = { + "LT": FINALIZED_EPOCH - 1, + "EQ": FINALIZED_EPOCH, + "GT": FINALIZED_EPOCH + 1, + }[dep] + wset = _s(sol, "builder_withdrawable_epoch_set") == "T" + withdrawable = spec.Epoch(current_epoch) if wset else spec.FAR_FUTURE_EPOCH + version = ( + spec.PAYLOAD_BUILDER_VERSION + if _s(sol, "builder_version_valid") == "T" + else spec.Uint8(1) + ) + + b2min = _s(sol, "builder_balance_to_min_balance") + balance = {"LT": min_balance - 1, "EQ": min_balance, "GT": min_balance + BIG}[b2min] + + pre.builders.append( + spec.Builder( + pubkey=spec.BLSPubkey(BUILDER_PUBKEY), + version=version, + execution_address=spec.ExecutionAddress(b"\x22" * 20), + balance=spec.Gwei(balance), + deposit_epoch=spec.Epoch(deposit_epoch), + withdrawable_epoch=withdrawable, + ) + ) + if pw: + pre.builder_pending_withdrawals.append( + spec.BuilderPendingWithdrawal( + fee_recipient=spec.ExecutionAddress(b"\x22" * 20), + amount=spec.Gwei(1), + builder_index=spec.BuilderIndex(0), + ) + ) + if pp: + pre.builder_pending_payments[0] = spec.BuilderPendingPayment( + weight=spec.Gwei(1), + withdrawal=spec.BuilderPendingWithdrawal( + fee_recipient=spec.ExecutionAddress(b"\x22" * 20), + amount=spec.Gwei(1), + builder_index=spec.BuilderIndex(0), + ), + proposer_index=spec.ValidatorIndex(0), + ) + else: + min_balance = 0 # unused + + # ---- builder_index --------------------------------------------------- + if self_build: + builder_index = spec.BUILDER_INDEX_SELF_BUILD + elif ref == "NON_EXISTING": + builder_index = spec.BuilderIndex(len(pre.builders)) # past end -> IndexError + else: + builder_index = spec.BuilderIndex(0) + + # ---- bid.value ------------------------------------------------------- + amt_pos = _b(sol, "amount_positive") + if ref == "EXISTING" and _s(sol, "builder_balance_to_min_balance") in ("EQ", "GT"): + available = int(pre.builders[0].balance) - min_balance + if not amt_pos: + value = 0 + else: + avail = _s(sol, "builder_available_to_bid") + value = {"LT": available + 1000, "EQ": available, "GT": available - 1000}[avail] + else: + value = 1 if amt_pos else 0 + + # ---- bid.slot -------------------------------------------------------- + slot_cmp = _s(sol, "bid_slot_to_state") + bid_slot = {"EQ": int(pre.slot), "LT": int(pre.slot) - 1, "GT": int(pre.slot) + 1}[slot_cmp] + + # ---- KZG commitments ------------------------------------------------- + max_blobs = spec.get_blob_parameters(spec.get_current_epoch(pre)).max_blobs_per_block + kzg = _s(sol, "bid_kzg_to_max") + n_kzg = {"LT": max(0, max_blobs - 1), "EQ": max_blobs, "GT": max_blobs + 1}[kzg] + commitments = [spec.KZGCommitment(bytes([i % 256]) * 48) for i in range(n_kzg)] + + # ---- block context --------------------------------------------------- + ph = _b(sol, "bid_parent_block_hash_matches") + rr = _b(sol, "bid_prev_randao_matches") + pr = _s(sol, "bid_parent_block_root_matches") + parent_block_hash = pre.latest_block_hash if ph else spec.Hash32(b"\x02" * 32) + prev_randao = ( + spec.get_randao_mix(pre, spec.get_current_epoch(pre)) + if rr + else spec.Bytes32(b"\x06" * 32) + ) + if pr == "T": + parent_block_root = spec.get_block_root_at_slot(pre, spec.Slot(int(pre.slot) - 1)) + else: # F or NA (genesis, not reached) — value unused + parent_block_root = spec.Root(b"\x04" * 32) + + bid = spec.ExecutionPayloadBid( + parent_block_hash=parent_block_hash, + parent_block_root=parent_block_root, + block_hash=spec.Hash32(b"\x07" * 32), + prev_randao=prev_randao, + fee_recipient=spec.ExecutionAddress(b"\x00" * 20), + gas_limit=spec.Uint64(30000000), + builder_index=builder_index, + slot=spec.Slot(bid_slot), + value=spec.Gwei(value), + execution_payment=spec.Gwei(0), + blob_kzg_commitments=spec.BlobKZGCommitments(data=commitments), + execution_requests_root=spec.Root(b"\x08" * 32), + ) + + # ---- signature ------------------------------------------------------- + if self_build: + if _s(sol, "self_build_signature_is_infinity") == "T": + signature = spec.bls.G2_POINT_AT_INFINITY + else: + signature = self._sign(pre, bid, builder_pubkey_to_privkey[BUILDER_PUBKEY]) + elif ref == "NON_EXISTING": + signature = spec.BLSSignature(b"\x00" * 96) # never verified (rejected earlier) + else: # EXISTING + key = BUILDER_PUBKEY if _s(sol, "builder_signature_valid") == "T" else WRONG_PUBKEY + signature = self._sign(pre, bid, builder_pubkey_to_privkey[key]) + + signed = spec.SignedExecutionPayloadBid(message=bid, signature=signature) + + # ---- derive post (accepted) or omit (rejected) ---------------------- + post = pre.copy() + accepted = True + try: + spec.process_execution_payload_bid(post, signed) + except (AssertionError, IndexError): + accepted = False + post = None + + claimed = { + name: (_s(sol, name) if not isinstance(getattr(sol, name), bool) else _b(sol, name)) + for name in _DIMS + } + parts: list[TestCasePart] = [ + ("pre", "ssz", pre.encode_bytes()), + ("execution_payload_bid", "ssz", signed.encode_bytes()), + ] + if accepted: + parts.append(("post", "ssz", post.encode_bytes())) # type: ignore[union-attr] + meta = { + "description": f"process_execution_payload_bid: {claimed['outcome']} " + f"(self_build={int(bool(claimed['self_build']))})", + "bls_setting": 1, + "claimed": claimed, + } + return meta, parts diff --git a/tests/generators/compliance_runners/state_transition/execution_payload_bid/models/coverage_smoke.mzn b/tests/generators/compliance_runners/state_transition/execution_payload_bid/models/coverage_smoke.mzn new file mode 100644 index 00000000000..db652a9bd19 --- /dev/null +++ b/tests/generators/compliance_runners/state_transition/execution_payload_bid/models/coverage_smoke.mzn @@ -0,0 +1,14 @@ +% Coverage formula (smoke scope): at most one gate fails. +% +% Yields ACCEPT plus single-fault situations — one decisive failing gate with +% every other applicable gate passing. Non-gate dimensions (pending balance, +% amount, comparison boundaries that still pass) remain free, so several +% assignments may share an outcome; the materializer reduces to the declared +% obligations (e.g. cover_each(outcome)) by coverage fingerprint. +% +% Richer profiles simply relax this bound (n_faults <= 2, or drop it entirely +% for exhaustive) without changing the handler or aspect models. + +include "handler_execution_payload_bid.mzn"; + +constraint n_faults <= 1; diff --git a/tests/generators/compliance_runners/state_transition/execution_payload_bid/models/handler_execution_payload_bid.mzn b/tests/generators/compliance_runners/state_transition/execution_payload_bid/models/handler_execution_payload_bid.mzn new file mode 100644 index 00000000000..477f7ab9cd7 --- /dev/null +++ b/tests/generators/compliance_runners/state_transition/execution_payload_bid/models/handler_execution_payload_bid.mzn @@ -0,0 +1,161 @@ +% Handler model: process_execution_payload_bid. +% +% Assembles the shared realization aspects, binds their applicability to this +% handler's entity reference, adds handler-local dimensions, and derives the +% outcome (first-failing gate in spec order), per-gate faults, effects, and a +% few trace dimensions. No solve item — a coverage model drives solving. +% +% Spec: specs/gloas/beacon-chain.md process_execution_payload_bid (:1611). + +include "../../aspects/entity_reference.mzn"; +include "../../aspects/builder_lifecycle.mzn"; +include "../../aspects/builder_version.mzn"; +include "../../aspects/builder_pending_balance.mzn"; +include "../../aspects/builder_funds.mzn"; +include "../../aspects/signed_message.mzn"; +include "../../aspects/self_build_signature.mzn"; +include "../../aspects/blob_kzg_capacity.mzn"; +include "../../aspects/slot_epoch.mzn"; +include "../../aspects/block_context.mzn"; + +% ---- Handler-local dimensions ------------------------------------------------ +var bool: amount_positive; % bid.value > 0 (self-build requires amount == 0) + +% ---- Builder instance: parameterized aspects bound to the referenced builder - +% Applicable only for a resolved existing builder; the self-build signature only +% for a self-build. (entity_reference, slot_epoch, block_context stay flat.) +var CMP_NA: builder_deposit_to_finalized_epoch; +var BOOLV_NA: builder_withdrawable_epoch_set; +constraint builder_lifecycle_ok(builder_deposit_to_finalized_epoch, + builder_withdrawable_epoch_set, builder_ref == EXISTING); +var bool: builder_active; +constraint builder_active <-> + builder_is_active(builder_deposit_to_finalized_epoch, builder_withdrawable_epoch_set); + +var BOOLV_NA: builder_version_valid; +constraint builder_version_ok(builder_version_valid, builder_ref == EXISTING); + +var BOOLV_NA: builder_has_pending_withdrawal; +var BOOLV_NA: builder_has_pending_payment; +constraint builder_pending_ok(builder_has_pending_withdrawal, builder_has_pending_payment, + builder_ref == EXISTING); +var bool: builder_has_pending_balance; +constraint builder_has_pending_balance <-> + builder_has_pending(builder_has_pending_withdrawal, builder_has_pending_payment); + +var CMP_NA: builder_balance_to_min_balance; +var CMP_NA: builder_available_to_bid; +constraint builder_funds_ok(builder_balance_to_min_balance, builder_available_to_bid, + builder_ref == EXISTING); +var bool: builder_can_cover_bid; +constraint builder_can_cover_bid <-> + builder_can_cover(builder_balance_to_min_balance, builder_available_to_bid); + +var BOOLV_NA: builder_signature_valid; +constraint signed_message_ok(builder_signature_valid, builder_ref == EXISTING); + +var BOOLV_NA: self_build_signature_is_infinity; +constraint self_build_signature_ok(self_build_signature_is_infinity, builder_ref == SELF_BUILD); + +constraint bid_parent_block_root_applicable <-> state_slot_past_genesis; + +% bid.value is the shared operand of the funds comparison and amount_positive: +% a zero bid pins the available/bid comparison to the balance/min gap; a positive +% bid at balance == min_balance is strictly greater (available/bid == LT). +constraint (builder_balance_to_min_balance == EQ /\ amount_positive) -> (builder_available_to_bid == LT); +constraint (builder_balance_to_min_balance == EQ /\ not amount_positive) -> (builder_available_to_bid == EQ); +constraint (builder_balance_to_min_balance == GT /\ not amount_positive) -> (builder_available_to_bid == GT); + +% ---- Gate pass predicates (spec order) --------------------------------------- +var bool: g_self_amount_ok = not amount_positive; % amount == 0 +var bool: g_self_sig_ok = self_build_signature_is_infinity == T; +var bool: g_active = builder_active; +var bool: g_version = builder_version_valid == T; +var bool: g_funds = builder_can_cover_bid; +var bool: g_sig = builder_signature_valid == T; +var bool: g_kzg = bid_kzg_under_limit; +var bool: g_slot = bid_slot_matches; +var bool: g_genesis = state_slot_past_genesis; +var bool: g_ph = bid_parent_block_hash_matches; +var bool: g_pr = bid_parent_block_root_matches == T; +var bool: g_rr = bid_prev_randao_matches; + +% ---- Outcome (first-failing gate) -------------------------------------------- +enum Outcome = { + ACCEPT, + REJECT_SELF_BUILD_NONZERO_AMOUNT, + REJECT_SELF_BUILD_BAD_SIGNATURE, + REJECT_BUILDER_NOT_FOUND, + REJECT_BUILDER_INACTIVE, + REJECT_WRONG_VERSION, + REJECT_UNDERFUNDED, + REJECT_BAD_SIGNATURE, + REJECT_KZG_OVER_LIMIT, + REJECT_WRONG_SLOT, + REJECT_NOT_PAST_GENESIS, + REJECT_PARENT_HASH, + REJECT_PARENT_ROOT, + REJECT_PREV_RANDAO +}; + +% Outcome once the branch-specific gates have passed (shared tail). +var Outcome: common_stage; +constraint common_stage = + if not g_kzg then REJECT_KZG_OVER_LIMIT + elseif not g_slot then REJECT_WRONG_SLOT + elseif not g_genesis then REJECT_NOT_PAST_GENESIS + elseif not g_ph then REJECT_PARENT_HASH + elseif not g_pr then REJECT_PARENT_ROOT + elseif not g_rr then REJECT_PREV_RANDAO + else ACCEPT + endif; + +var Outcome: outcome; +constraint outcome = + if self_build then + if not g_self_amount_ok then REJECT_SELF_BUILD_NONZERO_AMOUNT + elseif not g_self_sig_ok then REJECT_SELF_BUILD_BAD_SIGNATURE + else common_stage + endif + elseif builder_ref == NON_EXISTING then REJECT_BUILDER_NOT_FOUND + elseif not g_active then REJECT_BUILDER_INACTIVE + elseif not g_version then REJECT_WRONG_VERSION + elseif not g_funds then REJECT_UNDERFUNDED + elseif not g_sig then REJECT_BAD_SIGNATURE + else common_stage + endif; + +% ---- Faults (an applicable gate in its failing state) ------------------------ +% Used by coverage formulas. Not-applicable gates never count as faults. +var bool: fault_self_amount = self_build /\ not g_self_amount_ok; +var bool: fault_self_sig = self_build /\ not g_self_sig_ok; +var bool: fault_not_found = (builder_ref == NON_EXISTING); +var bool: fault_active = (builder_ref == EXISTING) /\ not g_active; +var bool: fault_version = (builder_ref == EXISTING) /\ not g_version; +var bool: fault_funds = (builder_ref == EXISTING) /\ not g_funds; +var bool: fault_sig = (builder_ref == EXISTING) /\ not g_sig; +var bool: fault_kzg = not g_kzg; +var bool: fault_slot = not g_slot; +var bool: fault_genesis = not g_genesis; +var bool: fault_ph = not g_ph; +var bool: fault_pr = bid_parent_block_root_matches == F; % NA is not a fault +var bool: fault_rr = not g_rr; + +var int: n_faults = + bool2int(fault_self_amount) + bool2int(fault_self_sig) + + bool2int(fault_not_found) + bool2int(fault_active) + + bool2int(fault_version) + bool2int(fault_funds) + bool2int(fault_sig) + + bool2int(fault_kzg) + bool2int(fault_slot) + bool2int(fault_genesis) + + bool2int(fault_ph) + bool2int(fault_pr) + bool2int(fault_rr); + +% ---- Effects ----------------------------------------------------------------- +var bool: pending_payment_written = (outcome == ACCEPT) /\ amount_positive; +var bool: latest_bid_cached = (outcome == ACCEPT); + +% ---- Trace (checks reached) -------------------------------------------------- +var bool: version_check_reached = (builder_ref == EXISTING) /\ g_active; +var bool: funds_check_reached = version_check_reached /\ g_version; +var bool: signature_check_reached = funds_check_reached /\ g_funds; +var bool: common_reached = + (self_build /\ g_self_amount_ok /\ g_self_sig_ok) + \/ ((builder_ref == EXISTING) /\ g_active /\ g_version /\ g_funds /\ g_sig); diff --git a/tests/generators/compliance_runners/state_transition/execution_payload_bid/validation.py b/tests/generators/compliance_runners/state_transition/execution_payload_bid/validation.py new file mode 100644 index 00000000000..80adc112c5c --- /dev/null +++ b/tests/generators/compliance_runners/state_transition/execution_payload_bid/validation.py @@ -0,0 +1,169 @@ +"""Independent validation of process_execution_payload_bid vectors. + +Recovers every applicable coverage dimension directly from the decoded pre state +and SignedExecutionPayloadBid via the real spec predicates, compares to the +serialized solution in dimensions.yaml, recomputes the outcome, and runs the +Imports neither the materializer nor the model. + +Usage: + uv run python -m tests.generators.compliance_runners.state_transition.execution_payload_bid.validation [REFTESTS_DIR] +""" + +from __future__ import annotations + +from typing import Any, TYPE_CHECKING + +from ruamel.yaml import YAML + +from eth_consensus_specs.gloas import minimal as spec +from tests.generators.compliance_runners.state_transition.validation import check_dimensions, decode + +if TYPE_CHECKING: + from pathlib import Path + + from tests.generators.compliance_runners.state_transition.validation import Check + +_YAML = YAML(typ="safe") + + +def _cmp(a: int, b: int) -> str: + return "LT" if a < b else ("EQ" if a == b else "GT") + + +def _tri(x: bool) -> str: + return "T" if x else "F" + + +def recover(pre: Any, signed: Any) -> dict[str, Any]: + bid = signed.message + idx = bid.builder_index + n_builders = len(pre.builders) + + if idx == spec.BUILDER_INDEX_SELF_BUILD: + ref = "SELF_BUILD" + elif int(idx) < n_builders: + ref = "EXISTING" + else: + ref = "NON_EXISTING" + self_build = ref == "SELF_BUILD" + current_epoch = spec.get_current_epoch(pre) + past_genesis = int(pre.slot) > spec.GENESIS_SLOT + + r: dict[str, Any] = { + "builder_ref": ref, + "self_build": self_build, + "amount_positive": int(bid.value) > 0, + "state_slot_past_genesis": past_genesis, + "bid_parent_block_hash_matches": bid.parent_block_hash == pre.latest_block_hash, + "bid_prev_randao_matches": bid.prev_randao == spec.get_randao_mix(pre, current_epoch), + } + + max_blobs = spec.get_blob_parameters(current_epoch).max_blobs_per_block + r["bid_kzg_to_max"] = _cmp(len(bid.blob_kzg_commitments), max_blobs) + r["bid_slot_to_state"] = _cmp(int(bid.slot), int(pre.slot)) + + # parent_block_root: only defined past genesis + if past_genesis: + expected = spec.get_block_root_at_slot(pre, spec.Slot(int(pre.slot) - 1)) + r["bid_parent_block_root_matches"] = _tri(bid.parent_block_root == expected) + else: + r["bid_parent_block_root_matches"] = "NA" + + # self-build signature + r["self_build_signature_is_infinity"] = ( + _tri(signed.signature == spec.bls.G2_POINT_AT_INFINITY) if self_build else "NA" + ) + + # EXISTING-only builder dimensions + if ref == "EXISTING": + b = pre.builders[idx] + finalized = int(pre.finalized_checkpoint.epoch) + min_balance = int(spec.MIN_DEPOSIT_AMOUNT) + int( + spec.get_pending_balance_to_withdraw_for_builder(pre, idx) + ) + r["builder_deposit_to_finalized_epoch"] = _cmp(int(b.deposit_epoch), finalized) + r["builder_withdrawable_epoch_set"] = _tri(b.withdrawable_epoch != spec.FAR_FUTURE_EPOCH) + r["builder_version_valid"] = _tri(b.version == spec.PAYLOAD_BUILDER_VERSION) + r["builder_has_pending_withdrawal"] = _tri( + any( + w.builder_index == idx and int(w.amount) > 0 + for w in pre.builder_pending_withdrawals + ) + ) + r["builder_has_pending_payment"] = _tri( + any( + p.withdrawal.builder_index == idx and int(p.withdrawal.amount) > 0 + for p in pre.builder_pending_payments + ) + ) + r["builder_balance_to_min_balance"] = _cmp(int(b.balance), min_balance) + r["builder_available_to_bid"] = ( + _cmp(int(b.balance) - min_balance, int(bid.value)) + if int(b.balance) >= min_balance + else "NA" + ) + r["builder_signature_valid"] = _tri( + spec.verify_execution_payload_bid_signature(pre, signed) + ) + r["builder_active"] = bool(spec.is_active_builder(pre, idx)) + r["builder_can_cover_bid"] = bool(spec.can_builder_cover_bid(pre, idx, bid.value)) + else: + for name in ( + "builder_deposit_to_finalized_epoch", + "builder_withdrawable_epoch_set", + "builder_version_valid", + "builder_has_pending_withdrawal", + "builder_has_pending_payment", + "builder_balance_to_min_balance", + "builder_available_to_bid", + "builder_signature_valid", + ): + r[name] = "NA" + r["builder_active"] = False + r["builder_can_cover_bid"] = False + + r["outcome"] = _derive_outcome(r) + return r + + +def _derive_outcome(r: dict[str, Any]) -> str: + def common() -> str: + if r["bid_kzg_to_max"] not in ("LT", "EQ"): + return "REJECT_KZG_OVER_LIMIT" + if r["bid_slot_to_state"] != "EQ": + return "REJECT_WRONG_SLOT" + if not r["state_slot_past_genesis"]: + return "REJECT_NOT_PAST_GENESIS" + if not r["bid_parent_block_hash_matches"]: + return "REJECT_PARENT_HASH" + if r["bid_parent_block_root_matches"] != "T": + return "REJECT_PARENT_ROOT" + if not r["bid_prev_randao_matches"]: + return "REJECT_PREV_RANDAO" + return "ACCEPT" + + if r["self_build"]: + if r["amount_positive"]: + return "REJECT_SELF_BUILD_NONZERO_AMOUNT" + if r["self_build_signature_is_infinity"] != "T": + return "REJECT_SELF_BUILD_BAD_SIGNATURE" + return common() + if r["builder_ref"] == "NON_EXISTING": + return "REJECT_BUILDER_NOT_FOUND" + if not r["builder_active"]: + return "REJECT_BUILDER_INACTIVE" + if r["builder_version_valid"] != "T": + return "REJECT_WRONG_VERSION" + if not r["builder_can_cover_bid"]: + return "REJECT_UNDERFUNDED" + if r["builder_signature_valid"] != "T": + return "REJECT_BAD_SIGNATURE" + return common() + + +def validate_case(case_dir: Path) -> list[Check]: + pre = decode(case_dir / "pre.ssz_snappy", spec.BeaconState) + signed = decode(case_dir / "execution_payload_bid.ssz_snappy", spec.SignedExecutionPayloadBid) + claimed = _YAML.load((case_dir / "dimensions.yaml").read_text())["claimed"] + actual = recover(pre, signed) + return check_dimensions(claimed, actual) diff --git a/tests/generators/compliance_runners/state_transition/generate_comptests.py b/tests/generators/compliance_runners/state_transition/generate_comptests.py new file mode 100644 index 00000000000..4a5dd350b4c --- /dev/null +++ b/tests/generators/compliance_runners/state_transition/generate_comptests.py @@ -0,0 +1,7 @@ +from __future__ import annotations + +from tests.generators.compliance_runners.state_transition.run import run + + +def test_generate_compliance_tests(comptests_output, handler, profile): + assert run(handler, comptests_output, profile) == 0 diff --git a/tests/generators/compliance_runners/state_transition/materializer.py b/tests/generators/compliance_runners/state_transition/materializer.py new file mode 100644 index 00000000000..8efc54ef3de --- /dev/null +++ b/tests/generators/compliance_runners/state_transition/materializer.py @@ -0,0 +1,86 @@ +"""Shared helpers for materializing state-transition test vectors.""" + +from __future__ import annotations + +import shutil +from typing import Any, TYPE_CHECKING + +from eth_consensus_specs.test.utils.dumper import Dumper +from tests.generators.compliance_runners.gen_base.gen_typing import ( + TestCase, + TestCasePart, + TestCaseResult, +) +from tests.generators.compliance_runners.gen_base.output import dump_test_case_result + +if TYPE_CHECKING: + from pathlib import Path + + +SUITE_NAME = "main" + + +class Materializer: + spec: Any + fork_name: str + preset_name: str + runner_name: str + handler_name: str + + def __init__( + self, + spec: Any, + fork_name: str = "gloas", + preset_name: str = "minimal", + ) -> None: + self.spec = spec + self.fork_name = fork_name + self.preset_name = preset_name + + def materialize_solution(self, solution: Any) -> tuple[dict, list[TestCasePart]]: + raise NotImplementedError("Subclasses must implement this method") + + def write_case(self, dumper: Dumper, output_dir: Path, index: int, solution: Any) -> None: + meta, parts = self.materialize_solution(solution) + claimed = meta.pop("claimed") + test_case = TestCase( + fork_name=self.fork_name, + preset_name=self.preset_name, + runner_name=self.runner_name, + handler_name=self.handler_name, + suite_name=SUITE_NAME, + case_name=f"case_{index:04d}", + ) + test_case.set_output_dir(str(output_dir)) + result = TestCaseResult(test_case=test_case, meta=meta, case_parts=parts) + dump_test_case_result(result, dumper) + dumper.dump_data( + result.test_case.dir, + "dimensions", + {"case": result.test_case.case_name, "claimed": claimed}, + ) + + def materialize_reps( + self, + output_dir: Path, + representatives: list[Any], + *, + case_offset: int = 0, + clean: bool = True, + ) -> int: + """Write representatives into a reference-test directory.""" + suite_dir = ( + output_dir + / self.preset_name + / self.fork_name + / self.runner_name + / self.handler_name + / SUITE_NAME + ) + if clean and suite_dir.exists(): + shutil.rmtree(suite_dir) + dumper = Dumper() + for index, solution in enumerate(representatives): + self.write_case(dumper, output_dir, case_offset + index, solution) + print(f"Generated {len(representatives)} test cases in {output_dir}") + return len(representatives) diff --git a/tests/generators/compliance_runners/state_transition/parent_execution_payload/__init__.py b/tests/generators/compliance_runners/state_transition/parent_execution_payload/__init__.py new file mode 100644 index 00000000000..a6ff4ca12c4 --- /dev/null +++ b/tests/generators/compliance_runners/state_transition/parent_execution_payload/__init__.py @@ -0,0 +1,9 @@ +"""Compliance generator for Gloas parent execution payload processing.""" + +from .coverage import build_profile +from .materializer import ParentExecutionPayloadMaterializer +from .validation import validate_case + +MATERIALIZER = ParentExecutionPayloadMaterializer + +__all__ = ("MATERIALIZER", "build_profile", "validate_case") diff --git a/tests/generators/compliance_runners/state_transition/parent_execution_payload/coverage.py b/tests/generators/compliance_runners/state_transition/parent_execution_payload/coverage.py new file mode 100644 index 00000000000..ab78a73363f --- /dev/null +++ b/tests/generators/compliance_runners/state_transition/parent_execution_payload/coverage.py @@ -0,0 +1,76 @@ +"""Coverage profiles for Gloas ``process_parent_execution_payload``.""" + +from __future__ import annotations + +from pathlib import Path + +from tests.generators.compliance_runners.state_transition.aspect_coverage import ( + build_profile as _build_profile, + enumerate_signatures, +) + +from .materializer import _DIMS + +INPUT_ASPECTS = { + "parent_delivery": [ + "parent_payload_revealed", + "requests_empty", + "requests_root_matches", + ], + "request_caps": [ + "withdrawals_within_cap", + "consolidations_within_cap", + "builder_deposits_within_cap", + "builder_exits_within_cap", + ], + "request_shape": ["deposits_nonempty"], + "payment": ["payment_settlement", "payment_value_nonzero"], +} +TRACE_ASPECT = { + "trace": [ + "requests_empty_checked", + "requests_root_checked", + "withdrawals_cap_checked", + "consolidations_cap_checked", + "builder_deposits_cap_checked", + "builder_exits_cap_checked", + ] +} +OUTCOME_ASPECT = { + "outcome": [ + "outcome", + "state_effected", + "payment_withdrawal_appended", + "payment_slot_cleared", + "dispatches_nonempty_requests", + ] +} +ALL_ASPECTS = {**INPUT_ASPECTS, **TRACE_ASPECT, **OUTCOME_ASPECT} +MODEL = Path(__file__).parent / "models" / "handler_parent_execution_payload.mzn" + + +def _nfaults(record: dict) -> int: + return ( + int(not record["requests_empty"] and not record["parent_payload_revealed"]) + + int(record["parent_payload_revealed"] and not record["requests_root_matches"]) + + int(not record["withdrawals_within_cap"]) + + int(not record["consolidations_within_cap"]) + + int(not record["builder_deposits_within_cap"]) + + int(not record["builder_exits_within_cap"]) + ) + + +def _records(): + return enumerate_signatures(MODEL, _DIMS, ALL_ASPECTS, _nfaults) + + +def build_profile(name: str): + return _build_profile( + _records(), + name, + ALL_ASPECTS, + INPUT_ASPECTS, + OUTCOME_ASPECT, + normal_outcome_aspect=OUTCOME_ASPECT, + exceptional_aspects={**TRACE_ASPECT, **OUTCOME_ASPECT}, + ) diff --git a/tests/generators/compliance_runners/state_transition/parent_execution_payload/materializer.py b/tests/generators/compliance_runners/state_transition/parent_execution_payload/materializer.py new file mode 100644 index 00000000000..eded2eb3397 --- /dev/null +++ b/tests/generators/compliance_runners/state_transition/parent_execution_payload/materializer.py @@ -0,0 +1,206 @@ +"""Materialize aspect-model solutions for parent execution payload processing.""" + +from __future__ import annotations + +from typing import Any, TYPE_CHECKING + +from eth_consensus_specs.test.helpers.genesis import create_genesis_state +from eth_consensus_specs.test.helpers.withdrawals import ( + set_parent_block_empty, + set_parent_block_full, +) +from tests.generators.compliance_runners.state_transition.materializer import Materializer + +if TYPE_CHECKING: + from tests.generators.compliance_runners.gen_base.gen_typing import TestCasePart + +EPOCHS_PAST_GENESIS = 10 +EVICTED_EPOCH_DISTANCE = 5 +DISPATCH_DEPOSITS_COUNT = 20 +FEE_RECIPIENT = b"\xab" * 20 +PAYMENT_VALUE = 50_000_000 + +_DIMS = [ + "parent_payload_revealed", + "requests_empty", + "requests_root_matches", + "withdrawals_within_cap", + "consolidations_within_cap", + "builder_deposits_within_cap", + "builder_exits_within_cap", + "deposits_nonempty", + "dispatches_nonempty_requests", + "payment_settlement", + "payment_value_nonzero", + "requests_empty_checked", + "requests_root_checked", + "withdrawals_cap_checked", + "consolidations_cap_checked", + "builder_deposits_cap_checked", + "builder_exits_cap_checked", + "outcome", + "state_effected", + "payment_withdrawal_appended", + "payment_slot_cleared", +] + + +def _b(solution: Any, name: str) -> bool: + return bool(getattr(solution, name)) + + +def _s(solution: Any, name: str) -> str: + return str(getattr(solution, name)) + + +class ParentExecutionPayloadMaterializer(Materializer): + runner_name = "operations" + handler_name = "parent_execution_payload" + """Build operations-format vectors from model representatives.""" + + def _base_state(self) -> Any: + spec = self.spec + state = create_genesis_state( + spec, + validator_balances=[spec.MAX_EFFECTIVE_BALANCE] * 64, + activation_threshold=spec.MAX_EFFECTIVE_BALANCE, + ) + state.slot = spec.Slot(EPOCHS_PAST_GENESIS * spec.SLOTS_PER_EPOCH) + return state + + def _request_list( + self, + container_type: Any, + request_type: Any, + within_cap: bool, + cap: int, + dispatch_nonempty: bool, + ) -> Any: + count = 1 if dispatch_nonempty else 0 + if not within_cap: + count = cap + 1 + return container_type(data=[request_type()] * count) + + def _requests(self, solution: Any) -> Any: + spec = self.spec + deposits_nonempty = _b(solution, "deposits_nonempty") + deposits_count = DISPATCH_DEPOSITS_COUNT if deposits_nonempty else 0 + return spec.ExecutionRequests( + deposits=spec.DepositRequests(data=[spec.DepositRequest()] * deposits_count), + withdrawals=self._request_list( + spec.WithdrawalRequests, + spec.WithdrawalRequest, + _b(solution, "withdrawals_within_cap"), + spec.MAX_WITHDRAWAL_REQUESTS_PER_PAYLOAD, + deposits_nonempty, + ), + consolidations=self._request_list( + spec.ConsolidationRequests, + spec.ConsolidationRequest, + _b(solution, "consolidations_within_cap"), + spec.MAX_CONSOLIDATION_REQUESTS_PER_PAYLOAD, + deposits_nonempty, + ), + builder_deposits=self._request_list( + spec.BuilderDepositRequests, + spec.BuilderDepositRequest, + _b(solution, "builder_deposits_within_cap"), + spec.MAX_BUILDER_DEPOSIT_REQUESTS_PER_PAYLOAD, + deposits_nonempty, + ), + builder_exits=self._request_list( + spec.BuilderExitRequests, + spec.BuilderExitRequest, + _b(solution, "builder_exits_within_cap"), + spec.MAX_BUILDER_EXIT_REQUESTS_PER_PAYLOAD, + deposits_nonempty, + ), + ) + + def _parent_slot(self, current_epoch: int, settlement: str) -> int: + if settlement == "CURRENT_EPOCH": + parent_epoch = current_epoch + elif settlement == "PREVIOUS_EPOCH": + parent_epoch = current_epoch - 1 + else: + parent_epoch = current_epoch - EVICTED_EPOCH_DISTANCE + return int(self.spec.compute_start_slot_at_epoch(parent_epoch)) + + def _payment_index(self, parent_slot: int, settlement: str) -> int: + offset = parent_slot % int(self.spec.SLOTS_PER_EPOCH) + if settlement == "CURRENT_EPOCH": + return int(self.spec.SLOTS_PER_EPOCH) + offset + return offset + + def materialize_solution(self, solution: Any) -> tuple[dict, list[TestCasePart]]: + spec = self.spec + pre = self._base_state() + if _b(solution, "parent_payload_revealed"): + set_parent_block_full(spec, pre) + else: + set_parent_block_empty(spec, pre) + + requests = self._requests(solution) + requests_root = spec.hash_tree_root(requests) + if _b(solution, "requests_root_matches"): + pre.latest_execution_payload_bid.execution_requests_root = requests_root + else: + mismatched_root = bytes(requests_root) + mismatched_root = bytes([mismatched_root[0] ^ 1]) + mismatched_root[1:] + pre.latest_execution_payload_bid.execution_requests_root = spec.Root(mismatched_root) + + settlement = _s(solution, "payment_settlement") + current_epoch = int(spec.get_current_epoch(pre)) + parent_slot = self._parent_slot(current_epoch, settlement) + parent_bid = pre.latest_execution_payload_bid + parent_bid.slot = spec.Slot(parent_slot) + parent_bid.fee_recipient = spec.ExecutionAddress(FEE_RECIPIENT) + parent_bid.builder_index = spec.BuilderIndex(0) + payment_value = spec.Gwei(PAYMENT_VALUE if _b(solution, "payment_value_nonzero") else 0) + if settlement == "EVICTED": + parent_bid.value = payment_value + else: + payment_index = self._payment_index(parent_slot, settlement) + pre.builder_pending_payments[payment_index] = spec.BuilderPendingPayment( + withdrawal=spec.BuilderPendingWithdrawal( + fee_recipient=spec.ExecutionAddress(FEE_RECIPIENT), + amount=payment_value, + builder_index=spec.BuilderIndex(0), + ) + ) + + availability_index = parent_slot % int(spec.SLOTS_PER_HISTORICAL_ROOT) + pre.execution_payload_availability[availability_index] = 0b0 + + block = spec.BeaconBlock() + block.body.signed_execution_payload_bid.message.parent_block_hash = spec.Hash32( + pre.latest_block_hash + ) + block.body.parent_execution_requests = requests + + post = pre.copy() + try: + spec.process_parent_execution_payload(post, block) + except (AssertionError, IndexError): + post = None + + claimed = { + name: ( + _b(solution, name) + if isinstance(getattr(solution, name), bool) + else _s(solution, name) + ) + for name in _DIMS + } + parts: list[TestCasePart] = [ + ("pre", "ssz", pre.encode_bytes()), + ("block", "ssz", block.encode_bytes()), + ] + if post is not None: + parts.append(("post", "ssz", post.encode_bytes())) + meta = { + "description": f"process_parent_execution_payload: {claimed['outcome']}", + "bls_setting": 1, + "claimed": claimed, + } + return meta, parts diff --git a/tests/generators/compliance_runners/state_transition/parent_execution_payload/models/handler_parent_execution_payload.mzn b/tests/generators/compliance_runners/state_transition/parent_execution_payload/models/handler_parent_execution_payload.mzn new file mode 100644 index 00000000000..9f11f97f638 --- /dev/null +++ b/tests/generators/compliance_runners/state_transition/parent_execution_payload/models/handler_parent_execution_payload.mzn @@ -0,0 +1,105 @@ +% Relational model: process_parent_execution_payload (Gloas). +% +% The request-cap predicates remain concrete even when an earlier gate rejects: +% they describe recoverable input properties. The *_checked dimensions model +% the handler's short-circuit trace separately. +% +% Spec: specs/gloas/beacon-chain.md process_parent_execution_payload and +% apply_parent_execution_payload. + +enum PaymentSettlement = { CURRENT_EPOCH, PREVIOUS_EPOCH, EVICTED }; +enum Outcome = { + REJECT_NONEMPTY_REQUESTS_FOR_EMPTY_PARENT, + EMPTY_PARENT_NOOP, + REJECT_REQUESTS_ROOT, + REJECT_WITHDRAWALS_CAP, + REJECT_CONSOLIDATIONS_CAP, + REJECT_BUILDER_DEPOSITS_CAP, + REJECT_BUILDER_EXITS_CAP, + APPLY_CURRENT_WITH_WITHDRAWAL, + APPLY_CURRENT_NO_WITHDRAWAL, + APPLY_PREVIOUS_WITH_WITHDRAWAL, + APPLY_EVICTED_WITH_WITHDRAWAL, + APPLY_EVICTED_NO_WITHDRAWAL +}; + +var bool: parent_payload_revealed; +var bool: requests_empty; +var bool: requests_root_matches; +var bool: withdrawals_within_cap; +var bool: consolidations_within_cap; +var bool: builder_deposits_within_cap; +var bool: builder_exits_within_cap; +var bool: deposits_nonempty; +var bool: dispatches_nonempty_requests; +var PaymentSettlement: payment_settlement; +var bool: payment_value_nonzero; + +% The materializer puts one item in every request list when a non-empty shape +% is requested. An over-cap list is necessarily non-empty. +constraint requests_empty <-> + withdrawals_within_cap /\ consolidations_within_cap /\ + builder_deposits_within_cap /\ builder_exits_within_cap /\ + not deposits_nonempty; + +% A previous-epoch zero-value case has the same observable branch effect as the +% current-epoch zero-value case, apart from the circular-buffer index. +constraint payment_settlement == PREVIOUS_EPOCH -> payment_value_nonzero; + +var bool: requests_empty_checked; +var bool: requests_root_checked; +var bool: withdrawals_cap_checked; +var bool: consolidations_cap_checked; +var bool: builder_deposits_cap_checked; +var bool: builder_exits_cap_checked; + +constraint requests_empty_checked <-> not parent_payload_revealed; +constraint requests_root_checked <-> parent_payload_revealed; +constraint withdrawals_cap_checked <-> + parent_payload_revealed /\ requests_root_matches; +constraint consolidations_cap_checked <-> + withdrawals_cap_checked /\ withdrawals_within_cap; +constraint builder_deposits_cap_checked <-> + consolidations_cap_checked /\ consolidations_within_cap; +constraint builder_exits_cap_checked <-> + builder_deposits_cap_checked /\ builder_deposits_within_cap; +constraint dispatches_nonempty_requests <-> + builder_exits_cap_checked /\ builder_exits_within_cap /\ not requests_empty; + +var Outcome: outcome; +constraint outcome = + if not parent_payload_revealed then + if requests_empty then EMPTY_PARENT_NOOP + else REJECT_NONEMPTY_REQUESTS_FOR_EMPTY_PARENT endif + elseif not requests_root_matches then REJECT_REQUESTS_ROOT + elseif not withdrawals_within_cap then REJECT_WITHDRAWALS_CAP + elseif not consolidations_within_cap then REJECT_CONSOLIDATIONS_CAP + elseif not builder_deposits_within_cap then REJECT_BUILDER_DEPOSITS_CAP + elseif not builder_exits_within_cap then REJECT_BUILDER_EXITS_CAP + elseif payment_settlement == CURRENT_EPOCH then + if payment_value_nonzero then APPLY_CURRENT_WITH_WITHDRAWAL + else APPLY_CURRENT_NO_WITHDRAWAL endif + elseif payment_settlement == PREVIOUS_EPOCH then + APPLY_PREVIOUS_WITH_WITHDRAWAL + else + if payment_value_nonzero then APPLY_EVICTED_WITH_WITHDRAWAL + else APPLY_EVICTED_NO_WITHDRAWAL endif + endif; + +set of Outcome: APPLIED = { + APPLY_CURRENT_WITH_WITHDRAWAL, + APPLY_CURRENT_NO_WITHDRAWAL, + APPLY_PREVIOUS_WITH_WITHDRAWAL, + APPLY_EVICTED_WITH_WITHDRAWAL, + APPLY_EVICTED_NO_WITHDRAWAL +}; + +var bool: state_effected; +var bool: payment_withdrawal_appended; +var bool: payment_slot_cleared; +constraint state_effected <-> outcome in APPLIED; +constraint payment_withdrawal_appended <-> + outcome in APPLIED /\ payment_value_nonzero; +constraint payment_slot_cleared <-> + outcome in APPLIED /\ + payment_settlement in {CURRENT_EPOCH, PREVIOUS_EPOCH}; diff --git a/tests/generators/compliance_runners/state_transition/parent_execution_payload/validation.py b/tests/generators/compliance_runners/state_transition/parent_execution_payload/validation.py new file mode 100644 index 00000000000..79f8ce7a029 --- /dev/null +++ b/tests/generators/compliance_runners/state_transition/parent_execution_payload/validation.py @@ -0,0 +1,120 @@ +"""Independent validation for parent-execution-payload compliance vectors.""" + +from __future__ import annotations + +from typing import Any, TYPE_CHECKING + +from ruamel.yaml import YAML + +from eth_consensus_specs.gloas import minimal as spec +from tests.generators.compliance_runners.state_transition.validation import check_dimensions, decode + +if TYPE_CHECKING: + from pathlib import Path + + from tests.generators.compliance_runners.state_transition.validation import Check + +_YAML = YAML(typ="safe") + + +def _payment_dimensions(pre: Any) -> tuple[str, bool]: + parent_bid = pre.latest_execution_payload_bid + parent_slot = int(parent_bid.slot) + parent_epoch = int(spec.compute_epoch_at_slot(parent_slot)) + current_epoch = int(spec.get_current_epoch(pre)) + if parent_epoch == current_epoch: + settlement = "CURRENT_EPOCH" + payment_index = int(spec.SLOTS_PER_EPOCH) + parent_slot % int(spec.SLOTS_PER_EPOCH) + nonzero = int(pre.builder_pending_payments[payment_index].withdrawal.amount) > 0 + elif parent_epoch == int(spec.get_previous_epoch(pre)): + settlement = "PREVIOUS_EPOCH" + payment_index = parent_slot % int(spec.SLOTS_PER_EPOCH) + nonzero = int(pre.builder_pending_payments[payment_index].withdrawal.amount) > 0 + else: + settlement = "EVICTED" + nonzero = int(parent_bid.value) > 0 + return settlement, nonzero + + +def recover(pre: Any, block: Any) -> dict[str, Any]: + """Recover input, trace, outcome, and effect dimensions from a vector.""" + parent_bid = pre.latest_execution_payload_bid + bid = block.body.signed_execution_payload_bid.message + requests = block.body.parent_execution_requests + + revealed = bid.parent_block_hash == parent_bid.block_hash + requests_empty = requests == spec.ExecutionRequests() + root_matches = spec.hash_tree_root(requests) == parent_bid.execution_requests_root + withdrawals_ok = len(requests.withdrawals) <= spec.MAX_WITHDRAWAL_REQUESTS_PER_PAYLOAD + consolidations_ok = len(requests.consolidations) <= spec.MAX_CONSOLIDATION_REQUESTS_PER_PAYLOAD + builder_deposits_ok = ( + len(requests.builder_deposits) <= spec.MAX_BUILDER_DEPOSIT_REQUESTS_PER_PAYLOAD + ) + builder_exits_ok = len(requests.builder_exits) <= spec.MAX_BUILDER_EXIT_REQUESTS_PER_PAYLOAD + settlement, value_nonzero = _payment_dimensions(pre) + + requests_empty_checked = not revealed + requests_root_checked = revealed + withdrawals_checked = revealed and root_matches + consolidations_checked = withdrawals_checked and withdrawals_ok + builder_deposits_checked = consolidations_checked and consolidations_ok + builder_exits_checked = builder_deposits_checked and builder_deposits_ok + dispatches = builder_exits_checked and builder_exits_ok and not requests_empty + + if not revealed: + outcome = ( + "EMPTY_PARENT_NOOP" if requests_empty else "REJECT_NONEMPTY_REQUESTS_FOR_EMPTY_PARENT" + ) + elif not root_matches: + outcome = "REJECT_REQUESTS_ROOT" + elif not withdrawals_ok: + outcome = "REJECT_WITHDRAWALS_CAP" + elif not consolidations_ok: + outcome = "REJECT_CONSOLIDATIONS_CAP" + elif not builder_deposits_ok: + outcome = "REJECT_BUILDER_DEPOSITS_CAP" + elif not builder_exits_ok: + outcome = "REJECT_BUILDER_EXITS_CAP" + elif settlement == "CURRENT_EPOCH": + outcome = ( + "APPLY_CURRENT_WITH_WITHDRAWAL" if value_nonzero else "APPLY_CURRENT_NO_WITHDRAWAL" + ) + elif settlement == "PREVIOUS_EPOCH": + outcome = "APPLY_PREVIOUS_WITH_WITHDRAWAL" + else: + outcome = ( + "APPLY_EVICTED_WITH_WITHDRAWAL" if value_nonzero else "APPLY_EVICTED_NO_WITHDRAWAL" + ) + + applied = outcome.startswith("APPLY_") + return { + "parent_payload_revealed": revealed, + "requests_empty": requests_empty, + "requests_root_matches": root_matches, + "withdrawals_within_cap": withdrawals_ok, + "consolidations_within_cap": consolidations_ok, + "builder_deposits_within_cap": builder_deposits_ok, + "builder_exits_within_cap": builder_exits_ok, + "deposits_nonempty": len(requests.deposits) > 0, + "dispatches_nonempty_requests": dispatches, + "payment_settlement": settlement, + "payment_value_nonzero": value_nonzero, + "requests_empty_checked": requests_empty_checked, + "requests_root_checked": requests_root_checked, + "withdrawals_cap_checked": withdrawals_checked, + "consolidations_cap_checked": consolidations_checked, + "builder_deposits_cap_checked": builder_deposits_checked, + "builder_exits_cap_checked": builder_exits_checked, + "outcome": outcome, + "state_effected": applied, + "payment_withdrawal_appended": applied and value_nonzero, + "payment_slot_cleared": applied and settlement in {"CURRENT_EPOCH", "PREVIOUS_EPOCH"}, + } + + +def validate_case(case_dir: Path) -> list[Check]: + pre = decode(case_dir / "pre.ssz_snappy", spec.BeaconState) + block = decode(case_dir / "block.ssz_snappy", spec.BeaconBlock) + claimed = _YAML.load((case_dir / "dimensions.yaml").read_text())["claimed"] + actual = recover(pre, block) + return check_dimensions(claimed, actual) diff --git a/tests/generators/compliance_runners/state_transition/payload_attestation/__init__.py b/tests/generators/compliance_runners/state_transition/payload_attestation/__init__.py new file mode 100644 index 00000000000..5dcf7b42ef1 --- /dev/null +++ b/tests/generators/compliance_runners/state_transition/payload_attestation/__init__.py @@ -0,0 +1,9 @@ +"""Aspect-based compliance runner for Gloas payload attestations.""" + +from .coverage import build_profile +from .materializer import PayloadAttestationMaterializer +from .validation import validate_case + +MATERIALIZER = PayloadAttestationMaterializer + +__all__ = ("MATERIALIZER", "build_profile", "validate_case") diff --git a/tests/generators/compliance_runners/state_transition/payload_attestation/coverage.py b/tests/generators/compliance_runners/state_transition/payload_attestation/coverage.py new file mode 100644 index 00000000000..e9ed23319f4 --- /dev/null +++ b/tests/generators/compliance_runners/state_transition/payload_attestation/coverage.py @@ -0,0 +1,37 @@ +"""Coverage profiles for Gloas ``process_payload_attestation``.""" + +from __future__ import annotations + +from pathlib import Path + +from tests.generators.compliance_runners.state_transition.aspect_coverage import ( + build_profile as _build_profile, + enumerate_signatures, +) + +from .materializer import _DIMS + +INPUT_ASPECTS = { + "block_context": ["parent_root_matches", "slot_is_previous"], + "participants": ["attesting_indices_profile", "attesting_indices_nonempty", "signature_valid"], +} +OUTCOME_ASPECT = {"outcome": ["outcome"]} +ALL_ASPECTS = {**INPUT_ASPECTS, **OUTCOME_ASPECT} +MODEL = Path(__file__).parent / "models" / "handler_payload_attestation.mzn" + + +def _nfaults(r: dict) -> int: + return ( + int(not r["parent_root_matches"]) + + int(not r["slot_is_previous"]) + + int(not r["attesting_indices_nonempty"]) + + int(r["signature_valid"] == "F") + ) + + +def _recs(): + return enumerate_signatures(MODEL, _DIMS, ALL_ASPECTS, _nfaults) + + +def build_profile(name): + return _build_profile(_recs(), name, ALL_ASPECTS, INPUT_ASPECTS, OUTCOME_ASPECT) diff --git a/tests/generators/compliance_runners/state_transition/payload_attestation/materializer.py b/tests/generators/compliance_runners/state_transition/payload_attestation/materializer.py new file mode 100644 index 00000000000..02983fa85e5 --- /dev/null +++ b/tests/generators/compliance_runners/state_transition/payload_attestation/materializer.py @@ -0,0 +1,92 @@ +"""Materialize aspect-model solutions for Gloas payload attestations.""" + +from __future__ import annotations + +from typing import Any, TYPE_CHECKING + +from eth_consensus_specs.test.helpers.genesis import create_genesis_state +from eth_consensus_specs.test.helpers.payload_attestation import prepare_signed_payload_attestation +from tests.generators.compliance_runners.state_transition.materializer import Materializer + +if TYPE_CHECKING: + from tests.generators.compliance_runners.gen_base.gen_typing import TestCasePart + +_DIMS = [ + "parent_root_matches", + "slot_is_previous", + "attesting_indices_profile", + "attesting_indices_nonempty", + "signature_valid", + "outcome", +] + + +def _s(sol: Any, name: str) -> str: + return str(getattr(sol, name)) + + +def _b(sol: Any, name: str) -> bool: + return bool(getattr(sol, name)) + + +class PayloadAttestationMaterializer(Materializer): + runner_name = "operations" + handler_name = "payload_attestation" + + def _base_state(self) -> Any: + state = create_genesis_state( + self.spec, + validator_balances=[self.spec.MAX_EFFECTIVE_BALANCE] * 64, + activation_threshold=self.spec.MAX_EFFECTIVE_BALANCE, + ) + self.spec.process_slots(state, self.spec.Slot(3)) + return state + + def materialize_solution(self, sol: Any) -> tuple[dict, list[TestCasePart]]: + spec, pre = self.spec, self._base_state() + slot = pre.slot - 1 if _b(sol, "slot_is_previous") else pre.slot + root = ( + pre.latest_block_header.parent_root + if _b(sol, "parent_root_matches") + else spec.Root(b"\x42" * 32) + ) + ptc = spec.get_ptc(pre, slot) + indices_profile = _s(sol, "attesting_indices_profile") + if indices_profile == "EMPTY": + attesting_indices = [] + elif indices_profile == "PARTIAL": + attesting_indices = ptc[: max(1, len(ptc) // 2)] + elif indices_profile == "ALL": + attesting_indices = None + else: + raise ValueError(f"unknown attesting indices profile: {indices_profile}") + nonempty = _b(sol, "attesting_indices_nonempty") + operation = prepare_signed_payload_attestation( + spec, + pre, + slot=slot, + beacon_block_root=root, + attesting_indices=attesting_indices, + valid_signature=nonempty and _s(sol, "signature_valid") == "T", + ) + post = pre.copy() + try: + spec.process_payload_attestation(post, operation) + except (AssertionError, IndexError): + post = None + claimed = { + name: (_b(sol, name) if isinstance(getattr(sol, name), bool) else _s(sol, name)) + for name in _DIMS + } + parts: list[TestCasePart] = [ + ("pre", "ssz", pre.encode_bytes()), + ("payload_attestation", "ssz", operation.encode_bytes()), + ] + if post is not None: + parts.append(("post", "ssz", post.encode_bytes())) + meta = { + "description": f"process_payload_attestation: {claimed['outcome']}", + "bls_setting": 1, + "claimed": claimed, + } + return meta, parts diff --git a/tests/generators/compliance_runners/state_transition/payload_attestation/models/handler_payload_attestation.mzn b/tests/generators/compliance_runners/state_transition/payload_attestation/models/handler_payload_attestation.mzn new file mode 100644 index 00000000000..bc5e097dc01 --- /dev/null +++ b/tests/generators/compliance_runners/state_transition/payload_attestation/models/handler_payload_attestation.mzn @@ -0,0 +1,33 @@ +% Handler model: process_payload_attestation (Gloas). +% +% An aggregate signature has no semantic truth value when its indexed +% attestation is empty: the helper rejects before aggregate verification. + +include "../../aspects/signed_message.mzn"; + +enum Outcome = { + REJECT_PARENT_ROOT, + REJECT_SLOT, + REJECT_EMPTY, + REJECT_SIGNATURE, + ACCEPT +}; + +enum AttestingIndicesProfile = { EMPTY, PARTIAL, ALL }; + +var bool: parent_root_matches; +var bool: slot_is_previous; +var AttestingIndicesProfile: attesting_indices_profile; +var bool: attesting_indices_nonempty; +constraint attesting_indices_nonempty <-> attesting_indices_profile != EMPTY; +var Dim: signature_valid; +constraint signed_message_ok(signature_valid, attesting_indices_nonempty); +constraint attesting_indices_nonempty -> signature_valid in BOOLV; + +var Outcome: outcome; +constraint outcome = + if not parent_root_matches then REJECT_PARENT_ROOT + elseif not slot_is_previous then REJECT_SLOT + elseif not attesting_indices_nonempty then REJECT_EMPTY + elseif signature_valid != T then REJECT_SIGNATURE + else ACCEPT endif; diff --git a/tests/generators/compliance_runners/state_transition/payload_attestation/validation.py b/tests/generators/compliance_runners/state_transition/payload_attestation/validation.py new file mode 100644 index 00000000000..35182b0c9db --- /dev/null +++ b/tests/generators/compliance_runners/state_transition/payload_attestation/validation.py @@ -0,0 +1,62 @@ +"""Independent validation for Gloas payload-attestation compliance vectors.""" + +from __future__ import annotations + +from typing import Any, TYPE_CHECKING + +from ruamel.yaml import YAML + +from eth_consensus_specs.gloas import minimal as spec +from tests.generators.compliance_runners.state_transition.validation import check_dimensions, decode + +if TYPE_CHECKING: + from pathlib import Path + + from tests.generators.compliance_runners.state_transition.validation import Check + +_YAML = YAML(typ="safe") + + +def recover(pre: Any, operation: Any) -> dict[str, Any]: + data = operation.data + indexed = spec.get_indexed_payload_attestation(pre, operation) + nonempty = len(indexed.attesting_indices) > 0 + aggregation_bits = list(operation.aggregation_bits) + if not any(aggregation_bits): + attesting_indices_profile = "EMPTY" + elif all(aggregation_bits): + attesting_indices_profile = "ALL" + else: + attesting_indices_profile = "PARTIAL" + signature_valid = ( + "NA" + if not nonempty + else ("T" if spec.is_valid_indexed_payload_attestation(pre, indexed) else "F") + ) + result = { + "parent_root_matches": data.beacon_block_root == pre.latest_block_header.parent_root, + "slot_is_previous": data.slot + 1 == pre.slot, + "attesting_indices_profile": attesting_indices_profile, + "attesting_indices_nonempty": nonempty, + "signature_valid": signature_valid, + } + if not result["parent_root_matches"]: + outcome = "REJECT_PARENT_ROOT" + elif not result["slot_is_previous"]: + outcome = "REJECT_SLOT" + elif not nonempty: + outcome = "REJECT_EMPTY" + elif signature_valid != "T": + outcome = "REJECT_SIGNATURE" + else: + outcome = "ACCEPT" + result["outcome"] = outcome + return result + + +def validate_case(case_dir: Path) -> list[Check]: + pre = decode(case_dir / "pre.ssz_snappy", spec.BeaconState) + operation = decode(case_dir / "payload_attestation.ssz_snappy", spec.PayloadAttestation) + claimed = _YAML.load((case_dir / "dimensions.yaml").read_text())["claimed"] + actual = recover(pre, operation) + return check_dimensions(claimed, actual) diff --git a/tests/generators/compliance_runners/state_transition/pending_deposits/__init__.py b/tests/generators/compliance_runners/state_transition/pending_deposits/__init__.py new file mode 100644 index 00000000000..e3cb0edd8b9 --- /dev/null +++ b/tests/generators/compliance_runners/state_transition/pending_deposits/__init__.py @@ -0,0 +1,9 @@ +"""Aspect-based compliance generator for ``process_pending_deposits``.""" + +from .coverage import build_profile +from .materializer import PendingDepositsMaterializer +from .validation import validate_case + +MATERIALIZER = PendingDepositsMaterializer + +__all__ = ("MATERIALIZER", "build_profile", "validate_case") diff --git a/tests/generators/compliance_runners/state_transition/pending_deposits/coverage.py b/tests/generators/compliance_runners/state_transition/pending_deposits/coverage.py new file mode 100644 index 00000000000..baf4aa2d834 --- /dev/null +++ b/tests/generators/compliance_runners/state_transition/pending_deposits/coverage.py @@ -0,0 +1,75 @@ +"""Coverage profiles for Gloas ``process_pending_deposits``.""" + +from __future__ import annotations + +from pathlib import Path + +from tests.generators.compliance_runners.state_transition.aspect_coverage import ( + build_profile as _build_profile, + enumerate_signatures, +) + +from .materializer import _DIMS + +# Fine-grained aspects remain part of the signature used by `all`; the normal +# profile uses the composite validator_state factor. +FINE_QUEUE_ASPECT = { + "queue_layout": ["queue_layout", "secondary_role"], + "finalization_and_limit": ["primary_reached"], +} +FINE_VALIDATOR_ASPECT = { + "validator_membership": ["validator_pubkey_found"], + "validator_lifecycle": ["validator_active", "validator_exiting"], + "withdrawable_boundary": ["withdrawable_epoch_to_next_epoch"], +} +FINE_DEPOSIT_ASPECT = {"deposit_signature": ["deposit_signature_valid"]} +FINE_CHURN_ASPECT = { + "carried_churn": ["initial_churn"], + "amount_to_available": ["primary_amount_to_available"], + "second_amount_to_remaining": ["second_amount_to_remaining"], + "state_effect": ["churn_effect"], +} +OUTCOME_ASPECT = {"outcome": ["outcome"]} +FINE_ALL_ASPECTS = { + **FINE_QUEUE_ASPECT, + **FINE_VALIDATOR_ASPECT, + **FINE_DEPOSIT_ASPECT, + **FINE_CHURN_ASPECT, + **OUTCOME_ASPECT, +} +QUEUE_ASPECT = { + "queue_layout": ["queue_layout", "secondary_role"], + "finalization_and_limit": ["primary_reached"], +} +VALIDATOR_ASPECT = { + "validator_state": [ + "validator_pubkey_found", + "validator_active", + "validator_exiting", + "withdrawable_epoch_to_next_epoch", + ], +} +DEPOSIT_ASPECT = {"deposit_signature": ["deposit_signature_valid"]} +CHURN_ASPECT = FINE_CHURN_ASPECT +ALL_ASPECTS = { + **QUEUE_ASPECT, + **VALIDATOR_ASPECT, + **DEPOSIT_ASPECT, + **CHURN_ASPECT, + **OUTCOME_ASPECT, +} +MODEL = Path(__file__).parent / "models" / "handler_pending_deposits.mzn" + + +def _recs(): + return enumerate_signatures(MODEL, _DIMS, FINE_ALL_ASPECTS, _nfaults) + + +def _nfaults(_r: dict) -> int: + return 0 + + +def build_profile(name: str): + return _build_profile( + _recs(), name, ALL_ASPECTS, ALL_ASPECTS, {"outcome": ["outcome"]}, normal_t=3 + ) diff --git a/tests/generators/compliance_runners/state_transition/pending_deposits/materializer.py b/tests/generators/compliance_runners/state_transition/pending_deposits/materializer.py new file mode 100644 index 00000000000..0a27c27030b --- /dev/null +++ b/tests/generators/compliance_runners/state_transition/pending_deposits/materializer.py @@ -0,0 +1,152 @@ +"""Materialize Gloas ``process_pending_deposits`` epoch-processing vectors.""" + +from __future__ import annotations + +from typing import Any, TYPE_CHECKING + +from eth_consensus_specs.test.helpers.deposits import prepare_pending_deposit +from eth_consensus_specs.test.helpers.genesis import create_genesis_state +from tests.generators.compliance_runners.state_transition.materializer import Materializer + +if TYPE_CHECKING: + from tests.generators.compliance_runners.gen_base.gen_typing import TestCasePart + +_DIMS = [ + "queue_layout", + "secondary_role", + "primary_reached", + "primary_role", + "deposit_signature_valid", + "validator_pubkey_found", + "validator_active", + "validator_exiting", + "withdrawable_epoch_to_next_epoch", + "initial_churn", + "primary_amount_to_available", + "second_amount_to_remaining", + "churn_effect", + "outcome", +] +# Minimal Gloas reaches the activation cap at 64 validators. Twice that count +# makes exit churn strictly larger, so GT cases distinguish activation-only +# deposit churn from the uncapped exit churn. +NUM_VALIDATORS = 128 + + +class PendingDepositsMaterializer(Materializer): + runner_name = "epoch_processing" + handler_name = "pending_deposits" + + def _base_state(self) -> Any: + state = create_genesis_state( + self.spec, + validator_balances=[self.spec.MAX_EFFECTIVE_BALANCE] * NUM_VALIDATORS, + activation_threshold=self.spec.MAX_EFFECTIVE_BALANCE, + ) + # Pending deposits can be unfinalized only after the chain has advanced. + # Keep finality at genesis: slot 1 is then in the past but unfinalized. + state.slot = self.spec.Slot(self.spec.SLOTS_PER_EPOCH) + return state + + def _deposit( + self, + state: Any, + validator_index: int, + amount: Any, + *, + signed: bool = True, + slot: Any = None, + ): + return prepare_pending_deposit( + self.spec, + validator_index, + amount, + signed=signed, + slot=self.spec.GENESIS_SLOT if slot is None else slot, + ) + + def materialize_solution(self, solution: Any) -> tuple[dict, list[TestCasePart]]: + spec = self.spec + pre = self._base_state() + layout = str(solution.queue_layout) + role = str(solution.primary_role) + carry = str(solution.initial_churn) + comparison = str(solution.primary_amount_to_available) + second_comparison = str(solution.second_amount_to_remaining) + next_epoch = spec.Epoch(spec.get_current_epoch(pre) + 1) + + if carry == "CARRY_NONZERO": + pre.deposit_balance_to_consume = spec.EFFECTIVE_BALANCE_INCREMENT + available = pre.deposit_balance_to_consume + spec.get_activation_churn_limit(pre) + amount = { + "LT": spec.EFFECTIVE_BALANCE_INCREMENT, + "EQ": available, + "GT": available + spec.EFFECTIVE_BALANCE_INCREMENT, + }.get(comparison, spec.EFFECTIVE_BALANCE_INCREMENT) + + def set_role(index: int, entry_role: str) -> None: + validator = pre.validators[index] + if entry_role == "EXITING": + validator.exit_epoch = spec.Epoch(0) + validator.withdrawable_epoch = ( + spec.Epoch(next_epoch + 1) + if str(solution.withdrawable_epoch_to_next_epoch) == "GT" + else next_epoch + ) + elif entry_role == "WITHDRAWN": + validator.exit_epoch = spec.Epoch(0) + validator.withdrawable_epoch = spec.Epoch(next_epoch - 1) + + def add_primary(entry_role: str, *, slot: Any = None) -> None: + if entry_role in {"ACTIVE", "EXITING", "WITHDRAWN"}: + set_role(0, entry_role) + pre.pending_deposits.append(self._deposit(pre, 0, amount, slot=slot)) + else: + pre.pending_deposits.append( + self._deposit( + pre, NUM_VALIDATORS, amount, signed=entry_role == "NEW_VALID", slot=slot + ) + ) + + if layout == "FIRST_UNFINALIZED": + add_primary(role, slot=spec.Slot(1)) + elif layout == "SINGLE": + add_primary(role) + elif layout == "POSTPONE_THEN_ACTIVE": + add_primary("EXITING") + pre.pending_deposits.append(self._deposit(pre, 1, spec.EFFECTIVE_BALANCE_INCREMENT)) + elif layout == "ACTIVE_THEN_UNFINALIZED": + add_primary(role) + pre.pending_deposits.append( + self._deposit(pre, 1, spec.EFFECTIVE_BALANCE_INCREMENT, slot=spec.Slot(1)) + ) + elif layout in {"TWO_PROCESSABLE", "INVALID_THEN_PROCESSABLE"}: + add_primary("NEW_INVALID" if layout == "INVALID_THEN_PROCESSABLE" else role) + remaining = available - amount + second_amount = { + "LT": spec.EFFECTIVE_BALANCE_INCREMENT, + "EQ": remaining, + "GT": remaining + spec.EFFECTIVE_BALANCE_INCREMENT, + }[second_comparison] + pre.pending_deposits.append(self._deposit(pre, 1, second_amount)) + elif layout == "LIMIT_AFTER_WITHDRAWN": + set_role(0, "WITHDRAWN") + for _ in range(int(spec.MAX_PENDING_DEPOSITS_PER_EPOCH)): + pre.pending_deposits.append(self._deposit(pre, 0, spec.EFFECTIVE_BALANCE_INCREMENT)) + add_primary(role) + elif layout != "EMPTY": + raise ValueError(f"unknown queue layout: {layout}") + + post = pre.copy() + spec.process_pending_deposits(post) + claimed = { + name: bool(value) if isinstance(value := getattr(solution, name), bool) else str(value) + for name in _DIMS + } + meta = { + "description": f"process_pending_deposits: {claimed['outcome']}", + "bls_setting": 1, + "claimed": claimed, + } + parts = [("pre", "ssz", pre.encode_bytes()), ("post", "ssz", post.encode_bytes())] + return meta, parts diff --git a/tests/generators/compliance_runners/state_transition/pending_deposits/models/handler_pending_deposits.mzn b/tests/generators/compliance_runners/state_transition/pending_deposits/models/handler_pending_deposits.mzn new file mode 100644 index 00000000000..4f192607539 --- /dev/null +++ b/tests/generators/compliance_runners/state_transition/pending_deposits/models/handler_pending_deposits.mzn @@ -0,0 +1,76 @@ +% Relational coverage model: process_pending_deposits (gloas). +% +% `queue_layout` is a bounded materialization shape, not an outcome. The +% independently constrained lifecycle, finalization, carried-churn, and churn +% comparison dimensions select semantic situations within that shape. + +include "../../aspects/base.mzn"; +include "../../aspects/validator_membership.mzn"; +include "../../aspects/validator_lifecycle.mzn"; + +enum QueueLayout = { EMPTY, FIRST_UNFINALIZED, SINGLE, POSTPONE_THEN_ACTIVE, + ACTIVE_THEN_UNFINALIZED, LIMIT_AFTER_WITHDRAWN, + TWO_PROCESSABLE, INVALID_THEN_PROCESSABLE }; +enum PrimaryRole = { ACTIVE, EXITING, WITHDRAWN, NEW_VALID, NEW_INVALID, ROLE_NA }; +enum SecondaryRole = { SECOND_NONE, SECOND_ACTIVE, SECOND_UNFINALIZED, SECOND_PROCESSABLE }; +enum ChurnCarry = { CARRY_ZERO, CARRY_NONZERO }; +enum ChurnEffect = { CHURN_CLEARED, CHURN_RETAINED }; +enum Outcome = { EMPTY_QUEUE, STOP_UNFINALIZED, STOP_PER_EPOCH_LIMIT, + STOP_CHURN_LIMIT, PROCESSED }; + +var QueueLayout: queue_layout; +var PrimaryRole: primary_role; +var SecondaryRole: secondary_role; +var ChurnCarry: initial_churn; +var BOOLV_NA: deposit_signature_valid; +var CMP_NA: primary_amount_to_available; +var CMP_NA: second_amount_to_remaining; +var CMP_NA: withdrawable_epoch_to_next_epoch; +var BOOLV_NA: validator_active; +var BOOLV_NA: validator_exiting; +var bool: primary_reached; +var Outcome: outcome; +var ChurnEffect: churn_effect; + +% Queue layout binds the fixed entry positions; role and amount dimensions +% remain independent wherever the protocol can observe them. +constraint (queue_layout == EMPTY) <-> (primary_role == ROLE_NA); +constraint (queue_layout == FIRST_UNFINALIZED) -> primary_role != ROLE_NA; +constraint (queue_layout in {SINGLE, ACTIVE_THEN_UNFINALIZED, TWO_PROCESSABLE}) -> primary_role in {ACTIVE, NEW_VALID}; +constraint (queue_layout == INVALID_THEN_PROCESSABLE) -> primary_role == NEW_INVALID; +constraint (queue_layout == POSTPONE_THEN_ACTIVE) -> primary_role == EXITING; +constraint (queue_layout == LIMIT_AFTER_WITHDRAWN) -> primary_role == WITHDRAWN; +constraint (queue_layout == POSTPONE_THEN_ACTIVE) <-> (secondary_role == SECOND_ACTIVE); +constraint (queue_layout == ACTIVE_THEN_UNFINALIZED) <-> (secondary_role == SECOND_UNFINALIZED); +constraint (queue_layout in {TWO_PROCESSABLE, INVALID_THEN_PROCESSABLE}) <-> (secondary_role == SECOND_PROCESSABLE); +constraint (queue_layout in {EMPTY, FIRST_UNFINALIZED, SINGLE, LIMIT_AFTER_WITHDRAWN}) <-> (secondary_role == SECOND_NONE); + +constraint validator_pubkey_found <-> primary_role in {ACTIVE, EXITING, WITHDRAWN}; +constraint validator_lifecycle_ok(validator_active, validator_exiting, validator_pubkey_found); +constraint (primary_role == EXITING) -> (validator_exiting == T); +constraint (primary_role == WITHDRAWN) -> (validator_exiting == T); +constraint (primary_role in {EXITING, WITHDRAWN}) -> validator_active == F; +constraint (primary_role == ACTIVE) -> (validator_exiting == F /\ validator_active == T); + +constraint (withdrawable_epoch_to_next_epoch == NA) <-> not (primary_role in {EXITING, WITHDRAWN}); +constraint (primary_role == WITHDRAWN) -> withdrawable_epoch_to_next_epoch == LT; +constraint (primary_role == EXITING) -> withdrawable_epoch_to_next_epoch in {EQ, GT}; + +constraint (deposit_signature_valid == T) <-> primary_role == NEW_VALID; +constraint (deposit_signature_valid == F) <-> primary_role == NEW_INVALID; +constraint (deposit_signature_valid == NA) <-> not (primary_role in {NEW_VALID, NEW_INVALID}); +constraint (primary_amount_to_available == NA) <-> (primary_role in {EXITING, WITHDRAWN, ROLE_NA}); +constraint (second_amount_to_remaining == NA) <-> not (queue_layout in {TWO_PROCESSABLE, INVALID_THEN_PROCESSABLE}); +constraint (queue_layout in {TWO_PROCESSABLE, INVALID_THEN_PROCESSABLE}) -> primary_amount_to_available == LT; +constraint primary_reached <-> not (queue_layout in {EMPTY, FIRST_UNFINALIZED, LIMIT_AFTER_WITHDRAWN}); + +% A new invalid deposit still passes the churn check before being dropped. +constraint (queue_layout == FIRST_UNFINALIZED) -> outcome == STOP_UNFINALIZED; +constraint (queue_layout == LIMIT_AFTER_WITHDRAWN) -> outcome == STOP_PER_EPOCH_LIMIT; +constraint (queue_layout == EMPTY) -> outcome == EMPTY_QUEUE; +constraint (primary_reached /\ primary_amount_to_available == GT) -> outcome == STOP_CHURN_LIMIT; +constraint (queue_layout == ACTIVE_THEN_UNFINALIZED /\ primary_amount_to_available != GT) -> outcome == STOP_UNFINALIZED; +constraint (queue_layout in {TWO_PROCESSABLE, INVALID_THEN_PROCESSABLE} /\ second_amount_to_remaining == GT) -> outcome == STOP_CHURN_LIMIT; +constraint (primary_reached /\ primary_amount_to_available != GT /\ not (queue_layout in {ACTIVE_THEN_UNFINALIZED, TWO_PROCESSABLE, INVALID_THEN_PROCESSABLE})) -> outcome == PROCESSED; +constraint (queue_layout in {TWO_PROCESSABLE, INVALID_THEN_PROCESSABLE} /\ second_amount_to_remaining != GT) -> outcome == PROCESSED; +constraint (churn_effect == CHURN_RETAINED) <-> outcome == STOP_CHURN_LIMIT; diff --git a/tests/generators/compliance_runners/state_transition/pending_deposits/validation.py b/tests/generators/compliance_runners/state_transition/pending_deposits/validation.py new file mode 100644 index 00000000000..9d636800bf8 --- /dev/null +++ b/tests/generators/compliance_runners/state_transition/pending_deposits/validation.py @@ -0,0 +1,218 @@ +"""Independent semantic validation for pending-deposit compliance vectors.""" + +from __future__ import annotations + +from typing import Any, TYPE_CHECKING + +from ruamel.yaml import YAML + +from eth_consensus_specs.gloas import minimal as spec +from tests.generators.compliance_runners.state_transition.validation import check_dimensions, decode + +if TYPE_CHECKING: + from pathlib import Path + + from tests.generators.compliance_runners.state_transition.validation import Check + +_YAML = YAML(typ="safe") + + +def _role(state: Any, deposit: Any, next_epoch: Any) -> str: + pubkeys = [validator.pubkey for validator in state.validators] + if deposit.pubkey not in pubkeys: + return ( + "NEW_VALID" + if spec.is_valid_deposit_signature( + deposit.pubkey, deposit.withdrawal_credentials, deposit.amount, deposit.signature + ) + else "NEW_INVALID" + ) + validator = state.validators[pubkeys.index(deposit.pubkey)] + if validator.withdrawable_epoch < next_epoch: + return "WITHDRAWN" + if validator.exit_epoch < spec.FAR_FUTURE_EPOCH: + return "EXITING" + return "ACTIVE" + + +def replay(pre: Any) -> dict[str, Any]: + """Recover the handler's loop trace without invoking the handler itself.""" + next_epoch = spec.Epoch(spec.get_current_epoch(pre) + 1) + available = pre.deposit_balance_to_consume + spec.get_activation_churn_limit(pre) + finalized_slot = spec.compute_start_slot_at_epoch(pre.finalized_checkpoint.epoch) + processed_amount = 0 + consumed = 0 + postponed: list[Any] = [] + applied: list[Any] = [] + gate = "EMPTY" + + for deposit in pre.pending_deposits: + if deposit.slot > finalized_slot: + gate = "UNFINALIZED" + break + if consumed >= spec.MAX_PENDING_DEPOSITS_PER_EPOCH: + gate = "PER_EPOCH_LIMIT" + break + role = _role(pre, deposit, next_epoch) + if role == "WITHDRAWN": + applied.append(deposit) + elif role == "EXITING": + postponed.append(deposit) + else: + if processed_amount + deposit.amount > available: + gate = "CHURN_LIMIT" + break + processed_amount += deposit.amount + if role != "NEW_INVALID": + applied.append(deposit) + consumed += 1 + else: + gate = "EXHAUSTED" + + return { + "gate": gate, + "consumed": consumed, + "processed_amount": processed_amount, + "postponed": postponed, + "applied": applied, + "expected_queue": list(pre.pending_deposits[consumed:]) + postponed, + "expected_churn": available - processed_amount if gate == "CHURN_LIMIT" else 0, + } + + +def recover_dimensions(pre: Any, trace: dict[str, Any]) -> dict[str, Any]: + deposits = pre.pending_deposits + if not deposits: + return { + "queue_layout": "EMPTY", + "secondary_role": "SECOND_NONE", + "primary_reached": False, + "primary_role": "ROLE_NA", + "deposit_signature_valid": "NA", + "validator_pubkey_found": False, + "validator_active": "NA", + "validator_exiting": "NA", + "withdrawable_epoch_to_next_epoch": "NA", + "initial_churn": "CARRY_NONZERO" if pre.deposit_balance_to_consume else "CARRY_ZERO", + "primary_amount_to_available": "NA", + "second_amount_to_remaining": "NA", + "churn_effect": "CHURN_CLEARED", + "outcome": "EMPTY_QUEUE", + } + candidate = ( + deposits[int(spec.MAX_PENDING_DEPOSITS_PER_EPOCH)] + if trace["gate"] == "PER_EPOCH_LIMIT" + else deposits[0] + ) + next_epoch = spec.Epoch(spec.get_current_epoch(pre) + 1) + role = _role(pre, candidate, next_epoch) + finalized_slot = spec.compute_start_slot_at_epoch(pre.finalized_checkpoint.epoch) + if trace["gate"] == "PER_EPOCH_LIMIT": + prefix = deposits[: int(spec.MAX_PENDING_DEPOSITS_PER_EPOCH)] + layout = ( + "LIMIT_AFTER_WITHDRAWN" + if len(prefix) == int(spec.MAX_PENDING_DEPOSITS_PER_EPOCH) + and all(_role(pre, deposit, next_epoch) == "WITHDRAWN" for deposit in prefix) + and role == "WITHDRAWN" + else "INVALID_LAYOUT" + ) + elif deposits[0].slot > finalized_slot: + layout = "FIRST_UNFINALIZED" + elif role == "EXITING" and len(deposits) > 1: + second = deposits[1] + layout = ( + "POSTPONE_THEN_ACTIVE" + if second.slot <= finalized_slot and _role(pre, second, next_epoch) == "ACTIVE" + else "INVALID_LAYOUT" + ) + elif len(deposits) > 1 and deposits[1].slot > finalized_slot: + layout = ( + "ACTIVE_THEN_UNFINALIZED" + if role in {"ACTIVE", "NEW_VALID", "NEW_INVALID"} + else "INVALID_LAYOUT" + ) + elif len(deposits) == 2 and role in {"ACTIVE", "NEW_VALID", "NEW_INVALID"}: + second = deposits[1] + second_role = _role(pre, second, next_epoch) + if second.slot <= finalized_slot and second_role == "ACTIVE": + layout = "INVALID_THEN_PROCESSABLE" if role == "NEW_INVALID" else "TWO_PROCESSABLE" + else: + layout = "INVALID_LAYOUT" + else: + layout = "SINGLE" + found = role in {"ACTIVE", "EXITING", "WITHDRAWN"} + validator = ( + pre.validators[[v.pubkey for v in pre.validators].index(candidate.pubkey)] + if found + else None + ) + withdrawable = "NA" + if validator is not None: + withdrawable = ( + "LT" + if validator.withdrawable_epoch < next_epoch + else ("EQ" if validator.withdrawable_epoch == next_epoch else "GT") + ) + available = pre.deposit_balance_to_consume + spec.get_activation_churn_limit(pre) + comparison = ( + "NA" + if role in {"EXITING", "WITHDRAWN"} + else ( + "LT" + if candidate.amount < available + else "EQ" + if candidate.amount == available + else "GT" + ) + ) + second_comparison = "NA" + if layout in {"TWO_PROCESSABLE", "INVALID_THEN_PROCESSABLE"}: + remaining = available - candidate.amount + second_amount = deposits[1].amount + second_comparison = ( + "LT" if second_amount < remaining else "EQ" if second_amount == remaining else "GT" + ) + outcome = { + "UNFINALIZED": "STOP_UNFINALIZED", + "PER_EPOCH_LIMIT": "STOP_PER_EPOCH_LIMIT", + "CHURN_LIMIT": "STOP_CHURN_LIMIT", + "EMPTY": "EMPTY_QUEUE", + }.get(trace["gate"], "PROCESSED") + return { + "queue_layout": layout, + "secondary_role": "SECOND_ACTIVE" + if layout == "POSTPONE_THEN_ACTIVE" + else ( + "SECOND_UNFINALIZED" + if layout == "ACTIVE_THEN_UNFINALIZED" + else "SECOND_PROCESSABLE" + if layout in {"TWO_PROCESSABLE", "INVALID_THEN_PROCESSABLE"} + else "SECOND_NONE" + ), + "primary_reached": layout not in {"EMPTY", "FIRST_UNFINALIZED", "LIMIT_AFTER_WITHDRAWN"}, + "primary_role": role, + "deposit_signature_valid": "T" + if role == "NEW_VALID" + else "F" + if role == "NEW_INVALID" + else "NA", + "validator_pubkey_found": found, + "validator_active": "T" if role == "ACTIVE" else "F" if found else "NA", + "validator_exiting": "T" if role in {"EXITING", "WITHDRAWN"} else "F" if found else "NA", + "withdrawable_epoch_to_next_epoch": withdrawable + if role in {"EXITING", "WITHDRAWN"} + else "NA", + "initial_churn": "CARRY_NONZERO" if pre.deposit_balance_to_consume else "CARRY_ZERO", + "primary_amount_to_available": comparison, + "second_amount_to_remaining": second_comparison, + "churn_effect": "CHURN_RETAINED" if trace["gate"] == "CHURN_LIMIT" else "CHURN_CLEARED", + "outcome": outcome, + } + + +def validate_case(case_dir: Path) -> list[Check]: + pre = decode(case_dir / "pre.ssz_snappy", spec.BeaconState) + claimed = _YAML.load((case_dir / "dimensions.yaml").read_text())["claimed"] + trace = replay(pre) + actual = recover_dimensions(pre, trace) + return check_dimensions(claimed, actual) diff --git a/tests/generators/compliance_runners/state_transition/proposer_slashing/__init__.py b/tests/generators/compliance_runners/state_transition/proposer_slashing/__init__.py new file mode 100644 index 00000000000..d8a939aa29d --- /dev/null +++ b/tests/generators/compliance_runners/state_transition/proposer_slashing/__init__.py @@ -0,0 +1,9 @@ +"""Aspect-based compliance runner for Gloas proposer slashings.""" + +from .coverage import build_profile +from .materializer import ProposerSlashingMaterializer +from .validation import validate_case + +MATERIALIZER = ProposerSlashingMaterializer + +__all__ = ("MATERIALIZER", "build_profile", "validate_case") diff --git a/tests/generators/compliance_runners/state_transition/proposer_slashing/coverage.py b/tests/generators/compliance_runners/state_transition/proposer_slashing/coverage.py new file mode 100644 index 00000000000..7e88f225251 --- /dev/null +++ b/tests/generators/compliance_runners/state_transition/proposer_slashing/coverage.py @@ -0,0 +1,48 @@ +"""Coverage profiles for Gloas ``process_proposer_slashing``.""" + +from __future__ import annotations + +from pathlib import Path + +from tests.generators.compliance_runners.state_transition.aspect_coverage import ( + build_profile as _build_profile, + enumerate_signatures, +) + +from .materializer import _DIMS + +INPUT_ASPECTS = { + "headers": ["slots_match", "proposers_match", "headers_different"], + "proposer_slashability": [ + "proposer_slashed", + "proposer_activated", + "proposer_withdrawable", + "proposer_exited", + ], + "signatures": ["signature_1_valid", "signature_2_valid"], + "pending_payment": ["payment_window", "payment_proposer_matches"], +} +OUTCOME_ASPECT = {"outcome": ["outcome", "pending_payment_cleared", "state_effected"]} +ALL_ASPECTS = {**INPUT_ASPECTS, **OUTCOME_ASPECT} +MODEL = Path(__file__).parent / "models" / "handler_proposer_slashing.mzn" + + +def _nfaults(r: dict) -> int: + return ( + int(not r["slots_match"]) + + int(not r["proposers_match"]) + + int(not r["headers_different"]) + + int(r["proposer_slashed"]) + + int(not r["proposer_activated"]) + + int(r["proposer_withdrawable"]) + + int(r["signature_1_valid"] != "T") + + int(r["signature_2_valid"] != "T") + ) + + +def _recs(): + return enumerate_signatures(MODEL, _DIMS, ALL_ASPECTS, _nfaults) + + +def build_profile(name): + return _build_profile(_recs(), name, ALL_ASPECTS, INPUT_ASPECTS, OUTCOME_ASPECT) diff --git a/tests/generators/compliance_runners/state_transition/proposer_slashing/materializer.py b/tests/generators/compliance_runners/state_transition/proposer_slashing/materializer.py new file mode 100644 index 00000000000..8f3b5be3edf --- /dev/null +++ b/tests/generators/compliance_runners/state_transition/proposer_slashing/materializer.py @@ -0,0 +1,142 @@ +"""Materialize aspect-model solutions for Gloas ``process_proposer_slashing``.""" + +from __future__ import annotations + +from typing import Any, TYPE_CHECKING + +from eth_consensus_specs.test.helpers.genesis import create_genesis_state +from eth_consensus_specs.test.helpers.keys import pubkey_to_privkey +from eth_consensus_specs.utils import bls +from tests.generators.compliance_runners.state_transition.materializer import Materializer + +if TYPE_CHECKING: + from tests.generators.compliance_runners.gen_base.gen_typing import TestCasePart + +EPOCHS_PAST_GENESIS = 10 +PROPOSER_INDEX = 1 +FOREIGN_INDEX = 0 +_DIMS = [ + "slots_match", + "proposers_match", + "headers_different", + "signature_1_valid", + "signature_2_valid", + "proposer_slashed", + "proposer_activated", + "proposer_withdrawable", + "proposer_exited", + "payment_window", + "payment_proposer_matches", + "pending_payment_cleared", + "state_effected", + "outcome", +] + + +def _s(sol: Any, name: str) -> str: + return str(getattr(sol, name)) + + +def _b(sol: Any, name: str) -> bool: + return bool(getattr(sol, name)) + + +class ProposerSlashingMaterializer(Materializer): + runner_name = "operations" + handler_name = "proposer_slashing" + + def _base_state(self) -> Any: + state = create_genesis_state( + self.spec, + validator_balances=[self.spec.MAX_EFFECTIVE_BALANCE] * 64, + activation_threshold=self.spec.MAX_EFFECTIVE_BALANCE, + ) + state.slot = self.spec.Slot(EPOCHS_PAST_GENESIS * self.spec.SLOTS_PER_EPOCH) + return state + + def _sign(self, state: Any, header: Any, valid: bool) -> Any: + if not valid: + return self.spec.SignedBeaconBlockHeader(message=header) + domain = self.spec.get_domain( + state, self.spec.DOMAIN_BEACON_PROPOSER, self.spec.compute_epoch_at_slot(header.slot) + ) + signature = bls.Sign( + pubkey_to_privkey[state.validators[header.proposer_index].pubkey], + self.spec.compute_signing_root(header, domain), + ) + return self.spec.SignedBeaconBlockHeader(message=header, signature=signature) + + def materialize_solution(self, sol: Any) -> tuple[dict, list[TestCasePart]]: + spec, pre = self.spec, self._base_state() + current = int(spec.get_current_epoch(pre)) + proposer = pre.validators[PROPOSER_INDEX] + proposer.slashed = _b(sol, "proposer_slashed") + proposer.activation_epoch = spec.Epoch(0 if _b(sol, "proposer_activated") else current + 1) + proposer.exit_epoch = spec.Epoch( + current if _b(sol, "proposer_exited") else spec.FAR_FUTURE_EPOCH + ) + proposer.withdrawable_epoch = spec.Epoch( + current if _b(sol, "proposer_withdrawable") else spec.FAR_FUTURE_EPOCH + ) + + window = _s(sol, "payment_window") + slot_1 = ( + int(pre.slot) + - int(spec.SLOTS_PER_EPOCH) * {"CURRENT": 0, "PREVIOUS": 1, "OLD": 2}[window] + ) + slot_2 = slot_1 if _b(sol, "slots_match") else slot_1 + 1 + proposer_2 = PROPOSER_INDEX if _b(sol, "proposers_match") else FOREIGN_INDEX + root_2 = b"\x22" * 32 if _b(sol, "headers_different") else b"\x11" * 32 + h1 = spec.BeaconBlockHeader( + slot=spec.Slot(slot_1), + proposer_index=spec.ValidatorIndex(PROPOSER_INDEX), + parent_root=b"\x11" * 32, + state_root=b"\x33" * 32, + body_root=b"\x44" * 32, + ) + h2 = spec.BeaconBlockHeader( + slot=spec.Slot(slot_2), + proposer_index=spec.ValidatorIndex(proposer_2), + parent_root=root_2, + state_root=b"\x33" * 32, + body_root=b"\x44" * 32, + ) + slashing = spec.ProposerSlashing( + signed_header_1=self._sign(pre, h1, _s(sol, "signature_1_valid") == "T"), + signed_header_2=self._sign(pre, h2, _s(sol, "signature_2_valid") == "T"), + ) + if window != "OLD": + index = (int(spec.SLOTS_PER_EPOCH) if window == "CURRENT" else 0) + slot_1 % int( + spec.SLOTS_PER_EPOCH + ) + pre.builder_pending_payments[index] = spec.BuilderPendingPayment( + weight=spec.Gwei(1), + withdrawal=spec.BuilderPendingWithdrawal( + fee_recipient=spec.ExecutionAddress(b"\xaa" * 20), + amount=spec.Gwei(1), + builder_index=spec.BuilderIndex(0), + ), + proposer_index=spec.ValidatorIndex( + PROPOSER_INDEX if _s(sol, "payment_proposer_matches") == "T" else FOREIGN_INDEX + ), + ) + post = pre.copy() + try: + spec.process_proposer_slashing(post, slashing) + except (AssertionError, IndexError): + post = None + claimed = { + n: (_b(sol, n) if isinstance(getattr(sol, n), bool) else _s(sol, n)) for n in _DIMS + } + parts: list[TestCasePart] = [ + ("pre", "ssz", pre.encode_bytes()), + ("proposer_slashing", "ssz", slashing.encode_bytes()), + ] + if post is not None: + parts.append(("post", "ssz", post.encode_bytes())) + meta = { + "description": f"process_proposer_slashing: {claimed['outcome']}", + "bls_setting": 1, + "claimed": claimed, + } + return meta, parts diff --git a/tests/generators/compliance_runners/state_transition/proposer_slashing/models/handler_proposer_slashing.mzn b/tests/generators/compliance_runners/state_transition/proposer_slashing/models/handler_proposer_slashing.mzn new file mode 100644 index 00000000000..772eea15603 --- /dev/null +++ b/tests/generators/compliance_runners/state_transition/proposer_slashing/models/handler_proposer_slashing.mzn @@ -0,0 +1,72 @@ +% Handler model: process_proposer_slashing (Gloas). +% +% The payment dimensions model the EIP-7732 two-epoch pending-payment window. +% Signature values remain applicable even when an earlier assertion rejects. + +include "../../aspects/signed_message.mzn"; + +enum PaymentWindow = { CURRENT, PREVIOUS, OLD }; +enum Outcome = { + REJECT_SLOT_MISMATCH, REJECT_PROPOSER_MISMATCH, REJECT_HEADERS_EQUAL, + REJECT_NOT_SLASHABLE_SLASHED, REJECT_NOT_ACTIVATED, + REJECT_NOT_SLASHABLE_WITHDRAWABLE, REJECT_SIGNATURE_1, REJECT_SIGNATURE_2, + ACCEPT_CURRENT_PAYMENT_CLEARED, ACCEPT_CURRENT_PAYMENT_RETAINED, + ACCEPT_PREVIOUS_PAYMENT_CLEARED, ACCEPT_PREVIOUS_PAYMENT_RETAINED, ACCEPT_OLD +}; + +var bool: slots_match; +var bool: proposers_match; +var bool: headers_different; + +constraint (not slots_match \/ not proposers_match) -> headers_different; + +var Dim: signature_1_valid; +var Dim: signature_2_valid; +constraint signed_message_ok(signature_1_valid, true); +constraint signed_message_ok(signature_2_valid, true); +constraint signature_1_valid in BOOLV; +constraint signature_2_valid in BOOLV; + +var bool: proposer_slashed; +var bool: proposer_activated; +var bool: proposer_withdrawable; +% `is_slashable_validator` deliberately does not check `exit_epoch`: a +% validator remains slashable after exit until its withdrawable epoch. +var bool: proposer_exited; + +var PaymentWindow: payment_window; +var BOOLV_NA: payment_proposer_matches; +constraint (payment_proposer_matches == NA) <-> payment_window == OLD; + +var bool: proposer_slashable; +constraint proposer_slashable <-> + not proposer_slashed /\ proposer_activated /\ not proposer_withdrawable; + +var Outcome: outcome; +constraint outcome = + if not slots_match then REJECT_SLOT_MISMATCH + elseif not proposers_match then REJECT_PROPOSER_MISMATCH + elseif not headers_different then REJECT_HEADERS_EQUAL + elseif not proposer_slashable then + if proposer_slashed then REJECT_NOT_SLASHABLE_SLASHED + elseif not proposer_activated then REJECT_NOT_ACTIVATED + else REJECT_NOT_SLASHABLE_WITHDRAWABLE endif + elseif signature_1_valid != T then REJECT_SIGNATURE_1 + elseif signature_2_valid != T then REJECT_SIGNATURE_2 + elseif payment_window == CURRENT then + if payment_proposer_matches == T then ACCEPT_CURRENT_PAYMENT_CLEARED + else ACCEPT_CURRENT_PAYMENT_RETAINED endif + elseif payment_window == PREVIOUS then + if payment_proposer_matches == T then ACCEPT_PREVIOUS_PAYMENT_CLEARED + else ACCEPT_PREVIOUS_PAYMENT_RETAINED endif + else ACCEPT_OLD endif; + +var bool: pending_payment_cleared; +constraint pending_payment_cleared <-> outcome in { + ACCEPT_CURRENT_PAYMENT_CLEARED, ACCEPT_PREVIOUS_PAYMENT_CLEARED +}; +var bool: state_effected; +constraint state_effected <-> outcome in { + ACCEPT_CURRENT_PAYMENT_CLEARED, ACCEPT_CURRENT_PAYMENT_RETAINED, + ACCEPT_PREVIOUS_PAYMENT_CLEARED, ACCEPT_PREVIOUS_PAYMENT_RETAINED, ACCEPT_OLD +}; diff --git a/tests/generators/compliance_runners/state_transition/proposer_slashing/validation.py b/tests/generators/compliance_runners/state_transition/proposer_slashing/validation.py new file mode 100644 index 00000000000..b3b06b23b95 --- /dev/null +++ b/tests/generators/compliance_runners/state_transition/proposer_slashing/validation.py @@ -0,0 +1,107 @@ +"""Independent validation for Gloas proposer-slashing compliance vectors.""" + +from __future__ import annotations + +from typing import Any, TYPE_CHECKING + +from ruamel.yaml import YAML + +from eth_consensus_specs.gloas import minimal as spec +from eth_consensus_specs.utils import bls +from tests.generators.compliance_runners.state_transition.validation import check_dimensions, decode + +if TYPE_CHECKING: + from pathlib import Path + + from tests.generators.compliance_runners.state_transition.validation import Check + +_YAML = YAML(typ="safe") + + +def recover(pre: Any, slashing: Any) -> dict[str, Any]: + h1, h2 = slashing.signed_header_1, slashing.signed_header_2 + m1, m2 = h1.message, h2.message + current, proposer = spec.get_current_epoch(pre), pre.validators[m1.proposer_index] + + def valid(signed: Any) -> bool: + domain = spec.get_domain( + pre, + spec.DOMAIN_BEACON_PROPOSER, + spec.compute_epoch_at_slot(signed.message.slot), + ) + return bool( + bls.Verify( + pre.validators[signed.message.proposer_index].pubkey, + spec.compute_signing_root(signed.message, domain), + signed.signature, + ) + ) + + epoch = spec.compute_epoch_at_slot(m1.slot) + if epoch == current: + window, payment_index = ( + "CURRENT", + int(spec.SLOTS_PER_EPOCH) + int(m1.slot) % int(spec.SLOTS_PER_EPOCH), + ) + elif epoch == spec.get_previous_epoch(pre): + window, payment_index = "PREVIOUS", int(m1.slot) % int(spec.SLOTS_PER_EPOCH) + else: + window, payment_index = "OLD", None + payment_matches = ( + "NA" + if payment_index is None + else ( + "T" + if pre.builder_pending_payments[payment_index].proposer_index == m1.proposer_index + else "F" + ) + ) + r = { + "slots_match": m1.slot == m2.slot, + "proposers_match": m1.proposer_index == m2.proposer_index, + "headers_different": m1 != m2, + "signature_1_valid": "T" if valid(h1) else "F", + "signature_2_valid": "T" if valid(h2) else "F", + "proposer_slashed": bool(proposer.slashed), + "proposer_activated": proposer.activation_epoch <= current, + "proposer_withdrawable": proposer.withdrawable_epoch <= current, + "proposer_exited": proposer.exit_epoch <= current, + "payment_window": window, + "payment_proposer_matches": payment_matches, + } + slashable = spec.is_slashable_validator(proposer, current) + if not r["slots_match"]: + outcome = "REJECT_SLOT_MISMATCH" + elif not r["proposers_match"]: + outcome = "REJECT_PROPOSER_MISMATCH" + elif not r["headers_different"]: + outcome = "REJECT_HEADERS_EQUAL" + elif not slashable: + if r["proposer_slashed"]: + outcome = "REJECT_NOT_SLASHABLE_SLASHED" + elif not r["proposer_activated"]: + outcome = "REJECT_NOT_ACTIVATED" + else: + outcome = "REJECT_NOT_SLASHABLE_WITHDRAWABLE" + elif r["signature_1_valid"] != "T": + outcome = "REJECT_SIGNATURE_1" + elif r["signature_2_valid"] != "T": + outcome = "REJECT_SIGNATURE_2" + elif window == "OLD": + outcome = "ACCEPT_OLD" + else: + outcome = f"ACCEPT_{window}_PAYMENT_{'CLEARED' if payment_matches == 'T' else 'RETAINED'}" + r.update( + outcome=outcome, + pending_payment_cleared=outcome.endswith("CLEARED"), + state_effected=outcome.startswith("ACCEPT_"), + ) + return r + + +def validate_case(case_dir: Path) -> list[Check]: + pre = decode(case_dir / "pre.ssz_snappy", spec.BeaconState) + operation = decode(case_dir / "proposer_slashing.ssz_snappy", spec.ProposerSlashing) + claimed = _YAML.load((case_dir / "dimensions.yaml").read_text())["claimed"] + actual = recover(pre, operation) + return check_dimensions(claimed, actual) diff --git a/tests/generators/compliance_runners/state_transition/ptc_window/__init__.py b/tests/generators/compliance_runners/state_transition/ptc_window/__init__.py new file mode 100644 index 00000000000..a1000605bf4 --- /dev/null +++ b/tests/generators/compliance_runners/state_transition/ptc_window/__init__.py @@ -0,0 +1,9 @@ +"""Compliance generator for Gloas ``process_ptc_window``.""" + +from .coverage import build_profile +from .materializer import PtcWindowMaterializer +from .validation import validate_case + +MATERIALIZER = PtcWindowMaterializer + +__all__ = ("MATERIALIZER", "build_profile", "validate_case") diff --git a/tests/generators/compliance_runners/state_transition/ptc_window/coverage.py b/tests/generators/compliance_runners/state_transition/ptc_window/coverage.py new file mode 100644 index 00000000000..859638a8414 --- /dev/null +++ b/tests/generators/compliance_runners/state_transition/ptc_window/coverage.py @@ -0,0 +1,28 @@ +from __future__ import annotations + +from pathlib import Path + +from tests.generators.compliance_runners.state_transition.aspect_coverage import ( + build_profile as _build_profile, + enumerate_signatures, +) + +from .materializer import _DIMS + +MODEL = Path(__file__).parent / "models" / "handler_ptc_window.mzn" +ASPECTS = { + "epoch_context": ["epoch_position"], + "state": ["validator_count", "validator_balance", "validator_activity"], +} + + +def _recs(): + return enumerate_signatures(MODEL, _DIMS, ASPECTS, _nfaults) + + +def _nfaults(_r: dict) -> int: + return 0 + + +def build_profile(name): + return _build_profile(_recs(), name, ASPECTS, ASPECTS, {"outcome": ["outcome"]}) diff --git a/tests/generators/compliance_runners/state_transition/ptc_window/materializer.py b/tests/generators/compliance_runners/state_transition/ptc_window/materializer.py new file mode 100644 index 00000000000..2dd1d0c6c96 --- /dev/null +++ b/tests/generators/compliance_runners/state_transition/ptc_window/materializer.py @@ -0,0 +1,64 @@ +from __future__ import annotations + +from typing import Any, TYPE_CHECKING + +from eth_consensus_specs.test.helpers.genesis import create_genesis_state +from eth_consensus_specs.test.helpers.gloas.state import initialize_ptc_window +from tests.generators.compliance_runners.state_transition.materializer import Materializer + +if TYPE_CHECKING: + from tests.generators.compliance_runners.gen_base.gen_typing import TestCasePart + +_DIMS = [ + "epoch_position", + "validator_count", + "validator_balance", + "validator_activity", +] + + +class PtcWindowMaterializer(Materializer): + runner_name = "epoch_processing" + handler_name = "ptc_window" + + def materialize_solution(self, sol: Any) -> tuple[dict, list[TestCasePart]]: + s = self.spec + validator_count = 64 if str(sol.validator_count) == "MINIMUM" else 128 + balance_profile = str(sol.validator_balance) + if balance_profile == "MINIMUM_BALANCE": + validator_balances = [s.EFFECTIVE_BALANCE_INCREMENT] * validator_count + activation_threshold = s.EFFECTIVE_BALANCE_INCREMENT + elif balance_profile == "MIXED_BALANCE": + lower_balance = s.MAX_EFFECTIVE_BALANCE - s.EFFECTIVE_BALANCE_INCREMENT + # Keep balance distribution independent of SOME_INACTIVE's every- + # fourth-validator selection: each activity group gets both tiers. + validator_balances = [ + s.MAX_EFFECTIVE_BALANCE if i % 8 < 4 else lower_balance + for i in range(validator_count) + ] + activation_threshold = lower_balance + else: # MAXIMUM_BALANCE + validator_balances = [s.MAX_EFFECTIVE_BALANCE] * validator_count + activation_threshold = s.MAX_EFFECTIVE_BALANCE + pre = create_genesis_state( + s, + validator_balances=validator_balances, + activation_threshold=activation_threshold, + ) + if str(sol.validator_activity) == "SOME_INACTIVE": + for i in range(0, len(pre.validators), 4): + validator = pre.validators[i] + validator.activation_eligibility_epoch = s.FAR_FUTURE_EPOCH + validator.activation_epoch = s.FAR_FUTURE_EPOCH + pre.genesis_validators_root = s.hash_tree_root(pre.validators) + pre.ptc_window = initialize_ptc_window(s, pre) + target = (1 if str(sol.epoch_position) == "GENESIS_END" else 2) * s.SLOTS_PER_EPOCH - 1 + s.process_slots(pre, s.Slot(target)) + post = pre.copy() + s.process_ptc_window(post) + claimed = { + n: (bool(v) if isinstance(v := getattr(sol, n), bool) else str(v)) for n in _DIMS + } + meta = {"description": "process_ptc_window", "claimed": claimed} + parts = [("pre", "ssz", pre.encode_bytes()), ("post", "ssz", post.encode_bytes())] + return meta, parts diff --git a/tests/generators/compliance_runners/state_transition/ptc_window/models/handler_ptc_window.mzn b/tests/generators/compliance_runners/state_transition/ptc_window/models/handler_ptc_window.mzn new file mode 100644 index 00000000000..6d11f776eeb --- /dev/null +++ b/tests/generators/compliance_runners/state_transition/ptc_window/models/handler_ptc_window.mzn @@ -0,0 +1,8 @@ +enum EpochPosition = { GENESIS_END, LATER_EPOCH_END }; +enum ValidatorCount = { MINIMUM, MANY }; +enum ValidatorBalance = { MINIMUM_BALANCE, MAXIMUM_BALANCE, MIXED_BALANCE }; +enum ValidatorActivity = { ALL_ACTIVE, SOME_INACTIVE }; +var EpochPosition: epoch_position; +var ValidatorCount: validator_count; +var ValidatorBalance: validator_balance; +var ValidatorActivity: validator_activity; diff --git a/tests/generators/compliance_runners/state_transition/ptc_window/validation.py b/tests/generators/compliance_runners/state_transition/ptc_window/validation.py new file mode 100644 index 00000000000..ee88c1d5b5b --- /dev/null +++ b/tests/generators/compliance_runners/state_transition/ptc_window/validation.py @@ -0,0 +1,47 @@ +from __future__ import annotations + +from typing import TYPE_CHECKING + +from ruamel.yaml import YAML + +from eth_consensus_specs.gloas import minimal as spec +from tests.generators.compliance_runners.state_transition.validation import ( + check_dimensions, + decode, +) + +if TYPE_CHECKING: + from pathlib import Path + + from tests.generators.compliance_runners.state_transition.validation import Check + +_YAML = YAML(typ="safe") + + +def validate_case(case_dir: Path) -> list[Check]: + pre = decode(case_dir / "pre.ssz_snappy", spec.BeaconState) + claimed = _YAML.load((case_dir / "dimensions.yaml").read_text())["claimed"] + actual = { + "epoch_position": "GENESIS_END" + if int(spec.get_current_epoch(pre)) == 0 + else "LATER_EPOCH_END", + "validator_count": "MINIMUM" if len(pre.validators) == 64 else "MANY", + "validator_balance": ( + "MAXIMUM_BALANCE" + if all(balance == spec.MAX_EFFECTIVE_BALANCE for balance in pre.balances) + else ( + "MINIMUM_BALANCE" + if all(balance == spec.EFFECTIVE_BALANCE_INCREMENT for balance in pre.balances) + else "MIXED_BALANCE" + ) + ), + "validator_activity": ( + "ALL_ACTIVE" + if all( + validator.activation_epoch <= spec.get_current_epoch(pre) + for validator in pre.validators + ) + else "SOME_INACTIVE" + ), + } + return check_dimensions(claimed, actual) diff --git a/tests/generators/compliance_runners/state_transition/run.py b/tests/generators/compliance_runners/state_transition/run.py new file mode 100644 index 00000000000..160d90298cf --- /dev/null +++ b/tests/generators/compliance_runners/state_transition/run.py @@ -0,0 +1,46 @@ +"""Generate and validate state-transition compliance cases. + +Usage: + uv run python -m tests.generators.compliance_runners.state_transition.run + uv run python -m tests.generators.compliance_runners.state_transition.run --handler withdrawals + uv run python -m tests.generators.compliance_runners.state_transition.run --profile smoke +""" + +from __future__ import annotations + +import argparse +from pathlib import Path + +from .catalog import HANDLERS +from .provider import materialize_handler + +PROFILES = ("all", "smoke", "normal", "exceptional", "standard") + + +def run( + handler: str, + comptests_output: Path | None = None, + profile: str = "standard", +) -> int: + handlers = HANDLERS if handler == "all" else (handler,) + for current_handler in handlers: + output_dir = ( + comptests_output + if comptests_output is not None + else Path(__file__).parent / current_handler / "reftests" + ) + materialize_handler(current_handler, profile, output_dir) + return 0 + + +def main() -> int: + parser = argparse.ArgumentParser() + parser.add_argument("--handler", choices=(*HANDLERS, "all"), default="all") + parser.add_argument("--profile", choices=PROFILES, default="standard") + parser.add_argument("--comptests-output", type=Path) + args = parser.parse_args() + return run(args.handler, args.comptests_output, args.profile) + + +if __name__ == "__main__": + raise SystemExit(main()) diff --git a/tests/generators/compliance_runners/state_transition/runner/__init__.py b/tests/generators/compliance_runners/state_transition/runner/__init__.py new file mode 100644 index 00000000000..294a951e46b --- /dev/null +++ b/tests/generators/compliance_runners/state_transition/runner/__init__.py @@ -0,0 +1 @@ +"""Runner for generated state-transition compliance vectors.""" diff --git a/tests/generators/compliance_runners/state_transition/runner/conftest.py b/tests/generators/compliance_runners/state_transition/runner/conftest.py new file mode 100644 index 00000000000..23fc4ca186f --- /dev/null +++ b/tests/generators/compliance_runners/state_transition/runner/conftest.py @@ -0,0 +1,19 @@ +def pytest_addoption(parser): + parser.addoption( + "--test-dir", + action="append", + default=None, + help=("Directory containing generated state-transition compliance tests. Can be repeated."), + ) + parser.addoption( + "--start", + type=int, + default=None, + help="Start index (0-based) into the generated test list.", + ) + parser.addoption( + "--limit", + type=int, + default=None, + help="Limit number of generated tests to validate.", + ) diff --git a/tests/generators/compliance_runners/state_transition/runner/test_run.py b/tests/generators/compliance_runners/state_transition/runner/test_run.py new file mode 100644 index 00000000000..67e6741ec70 --- /dev/null +++ b/tests/generators/compliance_runners/state_transition/runner/test_run.py @@ -0,0 +1,251 @@ +from __future__ import annotations + +from pathlib import Path +from typing import NamedTuple + +import pytest +from ruamel.yaml import YAML +from snappy import uncompress + +from eth_consensus_specs.test.context import expect_assertion_error +from eth_consensus_specs.test.helpers.forks import is_post_gloas +from eth_consensus_specs.test.helpers.specs import spec_targets +from eth_consensus_specs.utils import bls + +OPERATION_INPUTS = { + "attestation": ("attestation", "Attestation"), + "builder_deposit_request": ("builder_deposit_request", "BuilderDepositRequest"), + "builder_exit_request": ("builder_exit_request", "BuilderExitRequest"), + "consolidation_request": ("consolidation_request", "ConsolidationRequest"), + "deposit_request": ("deposit_request", "DepositRequest"), + "execution_payload_bid": ("execution_payload_bid", "SignedExecutionPayloadBid"), + "parent_execution_payload": ("block", "BeaconBlock"), + "payload_attestation": ("payload_attestation", "PayloadAttestation"), + "proposer_slashing": ("proposer_slashing", "ProposerSlashing"), + "attester_slashing": ("attester_slashing", "AttesterSlashing"), + "deposit": ("deposit", "Deposit"), + "bls_to_execution_change": ("address_change", "SignedBLSToExecutionChange"), + "voluntary_exit": ("voluntary_exit", "SignedVoluntaryExit"), + "withdrawal_request": ("withdrawal_request", "WithdrawalRequest"), + "sync_aggregate": ("sync_aggregate", "SyncAggregate"), +} + +OPERATION_PROCESSORS = { + "attestation": "process_attestation", + "builder_deposit_request": "process_builder_deposit_request", + "builder_exit_request": "process_builder_exit_request", + "consolidation_request": "process_consolidation_request", + "deposit_request": "process_deposit_request", + "execution_payload_bid": "process_execution_payload_bid", + "parent_execution_payload": "process_parent_execution_payload", + "payload_attestation": "process_payload_attestation", + "proposer_slashing": "process_proposer_slashing", + "attester_slashing": "process_attester_slashing", + "deposit": "process_deposit", + "bls_to_execution_change": "process_bls_to_execution_change", + "voluntary_exit": "process_voluntary_exit", + "withdrawal_request": "process_withdrawal_request", + "sync_aggregate": "process_sync_aggregate", + "withdrawals": "process_withdrawals", +} + +EPOCH_PROCESSORS = { + "builder_pending_payments": "process_builder_pending_payments", + "justification_and_finalization": "process_justification_and_finalization", + "registry_updates": "process_registry_updates", + "slashings": "process_slashings", + "pending_deposits": "process_pending_deposits", + "ptc_window": "process_ptc_window", + "pending_consolidations": "process_pending_consolidations", + "effective_balance_updates": "process_effective_balance_updates", + "inactivity_updates": "process_inactivity_updates", + "rewards_and_penalties": "process_rewards_and_penalties", + "participation_flag_updates": "process_participation_flag_updates", + "slashings_reset": "process_slashings_reset", + "randao_mixes_reset": "process_randao_mixes_reset", + "eth1_data_reset": "process_eth1_data_reset", + "historical_summaries_update": "process_historical_summaries_update", + "sync_committee_updates": "process_sync_committee_updates", +} + + +class StateTransitionTestInfo(NamedTuple): + preset: str + fork: str + runner: str + handler: str + suite: str + test_dir: Path + + +def read_yaml(path: Path): + yaml = YAML(typ="safe") + return yaml.load(path.read_text()) + + +def read_ssz_snappy(path: Path) -> bytes: + return uncompress(path.read_bytes()) + + +def decode_file(spec, test_dir: Path, name: str, typ): + return typ.decode_bytes(read_ssz_snappy(test_dir / f"{name}.ssz_snappy")) + + +def get_test_case(spec, test_dir: Path, handler: str): + return { + "meta": read_yaml(test_dir / "meta.yaml"), + "pre": decode_file(spec, test_dir, "pre", spec.BeaconState), + "operation": decode_optional_operation(spec, test_dir, handler), + "post": decode_optional_post(spec, test_dir), + } + + +def decode_optional_operation(spec, test_dir: Path, handler: str): + input_name = OPERATION_INPUTS.get(handler, (handler, None))[0] + if not (test_dir / f"{input_name}.ssz_snappy").exists(): + return None + return decode_operation(spec, test_dir, handler) + + +def decode_operation(spec, test_dir: Path, handler: str): + if handler in OPERATION_INPUTS: + input_name, type_name = OPERATION_INPUTS[handler] + return decode_file(spec, test_dir, input_name, getattr(spec, type_name)) + raise ValueError(f"Unsupported operations handler: {handler}") + + +def decode_optional_post(spec, test_dir: Path): + post_path = test_dir / "post.ssz_snappy" + if not post_path.exists(): + return None + return spec.BeaconState.decode_bytes(read_ssz_snappy(post_path)) + + +def run_test(test_info: StateTransitionTestInfo): + preset, fork, runner, handler, _, test_dir = test_info + spec = spec_targets[preset][fork] + + test_case = get_test_case(spec, Path(test_dir), handler) + state = test_case["pre"] + expected_post = test_case["post"] + old_bls_active = bls.bls_active + bls.bls_active = bool(test_case["meta"].get("bls_setting", 0)) + + try: + if runner == "epoch_processing": + run_epoch_processing_case(spec, state, handler, expected_post) + return + + if runner != "operations": + raise ValueError(f"Unsupported state-transition runner: {runner}") + + if handler in OPERATION_PROCESSORS: + process_fn = getattr(spec, OPERATION_PROCESSORS[handler]) + extra_args = () + if handler == "attestation" and is_post_gloas(spec): + extra_args = (spec.Slot(test_case["meta"]["parent_slot"]),) + run_processing_case( + process_fn, + state, + test_case["operation"], + expected_post, + extra_args, + ) + return + + raise ValueError(f"Unsupported operations handler: {handler}") + finally: + bls.bls_active = old_bls_active + + +def run_epoch_processing_case(spec, state, handler, expected_post): + if handler not in EPOCH_PROCESSORS: + raise ValueError(f"Unsupported epoch_processing handler: {handler}") + process_fn = getattr(spec, EPOCH_PROCESSORS[handler]) + run_processing_case(process_fn, state, None, expected_post) + + +def run_processing_case(process_fn, state, operation, expected_post, extra_args=()): + def run_processing(): + if operation is None: + process_fn(state, *extra_args) + else: + process_fn(state, operation, *extra_args) + + if expected_post is None: + expect_assertion_error(run_processing) + return + + run_processing() + assert state == expected_post + + +def gather_tests(tests_dir): + if isinstance(tests_dir, (list, tuple)): + for path in tests_dir: + yield from gather_tests(path) + return + + tests_path = Path(tests_dir) + reftests_dirs = ( + [tests_path] + if any(path.name in spec_targets for path in tests_path.glob("*")) + else sorted(tests_path.glob("*/reftests")) + ) + for reftests_dir in reftests_dirs: + for preset in [p.name for p in reftests_dir.glob("*") if p.name in spec_targets]: + for fork in [ + f.name for f in (reftests_dir / preset).glob("*") if f.name in spec_targets[preset] + ]: + for test_dir in sorted((reftests_dir / preset / fork).glob("*/*/*/*")): + manifest_path = test_dir / "manifest.yaml" + if not manifest_path.exists(): + continue + manifest = read_yaml(manifest_path) + yield StateTransitionTestInfo( + preset, + fork, + manifest["runner"], + manifest["handler"], + manifest["suite"], + test_dir, + ) + + +def select_tests(tests, start=None, limit=None): + if start is not None: + tests = tests[start:] + if limit is not None: + tests = tests[:limit] + return tests + + +def _test_id(test_info: StateTransitionTestInfo) -> str: + return ( + f"{test_info.preset}::{test_info.fork}::{test_info.runner}::" + f"{test_info.handler}::{test_info.suite}::{Path(test_info.test_dir).name}" + ) + + +def pytest_generate_tests(metafunc): + if "test_info" not in metafunc.fixturenames: + return + + tests_dir = metafunc.config.getoption("--test-dir") + if tests_dir is None: + raise pytest.UsageError( + "--test-dir is required when running state-transition compliance tests" + ) + + start = metafunc.config.getoption("--start") + limit = metafunc.config.getoption("--limit") + test_infos = select_tests(list(gather_tests(tests_dir)), start=start, limit=limit) + metafunc.parametrize( + "test_info", + test_infos, + ids=[_test_id(test_info) for test_info in test_infos], + ) + + +def test_run_state_transition_case(test_info): + run_test(test_info) diff --git a/tests/generators/compliance_runners/state_transition/validation.py b/tests/generators/compliance_runners/state_transition/validation.py new file mode 100644 index 00000000000..a9e6fe83440 --- /dev/null +++ b/tests/generators/compliance_runners/state_transition/validation.py @@ -0,0 +1,131 @@ +"""Shared case runner for state-transition compliance validators.""" + +from __future__ import annotations + +import argparse +from dataclasses import dataclass +from importlib import import_module +from pathlib import Path +from typing import Any, TYPE_CHECKING + +import snappy + +from .catalog import HANDLERS, RUNNERS +from .materializer import SUITE_NAME + +if TYPE_CHECKING: + from collections.abc import Callable + + +@dataclass +class Check: + dimension: str + claimed: Any + actual: Any + status: str + + +def check_dimensions(claimed: dict, actual: dict) -> list[Check]: + return [ + Check( + name, + value, + actual.get(name, ""), + "ok" if actual.get(name, "") == value else "mismatch", + ) + for name, value in claimed.items() + ] + + +def decode(path: Path, sedes: Any) -> Any: + return sedes.decode_bytes(snappy.decompress(path.read_bytes())) + + +RUNNER_BY_HANDLER = { + handler: runner for runner, handlers in RUNNERS.items() for handler in handlers +} + + +def validate_cases( + test_dir: Path, + handler: str, + validate_case: Callable[..., Any], + selected_cases: set[str] | None = None, +) -> int: + """Run a handler validator over its materialized reference-test cases.""" + phase = RUNNER_BY_HANDLER[handler] + case_dirs = sorted(test_dir.glob(f"**/{phase}/{handler}/{SUITE_NAME}/case_*")) + if selected_cases is not None: + case_dirs = [case_dir for case_dir in case_dirs if case_dir.name in selected_cases] + if not case_dirs: + suffix = " matching the requested cases" if selected_cases is not None else "" + print(f"No cases found under {test_dir}{suffix}") + return 1 + + total_mm = total_err = 0 + for case_dir in case_dirs: + result = validate_case(case_dir) + if isinstance(result, tuple): + checks, errors = result + else: + checks, errors = result, [] + mismatches = [check for check in checks if check.status == "mismatch"] + total_mm += len(mismatches) + total_err += len(errors) + status = "OK" if not mismatches and not errors else "FAIL" + outcome = next((check.claimed for check in checks if check.dimension == "outcome"), "?") + print(f"{case_dir.name}: {status} [{outcome}]") + for check in mismatches: + print(f" dim {check.dimension}: claimed={check.claimed!r} actual={check.actual!r}") + for error in errors: + print(f" oracle: {error}") + + print() + if total_mm or total_err: + print(f"FAILED: {total_mm} dimension mismatch(es), {total_err} oracle error(s)") + return 1 + print(f"PASSED: {len(case_dirs)} cases, all dimensions consistent") + return 0 + + +def discover_handlers(test_dir: Path) -> list[str]: + candidates = [] + for phase in ("operations", "epoch_processing"): + for handler in HANDLERS: + if list(test_dir.glob(f"**/{phase}/{handler}/**/case_*")): + candidates.append((phase, handler)) + if not candidates: + raise ValueError(f"could not discover a state-transition handler under {test_dir}") + return [handler for _, handler in candidates] + + +def main( + test_dir: Path | None = None, + selected_cases: set[str] | None = None, + handlers: tuple[str, ...] | None = None, +) -> int: + if test_dir is None: + parser = argparse.ArgumentParser() + parser.add_argument("--test-dir", type=Path, required=True) + parser.add_argument( + "--cases", + type=str, + help="comma-separated case names to validate, e.g. case_0205,case_0206", + ) + args = parser.parse_args() + test_dir = args.test_dir + if args.cases: + selected_cases = {case.strip() for case in args.cases.split(",") if case.strip()} + else: + selected_cases = None + + handlers = handlers if handlers is not None else tuple(discover_handlers(test_dir)) + result = 0 + for handler in handlers: + module = import_module(f".{handler}", __package__) + result |= validate_cases(test_dir, handler, module.validate_case, selected_cases) + return result + + +if __name__ == "__main__": + raise SystemExit(main()) diff --git a/tests/generators/compliance_runners/state_transition/withdrawal_request/__init__.py b/tests/generators/compliance_runners/state_transition/withdrawal_request/__init__.py new file mode 100644 index 00000000000..1b560af7690 --- /dev/null +++ b/tests/generators/compliance_runners/state_transition/withdrawal_request/__init__.py @@ -0,0 +1,7 @@ +from .coverage import build_profile +from .materializer import WithdrawalRequestMaterializer +from .validation import validate_case + +MATERIALIZER = WithdrawalRequestMaterializer + +__all__ = ("MATERIALIZER", "build_profile", "validate_case") diff --git a/tests/generators/compliance_runners/state_transition/withdrawal_request/coverage.py b/tests/generators/compliance_runners/state_transition/withdrawal_request/coverage.py new file mode 100644 index 00000000000..65af851e265 --- /dev/null +++ b/tests/generators/compliance_runners/state_transition/withdrawal_request/coverage.py @@ -0,0 +1,74 @@ +"""Coverage profiles for process_withdrawal_request. + +Handler-specific instantiation of the shared ``..aspect_coverage`` engine. Uses +the validator aspect family (membership / credential / lifecycle / balance / +pending) and REUSES source_authorization (shared with builder_exit_request). + +Run: + uv run python -m ...withdrawal_request.coverage + uv run python -m ...withdrawal_request.coverage standard --materialize +""" + +from __future__ import annotations + +from pathlib import Path + +from tests.generators.compliance_runners.state_transition.aspect_coverage import ( + build_profile as _build_profile, + enumerate_signatures, +) + +from .materializer import _DIMS + +# Fine-grained input aspects remain part of the signature used by `all`; the +# normal/exceptional profiles use the composite validator_state factor. +FINE_INPUT_ASPECTS = { + "withdrawal_amount": ["is_full_exit_request"], + "partial_queue_capacity": ["partial_queue_full"], + "validator_membership": ["validator_pubkey_found"], + "validator_credential": ["validator_credential"], + "source_authorization": ["source_address_matches"], + "validator_lifecycle": ["validator_active", "validator_exiting", "validator_old_enough"], + "validator_pending_withdrawal": ["has_pending_partial_withdrawal"], + "validator_balance": ["sufficient_effective_balance", "has_excess_balance"], +} +OUTCOME_ASPECT = {"outcome": ["outcome"]} +INPUT_ASPECTS = { + "withdrawal_amount": ["is_full_exit_request"], + "partial_queue_capacity": ["partial_queue_full"], + "validator_state": [ + "validator_pubkey_found", + "validator_credential", + "source_address_matches", + "validator_active", + "validator_exiting", + "validator_old_enough", + "has_pending_partial_withdrawal", + "sufficient_effective_balance", + "has_excess_balance", + ], +} +FINE_ALL_ASPECTS = {**FINE_INPUT_ASPECTS, **OUTCOME_ASPECT} +ALL_ASPECTS = {**INPUT_ASPECTS, **OUTCOME_ASPECT} +MODEL = Path(__file__).parent / "models" / "handler_withdrawal_request.mzn" + + +def _nfaults(r: dict) -> int: + faults = int(r["partial_queue_full"] and not r["is_full_exit_request"]) + faults += int(not r["validator_pubkey_found"]) + if r["validator_pubkey_found"]: + faults += int( + not (r["validator_has_execution_credential"] and r["source_address_matches"] == "T") + ) + faults += int(r["validator_active"] != "T") + faults += int(r["validator_exiting"] != "F") + faults += int(r["validator_old_enough"] != "T") + return faults + + +def build_profile(name): + return _build_profile(_recs(), name, ALL_ASPECTS, INPUT_ASPECTS, OUTCOME_ASPECT) + + +def _recs(): + return enumerate_signatures(MODEL, _DIMS, FINE_ALL_ASPECTS, _nfaults) diff --git a/tests/generators/compliance_runners/state_transition/withdrawal_request/materializer.py b/tests/generators/compliance_runners/state_transition/withdrawal_request/materializer.py new file mode 100644 index 00000000000..8b1086277a7 --- /dev/null +++ b/tests/generators/compliance_runners/state_transition/withdrawal_request/materializer.py @@ -0,0 +1,167 @@ +"""Materialize aspect-model solutions into process_withdrawal_request cases. + +Realizes each applicable coverage dimension onto a genesis validator (or leaves +the request pubkey absent), constructs a WithdrawalRequest, and derives post. +No BLS, no churn gate. The operation never raises, so `post` is always present. + +Spec: specs/electra/beacon-chain.md process_withdrawal_request (inherited by gloas). +""" + +from __future__ import annotations + +from typing import Any, TYPE_CHECKING + +from eth_consensus_specs.test.helpers.genesis import create_genesis_state +from eth_consensus_specs.test.helpers.keys import pubkeys +from tests.generators.compliance_runners.state_transition.materializer import Materializer + +if TYPE_CHECKING: + from tests.generators.compliance_runners.gen_base.gen_typing import TestCasePart + +NUM_VALIDATORS = 64 +TARGET_INDEX = 0 +ABSENT_PUBKEY = pubkeys[NUM_VALIDATORS] # not in a NUM_VALIDATORS-validator genesis +CURRENT_EPOCH = 70 # > SHARD_COMMITTEE_PERIOD (64), for old-enough headroom +ADDRESS = b"\x22" * 20 +OTHER_ADDRESS = b"\x33" * 20 +PARTIAL_AMOUNT = 10**9 + +_PREFIX = {"CRED_BLS": b"\x00", "CRED_ETH1": b"\x01", "CRED_COMPOUNDING": b"\x02"} + +_DIMS = [ + "is_full_exit_request", + "partial_queue_full", + "validator_pubkey_found", + "validator_credential", + "source_address_matches", + "validator_active", + "validator_exiting", + "validator_old_enough", + "has_pending_partial_withdrawal", + "sufficient_effective_balance", + "has_excess_balance", + "validator_has_execution_credential", + "validator_has_compounding_credential", + "outcome", + "withdrawal_effected", +] + + +def _s(sol: Any, n: str) -> str: + return str(getattr(sol, n)) + + +def _b(sol: Any, n: str) -> bool: + return bool(getattr(sol, n)) + + +class WithdrawalRequestMaterializer(Materializer): + runner_name = "operations" + handler_name = "withdrawal_request" + + def _base_state(self) -> Any: + spec = self.spec + state = create_genesis_state( + spec, + validator_balances=[spec.MAX_EFFECTIVE_BALANCE] * NUM_VALIDATORS, + activation_threshold=spec.MAX_EFFECTIVE_BALANCE, + ) + state.slot = spec.Slot(CURRENT_EPOCH * spec.SLOTS_PER_EPOCH) + return state + + def _epochs(self, active: bool, exiting: bool, old_enough: bool) -> tuple[int, int]: + """(activation_epoch, exit_epoch) realizing the lifecycle triple at CURRENT_EPOCH.""" + spec = self.spec + far = int(spec.FAR_FUTURE_EPOCH) + activation = 0 if old_enough else CURRENT_EPOCH - 10 # <= C-64 vs in (C-64, C] + if active: + exit_epoch = (CURRENT_EPOCH + 10) if exiting else far # future exit still active + elif exiting: + exit_epoch = CURRENT_EPOCH - 1 # exited (epoch >= exit) + else: + activation = CURRENT_EPOCH + 10 # not yet activated + exit_epoch = far + return activation, exit_epoch + + def materialize_solution(self, sol: Any) -> tuple[dict, list[TestCasePart]]: + spec = self.spec + pre = self._base_state() + found = _b(sol, "validator_pubkey_found") + is_full = _b(sol, "is_full_exit_request") + + source_address = ADDRESS + if found: + v = pre.validators[TARGET_INDEX] + cred = _s(sol, "validator_credential") + v.withdrawal_credentials = spec.Bytes32(_PREFIX[cred] + b"\x00" * 11 + ADDRESS) + source_address = ADDRESS if _s(sol, "source_address_matches") == "T" else OTHER_ADDRESS + + activation, exit_epoch = self._epochs( + _s(sol, "validator_active") == "T", + _s(sol, "validator_exiting") == "T", + _s(sol, "validator_old_enough") == "T", + ) + v.activation_epoch = spec.Epoch(activation) + v.exit_epoch = spec.Epoch(exit_epoch) + v.effective_balance = spec.Gwei( + spec.MIN_ACTIVATION_BALANCE + if _s(sol, "sufficient_effective_balance") == "T" + else spec.MIN_ACTIVATION_BALANCE - 1 + ) + + # Pending-partial-withdrawals queue: target entry (for has_pending) + padding + # for partial_queue_full, keeping the queue length exactly at the limit. + pending_for_target = found and _s(sol, "has_pending_partial_withdrawal") == "T" + entries = [] + if pending_for_target: + entries.append( + spec.PendingPartialWithdrawal( + validator_index=spec.ValidatorIndex(TARGET_INDEX), + amount=spec.Gwei(1), + withdrawable_epoch=spec.Epoch(CURRENT_EPOCH), + ) + ) + if _b(sol, "partial_queue_full"): + filler_index = spec.ValidatorIndex(1) + while len(entries) < int(spec.PENDING_PARTIAL_WITHDRAWALS_LIMIT): + entries.append( + spec.PendingPartialWithdrawal( + validator_index=filler_index, + amount=spec.Gwei(1), + withdrawable_epoch=spec.Epoch(CURRENT_EPOCH), + ) + ) + pre.pending_partial_withdrawals = spec.PendingPartialWithdrawals(data=entries) + + if found: + pending_amount = 1 if pending_for_target else 0 + if _s(sol, "has_excess_balance") == "T": + balance = spec.MIN_ACTIVATION_BALANCE + pending_amount + PARTIAL_AMOUNT + else: + balance = spec.MIN_ACTIVATION_BALANCE + pending_amount # not strictly greater + pre.balances[TARGET_INDEX] = spec.Gwei(balance) + + request = spec.WithdrawalRequest( + source_address=spec.ExecutionAddress(source_address), + validator_pubkey=spec.BLSPubkey( + pre.validators[TARGET_INDEX].pubkey if found else ABSENT_PUBKEY + ), + amount=spec.Gwei(0) if is_full else spec.Gwei(PARTIAL_AMOUNT), + ) + + post = pre.copy() + spec.process_withdrawal_request(post, request) # never raises + + claimed = { + n: (_b(sol, n) if isinstance(getattr(sol, n), bool) else _s(sol, n)) for n in _DIMS + } + meta = { + "description": f"process_withdrawal_request: {claimed['outcome']}", + "claimed": claimed, + } + parts = [ + ("pre", "ssz", pre.encode_bytes()), + ("withdrawal_request", "ssz", request.encode_bytes()), + ("post", "ssz", post.encode_bytes()), + ] + return meta, parts diff --git a/tests/generators/compliance_runners/state_transition/withdrawal_request/models/handler_withdrawal_request.mzn b/tests/generators/compliance_runners/state_transition/withdrawal_request/models/handler_withdrawal_request.mzn new file mode 100644 index 00000000000..8dc02a75cfa --- /dev/null +++ b/tests/generators/compliance_runners/state_transition/withdrawal_request/models/handler_withdrawal_request.mzn @@ -0,0 +1,94 @@ +% Handler model: process_withdrawal_request. +% +% Uses the parameterized validator aspects (lifecycle / seasoning / credential +% applied to a single validator) plus flat aspects (membership, authorization, +% pending, balance) and REUSES source_authorization (shared with +% builder_exit_request). No BLS, no churn gate. No solve item. +% +% Spec: specs/electra/beacon-chain.md process_withdrawal_request (inherited by gloas). + +include "../../aspects/withdrawal_amount.mzn"; +include "../../aspects/partial_queue_capacity.mzn"; +include "../../aspects/validator_membership.mzn"; +include "../../aspects/validator_credential.mzn"; % parameterized +include "../../aspects/validator_lifecycle.mzn"; % parameterized +include "../../aspects/validator_seasoning.mzn"; % parameterized +include "../../aspects/source_authorization.mzn"; % shared with builder_exit_request +include "../../aspects/validator_pending_withdrawal.mzn"; +include "../../aspects/validator_balance.mzn"; + +% ---- Validator instance (single role) --------------------------------------- +var ValidatorCredentialKind: validator_credential; +var BOOLV_NA: validator_active; +var BOOLV_NA: validator_exiting; +var BOOLV_NA: validator_old_enough; +constraint validator_credential_ok(validator_credential, validator_pubkey_found); +constraint validator_lifecycle_ok(validator_active, validator_exiting, validator_pubkey_found); +constraint validator_seasoning_ok(validator_old_enough, validator_pubkey_found); +% lifecycle/seasoning coherence: an activated (old-enough), non-exiting validator is active +constraint (validator_old_enough == T /\ validator_exiting == F) -> (validator_active == T); + +% Derived credential booleans (exposed for coverage/validation). +var bool: validator_has_execution_credential; +var bool: validator_has_compounding_credential; +constraint validator_has_execution_credential <-> cred_has_execution(validator_credential); +constraint validator_has_compounding_credential <-> cred_has_compounding(validator_credential); + +% ---- Applicability bindings for the flat aspects ---------------------------- +constraint source_authorization_applicable <-> validator_pubkey_found; +constraint validator_pending_applicable <-> validator_pubkey_found; +constraint validator_balance_applicable <-> validator_pubkey_found; + +% ---- Gate passes (spec order) ----------------------------------------------- +var bool: g_cred = validator_has_execution_credential /\ source_address_matches == T; +var bool: g_active = validator_active == T; +var bool: g_not_exiting = validator_exiting == F; +var bool: g_old = validator_old_enough == T; + +% ---- Outcome (first-failing gate, then branch) ------------------------------ +enum Outcome = { + REJECTED_QUEUE_FULL, + REJECTED_NOT_FOUND, + REJECTED_CREDENTIALS, + REJECTED_INACTIVE, + REJECTED_EXITING, + REJECTED_TOO_YOUNG, + FULL_EXIT_INITIATED, + FULL_EXIT_NOOP_PENDING, + PARTIAL_NOOP_NOT_COMPOUNDING, + PARTIAL_NOOP_INSUFFICIENT_EFFECTIVE_BALANCE, + PARTIAL_NOOP_NO_EXCESS_BALANCE, + PARTIAL_QUEUED +}; + +var Outcome: outcome; +constraint outcome = + if partial_queue_full /\ not is_full_exit_request then REJECTED_QUEUE_FULL + elseif not validator_pubkey_found then REJECTED_NOT_FOUND + elseif not g_cred then REJECTED_CREDENTIALS + elseif not g_active then REJECTED_INACTIVE + elseif not g_not_exiting then REJECTED_EXITING + elseif not g_old then REJECTED_TOO_YOUNG + elseif is_full_exit_request then + (if has_pending_partial_withdrawal == T then FULL_EXIT_NOOP_PENDING else FULL_EXIT_INITIATED endif) + else + (if not validator_has_compounding_credential then PARTIAL_NOOP_NOT_COMPOUNDING + elseif sufficient_effective_balance != T then PARTIAL_NOOP_INSUFFICIENT_EFFECTIVE_BALANCE + elseif has_excess_balance != T then PARTIAL_NOOP_NO_EXCESS_BALANCE + else PARTIAL_QUEUED endif) + endif; + +% ---- Faults ----------------------------------------------------------------- +var bool: fault_queue = partial_queue_full /\ not is_full_exit_request; +var bool: fault_found = not validator_pubkey_found; +var bool: fault_cred = validator_pubkey_found /\ not g_cred; +var bool: fault_active = validator_pubkey_found /\ not g_active; +var bool: fault_exiting = validator_pubkey_found /\ not g_not_exiting; +var bool: fault_young = validator_pubkey_found /\ not g_old; +var int: n_faults = + bool2int(fault_queue) + bool2int(fault_found) + bool2int(fault_cred) + + bool2int(fault_active) + bool2int(fault_exiting) + bool2int(fault_young); + +% ---- Effect ----------------------------------------------------------------- +var bool: withdrawal_effected; +constraint withdrawal_effected <-> (outcome in {FULL_EXIT_INITIATED, PARTIAL_QUEUED}); diff --git a/tests/generators/compliance_runners/state_transition/withdrawal_request/validation.py b/tests/generators/compliance_runners/state_transition/withdrawal_request/validation.py new file mode 100644 index 00000000000..88701755e7f --- /dev/null +++ b/tests/generators/compliance_runners/state_transition/withdrawal_request/validation.py @@ -0,0 +1,126 @@ +"""Independent validation of process_withdrawal_request vectors. + +Recovers every applicable coverage dimension from the decoded pre state and +WithdrawalRequest via the real spec predicates, recomputes the outcome, and runs +recomputes the outcome. Imports neither the materializer nor the model. +""" + +from __future__ import annotations + +from typing import Any, TYPE_CHECKING + +from ruamel.yaml import YAML + +from eth_consensus_specs.gloas import minimal as spec +from tests.generators.compliance_runners.state_transition.validation import check_dimensions, decode + +if TYPE_CHECKING: + from pathlib import Path + + from tests.generators.compliance_runners.state_transition.validation import Check + +_YAML = YAML(typ="safe") +_ACCEPT = {"FULL_EXIT_INITIATED", "PARTIAL_QUEUED"} + + +def _tri(x: bool) -> str: + return "T" if x else "F" + + +def _credential(v: Any) -> str: + prefix = bytes(v.withdrawal_credentials[:1]) + if prefix == bytes(spec.COMPOUNDING_WITHDRAWAL_PREFIX): + return "CRED_COMPOUNDING" + if prefix == bytes(spec.ETH1_ADDRESS_WITHDRAWAL_PREFIX): + return "CRED_ETH1" + return "CRED_BLS" + + +def recover(pre: Any, request: Any) -> dict[str, Any]: + current_epoch = spec.get_current_epoch(pre) + pubkeys = [v.pubkey for v in pre.validators] + found = request.validator_pubkey in pubkeys + + r: dict[str, Any] = { + "is_full_exit_request": int(request.amount) == int(spec.FULL_EXIT_REQUEST_AMOUNT), + "partial_queue_full": len(pre.pending_partial_withdrawals) + == int(spec.PENDING_PARTIAL_WITHDRAWALS_LIMIT), + "validator_pubkey_found": found, + } + + if found: + idx = spec.ValidatorIndex(pubkeys.index(request.validator_pubkey)) + v = pre.validators[idx] + pending = int(spec.get_pending_balance_to_withdraw(pre, idx)) + r["validator_credential"] = _credential(v) + r["validator_has_execution_credential"] = bool(spec.has_execution_withdrawal_credential(v)) + r["validator_has_compounding_credential"] = bool( + spec.has_compounding_withdrawal_credential(v) + ) + r["source_address_matches"] = _tri(v.withdrawal_credentials[12:] == request.source_address) + r["validator_active"] = _tri(bool(spec.is_active_validator(v, current_epoch))) + r["validator_exiting"] = _tri(v.exit_epoch != spec.FAR_FUTURE_EPOCH) + r["validator_old_enough"] = _tri( + int(current_epoch) >= int(v.activation_epoch) + int(spec.config.SHARD_COMMITTEE_PERIOD) + ) + r["has_pending_partial_withdrawal"] = _tri(pending > 0) + r["sufficient_effective_balance"] = _tri( + int(v.effective_balance) >= int(spec.MIN_ACTIVATION_BALANCE) + ) + r["has_excess_balance"] = _tri( + int(pre.balances[idx]) > int(spec.MIN_ACTIVATION_BALANCE) + pending + ) + else: + r["validator_credential"] = "CRED_NA" + r["validator_has_execution_credential"] = False + r["validator_has_compounding_credential"] = False + for n in ( + "source_address_matches", + "validator_active", + "validator_exiting", + "validator_old_enough", + "has_pending_partial_withdrawal", + "sufficient_effective_balance", + "has_excess_balance", + ): + r[n] = "NA" + + r["outcome"] = _derive(r) + r["withdrawal_effected"] = r["outcome"] in _ACCEPT + return r + + +def _derive(r: dict) -> str: + if r["partial_queue_full"] and not r["is_full_exit_request"]: + return "REJECTED_QUEUE_FULL" + if not r["validator_pubkey_found"]: + return "REJECTED_NOT_FOUND" + if not (r["validator_has_execution_credential"] and r["source_address_matches"] == "T"): + return "REJECTED_CREDENTIALS" + if r["validator_active"] != "T": + return "REJECTED_INACTIVE" + if r["validator_exiting"] != "F": + return "REJECTED_EXITING" + if r["validator_old_enough"] != "T": + return "REJECTED_TOO_YOUNG" + if r["is_full_exit_request"]: + return ( + "FULL_EXIT_NOOP_PENDING" + if r["has_pending_partial_withdrawal"] == "T" + else "FULL_EXIT_INITIATED" + ) + if not r["validator_has_compounding_credential"]: + return "PARTIAL_NOOP_NOT_COMPOUNDING" + if r["sufficient_effective_balance"] != "T": + return "PARTIAL_NOOP_INSUFFICIENT_EFFECTIVE_BALANCE" + if r["has_excess_balance"] != "T": + return "PARTIAL_NOOP_NO_EXCESS_BALANCE" + return "PARTIAL_QUEUED" + + +def validate_case(case_dir: Path) -> list[Check]: + pre = decode(case_dir / "pre.ssz_snappy", spec.BeaconState) + request = decode(case_dir / "withdrawal_request.ssz_snappy", spec.WithdrawalRequest) + claimed = _YAML.load((case_dir / "dimensions.yaml").read_text())["claimed"] + actual = recover(pre, request) + return check_dimensions(claimed, actual) diff --git a/tests/generators/compliance_runners/state_transition/withdrawals/__init__.py b/tests/generators/compliance_runners/state_transition/withdrawals/__init__.py new file mode 100644 index 00000000000..caba0146b3f --- /dev/null +++ b/tests/generators/compliance_runners/state_transition/withdrawals/__init__.py @@ -0,0 +1,9 @@ +"""Aspect-based compliance generator for Gloas ``process_withdrawals``.""" + +from .coverage import build_profile +from .materializer import WithdrawalsMaterializer +from .validation import validate_case + +MATERIALIZER = WithdrawalsMaterializer + +__all__ = ("MATERIALIZER", "build_profile", "validate_case") diff --git a/tests/generators/compliance_runners/state_transition/withdrawals/coverage.py b/tests/generators/compliance_runners/state_transition/withdrawals/coverage.py new file mode 100644 index 00000000000..0b3ab4b8a74 --- /dev/null +++ b/tests/generators/compliance_runners/state_transition/withdrawals/coverage.py @@ -0,0 +1,46 @@ +"""Coverage profiles for the Gloas ``process_withdrawals`` handler. + +Aspects follow the handler body: the parent guard, one aspect per stage of +``get_expected_withdrawals``, the pre-state bookkeeping the getter does not +determine, and one effect aspect per group of state updates. +""" + +from __future__ import annotations + +from pathlib import Path + +from tests.generators.compliance_runners.state_transition.aspect_coverage import ( + build_profile as _build_profile, + enumerate_signatures, +) +from tests.generators.compliance_runners.state_transition.withdrawals.materializer import ( + _DIMS, +) + +INPUT_ASPECTS = { + "parent": ["parent_payload_revealed"], + "builder_pending": ["builder_pending_nonempty"], + "pending_partial": ["pending_partial_nonempty"], + "builder_sweep": ["builder_sweep_nonempty"], + "validator_sweep": ["validator_sweep_nonempty"], + "capacity": ["withdrawals_over_limit"], +} +EFFECT_ASPECTS = { + "outcome": ["outcome"], + "effects": ["state_effected"], +} +OUTCOME_ASPECT = {"outcome": ["outcome"]} +ALL_ASPECTS = {**INPUT_ASPECTS, **EFFECT_ASPECTS} +MODEL = Path(__file__).parent / "models" / "handler_withdrawals.mzn" + + +def _nfaults(record: dict) -> int: + return 0 + + +def _recs(): + return enumerate_signatures(MODEL, _DIMS, ALL_ASPECTS, _nfaults) + + +def build_profile(name: str): + return _build_profile(_recs(), name, ALL_ASPECTS, ALL_ASPECTS, OUTCOME_ASPECT) diff --git a/tests/generators/compliance_runners/state_transition/withdrawals/materializer.py b/tests/generators/compliance_runners/state_transition/withdrawals/materializer.py new file mode 100644 index 00000000000..0de8e91670f --- /dev/null +++ b/tests/generators/compliance_runners/state_transition/withdrawals/materializer.py @@ -0,0 +1,122 @@ +"""Materialize aspect-model solutions for Gloas ``process_withdrawals``. + +The solver selects semantic source presence and the payload-capacity boundary. +This module only chooses the concrete builders and validators needed to realize +that assignment, then records the original solution with the vector. +""" + +from __future__ import annotations + +from typing import Any, TYPE_CHECKING + +from eth_consensus_specs.test.helpers.genesis import create_genesis_state +from eth_consensus_specs.test.helpers.keys import builder_pubkeys +from eth_consensus_specs.test.helpers.withdrawals import prepare_process_withdrawals +from tests.generators.compliance_runners.state_transition.materializer import Materializer + +if TYPE_CHECKING: + from tests.generators.compliance_runners.gen_base.gen_typing import TestCasePart + +_DIMS = [ + "parent_payload_revealed", + "builder_pending_nonempty", + "pending_partial_nonempty", + "builder_sweep_nonempty", + "validator_sweep_nonempty", + "withdrawals_over_limit", + "state_effected", + "outcome", +] +_BUILDER_ADDRESS = b"\x42" * 20 + + +def _b(solution: Any, name: str) -> bool: + return bool(getattr(solution, name)) + + +def _s(solution: Any, name: str) -> str: + return str(getattr(solution, name)) + + +class WithdrawalsMaterializer(Materializer): + runner_name = "operations" + handler_name = "withdrawals" + + def _base_state(self) -> Any: + spec = self.spec + state = create_genesis_state( + spec, + validator_balances=[spec.MAX_EFFECTIVE_BALANCE] * 64, + activation_threshold=spec.MAX_EFFECTIVE_BALANCE, + ) + state.builders = type(state.builders)() + return state + + def _add_builders(self, state: Any, count: int) -> None: + spec = self.spec + epoch = spec.get_current_epoch(state) + for index in range(count): + state.builders.append( + spec.Builder( + pubkey=spec.BLSPubkey(builder_pubkeys[index]), + version=spec.PAYLOAD_BUILDER_VERSION, + execution_address=spec.ExecutionAddress(bytes([0x42 + index]) * 20), + balance=spec.Gwei(1_000_000_000), + deposit_epoch=spec.Epoch(0), + withdrawable_epoch=spec.Epoch(epoch + 1), + ) + ) + + def materialize_solution(self, solution: Any) -> tuple[dict, list[TestCasePart]]: + spec = self.spec + pre = self._base_state() + parent_full = _b(solution, "parent_payload_revealed") + builder_pending = _b(solution, "builder_pending_nonempty") + pending_partial = _b(solution, "pending_partial_nonempty") + builder_sweep = _b(solution, "builder_sweep_nonempty") + validator_sweep = _b(solution, "validator_sweep_nonempty") + at_limit = _b(solution, "withdrawals_over_limit") + + # Four sources can coexist. A Gloas full payload always has a validator + # sweep withdrawal (the other source stages reserve its final slot). + count = int(spec.MAX_WITHDRAWALS_PER_PAYLOAD) if at_limit else 1 + builder_count = ( + count + if at_limit and (builder_pending or builder_sweep) + else int(builder_pending or builder_sweep) + ) + if builder_count: + self._add_builders(pre, builder_count) + + kwargs: dict[str, Any] = { + "parent_block_full": parent_full, + "parent_block_empty": not parent_full, + } + if builder_pending: + kwargs["builder_indices"] = list(range(count if at_limit else 1)) + if pending_partial: + kwargs["pending_partial_indices"] = [8] + if builder_sweep: + # Keep pending-withdrawal builders separate from swept builders. + start = count if builder_pending else 0 + needed = count if at_limit and not builder_pending else 1 + if start + needed > len(pre.builders): + self._add_builders(pre, start + needed - len(pre.builders)) + kwargs["builder_sweep_indices"] = list(range(start, start + needed)) + if validator_sweep: + kwargs["full_withdrawal_indices"] = list(range(count if at_limit else 1)) + + prepare_process_withdrawals(spec, pre, **kwargs) + post = pre.copy() + spec.process_withdrawals(post) + claimed = { + name: ( + _b(solution, name) + if isinstance(getattr(solution, name), bool) + else _s(solution, name) + ) + for name in _DIMS + } + meta = {"description": f"process_withdrawals: {claimed['outcome']}", "claimed": claimed} + parts = [("pre", "ssz", pre.encode_bytes()), ("post", "ssz", post.encode_bytes())] + return meta, parts diff --git a/tests/generators/compliance_runners/state_transition/withdrawals/models/handler_withdrawals.mzn b/tests/generators/compliance_runners/state_transition/withdrawals/models/handler_withdrawals.mzn new file mode 100644 index 00000000000..c44ec01f3c2 --- /dev/null +++ b/tests/generators/compliance_runners/state_transition/withdrawals/models/handler_withdrawals.mzn @@ -0,0 +1,56 @@ +% Handler model: process_withdrawals (Gloas). +% +% The four sources are considered in protocol order: builder-pending, +% pending-partial, builder sweep, then validator sweep. ``over_limit`` models +% the MAX_WITHDRAWALS_PER_PAYLOAD boundary, rather than a separate source. +% +% Spec: specs/gloas/beacon-chain.md process_withdrawals. + +int: MAX_WITHDRAWALS_PER_PAYLOAD = 4; + +enum Outcome = { + PARENT_EMPTY_NOOP, + FULL_NO_WITHDRAWALS, + BUILDER_PENDING, + PENDING_PARTIAL, + BUILDER_SWEEP, + VALIDATOR_SWEEP, + MIXED_WITHDRAWALS, + MAX_WITHDRAWALS_LIMIT +}; + +var bool: parent_payload_revealed; +var bool: builder_pending_nonempty; +var bool: pending_partial_nonempty; +var bool: builder_sweep_nonempty; +var bool: validator_sweep_nonempty; +var bool: withdrawals_over_limit; + +var int: active_sources = bool2int(builder_pending_nonempty) + + bool2int(pending_partial_nonempty) + + bool2int(builder_sweep_nonempty) + + bool2int(validator_sweep_nonempty); + +constraint active_sources >= MAX_WITHDRAWALS_PER_PAYLOAD -> withdrawals_over_limit; + +% Builder pending, pending partials, and builder sweep each reserve the final +% slot; a full payload therefore always contains a validator-sweep withdrawal. +constraint withdrawals_over_limit -> parent_payload_revealed /\ validator_sweep_nonempty; +constraint not parent_payload_revealed -> + (not builder_pending_nonempty /\ not pending_partial_nonempty /\ + not builder_sweep_nonempty /\ not validator_sweep_nonempty /\ + not withdrawals_over_limit); + +var Outcome: outcome; +constraint outcome = + if not parent_payload_revealed then PARENT_EMPTY_NOOP + elseif withdrawals_over_limit then MAX_WITHDRAWALS_LIMIT + elseif active_sources == 0 then FULL_NO_WITHDRAWALS + elseif active_sources >= 2 then MIXED_WITHDRAWALS + elseif builder_pending_nonempty then BUILDER_PENDING + elseif pending_partial_nonempty then PENDING_PARTIAL + elseif builder_sweep_nonempty then BUILDER_SWEEP + else VALIDATOR_SWEEP endif; + +var bool: state_effected; +constraint state_effected <-> parent_payload_revealed; diff --git a/tests/generators/compliance_runners/state_transition/withdrawals/validation.py b/tests/generators/compliance_runners/state_transition/withdrawals/validation.py new file mode 100644 index 00000000000..bcb89a59942 --- /dev/null +++ b/tests/generators/compliance_runners/state_transition/withdrawals/validation.py @@ -0,0 +1,74 @@ +"""Independently validate Gloas ``process_withdrawals`` compliance vectors.""" + +from __future__ import annotations + +from typing import Any, TYPE_CHECKING + +from ruamel.yaml import YAML + +from eth_consensus_specs.gloas import minimal as spec +from tests.generators.compliance_runners.state_transition.validation import check_dimensions, decode + +if TYPE_CHECKING: + from pathlib import Path + + from tests.generators.compliance_runners.state_transition.validation import Check + +_YAML = YAML(typ="safe") + + +def recover(pre: Any) -> dict[str, Any]: + parent_full = pre.latest_block_hash == pre.latest_execution_payload_bid.block_hash + current_epoch = spec.get_current_epoch(pre) + builder_pending = bool(pre.builder_pending_withdrawals) + pending_partial = bool(pre.pending_partial_withdrawals) + builder_sweep = any( + builder.withdrawable_epoch <= current_epoch and builder.balance > 0 + for builder in pre.builders + ) + validator_sweep = any( + spec.is_fully_withdrawable_validator(validator, pre.balances[index], current_epoch) + or spec.is_partially_withdrawable_validator(validator, pre.balances[index]) + for index, validator in enumerate(pre.validators) + ) + if not parent_full: + builder_pending = pending_partial = builder_sweep = validator_sweep = False + over_limit = False + else: + over_limit = ( + len(spec.get_expected_withdrawals(pre).withdrawals) == spec.MAX_WITHDRAWALS_PER_PAYLOAD + ) + active_sources = sum((builder_pending, pending_partial, builder_sweep, validator_sweep)) + if not parent_full: + outcome = "PARENT_EMPTY_NOOP" + elif over_limit: + outcome = "MAX_WITHDRAWALS_LIMIT" + elif active_sources == 0: + outcome = "FULL_NO_WITHDRAWALS" + elif active_sources >= 2: + outcome = "MIXED_WITHDRAWALS" + elif builder_pending: + outcome = "BUILDER_PENDING" + elif pending_partial: + outcome = "PENDING_PARTIAL" + elif builder_sweep: + outcome = "BUILDER_SWEEP" + else: + outcome = "VALIDATOR_SWEEP" + return { + "parent_payload_revealed": parent_full, + "builder_pending_nonempty": builder_pending, + "pending_partial_nonempty": pending_partial, + "builder_sweep_nonempty": builder_sweep, + "validator_sweep_nonempty": validator_sweep, + "withdrawals_over_limit": over_limit, + "state_effected": parent_full, + "outcome": outcome, + } + + +def validate_case(case_dir: Path) -> list[Check]: + pre = decode(case_dir / "pre.ssz_snappy", spec.BeaconState) + claimed = _YAML.load((case_dir / "dimensions.yaml").read_text())["claimed"] + actual = recover(pre) + return check_dimensions(claimed, actual)