All pull requests

Pull requests

• chore!: rename the module root to CslibFrontier (flag day; DO NOT QUEUE)

  #3712·SamuelSchlesinger opened Nov 8, 2026Collaborator·

  ·

• doc: generalize the documentation for cslib-frontier

  #3711·SamuelSchlesinger opened Nov 8, 2026Collaborator·

  ·

• refactor(Foundations): split long SimpleGraph proofs

  #3710·SamuelSchlesinger opened Nov 8, 2026Collaborator·

  ·

• perf(Complexity): make ComputableInPolyTime locally irreducible in slow fun_prop modules

  #3709·SamuelSchlesinger opened Nov 8, 2026Collaborator·

  ·

• feat(crypto): subroutine replacement and the UC composition theorem

  #3708·karnseth opened Nov 8, 2026Collaborator·

  ·

• refactor(Circuit): share duplicated gate cases in the tableau proofs

  #3707·SamuelSchlesinger opened Nov 8, 2026Collaborator·

  ·

• refactor(Complexity): add inputAt lookup lemmas and shorten input-symbol realization proofs

  #3706·SamuelSchlesinger opened Nov 8, 2026Collaborator·

  ·

• refactor(Algorithms/Lean/MaxFlow): name the visited-table facts in the Hopcroft-Karp DFS proof

  #3705·SamuelSchlesinger opened Nov 8, 2026Collaborator·

  ·

• refactor(QuotientFilter): restructure insert/delete invariant proofs around shared cluster lemmas

  #3704·SamuelSchlesinger opened Nov 8, 2026Collaborator·

  ·

• feat(DataStructure/BTree): port B-tree node-visit bounds from EpsilonEridani

  #3702·SamuelSchlesinger opened Nov 8, 2026Collaborator·

  ·
  1

• feat(DataStructure/BTree): port B-tree erasure from EpsilonEridani

  #3701·SamuelSchlesinger opened Nov 8, 2026Collaborator·

  ·

• refactor(PolyTime): split bounded-incidence exactness proofs into named lemmas

  #3700·SamuelSchlesinger opened Nov 8, 2026Collaborator·

  ·

• perf(Circuit): avoid unfolding ComputableInPolyTime in FastContractionMachine and PathNetworkPolyTime

  #3699·SamuelSchlesinger opened Nov 8, 2026Collaborator·

  ·

• feat(WordRAM): add Resizable Word RAM model, ExecBounded realize bridge, and ExecRCodeDist

  #3698·orbitingflea opened Nov 8, 2026Collaborator·

  ·

• refactor(Crypto): move general ZMod (N ^ 2) lemmas out of Paillier

  #3697·SamuelSchlesinger opened Nov 8, 2026Collaborator·

  ·

• feat(DataStructure/BTree): port B-tree insertion and bulk loading from EpsilonEridani

  #3696·SamuelSchlesinger opened Nov 8, 2026Collaborator·

  ·

• feat(DataStructure/BTree): port B-tree point and range queries from EpsilonEridani

  #3695·SamuelSchlesinger opened Nov 8, 2026Collaborator·

  ·

• feat(DataStructure/BTree): port B-tree structure and height bounds from EpsilonEridani

  #3694·SamuelSchlesinger opened Nov 8, 2026Collaborator·

  ·

• feat(Foundations/Data/List): port sorted association lists from EpsilonEridani

  #3693·SamuelSchlesinger opened Nov 8, 2026Collaborator·

  ·
  1

• refactor(Problems): split the padMajority model count into its steps

  #3692·SamuelSchlesinger opened Nov 8, 2026Collaborator·

  ·

• refactor(Foundations): split long LinearAlgebra/Matrix proofs

  #3691·SamuelSchlesinger opened Nov 8, 2026Collaborator·

  ·

• perf(tests): run concrete word-RAM programs with a proved fast interpreter

  #3690·SamuelSchlesinger opened Nov 8, 2026Collaborator·

  ·

• refactor(FineGrained): shorten exhaustive-search and reduction time bounds

  #3689·SamuelSchlesinger opened Nov 8, 2026Collaborator·

  ·

• chore(scripts): three-way aggregate style detection and #3610 follow-ups (#3624)

  #3688·SamuelSchlesinger opened Nov 8, 2026Collaborator·Queued
  1

• refactor(Algorithms/Lean/GomoryHu): name the tree-edge facts in Gusfield's uncrossing step

  #3687·SamuelSchlesinger opened Nov 8, 2026Collaborator·

  ·