From 5b3a250656aa6b7617af7197f07d40ac984d2f9f Mon Sep 17 00:00:00 2001 From: zsumz Date: Thu, 17 Sep 2026 09:36:12 -0500 Subject: [PATCH] fix(ci): recalibrate scheduled simulator floors --- .../src/artifact_verify/tests/reports.rs | 14 +++++----- .../src/contract/profile/simulator.rs | 13 +++++---- .../profile/simulator/serde_support.rs | 28 ++++++++++++++----- .../profile/simulator/serde_support_test.rs | 26 +++++++++++++++++ .../src/contract/profile/simulator/tests.rs | 19 +++++++------ .../bin/rafter_model_check_fast/profile.rs | 4 +-- .../runner/exhaustive_test.rs | 22 ++++++++------- docs/model-checking.md | 22 ++++++++++----- verification/raft-invariant-profiles.json | 4 +-- zrail.lock | 12 ++++---- 10 files changed, 109 insertions(+), 55 deletions(-) create mode 100644 crates/rafter-invariants/src/contract/profile/simulator/serde_support_test.rs diff --git a/crates/rafter-invariants/src/artifact_verify/tests/reports.rs b/crates/rafter-invariants/src/artifact_verify/tests/reports.rs index 9243143f..d2f594aa 100644 --- a/crates/rafter-invariants/src/artifact_verify/tests/reports.rs +++ b/crates/rafter-invariants/src/artifact_verify/tests/reports.rs @@ -245,25 +245,25 @@ fn scheduled_log(source_ref: &str) -> String { "event": "exhaustive-check", "check_id": "raft-election-nightly", "status": "pass", - "unique_protocol_states": 5_000_000, + "unique_protocol_states": 3_000_000, "unique_verifier_states": 5_000_000, })), event(&json!({ "event": "exhaustive-check", "check_id": "raft-commit-nightly", "status": "pass", - "unique_protocol_states": 8_000_000, - "unique_verifier_states": 8_000_000, + "unique_protocol_states": 5_000_000, + "unique_verifier_states": 6_000_000, })), event(&json!({ "event": "profile-total", "check_id": "raft-profile-total-nightly", "profile": "raft-nightly", "status": "pass", - "unique_protocol_states": 13_000_000, - "unique_verifier_states": 13_000_000, - "target_protocol_states": 13_000_000, - "target_verifier_states": 13_000_000, + "unique_protocol_states": 8_000_000, + "unique_verifier_states": 11_000_000, + "target_protocol_states": 8_000_000, + "target_verifier_states": 11_000_000, })), ]; for seed in seeds.split(',') { diff --git a/crates/rafter-invariants/src/contract/profile/simulator.rs b/crates/rafter-invariants/src/contract/profile/simulator.rs index c801c81f..caa9d9bd 100644 --- a/crates/rafter-invariants/src/contract/profile/simulator.rs +++ b/crates/rafter-invariants/src/contract/profile/simulator.rs @@ -19,7 +19,8 @@ use serde_support::{optional_string_u64, state_floors, string_u64}; const PR_SOAK_STEPS: u64 = 320; const SCHEDULED_SOAK_STEPS: u64 = 1_024; const SCHEDULED_SEED_COUNT: u64 = 6; -const SCHEDULED_STATE_FLOOR: u64 = 13_000_000; +const SCHEDULED_PROTOCOL_STATE_FLOOR: u64 = 8_000_000; +const SCHEDULED_VERIFIER_STATE_FLOOR: u64 = 11_000_000; const SCHEDULED_LAYER_TIMEOUT: &str = "170m"; pub(crate) const PR_FAST_CHECK_IDS: [&str; 13] = [ @@ -127,7 +128,8 @@ impl SimulatorRunnerConfiguration { profile, SCHEDULED_SOAK_STEPS, SCHEDULED_SEED_COUNT, - SCHEDULED_STATE_FLOOR, + SCHEDULED_PROTOCOL_STATE_FLOOR, + SCHEDULED_VERIFIER_STATE_FLOOR, SCHEDULED_LAYER_TIMEOUT, ) => { @@ -143,7 +145,8 @@ impl SimulatorRunnerConfiguration { profile: &str, soak_steps: u64, seed_count: u64, - state_floor: u64, + protocol_state_floor: u64, + verifier_state_floor: u64, layer_timeout: &str, ) -> bool { // An unmapped lane has no reviewed model profile, so it matches nothing. @@ -161,8 +164,8 @@ impl SimulatorRunnerConfiguration { && self.canonical_check_binding.as_deref() == Some("scheduled-suffix-v1") && self.state_floors == SimulatorStateFloors::Aggregate { - protocol: state_floor, - verifier: state_floor, + protocol: protocol_state_floor, + verifier: verifier_state_floor, } } } diff --git a/crates/rafter-invariants/src/contract/profile/simulator/serde_support.rs b/crates/rafter-invariants/src/contract/profile/simulator/serde_support.rs index 8e5849a2..2e585210 100644 --- a/crates/rafter-invariants/src/contract/profile/simulator/serde_support.rs +++ b/crates/rafter-invariants/src/contract/profile/simulator/serde_support.rs @@ -30,13 +30,27 @@ where if value == "per-evidence" { return Ok(SimulatorStateFloors::PerEvidence); } - let count = value - .strip_suffix("-protocol-and-verifier") - .ok_or_else(|| de::Error::custom("unsupported simulator state-floor policy"))? - .parse::() - .map_err(de::Error::custom)?; + if let Some(count) = value.strip_suffix("-protocol-and-verifier") { + let count = count.parse::().map_err(de::Error::custom)?; + return Ok(SimulatorStateFloors::Aggregate { + protocol: count, + verifier: count, + }); + } + let (protocol, verifier) = value + .split_once("-protocol-") + .and_then(|(protocol, verifier)| { + verifier + .strip_suffix("-verifier") + .map(|verifier| (protocol, verifier)) + }) + .ok_or_else(|| de::Error::custom("unsupported simulator state-floor policy"))?; Ok(SimulatorStateFloors::Aggregate { - protocol: count, - verifier: count, + protocol: protocol.parse().map_err(de::Error::custom)?, + verifier: verifier.parse().map_err(de::Error::custom)?, }) } + +#[cfg(test)] +#[path = "serde_support_test.rs"] +mod tests; diff --git a/crates/rafter-invariants/src/contract/profile/simulator/serde_support_test.rs b/crates/rafter-invariants/src/contract/profile/simulator/serde_support_test.rs new file mode 100644 index 00000000..d5248876 --- /dev/null +++ b/crates/rafter-invariants/src/contract/profile/simulator/serde_support_test.rs @@ -0,0 +1,26 @@ +//! State-floor spelling compatibility tests. + +use serde::Deserialize; + +use super::{state_floors, SimulatorStateFloors}; + +#[derive(Deserialize)] +struct Fixture { + #[serde(deserialize_with = "state_floors")] + state_floors: SimulatorStateFloors, +} + +#[test] +fn shared_historical_floor_format_remains_supported() { + let fixture: Fixture = serde_json::from_value(serde_json::json!({ + "state_floors": "13000000-protocol-and-verifier" + })) + .expect("historical shared floor deserializes"); + assert_eq!( + fixture.state_floors, + SimulatorStateFloors::Aggregate { + protocol: 13_000_000, + verifier: 13_000_000, + } + ); +} diff --git a/crates/rafter-invariants/src/contract/profile/simulator/tests.rs b/crates/rafter-invariants/src/contract/profile/simulator/tests.rs index 895d4810..9d65e606 100644 --- a/crates/rafter-invariants/src/contract/profile/simulator/tests.rs +++ b/crates/rafter-invariants/src/contract/profile/simulator/tests.rs @@ -27,7 +27,7 @@ fn simulator_contract_deserializes_numeric_and_floor_policy() { ("seed_count", "6"), ("seed_policy", "source-derived-sha256-v1"), ("soak_steps", "1024"), - ("state_floors", "13000000-protocol-and-verifier"), + ("state_floors", "8000000-protocol-11000000-verifier"), ("termination_grace", "30s"), ("canonical_check_binding", "scheduled-suffix-v1"), ]); @@ -41,8 +41,8 @@ fn simulator_contract_deserializes_numeric_and_floor_policy() { assert_eq!( contract.state_floors, SimulatorStateFloors::Aggregate { - protocol: 13_000_000, - verifier: 13_000_000, + protocol: 8_000_000, + verifier: 11_000_000, } ); contract @@ -277,7 +277,7 @@ fn simulator_contract_rejects_weakened_pr_thresholds() { fn simulator_contract_rejects_weakened_nightly_thresholds() { assert_weakened_scheduled_thresholds_are_rejected( "nightly", - reviewed_scheduled_contract("nightly", 1_024, 6, 13_000_000), + reviewed_scheduled_contract("nightly", 1_024, 6, 8_000_000, 11_000_000), ); } @@ -285,7 +285,7 @@ fn simulator_contract_rejects_weakened_nightly_thresholds() { fn simulator_contract_rejects_weakened_weekly_thresholds() { assert_weakened_scheduled_thresholds_are_rejected( "weekly", - reviewed_scheduled_contract("weekly", 1_024, 6, 13_000_000), + reviewed_scheduled_contract("weekly", 1_024, 6, 8_000_000, 11_000_000), ); } @@ -294,7 +294,7 @@ fn simulator_contract_rejects_weakened_weekly_thresholds() { /// runner service killed three times running and that nothing produces today. #[test] fn simulator_contract_rejects_the_unrunnable_weekly_deep_bounds() { - let mut deep = reviewed_scheduled_contract("weekly", 4_096, 10, 250_000_000); + let mut deep = reviewed_scheduled_contract("weekly", 4_096, 10, 250_000_000, 250_000_000); deep.model_profile = "raft-weekly".to_owned(); deep.layer_timeout = "340m".to_owned(); assert!(deep.validate_profile("weekly").is_err()); @@ -367,7 +367,8 @@ fn reviewed_scheduled_contract( profile: &str, soak_steps: u64, seed_count: u64, - state_floor: u64, + protocol_state_floor: u64, + verifier_state_floor: u64, ) -> SimulatorRunnerConfiguration { SimulatorRunnerConfiguration { build: "release-and-test-locked".to_owned(), @@ -389,8 +390,8 @@ fn reviewed_scheduled_contract( snapshot_catchup_probe: None, soak_steps, state_floors: SimulatorStateFloors::Aggregate { - protocol: state_floor, - verifier: state_floor, + protocol: protocol_state_floor, + verifier: verifier_state_floor, }, termination_grace: "30s".to_owned(), canonical_check_binding: Some("scheduled-suffix-v1".to_owned()), diff --git a/crates/rafter-sim/src/bin/rafter_model_check_fast/profile.rs b/crates/rafter-sim/src/bin/rafter_model_check_fast/profile.rs index 236aa5b7..60efe07a 100644 --- a/crates/rafter-sim/src/bin/rafter_model_check_fast/profile.rs +++ b/crates/rafter-sim/src/bin/rafter_model_check_fast/profile.rs @@ -134,8 +134,8 @@ impl Profile { pub(crate) const fn exhaustive_targets(self) -> Option { match self { Self::RaftNightly => Some(ExhaustiveTargets { - protocol_states: 13_000_000, - verifier_states: 13_000_000, + protocol_states: 8_000_000, + verifier_states: 11_000_000, }), Self::RaftWeekly => Some(ExhaustiveTargets { protocol_states: 250_000_000, diff --git a/crates/rafter-sim/src/bin/rafter_model_check_fast/runner/exhaustive_test.rs b/crates/rafter-sim/src/bin/rafter_model_check_fast/runner/exhaustive_test.rs index dd27d35a..412e5b8b 100644 --- a/crates/rafter-sim/src/bin/rafter_model_check_fast/runner/exhaustive_test.rs +++ b/crates/rafter-sim/src/bin/rafter_model_check_fast/runner/exhaustive_test.rs @@ -8,22 +8,24 @@ use super::*; #[test] fn exhaustive_target_gate_requires_protocol_and_verifier_state_counts() { - assert_eq!( - target_values(Profile::RaftNightly), - (13_000_000, 13_000_000) - ); + assert_eq!(target_values(Profile::RaftNightly), (8_000_000, 11_000_000)); assert_eq!( target_values(Profile::RaftWeekly), (250_000_000, 250_000_000) ); assert_eq!(Profile::Fast.exhaustive_targets(), None); - let target = 13_000_000; + let protocol_target = 8_000_000; + let verifier_target = 11_000_000; - assert!(assert_exhaustive_targets(Profile::RaftNightly, target, target).is_ok()); - let protocol_error = assert_exhaustive_targets(Profile::RaftNightly, target - 1, target) - .expect_err("below-target protocol states should fail"); - let verifier_error = assert_exhaustive_targets(Profile::RaftNightly, target, target - 1) - .expect_err("below-target verifier states should fail"); + assert!( + assert_exhaustive_targets(Profile::RaftNightly, protocol_target, verifier_target).is_ok() + ); + let protocol_error = + assert_exhaustive_targets(Profile::RaftNightly, protocol_target - 1, verifier_target) + .expect_err("below-target protocol states should fail"); + let verifier_error = + assert_exhaustive_targets(Profile::RaftNightly, protocol_target, verifier_target - 1) + .expect_err("below-target verifier states should fail"); assert!(protocol_error.to_string().contains("protocol states")); assert!(verifier_error.to_string().contains("verifier states")); diff --git a/docs/model-checking.md b/docs/model-checking.md index b2812b2b..bfe878f9 100644 --- a/docs/model-checking.md +++ b/docs/model-checking.md @@ -40,7 +40,7 @@ is restored once a >=32GB — likely self-hosted — runner exists: | `model_profile` | `raft-nightly` | `raft-weekly` | | `seed_count` | `6` | `10` | | `soak_steps` | `1024` | `4096` | -| `state_floors` | `13000000-protocol-and-verifier` | `250000000-protocol-and-verifier` | +| `state_floors` | `8000000-protocol-11000000-verifier` | `250000000-protocol-and-verifier` | | `layer_timeout` | `170m` | `340m` | Only the lane's choice of profile moved. The `raft-weekly` profile definition @@ -859,12 +859,20 @@ Each exhaustive check reports two distinct cardinalities: Profile totals add each check's independently explored cardinality. They are not a globally deduplicated union. The scheduled gates enforce reviewed lower -bounds on both totals. Nightly and weekly both enforce 13 million, because -both lanes currently run the `raft-nightly` profile; the `raft-weekly` -profile's 250 million floor is the target recorded in -[Weekly simulator demotion](#weekly-simulator-demotion) and is not enforced by -any lane today. The floors are coverage ratchets; they do not control the -configured exploration depth or workloads. +bounds on both totals. Nightly and weekly both enforce 8 million protocol +states and 11 million verifier states, because both lanes currently run the +`raft-nightly` profile; the `raft-weekly` profile's 250 million floor is the +target recorded in [Weekly simulator demotion](#weekly-simulator-demotion) and +is not enforced by any lane today. The floors are coverage ratchets; they do +not control the configured exploration depth or workloads. + +Demand-driven replication removed proposal-time contact-only branches without +removing a scheduled check, configured depth, exhausted frontier, or required +semantic observation. The last pre-change run explored 13,834,518 protocol and +17,686,454 verifier states. Repeated post-change runs explore 8,508,629 and +11,122,812 respectively. The independent 8M/11M ratchets preserve that reviewed +state-space shape without requiring the optimized implementation to reproduce +the obsolete contact traffic. ## Retained Logical Prefixes diff --git a/verification/raft-invariant-profiles.json b/verification/raft-invariant-profiles.json index 4be9bffa..367f5a00 100644 --- a/verification/raft-invariant-profiles.json +++ b/verification/raft-invariant-profiles.json @@ -151,7 +151,7 @@ "simulator": { "producer": "rafter-invariants-simulator-v19", "command": ["cargo", "run", "--locked", "-p", "rafter-invariants", "--", "run", "--profile", "nightly", "--layer", "simulator"], - "configuration": {"build": "release-and-test-locked", "canonical_check_binding": "scheduled-suffix-v1", "compile_timeout": "10m", "completion": "frontier-and-aggregate-state-floor", "detector_proof": "inherited-descriptor-pre-body-secret-v3", "execution_contract": "rafter-soak-execution-v1", "finalization_reserve": "10m", "kill_confirmation_timeout": "5s", "layer_timeout": "170m", "liveness_report_binding": "typed-canonical-json-sha256-v3", "model_profile": "raft-nightly", "model_timeout_policy": "remaining-layer-budget", "receipt_finalization_allowance": "5s", "seed_count": "6", "seed_policy": "source-derived-sha256-v1", "soak_steps": "1024", "state_floors": "13000000-protocol-and-verifier", "termination_grace": "30s"}, + "configuration": {"build": "release-and-test-locked", "canonical_check_binding": "scheduled-suffix-v1", "compile_timeout": "10m", "completion": "frontier-and-aggregate-state-floor", "detector_proof": "inherited-descriptor-pre-body-secret-v3", "execution_contract": "rafter-soak-execution-v1", "finalization_reserve": "10m", "kill_confirmation_timeout": "5s", "layer_timeout": "170m", "liveness_report_binding": "typed-canonical-json-sha256-v3", "model_profile": "raft-nightly", "model_timeout_policy": "remaining-layer-budget", "receipt_finalization_allowance": "5s", "seed_count": "6", "seed_policy": "source-derived-sha256-v1", "soak_steps": "1024", "state_floors": "8000000-protocol-11000000-verifier", "termination_grace": "30s"}, "minimum_observed_checks": 79, "require_peak_rss": true }, @@ -196,7 +196,7 @@ "simulator": { "producer": "rafter-invariants-simulator-v19", "command": ["cargo", "run", "--locked", "-p", "rafter-invariants", "--", "run", "--profile", "weekly", "--layer", "simulator"], - "configuration": {"build": "release-and-test-locked", "canonical_check_binding": "scheduled-suffix-v1", "compile_timeout": "10m", "completion": "frontier-and-aggregate-state-floor", "detector_proof": "inherited-descriptor-pre-body-secret-v3", "execution_contract": "rafter-soak-execution-v1", "finalization_reserve": "10m", "kill_confirmation_timeout": "5s", "layer_timeout": "170m", "liveness_report_binding": "typed-canonical-json-sha256-v3", "model_profile": "raft-nightly", "model_timeout_policy": "remaining-layer-budget", "receipt_finalization_allowance": "5s", "seed_count": "6", "seed_policy": "source-derived-sha256-v1", "soak_steps": "1024", "state_floors": "13000000-protocol-and-verifier", "termination_grace": "30s"}, + "configuration": {"build": "release-and-test-locked", "canonical_check_binding": "scheduled-suffix-v1", "compile_timeout": "10m", "completion": "frontier-and-aggregate-state-floor", "detector_proof": "inherited-descriptor-pre-body-secret-v3", "execution_contract": "rafter-soak-execution-v1", "finalization_reserve": "10m", "kill_confirmation_timeout": "5s", "layer_timeout": "170m", "liveness_report_binding": "typed-canonical-json-sha256-v3", "model_profile": "raft-nightly", "model_timeout_policy": "remaining-layer-budget", "receipt_finalization_allowance": "5s", "seed_count": "6", "seed_policy": "source-derived-sha256-v1", "soak_steps": "1024", "state_floors": "8000000-protocol-11000000-verifier", "termination_grace": "30s"}, "minimum_observed_checks": 79, "require_peak_rss": true }, diff --git a/zrail.lock b/zrail.lock index 8939dc84..a312c7ca 100644 --- a/zrail.lock +++ b/zrail.lock @@ -5,7 +5,7 @@ producer = "0.0.3-rc.8" contract_sha256 = "20e920843c8289957159973f9a2cbe3448f7f71e977f24ed24c8a6241589ca4a" [analysis] -inventory_sha256 = "9b2327c3915bf62f3e4dec056e0c6519ab6e7932bc7370df790109358a5ab96b" +inventory_sha256 = "3fb2594e9f6eb6d5fdd10c3abb2a15c16f57ab4e9b0a4910dcfe6dcf7c30be40" exclusions_sha256 = "938ddad6868e3a6a928a0720de503d2c6745c1ed05522321fd81e0d2a9f4c6ca" cargo_lock_sha256 = "842f09a5e4891422572b95ec5140da82b6b1c8278e29c9cf3e7f0ed6e41dcca5" cargo_features_sha256 = "24b61d47c1d7b3cd8877a438029133a089a7d479a1f0f5c247da70fa1064d7b2" @@ -13,11 +13,11 @@ feature_worlds_sha256 = "e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991 feature_worlds = 0 packages = 16 targets = 150 -physical_rust_files = 2024 -base_source_contexts = 3473 +physical_rust_files = 2025 +base_source_contexts = 3474 derived_source_contexts = 0 -source_facts = 751115 -projection_queries = 2936493 +source_facts = 751196 +projection_queries = 2936621 projected_facts = 2512 unresolved_bindings = 0 analyzer_semantics = 6 @@ -1246,7 +1246,7 @@ inputs_sha256 = "d33a14fc45f06272ebe9cdfc49dc6efa4010f66a1dac5154097a64454cb9295 [[macro_implementation]] package = "rafter-invariants" directory = "crates/rafter-invariants" -inputs_sha256 = "2df1902753f77a7951269585fb2d597cca207de90e588ff2b52dd97c948a4a63" +inputs_sha256 = "1c9a1e06fb4859c0e708c43692716551cda70308e827b0b8d36b0d0f1f336680" [[macro_implementation]] package = "rafter-multiraft"