Skip to content

feat(uc): add reassociation-stable scheduler model - #174

Open
quangvdao wants to merge 1 commit into
mainfrom
codex/uc-scheduler-frontier
Open

feat(uc): add reassociation-stable scheduler model#174
quangvdao wants to merge 1 commit into
mainfrom
codex/uc-scheduler-frontier

Conversation

@quangvdao

@quangvdao quangvdao commented Aug 29, 2026

Copy link
Copy Markdown
Collaborator

Summary

The legacy UC process model installs the same Boolean sampler at every binary composition node. Consequently, a three-component system gives different effective scheduling weights to its leaves depending on whether it is parsed as (P ∥ Q) ∥ C, P ∥ (C ∥ Q), or Q ∥ (C ∥ P).

This PR adds the generic, probability-free foundation for fixing that problem:

  • ScheduleMass records a strictly positive frontier weight and adds under composition.
  • BinaryScheduler receives the masses of both subtrees instead of blindly flipping the same Boolean sampler.
  • IsFlat states the key semantic law: every hierarchical three-way draw agrees with one parenthesization-free flat draw; IsCoherent derives the swap and reassociation laws needed by UC factorization.
  • ScheduledOpenProcess preserves the existing binary process representation while carrying total frontier mass and using the mass-aware scheduler at composition nodes.
  • A canary demonstrates that merely carrying masses is not enough: a deterministic mass-sensitive policy can still violate reassociation, so the IsFlat premise is substantive.

This is deliberately probability-neutral. The next PolyFun slice is #176, and the concrete downstream ProbComp scheduler and its exact denotational flatness proof are in Verified-zkEVM/VCVio#572.

Validation

  • ./scripts/validate.sh --lint --test --axioms
  • zero sorry/axiom debt across the PolyFun namespace

@quangvdao
quangvdao force-pushed the codex/uc-scheduler-frontier branch from e5395b3 to 0288b73 Compare August 29, 2026 05:27
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant