refactor(control_tree): include reads in StepTreeContract signature

Phase 124-P2:
- Add reads: BTreeSet<String> to StepTreeContract
- Include reads in signature_basis_string (format: ...;reads=...;...)
- Update from_facts() to copy reads from StepTreeFacts
- Update all StepTreeContract construction sites (builder.rs, parity.rs tests)
- Update test expected signature to include reads field
- Maintains determinism: BTreeSet guarantees stable iteration order

src/mir/control_tree/normalized_shadow/builder.rs

@@ -510,6 +510,7 @@ mod tests {
             contract: StepTreeContract {
                 exits: Default::default(),
                 writes: Default::default(),
+                reads: Default::default(), // Phase 124
                 required_caps: Default::default(),
                 cond_sig: Default::default(),
             },
@@ -532,6 +533,7 @@ mod tests {
             contract: StepTreeContract {
                 exits: Default::default(),
                 writes: Default::default(),
+                reads: Default::default(), // Phase 124
                 required_caps: Default::default(),
                 cond_sig: Default::default(),
             },

src/mir/control_tree/normalized_shadow/parity.rs

@@ -202,6 +202,7 @@ mod tests {
         StepTreeContract {
             exits: exits.into_iter().collect(),
             writes: writes.into_iter().map(String::from).collect(),
+            reads: Default::default(), // Phase 124
             required_caps: Default::default(),
             cond_sig: Default::default(),
         }

src/mir/control_tree/step_tree.rs

@@ -833,7 +833,7 @@ mod tests {
         let basis = tree.signature_basis_string();
         assert_eq!(
             basis,
-            "kinds=Block,Stmt(local(x)),If,Block,If,Block,Stmt(assign(x)),Block,Stmt(assign(x)),Block,Stmt(assign(x)),Stmt(print);exits=;writes=x;caps=If,NestedIf;conds=(lit:str:x == lit:str:x)|(lit:str:y == lit:str:z)"
+            "kinds=Block,Stmt(local(x)),If,Block,If,Block,Stmt(assign(x)),Block,Stmt(assign(x)),Block,Stmt(assign(x)),Stmt(print);exits=;writes=x;reads=;caps=If,NestedIf;conds=(lit:str:x == lit:str:x)|(lit:str:y == lit:str:z)"
         );
 
         let tree2 = StepTreeBuilderBox::build_from_block(&ast);

src/mir/control_tree/step_tree_contract_box.rs

@@ -1,4 +1,4 @@
-//! StepTreeContractBox - facts → contract transformation (Phase 120)
+//! StepTreeContractBox - facts → contract transformation (Phase 120, Phase 124)
 //!
 //! Responsibility:
 //! - Transform StepTreeFacts into StepTreeContract
@@ -10,6 +10,10 @@
 //! - Pure transformation: facts → contract (idempotent)
 //! - No AST traversal, no interpretation
 //! - Contract is the formatted representation of facts
+//!
+//! Phase 124 Changes:
+//! - Added reads to StepTreeContract
+//! - reads included in signature_basis_string
 
 use crate::mir::control_tree::step_tree_facts::StepTreeFacts;
 use crate::mir::control_tree::{ExitKind, StepCapability};
@@ -20,6 +24,8 @@ use std::collections::BTreeSet;
 pub struct StepTreeContract {
     pub exits: BTreeSet<ExitKind>,
     pub writes: BTreeSet<String>,
+    /// Phase 124: Variable reads (for Return(Variable) support)
+    pub reads: BTreeSet<String>,
     pub required_caps: BTreeSet<StepCapability>,
     pub cond_sig: Vec<String>,
 }
@@ -28,12 +34,14 @@ impl StepTreeContract {
     /// Generate signature basis string (stable representation for hashing)
     ///
     /// This is used for StepTreeSignature computation.
-    /// Format: "kinds=...;exits=...;writes=...;caps=...;conds=..."
+    /// Format: "kinds=...;exits=...;writes=...;reads=...;caps=...;conds=..."
     ///
     /// Invariants:
     /// - Span is NOT included (determinism)
     /// - BTreeSet iteration order is stable
     /// - cond_sig order is preserved from traversal
+    ///
+    /// Phase 124: reads added to signature
     pub fn signature_basis_string(&self, node_kinds: &str) -> String {
         let exits = self
             .exits
@@ -46,6 +54,7 @@ impl StepTreeContract {
             .collect::<Vec<_>>()
             .join(",");
         let writes = self.writes.iter().cloned().collect::<Vec<_>>().join(",");
+        let reads = self.reads.iter().cloned().collect::<Vec<_>>().join(",");
         let caps = self
             .required_caps
             .iter()
@@ -70,8 +79,8 @@ impl StepTreeContract {
         let cond_sig = self.cond_sig.join("|");
 
         format!(
-            "kinds={};exits={};writes={};caps={};conds={}",
+            "kinds={};exits={};writes={};reads={};caps={};conds={}",
-            node_kinds, exits, writes, caps, cond_sig
+            node_kinds, exits, writes, reads, caps, cond_sig
         )
     }
 }
@@ -86,10 +95,13 @@ impl StepTreeContractBox {
     /// - No decision-making
     /// - No AST traversal
     /// - Same facts → same contract (idempotent)
+    ///
+    /// Phase 124: reads added to contract
     pub fn from_facts(facts: &StepTreeFacts) -> StepTreeContract {
         StepTreeContract {
             exits: facts.exits.clone(),
             writes: facts.writes.clone(),
+            reads: facts.reads.clone(), // Phase 124
             required_caps: facts.required_caps.clone(),
             cond_sig: facts.cond_sig.clone(),
         }