bind_vcgen_sum — a mapSum-extended run-to-completion driver

spcomp_normalize_sum / bind_vcgen_sum extend the base spcomp_normalize / bind_vcgen drivers (run-to-completion for SPComp-equality goals) with the mapSum .inl/.inr rewrites, so a bind-chain that dispatches on a Sum-typed interface flattens. This is what the genuine-UC view equalities over Sum-typed interfaces need (e.g. pedersen_view_eq, sigma_view_eq). The mapSum lemmas live in CatCryptCore.Crypto.UC, above the base BindVcgen layer.

def CatCrypt.Tactic.tacticSpcomp_normalize_sum : Lean.ParserDescr

mapSum-extended normalization: like spcomp_normalize, but the simp only set additionally fires mapSum_inr / mapSum_inl, so a bind-chain that dispatches on a Sum-typed interface flattens. Fails cleanly on no progress (safe inside first / repeat).

Equations

• CatCrypt.Tactic.tacticSpcomp_normalize_sum = Lean.ParserDescr.node `CatCrypt.Tactic.tacticSpcomp_normalize_sum 1024 (Lean.ParserDescr.nonReservedSymbol "spcomp_normalize_sum" false)

def CatCrypt.Tactic.tacticBind_vcgen_sumUsing_ : Lean.ParserDescr

mapSum-extended run-to-completion driver for SPComp-equality goals: the bind_vcgen loop with spcomp_normalize_sum in place of spcomp_normalize, so it also closes the mapSum reassociation steps of Sum-typed view equalities.

bind_vcgen_sum using e applies the change of variables SPComp.sample_bind_equiv e to the sample-residual (right-hand side only), then peels again.

Equations

• One or more equations did not get rendered due to their size.