All pull requests

Pull requests

• A join's heap merge states location axioms on every path: carry the region a heap exists on

  #71·The-Ray-Man opened Nov 13, 2026Collaborator·

  ·

• A summarized consume leaves drained members holding a residue that looks held, and every later join and consume multiplies over them

  #60·JonasAlaif opened Nov 10, 2026Contributor·

  ·

• Magic wands are rejected: model a wand as a resource identified by its structure and hole values

  #57·JonasAlaif opened Nov 9, 2026Contributor·

  ·

• A quantifier in an assertion cannot read the heap: old(..), field reads and heap-dependent calls inside a forall are rejected

  #56·JonasAlaif opened Nov 8, 2026Contributor·

  ·

• Fix six more soundness bugs in path conditions, joins, labels and loop cuts, and a latent zero-demand incompleteness (supersedes #52, #53, #23, #24)

  #54·JonasAlaif opened Nov 8, 2026Contributor·

  ·

• Axiomatizing a unit costs O(axioms × graph): evaluate and saturate the domain axioms once per program

  #51·JonasAlaif opened Nov 6, 2026Contributor·

  ·

• Fix three soundness bugs in the permission heap (supersedes #30, #39)

  #49·The-Ray-Man opened Nov 4, 2026Collaborator·

  ·
  1

• Skip the zero-demand proof for a wildcard demand known positive

  #47·The-Ray-Man opened Nov 3, 2026Collaborator·

  ·

• E-matching costs what changed since a rule last ran, not the size of the e-graph

  #45·JonasAlaif opened Nov 3, 2026Contributor·

  ·

• Case towers whose default arm is unreachable cannot be inverted without a case split

  #44·JonasAlaif opened Nov 2, 2026Contributor·

  ·

• The block scratch does not see what ground derives after it was built

  #43·JonasAlaif opened Nov 2, 2026Contributor·

  ·

• Saturation is bounded by the size of the graph, not by what a run derives

  #40·JonasAlaif opened Nov 2, 2026Contributor·

  ·

• Decide a location's alias set against the operation's context instead of enumerating alias configurations

  #38·JonasAlaif opened Nov 2, 2026Contributor·

  ·

• The e-class analysis knows only constants: add an integer range domain

  #28·JonasAlaif opened Oct 29, 2026Contributor·

  ·

• A scaled permission cannot be shown positive: decide positivity by the term's sign

  #19·JonasAlaif opened Oct 7, 2026Contributor·

  ·
  1

• E-graph maintenance cost is proportional to what changed, not to graph size

  #17·JonasAlaif opened Oct 7, 2026Contributor·

  ·
  1

• One opt-in, structured trace of the verifier's work, replacing ad-hoc env-var diagnostics

  #14·JonasAlaif opened Oct 6, 2026Contributor·

  ·

• Remove behavioural A/B env toggles (and the latent unsoundness one of them carried)

  #13·JonasAlaif opened Oct 6, 2026Contributor·

  ·