light-client: uncomment model-based tests

[melekes]

Follow-up to #82

We need to find a way to regenerate JSON fixtures in the single_step folder. #82 brought v1.0.0 support, but broke the validator structure (pub_key_type and pub_key_bytes are now used instead of pub_key https://buf.build/cometbft/cometbft/docs/main:cometbft.types.v1#cometbft.types.v1.Validator).

In my last attempt to fix the tests, Apalache was giving me this error:

  Running model-based single-step test: TestMoreThanTwoThirdsSign
  > running Apalache...
Apalache run: # Usage statistics is OFF. We care about your privacy.
# If you want to help our project, consider enabling statistics with config --enable-stats=true.

Output directory: /private/var/folders/x_/bh7wnpbn4nvdbmt6vtw90xx40000gn/T/.tmptbyyXL/_apalache-out/MC4_4_faulty.tla/2025-06-03T15-37-47_3513012226433067632
# APALACHE version: 0.47.2 | build: def5e8e                       I@15:37:47.399
Tuning: search.outputTraces=false                                 I@15:37:47.408
PASS #0: SanyParser                                               I@15:37:47.506
Parsing file /private/var/folders/x_/bh7wnpbn4nvdbmt6vtw90xx40000gn/T/.tmptbyyXL/MC4_4_faulty.tla
Parsing file /private/var/folders/x_/bh7wnpbn4nvdbmt6vtw90xx40000gn/T/.tmptbyyXL/LightTests.tla
Parsing file /private/var/folders/x_/bh7wnpbn4nvdbmt6vtw90xx40000gn/T/.tmptbyyXL/Lightclient_003_draft.tla
Parsing file /private/var/folders/x_/bh7wnpbn4nvdbmt6vtw90xx40000gn/T/SANYXXXXXXXXXX.T7KBeOhJpX/Integers.tla
Parsing file /private/var/folders/x_/bh7wnpbn4nvdbmt6vtw90xx40000gn/T/SANYXXXXXXXXXX.T7KBeOhJpX/FiniteSets.tla
Parsing file /private/var/folders/x_/bh7wnpbn4nvdbmt6vtw90xx40000gn/T/SANYXXXXXXXXXX.T7KBeOhJpX/Naturals.tla
Parsing file /private/var/folders/x_/bh7wnpbn4nvdbmt6vtw90xx40000gn/T/.tmptbyyXL/Blockchain_003_draft.tla
Parsing file /private/var/folders/x_/bh7wnpbn4nvdbmt6vtw90xx40000gn/T/SANYXXXXXXXXXX.T7KBeOhJpX/__rewire_sequences_in_apalache.tla
Parsing file /private/var/folders/x_/bh7wnpbn4nvdbmt6vtw90xx40000gn/T/SANYXXXXXXXXXX.T7KBeOhJpX/__apalache_folds.tla
PASS #1: TypeCheckerSnowcat                                       I@15:37:47.838
 > Running Snowcat .::.                                           I@15:37:47.838
Operator MC4TypeAliases: Deprecated syntax in type alias BLOCKHEADER. Use camelCase of Type System 1.2. W@15:37:47.863
Operator MC4TypeAliases: Deprecated syntax in type alias BLOCK. Use camelCase of Type System 1.2. W@15:37:47.867
Operator MC4TypeAliases: Deprecated syntax in type alias BLOCKSTATUS. Use camelCase of Type System 1.2. W@15:37:47.868
Operator MC4TypeAliases: Deprecated syntax in type alias BLOCKS. Use camelCase of Type System 1.2. W@15:37:47.869
Operator BC!BCTypeAliases: Deprecated syntax in type alias BLOCKHEADER. Use camelCase of Type System 1.2. W@15:37:47.871
Operator BC!BCTypeAliases: Deprecated syntax in type alias BLOCKCHAIN. Use camelCase of Type System 1.2. W@15:37:47.872
Operator BC!BCTypeAliases: Deprecated syntax in type alias BLOCK. Use camelCase of Type System 1.2. W@15:37:47.874
Operator LCTypeAliases: Deprecated syntax in type alias BLOCKHEADER. Use camelCase of Type System 1.2. W@15:37:47.876
Operator LCTypeAliases: Deprecated syntax in type alias BLOCK. Use camelCase of Type System 1.2. W@15:37:47.878
Operator LCTypeAliases: Deprecated syntax in type alias BLOCKSTATUS. Use camelCase of Type System 1.2. W@15:37:47.878
Operator LCTypeAliases: Deprecated syntax in type alias BLOCKS. Use camelCase of Type System 1.2. W@15:37:47.878
 > Your types are purrfect!                                       I@15:37:48.381
 > All expressions are typed                                      I@15:37:48.381
PASS #2: ConfigurationPass                                        I@15:37:48.381
  > Set the initialization predicate to InitTest                  I@15:37:48.383
  > Set the transition predicate to NextTest                      I@15:37:48.383
  > Set an invariant to TestMoreThanTwoThirdsSignInv              I@15:37:48.383
PASS #3: DesugarerPass                                            I@15:37:48.386
  > Desugaring...                                                 I@15:37:48.386
PASS #4: InlinePass                                               I@15:37:48.395
Leaving only relevant operators: CInitPrimed, InitTest, InitTestPrimed, NextTest, TestMoreThanTwoThirdsSignInv I@15:37:48.395
PASS #5: TemporalPass                                             I@15:37:48.431
  > Rewriting temporal operators...                               I@15:37:48.431
  > No temporal property specified, nothing to encode             I@15:37:48.431
PASS #6: InlinePass                                               I@15:37:48.431
Leaving only relevant operators: CInitPrimed, InitTest, InitTestPrimed, NextTest, TestMoreThanTwoThirdsSignInv I@15:37:48.431
PASS #7: PrimingPass                                              I@15:37:48.435
  > Introducing InitTestPrimed for InitTest'                      I@15:37:48.436
PASS #8: VCGen                                                    I@15:37:48.513
  > Producing verification conditions from the invariant TestMoreThanTwoThirdsSignInv I@15:37:48.513
  > VCGen produced 1 verification condition(s)                    I@15:37:48.515
PASS #9: PreprocessingPass                                        I@15:37:48.515
  > Before preprocessing: unique renaming                         I@15:37:48.515
 > Applying standard transformations:                             I@15:37:48.518
  > PrimePropagation                                              I@15:37:48.518
  > Desugarer                                                     I@15:37:48.519
  > UniqueRenamer                                                 I@15:37:48.522
  > Normalizer                                                    I@15:37:48.525
  > Keramelizer                                                   I@15:37:48.528
  > After preprocessing: UniqueRenamer                            I@15:37:48.537
PASS #10: TransitionFinderPass                                    I@15:37:48.542
  > Found 1 initializing transitions                              I@15:37:48.579
  > Found 7 transitions                                           I@15:37:48.585
  > No constant initializer                                       I@15:37:48.585
  > Applying unique renaming                                      I@15:37:48.586
PASS #11: OptimizationPass                                        I@15:37:48.592
 > Applying optimizations:                                        I@15:37:48.595
  > ConstSimplifier                                               I@15:37:48.595
  > ExprOptimizer                                                 I@15:37:48.606
  > SetMembershipSimplifier                                       I@15:37:48.615
  > ConstSimplifier                                               I@15:37:48.618
PASS #12: AnalysisPass                                            I@15:37:48.629
 > Marking skolemizable existentials and sets to be expanded...   I@15:37:48.630
  > Skolemization                                                 I@15:37:48.630
  > Expansion                                                     I@15:37:48.631
  > Remove unused let-in defs                                     I@15:37:48.636
 > Running analyzers...                                           I@15:37:48.640
  > Introduced expression grades                                  I@15:37:48.643
PASS #13: BoundedChecker                                          I@15:37:48.643
State 0: Checking 1 state invariants                              I@15:37:49.571
State 0: state invariant 0 holds.                                 I@15:37:49.575
Step 0: picking a transition out of 1 transition(s)               I@15:37:49.577
State 1: Checking 1 state invariants                              I@15:37:49.620
State 1: state invariant 0 holds.                                 I@15:37:49.628
State 1: Checking 1 state invariants                              I@15:37:49.685
State 1: state invariant 0 holds.                                 I@15:37:49.695
State 1: Checking 1 state invariants                              I@15:37:49.744
State 1: state invariant 0 holds.                                 I@15:37:49.752
Step 1: Transition #3 is disabled                                 I@15:37:49.756
Step 1: Transition #4 is disabled                                 I@15:37:49.778
Step 1: Transition #5 is disabled                                 I@15:37:49.798
Step 1: Transition #6 is disabled                                 I@15:37:49.819
Step 1: picking a transition out of 3 transition(s)               I@15:37:49.820
State 2: Checking 1 state invariants                              I@15:37:49.890
State 2: state invariant 0 holds.                                 I@15:37:49.905
State 2: Checking 1 state invariants                              I@15:37:49.992
State 2: state invariant 0 holds.                                 I@15:37:50.009
State 2: Checking 1 state invariants                              I@15:37:50.061
State 2: state invariant 0 holds.                                 I@15:37:50.079
Step 2: Transition #3 is disabled                                 I@15:37:50.093
State 2: Checking 1 state invariants                              I@15:37:50.155
State 2: state invariant 0 holds.                                 I@15:37:50.178
State 2: Checking 1 state invariants                              I@15:37:50.249
State 2: state invariant 0 holds.                                 I@15:37:50.262
Step 2: Transition #6 is disabled                                 I@15:37:50.314
Step 2: picking a transition out of 5 transition(s)               I@15:37:50.315
State 3: Checking 1 state invariants                              I@15:37:50.481
Check the trace in: /private/var/folders/x_/bh7wnpbn4nvdbmt6vtw90xx40000gn/T/.tmptbyyXL/_apalache-out/MC4_4_faulty.tla/2025-06-03T15-37-47_3513012226433067632/violation1.tla, /private/var/folders/x_/bh7wnpbn4nvdbmt6vtw90xx40000gn/T/.tmptbyyXL/_apalache-out/MC4_4_faulty.tla/2025-06-03T15-37-47_3513012226433067632/MCviolation1.out, /private/var/folders/x_/bh7wnpbn4nvdbmt6vtw90xx40000gn/T/.tmptbyyXL/_apalache-out/MC4_4_faulty.tla/2025-06-03T15-37-47_3513012226433067632/violation1.json, /private/var/folders/x_/bh7wnpbn4nvdbmt6vtw90xx40000gn/T/.tmptbyyXL/_apalache-out/MC4_4_faulty.tla/2025-06-03T15-37-47_3513012226433067632/violation1.itf.json I@15:37:50.709
State 3: state invariant 0 violated.                              I@15:37:50.709
Found 1 error(s)                                                  I@15:37:50.710
The outcome is: Error                                             I@15:37:50.721
Checker has found an error                                        I@15:37:50.727
It took me 0 days  0 hours  0 min  3 sec                          I@15:37:50.727
Total time: 3.327 sec                                             I@15:37:50.727
EXITCODE: ERROR (12)

Apalache version: https://github.com/apalache-mc/apalache/releases/tag/v0.47.2

[bugarela]

@melekes I took a quick look and it seems like this is where you need to update the new fields: https://github.com/cometbft/cometbft-rs/blob/main/testgen/src/validator.rs#L157

Do you think you could try and make the change? I haven't even figure out how to run the MBT tests on my machine yet, I just browsed around so far - so maybe it's more productive if you try it in your setup, but let me know what you prefer.

[melekes]

Most of the tests are now uncommented ✔ thanks to @bugarela! The remaining we will have to look in later.