Commit 250e28a
refactor(forks): add Spec delegator surface (Stage 4A of leanEthereum#686) (leanEthereum#702)
* refactor(forks): add Spec delegator surface (Stage 4A of leanEthereum#686)
Adds the LstarSpec method surface that mirrors the existing
State / Store / SignedBlock methods one-for-one:
- State transition: state_transition, process_slots, process_block,
process_block_header, process_attestations, build_block.
- Forkchoice: on_block, on_tick, on_gossip_attestation,
on_gossip_aggregated_attestation, produce_attestation_data,
produce_block_with_signatures, get_proposal_head.
- Block signatures: verify_signatures.
Each method is a pure delegator to the corresponding container method.
No call sites change — the new surface is unused initially. Stage 4B
will rewrite call sites to go through the spec; Stage 4C will move
the bodies in and replace literal Block/State/Store references with
self.*_class(...).
Tests use unittest.mock.patch.object to verify each delegator
forwards its arguments unchanged and returns the container method's
result verbatim.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
* docs: tighten delegator surface docstrings
Rewrite the per-method docstrings on the fork-class delegators and
the delegator test suite to follow the project documentation rules:
- Each docstring describes the operation in plain English.
- No explicit class or method names that rot when renamed.
- No issue/stage references that belong in the PR description.
- No banner-style separator comments inside the class body.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
* feat(forks): add inner-type class pointers and structural protocols
Extend ForkProtocol with class pointers for the inner container types
(BlockBody, BlockHeader, AggregatedAttestations, AttestationSignatures)
and the matching structural protocols. Hook them up on LstarSpec.
This is the scaffolding the next stages of leanEthereum#686 need so that moving
container method bodies into the spec can replace literal Block(...),
BlockBody(...), AggregatedAttestations(...) constructors with
self.<name>_class(...) — keeping inheriting forks free to swap any
single inner type without re-implementing the parent's logic.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
---------
Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>1 parent 4d1816d commit 250e28a
3 files changed
Lines changed: 405 additions & 0 deletions
File tree
- src/lean_spec/forks
- lstar
- tests/lean_spec/forks
| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
1 | 1 | | |
2 | 2 | | |
| 3 | + | |
| 4 | + | |
3 | 5 | | |
4 | 6 | | |
5 | 7 | | |
6 | 8 | | |
7 | 9 | | |
8 | 10 | | |
9 | 11 | | |
| 12 | + | |
| 13 | + | |
10 | 14 | | |
11 | 15 | | |
12 | 16 | | |
13 | 17 | | |
14 | 18 | | |
15 | 19 | | |
16 | 20 | | |
| 21 | + | |
| 22 | + | |
| 23 | + | |
| 24 | + | |
17 | 25 | | |
18 | 26 | | |
| 27 | + | |
| 28 | + | |
| 29 | + | |
| 30 | + | |
19 | 31 | | |
20 | 32 | | |
21 | 33 | | |
| |||
32 | 44 | | |
33 | 45 | | |
34 | 46 | | |
| 47 | + | |
| 48 | + | |
35 | 49 | | |
36 | 50 | | |
| 51 | + | |
| 52 | + | |
37 | 53 | | |
38 | 54 | | |
39 | 55 | | |
| |||
57 | 73 | | |
58 | 74 | | |
59 | 75 | | |
| 76 | + | |
| 77 | + | |
| 78 | + | |
| 79 | + | |
| 80 | + | |
| 81 | + | |
| 82 | + | |
| 83 | + | |
| 84 | + | |
| 85 | + | |
| 86 | + | |
| 87 | + | |
| 88 | + | |
| 89 | + | |
| 90 | + | |
| 91 | + | |
| 92 | + | |
| 93 | + | |
| 94 | + | |
| 95 | + | |
| 96 | + | |
| 97 | + | |
| 98 | + | |
| 99 | + | |
| 100 | + | |
| 101 | + | |
| 102 | + | |
| 103 | + | |
| 104 | + | |
| 105 | + | |
| 106 | + | |
| 107 | + | |
| 108 | + | |
| 109 | + | |
| 110 | + | |
| 111 | + | |
| 112 | + | |
| 113 | + | |
| 114 | + | |
| 115 | + | |
| 116 | + | |
| 117 | + | |
| 118 | + | |
| 119 | + | |
| 120 | + | |
| 121 | + | |
| 122 | + | |
| 123 | + | |
| 124 | + | |
| 125 | + | |
| 126 | + | |
| 127 | + | |
| 128 | + | |
| 129 | + | |
| 130 | + | |
| 131 | + | |
| 132 | + | |
| 133 | + | |
| 134 | + | |
| 135 | + | |
| 136 | + | |
| 137 | + | |
| 138 | + | |
| 139 | + | |
| 140 | + | |
| 141 | + | |
| 142 | + | |
| 143 | + | |
| 144 | + | |
| 145 | + | |
| 146 | + | |
| 147 | + | |
| 148 | + | |
| 149 | + | |
| 150 | + | |
| 151 | + | |
| 152 | + | |
| 153 | + | |
| 154 | + | |
| 155 | + | |
| 156 | + | |
| 157 | + | |
| 158 | + | |
| 159 | + | |
| 160 | + | |
| 161 | + | |
| 162 | + | |
| 163 | + | |
| 164 | + | |
| 165 | + | |
| 166 | + | |
| 167 | + | |
| 168 | + | |
| 169 | + | |
| 170 | + | |
| 171 | + | |
| 172 | + | |
| 173 | + | |
| 174 | + | |
| 175 | + | |
| 176 | + | |
| 177 | + | |
| 178 | + | |
| 179 | + | |
| 180 | + | |
| 181 | + | |
| 182 | + | |
| 183 | + | |
| 184 | + | |
| 185 | + | |
| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
71 | 71 | | |
72 | 72 | | |
73 | 73 | | |
| 74 | + | |
| 75 | + | |
| 76 | + | |
| 77 | + | |
| 78 | + | |
| 79 | + | |
| 80 | + | |
| 81 | + | |
| 82 | + | |
| 83 | + | |
| 84 | + | |
| 85 | + | |
| 86 | + | |
| 87 | + | |
| 88 | + | |
| 89 | + | |
| 90 | + | |
| 91 | + | |
| 92 | + | |
| 93 | + | |
| 94 | + | |
| 95 | + | |
| 96 | + | |
| 97 | + | |
| 98 | + | |
| 99 | + | |
| 100 | + | |
| 101 | + | |
| 102 | + | |
| 103 | + | |
| 104 | + | |
| 105 | + | |
74 | 106 | | |
75 | 107 | | |
76 | 108 | | |
| |||
282 | 314 | | |
283 | 315 | | |
284 | 316 | | |
| 317 | + | |
| 318 | + | |
| 319 | + | |
| 320 | + | |
| 321 | + | |
| 322 | + | |
285 | 323 | | |
286 | 324 | | |
287 | 325 | | |
288 | 326 | | |
289 | 327 | | |
290 | 328 | | |
| 329 | + | |
| 330 | + | |
| 331 | + | |
| 332 | + | |
| 333 | + | |
| 334 | + | |
291 | 335 | | |
292 | 336 | | |
293 | 337 | | |
| |||
0 commit comments