fix(ci): recalibrate scheduled simulator floors

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(',') {

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,
                 }
     }
 }

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::<u64>()
-        .map_err(de::Error::custom)?;
+    if let Some(count) = value.strip_suffix("-protocol-and-verifier") {
+        let count = count.parse::<u64>().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;

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,
+        }
+    );
+}

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,15 +277,15 @@ 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),
     );
 }
 
 #[test]
 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()),

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<ExhaustiveTargets> {
         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,

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"));

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
 

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
         },

zrail.lock

@@ -5,19 +5,19 @@ 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"
 feature_worlds_sha256 = "e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855"
 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"