Repository navigation
refactor(crypto): share pointwise and mixture game advantage bounds #802
Description
Extract the two generic Game.advantage_le_of_apply_le and Game.advantage_bind_le lemmas from reviewed #752 into their own shared-support PR, as required by #733 and the current review. Main currently has neither lemma; Game.coe_succProbability already exists and should be reused.
Scope: preserve the exact statements/proofs and original Jetski author/session credit, place them in the existing shared Game module, and validate representative existing game use plus required repository checks. No new game model or Feistel mathematics, no quantitative CCA completion claim, and no change to the remaining #748 objective. #752 must later restack on the actual shared-support squash.
Coordinator-codex-01a16ab8 assigns the bounded extraction to worker /root/audit_prerequisites on a fresh isolated branch. The author has not responded since the current changes-requested handoff exceeded three hours; this is only the independently deliverable shared prerequisite, not takeover of the whole Feistel PR. The mandatory automation/Crypto sweep integration retains priority and may preempt at a preserved checkpoint. Refs #733, #748.
Activity
SamuelSchlesinger commentedon Oct 24, 2026
Worker coordinator-codex-01a16ab8/audit_prerequisites claims this bounded shared prerequisite on branch
refactor/game-advantage-bounds-802-codex, new worktree/home/samuel/Code/complexitylib-codex/game-advantage-802, based on actual main13759271. I will extract onlyGame.advantage_le_of_apply_leandGame.advantage_bind_lefrom reviewed31bbf19f, preserving Jetski proof/credit and reusing existingGame.coe_succProbability. No Feistel mathematics, branch edits or CCA completion claim. This can pause at a clean checkpoint for the higher-priority Crypto integration.SamuelSchlesinger commentedon Oct 24, 2026
Worker coordinator-codex-01a16ab8/audit_prerequisites: awaiting independent review at PR #804, exact9fd1fdf0. All six local gates, strict S3, hygiene and catalogue pass; the two source/proof blocks retain Jetski's reviewed31bbf19f code. No Feistel source or remaining CCA objective is changed. The clean worktree is preserved while the coordinator preempts this worker for mandatory Crypto integration.
refactor(crypto): share pointwise and mixture advantage bounds (cslib…
feat(crypto): Feistel networks and the Luby-Rackoff theorem (#748)
feat(crypto): Feistel networks and the Luby-Rackoff theorem (cslib-co…