All pull requests

Pull requests

• Smt translation: Bug fix for issues 194 and 195

  #268·etiennejf opened Sep 23, 2026Collaborator·

  ·
  

• Bug Fix for Issues 143, 152 and 262

  #267·etiennejf opened Sep 19, 2026Collaborator·

  ·
  1

  5

  

• Kernel-check the reconstruction gate and rewrite hypotheses on replay

  #261·felipeperet opened Sep 16, 2026Collaborator·

  ·

• 181 eq hardening additivemultiplicative cancellation reductions

  #258·MarcoNardell1 opened Sep 15, 2026Collaborator·

  ·
  4

• Restrict instantiateSharedRevRange to zero begin index

  #255·etiennejf opened Sep 15, 2026Collaborator·

  ·
  

• Emit proof steps for constructor Eq reductions

  #252·felipeperet opened Sep 11, 2026Collaborator·

  ·

• Avoid exponential hash-consing of shared input expressions

  #250·RSoulatIOHK opened Sep 10, 2026Collaborator·

  ·

• Reduce optimizer stack allocation

  #248·RSoulatIOHK opened Sep 9, 2026Collaborator·

  ·

• Lift two SellNFT recursive searches with certified Lean workers

  #247·RSoulatIOHK opened Sep 9, 2026Collaborator·

  ·

• Preserve dependent matcher motives and reduce known indexed branches

  #246·RSoulatIOHK opened Sep 9, 2026Collaborator·

  ·

• Specialize static CEK control before dynamic payloads

  #244·RSoulatIOHK opened Sep 9, 2026Collaborator·

  ·

• Fix cyclic beta-cache assignments on re-entry

  #243·RSoulatIOHK opened Sep 9, 2026Collaborator·

  ·

• Profile Cardano preparation and gate accepting global executions

  #241·RSoulatIOHK opened Sep 9, 2026Collaborator·

  ·

• Experiment with scoped constructor-choice retention (Issue238)

  #240·RSoulatIOHK opened Sep 9, 2026Collaborator·

  ·

• Measure Cardano preparation separately from proof checking

  #239·RSoulatIOHK opened Sep 9, 2026Collaborator·

  ·

• Complete empty-domain function typing; investigate solver regressions

  #237·RSoulatIOHK opened Sep 9, 2026Collaborator·

  ·

• Prevent opaque functions from fabricating empty-type inhabitants

  #236·RSoulatIOHK opened Sep 9, 2026Collaborator·

  ·

• Simplify list append and drop through symbolic tails

  #235·RSoulatIOHK opened Sep 9, 2026Collaborator·

  ·

• Preserve SMT sharing with scope-safe let emission

  #234·RSoulatIOHK opened Sep 9, 2026Collaborator·

  ·

• Reduce shared-factor Nat.mod goals before SMT solving

  #230·RSoulatIOHK opened Sep 9, 2026Collaborator·

  ·

• Fix false Valid results from empty types and type classes

  #224·RSoulatIOHK opened Sep 9, 2026Collaborator·

  ·

• Fix false Valid results from constructor proof fields

  #223·RSoulatIOHK opened Sep 9, 2026Collaborator·

  ·

• Emit proof steps for the Bool-not/decide bridge and nominal decide re…

  #222·felipeperet opened Sep 8, 2026Collaborator·

  ·

• Bool binary, Prop connectives, and relational LE

  #221·felipeperet opened Sep 4, 2026Collaborator·

  ·

• 180 eq hardening int negation and zero equals reductions

  #220·MarcoNardell1 opened Sep 4, 2026Collaborator·

  ·
  14