All pull requests

Pull requests

• docs(circuit): document loop combinator contracts

  #512·weiscadence opened Nov 11, 2026·

  ·

• test(resources): cover complete frontiers and refresh elimination

  #508·dtumad opened Nov 7, 2026Contributor·

  ·

• Read-write memory for VMs, on Devon's resource histories

  #504·mitschabaude-bot opened Nov 3, 2026Collaborator·

  ·
  3

• Bound the steps of VM soundness by the interaction count

  #498·mitschabaude-bot opened Nov 1, 2026Collaborator·

  ·

• Closed channels: read-only memory and counter channels

  #494·mitschabaude-bot opened Oct 27, 2026Collaborator·

  ·
  1

• keccak-air showcase: end-to-end soundness at 100 proven bits, byte-identical proofs with Plonky3

  #492·mitschabaude-bot opened Oct 22, 2026Collaborator·

  ·

• Segment programs and fast witness generation: keccak-air's trace at Plonky3's speed

  #491·mitschabaude-bot opened Oct 22, 2026Collaborator·

  ·

• feat(backends): CompStark backend with transfer and knowledge soundness theorems

  #490·mitschabaude-bot opened Oct 22, 2026Collaborator·

  ·

• Plonky3's keccak-air as a two-row component, proved sound

  #489·mitschabaude-bot opened Oct 22, 2026Collaborator·

  ·

• Two-row components: next-row access and Plonky3 selectors

  #488·mitschabaude-bot opened Oct 22, 2026Collaborator·

  ·

• Clean 2: verifier challenges — design proposal (challenge op, rare events, phase contract, extension fields)

  #484·mitschabaude opened Oct 14, 2026Collaborator·

  ·

• Lazy prover-data cells defined by their first read

  #481·mitschabaude-bot opened Oct 13, 2026Collaborator·

  ·

• Generator correctness and completeness

  #480·mitschabaude-bot opened Oct 12, 2026Collaborator·

  ·

• Clean 2: a new experimental core

  #476·gio54321 opened Oct 5, 2026Collaborator·

  ·

• feat: add ordered resource histories for mutable AIR state

  #475·dtumad opened Oct 4, 2026Contributor·

  ·

• feat(R1CS): R1CS semantics and soundness of the export

  #473·hecmas opened Sep 28, 2026·

  ·
  3

• feat(operations): certified constraint simplification on Operations

  #472·hecmas opened Sep 28, 2026·

  ·
  5

• feat(r1cs): certified R1CS constraint simplification

  #471·hecmas opened Sep 28, 2026·

  ·
  7

• feat(circom): product absorption in R1CS lowering

  #470·VanshSahay opened Sep 25, 2026Contributor·

  ·
  1

• Consumed-cell provenance: copies and witness reads under one predicate

  #467·daira opened Sep 20, 2026·

  ·
  4

• computableWitnesses: compositional statement and law library

  #448·mitschabaude-bot opened Aug 10, 2026Collaborator·

  ·

• Witgen eval: high-level normal form (concrete reduces, hints stay atoms)

  #430·mitschabaude-bot opened Jul 24, 2026Collaborator·

  ·

• Halo2-Clean, supporting the Ironwood formalization

  #418·mitschabaude opened Jul 3, 2026Collaborator·

  ·

• BabyJubJub spec and point addition circuit

  #410·VanshSahay opened Jul 3, 2026Contributor·11 of 14 tasks·

  ·
  4

• Orchard in Clean

  #402·mitschabaude opened Jun 10, 2026Collaborator·

  ·
  4