test(control_tree): cover facts→contract determinism

src/mir/control_tree/step_tree_contract_box.rs

@@ -130,4 +130,38 @@ mod tests {
         // BTreeSet should give stable order: a, m, z
         assert!(basis1.contains("writes=a,m,z"));
     }
+
+    #[test]
+    fn facts_are_order_independent() {
+        // Phase 120: Contract requirement - facts collection order doesn't affect contract
+        let mut facts1 = StepTreeFacts::new();
+        facts1.add_exit(ExitKind::Break);
+        facts1.add_exit(ExitKind::Return);
+        facts1.add_write("x".to_string());
+        facts1.add_write("y".to_string());
+        facts1.add_capability(StepCapability::Loop);
+        facts1.add_capability(StepCapability::If);
+
+        let mut facts2 = StepTreeFacts::new();
+        // Different order
+        facts2.add_capability(StepCapability::If);
+        facts2.add_write("y".to_string());
+        facts2.add_exit(ExitKind::Return);
+        facts2.add_capability(StepCapability::Loop);
+        facts2.add_write("x".to_string());
+        facts2.add_exit(ExitKind::Break);
+
+        let contract1 = StepTreeContractBox::from_facts(&facts1);
+        let contract2 = StepTreeContractBox::from_facts(&facts2);
+
+        // Contracts should be identical (BTreeSet guarantees stable order)
+        assert_eq!(contract1.exits, contract2.exits);
+        assert_eq!(contract1.writes, contract2.writes);
+        assert_eq!(contract1.required_caps, contract2.required_caps);
+
+        // Signature basis should match
+        let basis1 = contract1.signature_basis_string("Block");
+        let basis2 = contract2.signature_basis_string("Block");
+        assert_eq!(basis1, basis2);
+    }
 }