Enforce single-commit PR

Workflow runs for Enforce single-commit PR

• fix(ecPhlEqobs): eqobs_in must not assume an abstract call preserves glob A for distinct oracles

  completed successfully:
  Enforce single-commit PR#1013:Pull request#1143synchronizebynamasikanam
  fix/eqobs-abs-oracle-glob

  Nov 13, 20266s
  More actions for workflow run 1013

• [docker] bump z3 and alt-ergo patches

  completed successfully:
  Enforce single-commit PR#1012:Pull request#1231synchronizebyfdupress
  docker-z3-5.3.4

  Nov 11, 20265s
  More actions for workflow run 1012

• Pocklington primality certificates

  completed successfully:
  Enforce single-commit PR#1011:Pull request#1233reopenedbybgregoir
  pocklington

  Nov 11, 20266s
  More actions for workflow run 1011

• ChaChaPoly: prove the Poly1305 bound and instantiate with RFC 8439

  failed:
  Enforce single-commit PR#1010:Pull request#1237synchronizebybgregoir
  poly1305

  Nov 11, 20268s
  More actions for workflow run 1010

• ChaChaPoly: prove the Poly1305 bound and instantiate with RFC 8439

  failed:
  Enforce single-commit PR#1009:Pull request#1237synchronizebybgregoir
  poly1305

  Nov 11, 20266s
  More actions for workflow run 1009

• ChaChaPoly: prove the Poly1305 bound and instantiate with RFC 8439

  failed:
  Enforce single-commit PR#1008:Pull request#1237synchronizebybgregoir
  poly1305

  Nov 10, 20265s
  More actions for workflow run 1008

• Pocklington primality certificates

  failed:
  Enforce single-commit PR#1007:Pull request#1233synchronizebybgregoir
  pocklington

  Nov 10, 20267s
  More actions for workflow run 1007

• ZModP: clone ZModpField with <= substitutions

  completed successfully:
  Enforce single-commit PR#1006:Pull request#1238openedbybgregoir
  zmodp-subst

  Nov 10, 20266s
  More actions for workflow run 1006

• ChaChaPoly: prove the Poly1305 bound and instantiate with RFC 8439

  failed:
  Enforce single-commit PR#1005:Pull request#1237synchronizebybgregoir
  poly1305

  Nov 10, 20268s
  More actions for workflow run 1005

• Pocklington primality certificates

  completed successfully:
  Enforce single-commit PR#1004:Pull request#1233synchronizebybgregoir
  pocklington

  Nov 10, 20265s
  More actions for workflow run 1004

• ChaChaPoly: prove the Poly1305 bound and instantiate with RFC 8439

  failed:
  Enforce single-commit PR#1003:Pull request#1237openedbybgregoir
  poly1305

  Nov 10, 20266s
  More actions for workflow run 1003

• [docker] bump z3 and alt-ergo patches

  completed successfully:
  Enforce single-commit PR#1002:Pull request#1231synchronizebyfdupress
  docker-z3-5.3.4

  Nov 10, 20266s
  More actions for workflow run 1002

• Pocklington primality certificates

  failed:
  Enforce single-commit PR#1001:Pull request#1233openedbybgregoir
  pocklington

  Nov 10, 20266s
  More actions for workflow run 1001

• algebra(Poly): evaluation, factor theorem, divisibility and root counting

  completed successfully:
  Enforce single-commit PR#1000:Pull request#1232openedbybgregoir
  poly-roots

  Nov 10, 20266s
  More actions for workflow run 1000

• [docker] bump z3 and alt-ergo patches

  completed successfully:
  Enforce single-commit PR#999:Pull request#1231openedbyfdupress
  docker-z3-5.3.4

  Nov 10, 20266s
  More actions for workflow run 999

• fix(ecPhlEqobs): eqobs_in must not assume an abstract call preserves glob A for distinct oracles

  completed successfully:
  Enforce single-commit PR#998:Pull request#1143synchronizebynamasikanam
  fix/eqobs-abs-oracle-glob

  Nov 6, 20267s
  More actions for workflow run 998

• fix(ecPhlEqobs): eqobs_in must not assume an abstract call preserves glob A for distinct oracles

  completed successfully:
  Enforce single-commit PR#997:Pull request#1143synchronizebynamasikanam
  fix/eqobs-abs-oracle-glob

  Nov 6, 20266s
  More actions for workflow run 997

• fix(ecPhlEqobs): eqobs_in must not assume an abstract call preserves glob A for distinct oracles

  completed successfully:
  Enforce single-commit PR#996:Pull request#1143synchronizebynamasikanam
  fix/eqobs-abs-oracle-glob

  Nov 6, 20268s
  More actions for workflow run 996

• fix: require bd <= 1 in the pHL while I v k eps rule

  completed successfully:
  Enforce single-commit PR#995:Pull request#1228synchronizebystrub
  fix/while-geq-bound

  Nov 6, 20265s
  More actions for workflow run 995

• fix(env): keep calls to applied parameters in partial applications

  completed successfully:
  Enforce single-commit PR#994:Pull request#1229openedbystrub
  fix-unsuspend-oinfos

  Nov 6, 20267s
  More actions for workflow run 994

• Enforce single-commit PR

  completed successfully:
  Enforce single-commit PR#993:Merge group checks requested
  Nov 4, 20267s
  More actions for workflow run 993

• fix: require bd <= 1 in the pHL while I v k eps rule

  completed successfully:
  Enforce single-commit PR#992:Pull request#1228openedbystrub
  fix/while-geq-bound

  Nov 4, 20267s
  More actions for workflow run 992

• fix(phl): check the bound of the upper-bound while rule on all memories

  completed successfully:
  Enforce single-commit PR#991:Pull request#1130synchronizebystrub
  Yiping106283:fix-phoare-while-le-bound

  Nov 4, 20266s
  More actions for workflow run 991

• feat(theories): make FinType.card abstract, specified by card_spec

  requires action with the application:
  Enforce single-commit PR#990:Pull request#1224synchronizebystrub
  mattc-try:feat/fintype-abstract-card

  Nov 4, 2026Action required
  More actions for workflow run 990

• fix(crush): the activated simplify databases apply to every reduction of crush

  completed successfully:
  Enforce single-commit PR#989:Pull request#1227synchronizebystrub
  fix/crush-hint-dbs

  Nov 3, 20266s
  More actions for workflow run 989