proof: add mul expression helper bridges

[Th0rgal]

Summary

• add shared source/Yul value facts for Expr.mul
• add compile/source/builtin lemmas for compiled mul expressions
• add right- and left-threaded compositional and post-state helper bridges for Expr.mul
• regenerate PrintAxioms for the eight new public lemmas

Validation

• lean-slot lake build Compiler.Proofs.HelperStepProofs
• python3 scripts/check_proof_length.py
• python3 scripts/generate_print_axioms.py
• python3 scripts/generate_print_axioms.py --check
• git diff --check
• rg -n '\bsorry\b|\badmit\b|axiom |True :=|\t' Compiler/Proofs/HelperStepProofs.lean PrintAxioms.lean

[vercel]

The latest updates on your projects. Learn more about Vercel for GitHub.

Project	Deployment	Actions	Updated (UTC)
verity	Ready	Preview, Comment	Jul 11, 2026 8:11am