Skip to content

Commit 046b701

Browse files
committed
Keep multi-seed Foundry lane bounded
1 parent 926a09c commit 046b701

6 files changed

Lines changed: 19 additions & 8 deletions

File tree

.github/workflows/verify.yml

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1621,7 +1621,8 @@ jobs:
16211621
run: |
16221622
echo "::group::Testing with seed ${{ matrix.seed }}"
16231623
echo "DIFFTEST_RANDOM_SEED=${{ matrix.seed }}"
1624-
forge test
1624+
echo "Skipping Random10000 here; the sharded seed-42 Foundry job owns that stress lane."
1625+
forge test --no-match-test "Random10000"
16251626
echo "::endgroup::"
16261627
16271628
- name: Report seed-specific failure

docs/VERIFICATION_STATUS.md

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -225,7 +225,7 @@ Also note that the macro-generated `*_semantic_preservation` theorems are not co
225225

226226
## Differential Testing
227227

228-
**Status**: CI runs large sharded randomized differential suites against the current contract set, comparing EDSL interpreter output against Solidity-compiled EVM execution.
228+
**Status**: CI runs large sharded randomized differential suites against the current contract set, comparing EDSL interpreter output against Solidity-compiled EVM execution. The seed-42 shard set owns the `Random10000` stress lane; the multi-seed lane skips that target so it can cover cheaper randomized/property tests across several seeds without serially repeating the slowest stress suite.
229229

230230
## Solidity Interop Support Matrix (Issue #586)
231231

scripts/check_verify_sync.py

Lines changed: 7 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1294,8 +1294,13 @@ def env(job_body: str, key: str, ctx: str) -> str:
12941294
"foundry-patched --no-match-test target mismatch: "
12951295
f"workflow={patched_target!r}, spec={spec['expected_foundry_patched']['no_match_test']!r}"
12961296
)
1297-
if _extract_no_match_target(multiseed_cmd) is not None:
1298-
errors.append("foundry-multi-seed must not use --no-match-test")
1297+
multiseed_expected = spec["expected_foundry_multi_seed"]
1298+
multiseed_target = _extract_no_match_target(multiseed_cmd)
1299+
if multiseed_target != multiseed_expected["no_match_test"]:
1300+
errors.append(
1301+
"foundry-multi-seed --no-match-test target mismatch: "
1302+
f"workflow={multiseed_target!r}, spec={multiseed_expected['no_match_test']!r}"
1303+
)
12991304

13001305
patched_expected = spec["expected_foundry_patched"]
13011306
for key, expected in [

scripts/test_multiple_seeds.sh

Lines changed: 5 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -34,7 +34,10 @@ for seed in "${SEEDS[@]}"; do
3434
echo "Testing seed: $seed"
3535
echo "--------------------------------------"
3636

37-
if FOUNDRY_PROFILE=difftest DIFFTEST_RANDOM_SEED="$seed" DIFFTEST_SHARD_COUNT=1 DIFFTEST_SHARD_INDEX=0 DIFFTEST_RANDOM_SMALL=100 DIFFTEST_RANDOM_LARGE=10000 forge test; then
37+
# The sharded seed-42 CI lane owns Random10000 stress coverage. This
38+
# script is the multi-seed lane, so keep it focused on cheaper randomized
39+
# and property coverage across seeds.
40+
if FOUNDRY_PROFILE=difftest DIFFTEST_RANDOM_SEED="$seed" DIFFTEST_SHARD_COUNT=1 DIFFTEST_SHARD_INDEX=0 DIFFTEST_RANDOM_SMALL=100 DIFFTEST_RANDOM_LARGE=10000 forge test --no-match-test "Random10000"; then
3841
echo "✅ Seed $seed: PASSED"
3942
else
4043
echo "❌ Seed $seed: FAILED"
@@ -56,7 +59,7 @@ if [ ${#FAILED_SEEDS[@]} -gt 0 ]; then
5659
echo ""
5760
echo "To reproduce a failure:"
5861
for failed_seed in "${FAILED_SEEDS[@]}"; do
59-
echo " FOUNDRY_PROFILE=difftest DIFFTEST_RANDOM_SEED=$failed_seed DIFFTEST_SHARD_COUNT=1 DIFFTEST_SHARD_INDEX=0 DIFFTEST_RANDOM_SMALL=100 DIFFTEST_RANDOM_LARGE=10000 forge test -vv"
62+
echo " FOUNDRY_PROFILE=difftest DIFFTEST_RANDOM_SEED=$failed_seed DIFFTEST_SHARD_COUNT=1 DIFFTEST_SHARD_INDEX=0 DIFFTEST_RANDOM_SMALL=100 DIFFTEST_RANDOM_LARGE=10000 forge test --no-match-test \"Random10000\" -vv"
6063
done
6164
exit 1
6265
else

scripts/verify_sync_spec.json

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -810,7 +810,8 @@
810810
999,
811811
12345,
812812
67890
813-
]
813+
],
814+
"no_match_test": "Random10000"
814815
},
815816
"expected_foundry_gas_calibration": {
816817
"profile": "difftest",

scripts/verify_sync_spec_source.py

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -695,7 +695,8 @@
695695
'shard_count': 1,
696696
'shard_index': 0,
697697
'no_match_test': 'Random10000'},
698-
'expected_foundry_multi_seed': {'seeds': [0, 1, 42, 123, 999, 12345, 67890]},
698+
'expected_foundry_multi_seed': {'seeds': [0, 1, 42, 123, 999, 12345, 67890],
699+
'no_match_test': 'Random10000'},
699700
'expected_foundry_gas_calibration': {'profile': 'difftest',
700701
'artifact': 'static-gas-report',
701702
'command': 'python3 scripts/check_gas.py calibration '

0 commit comments

Comments
 (0)