---
id: H19
title: The 9-step local collision holds with probability 1 in the XOR-linearised model and with low, position-dependent probability
  in the real step function
axis: C
kind: sha256
statement: The Chabaud–Joux/Gilbert–Handschuh correction pattern cancels any single-bit difference after 9 linearised steps
  (machine-checked); with modular additions the same pattern succeeds with probability ≈ 2^-c (c measured per bit position,
  highest at the MSB), and SAT finds conforming message words in seconds.
motivation: C3/C4.
assumptions: Linearisation of Ch and Maj as in Gilbert–Handschuh 2003.
expected_contribution: Reproduction of a classical result with a formal proof of the linear part.
related_work:
- chabaud1998differential
- gilbert2003security
- nikolic2008collisions
possible_counterexamples: Linearised cancellation failing for some δ (ruled out by bv_decide).
verification_strategy: experiments/reduced_round_sha256/local_collision.py + formal/ Lean theorem.
computational_budget: minutes
status: evaluated
classification: known_reproduced
evidence:
- results/reduced_round_sha256/summary.json
- results/reduced_round_sha256/local_collision.json
- formal/README.md
verdict: 'Pattern (δ, Σ0δ⊕Σ1δ, Σ1(Σ0δ), 0, δ, Σ0δ⊕Σ1δ, 0, 0, δ) cancels in the linearised model for all δ (GF(2) check + Lean
  theorem localCollision_absorb). Real step: 0 collisions in 32 × 100 000 samples (bound 3·10⁻⁵); survival after step i 0.25
  (bits 0–30) / 1.0 (bit 31), after i+1 ≈ 10⁻⁴, after i+2 zero. SAT finds conforming pairs for all 32 positions in 4.4–118
  s, all verified.'
---

# H19 — The 9-step local collision holds with probability 1 in the XOR-linearised model and with low, position-dependent probability in the real step function

The Chabaud–Joux/Gilbert–Handschuh correction pattern cancels any single-bit difference after 9 linearised steps (machine-checked); with modular additions the same pattern succeeds with probability ≈ 2^-c (c measured per bit position, highest at the MSB), and SAT finds conforming message words in seconds.