6.3. Algorithm
The tactic operates in five phases:
6.3.1. Goal parsing
Extract the computations from a goal of the form
Pr[= z | LHS] = Pr[= z | RHS] (or the probEvent variant).
6.3.2. Bind chain extraction
Walk each computation's right-associated bind chain, collecting the sequence of draw computations and the residual body expression.
6.3.3. Draw matching
Traverse the LHS and RHS bodies in parallel, collecting pairs of
de Bruijn indices at corresponding positions. Each pair (i, j)
means "LHS draw i fills the same role as RHS draw j." Draws
that appear in one body but not the other are classified as unused.
6.3.4. Unused draw insertion
If the RHS has more draws than the LHS (e.g., the DDH random
experiment samples an extra scalar c that does not appear in
the body), the tactic inserts matching unused draws at position 0
in the LHS using probOutput_bind_const.
6.3.5. Permutation and swap emission
The draw correspondence defines a permutation. The tactic decomposes
it into adjacent transpositions via bubble sort, then emits one
conv_lhs rewrite per swap using probEvent_bind_bind_swap (with
probEvent_bind_congr for nested swaps).