All pull requests

Pull requests

• 352 elaborate the testoptimize input once so the proof gate maps anonymous instance binders

  #408·MarcoNardell1 opened Oct 21, 2026Collaborator·6 of 21 tasks·

  ·

• Soundness: only canonical LT/LE instances and instance arguments of function values

  #368·SeungheonOh opened Oct 21, 2026·

  ·
  1

• CVC5 FF Integration [WIP Draft]

  #367·Riley-Kilgore opened Oct 20, 2026Member·

  ·

• Experiment with deferred constructor match propagation

  #366·RSoulatIOHK opened Oct 20, 2026Collaborator·

  ·

• Publish PR benchmark results from isolated workflow

  #365·RSoulatIOHK opened Oct 20, 2026Collaborator·

  ·

• Balance the four PR benchmark runners

  #364·RSoulatIOHK opened Oct 20, 2026Collaborator·

  ·

• chore(benchmark): weekly results update

  #360·github-actions[bot] opened Oct 19, 2026Bot·

  ·

• [285 split 16/16] Export assembled induction and replay proofs as standalone Lean files

  #347·RSoulatIOHK opened Oct 16, 2026Collaborator·

  ·

• [285 split 15/16] Infer machine invariants through Horn clauses and replay every obligation

  #346·RSoulatIOHK opened Oct 16, 2026Collaborator·

  ·
  1

• [285 split 14/16] Reconstruct machine proofs from recorded exploration and supplied invariants

  #345·RSoulatIOHK opened Oct 16, 2026Collaborator·

  ·

• [285 split 13/16] Record symbolic machine exploration with joins and procedure shapes

  #344·RSoulatIOHK opened Oct 16, 2026Collaborator·

  ·

• [285 split 12/16] Prove recursive programs by functional induction with opaque SMT leaves

  #343·RSoulatIOHK opened Oct 16, 2026Collaborator·

  ·

• [285 split 11/16] Instantiate proved summaries and register imported library facts

  #342·RSoulatIOHK opened Oct 16, 2026Collaborator·

  ·

• [285 split 10/16] Track rewrite dependencies and memoize shared expression queries

  #341·RSoulatIOHK opened Oct 16, 2026Collaborator·

  ·

• [285 split 09/16] Retain choices inside constructor fields and reduce their consumers

  #340·RSoulatIOHK opened Oct 16, 2026Collaborator·

  ·

• [285 split 08/16] Keep recursive functions opaque while retaining selected constructor equations

  #339·RSoulatIOHK opened Oct 16, 2026Collaborator·

  ·

• [285 split 07/16] Search Horn-clause invariants by Houdini candidate elimination

  #338·RSoulatIOHK opened Oct 16, 2026Collaborator·

  ·

• [285 split 06/16] Read and print explicit kernel terms with sharing

  #337·RSoulatIOHK opened Oct 16, 2026Collaborator·

  ·

• [285 split 05/16] Normalize saturated natural subtraction and surjective Int.toNat binders

  #336·RSoulatIOHK opened Oct 16, 2026Collaborator·

  ·

• [285 split 04/16] Translate only live match fields and declare higher-order pattern types

  #335·RSoulatIOHK opened Oct 16, 2026Collaborator·

  ·

• [285 split 03/16] Model closed Fin bounds with exact SMT range

  #334·RSoulatIOHK opened Oct 16, 2026Collaborator·

  ·
  2

• [285 split 02/16] Keep closed-expression rewrites inside their assumption scope

  #333·RSoulatIOHK opened Oct 16, 2026Collaborator·

  ·
  1

• [285 split 01/16] Preserve build failures and compile every Lean source

  #332·RSoulatIOHK opened Oct 16, 2026Collaborator·

  ·

• Emit proof steps for the ite and dite bridge to dite'

  #328·felipeperet opened Oct 14, 2026Collaborator·12 of 21 tasks·

  ·

• 326 close the m1 reconstruction gaps

  #327·felipeperet opened Oct 14, 2026Collaborator·12 of 21 tasks·

  ·