|
| 1 | +# Half-Tree DPF Spec Corrections |
| 2 | + |
| 3 | +Corrections to the algorithm spec extracted from "Half-Tree: Halving the Cost of Tree Expansion in COT and DPF" (Guo et al., Eurocrypt 2023). Found during implementation and verified by invariant analysis + 27 passing tests. |
| 4 | + |
| 5 | +## 1. CW formula (levels 1..n-1) |
| 6 | + |
| 7 | +Spec says: |
| 8 | +``` |
| 9 | +CW_i = H_S(node_0) ^ H_S(node_1) ^ alpha_i * Delta |
| 10 | +``` |
| 11 | + |
| 12 | +Correct formula: |
| 13 | +``` |
| 14 | +CW_i = H_S(node_0) ^ H_S(node_1) ^ (1 - alpha_i) * Delta |
| 15 | +``` |
| 16 | + |
| 17 | +Reason: the CW must make the off-path (non-alpha) direction converge (shares equal). When alpha_i = 0, on-path is left and off-path is right. The right child is `left ^ parent`, so its party difference includes Delta from the parent. XORing Delta into the CW cancels it for the right child while preserving Delta for the left (on-path) child. |
| 18 | + |
| 19 | +Derivation: for on-path parent (node0 ^ node1 = Delta, t0 ^ t1 = 1), the corrected child difference for direction x_i is: |
| 20 | + |
| 21 | +``` |
| 22 | +diff(x_i) = x_i * Delta ^ CW_term |
| 23 | +``` |
| 24 | + |
| 25 | +where CW_term = (1 - alpha_i) * Delta. So: |
| 26 | +- x_i = alpha_i (on-path): diff = alpha_i * Delta ^ (1-alpha_i) * Delta = Delta |
| 27 | +- x_i != alpha_i (off-path): diff = (1-alpha_i) * Delta ^ (1-alpha_i) * Delta = 0 |
| 28 | + |
| 29 | +## 2. HCW (level n) |
| 30 | + |
| 31 | +Spec says: |
| 32 | +``` |
| 33 | +HCW = high_{alpha_n}_0 ^ high_{alpha_n}_1 |
| 34 | +``` |
| 35 | + |
| 36 | +Correct formula: |
| 37 | +``` |
| 38 | +HCW = high_{!alpha_n}_0 ^ high_{!alpha_n}_1 |
| 39 | +``` |
| 40 | + |
| 41 | +Reason: HCW corrects the non-alpha direction so both parties converge on the high bits. The alpha direction's mismatch is absorbed by the output correction word (ocw/CW_{n+1}). |
| 42 | + |
| 43 | +## 3. LCW (level n) |
| 44 | + |
| 45 | +Spec says: |
| 46 | +``` |
| 47 | +LCW_0 = low_0_party0 ^ low_0_party1 ^ alpha_n |
| 48 | +LCW_1 = low_1_party0 ^ low_1_party1 ^ alpha_n |
| 49 | +``` |
| 50 | + |
| 51 | +Correct formula: |
| 52 | +``` |
| 53 | +LCW_0 = low_0_party0 ^ low_0_party1 ^ !alpha_n |
| 54 | +LCW_1 = low_1_party0 ^ low_1_party1 ^ alpha_n |
| 55 | +``` |
| 56 | + |
| 57 | +Reason: the corrected low-bit difference for sigma direction is: |
| 58 | +``` |
| 59 | +corrected_diff(sigma) = (low_sigma_0 ^ low_sigma_1) ^ LCW_sigma |
| 60 | +``` |
| 61 | + |
| 62 | +We need: alpha direction (sigma = alpha_n) has diff = 1, non-alpha direction (sigma = !alpha_n) has diff = 0. |
| 63 | + |
| 64 | +With the corrected formula: |
| 65 | +- sigma = 0: corrected diff = !alpha_n (so diff=1 when alpha_n=0, diff=0 when alpha_n=1) |
| 66 | +- sigma = 1: corrected diff = alpha_n (so diff=0 when alpha_n=0, diff=1 when alpha_n=1) |
| 67 | + |
| 68 | +This ensures exactly the alpha direction has low diff = 1 (one party adds ocw) and the non-alpha direction has low diff = 0 (cancellation). |
0 commit comments