All pull requests

Pull requests

• armv8a: print Mach-O relocation operators on macOS

  #1594·athexweb3 opened Sep 30, 2026Contributor·

  ·
  1

• Add an ARMv8-M backend

  #1590·clebreto opened Sep 28, 2026Contributor·

  ·
  2

• Prove the wint_int pass correct

  #1586·bgregoir opened Sep 24, 2026Contributor·

  ·

• Use events for random sampling

  #1580·sarranz opened Sep 23, 2026Collaborator·

  ·
  2

• Emit the global data in .rodata

  #1578·strub opened Sep 23, 2026Member·

  ·
  11

• Port parts of EasyCrypt extraction to Rocq

  #1574·henridoh opened Sep 20, 2026·

  ·
  11

• Safety checker: the safety conditions as assertions, and its soundness proof

  #1572·bgregoir opened Sep 17, 2026Contributor·

  ·

• The mode in the semantics of expressions

  #1571·bgregoir opened Sep 17, 2026Contributor·

  ·

• The total mode of the memory and array accesses

  #1567·bgregoir opened Sep 15, 2026Contributor·

  ·

• One language for the safety conditions of the instructions

  #1566·bgregoir opened Sep 13, 2026Contributor·

  ·

• Define the semantics of the instructions from a total function and its safety and init conditions

  #1565·bgregoir opened Sep 13, 2026Contributor·

  ·

• Save the return address of export functions in the stack frame (arm64, risc-v)

  #1550·clebreto opened Sep 4, 2026Contributor·

  ·
  1

• Verify the transformations in EasyCrypt extraction

  #1531·sarranz opened Aug 1, 2026Collaborator·

  ·

• paco => rocq-coinduction

  #1514·rudynicolop opened Jul 10, 2026Contributor·

  ·

• docs: syntax reference

  #1468·sarranz opened May 29, 2026Collaborator·

  ·

• Rework ArrayCast / ArrayWord / SubArray th + extraction

  #1448·guilhemmizrahi-jpg opened May 5, 2026·

  ·

• Implement error resilience in pretyping by accumulating typing errors

  #1445·clebreto opened Apr 29, 2026Contributor·

  ·
  4

• Regalloc hints

  #1439·sarranz opened Apr 17, 2026Collaborator·

  ·
  1

• Emit vmovdqa instructions on x86

  #1424·vbgl opened Mar 27, 2026Member·

  ·
  10

• Arrays with non-constant lengths

  #1325·eponier opened Nov 19, 2025Contributor·

  ·
  2

• jasmin2ec: allow to extract declassified values

  #1282·loutr opened Sep 17, 2025Collaborator·

  ·

• Experiment: dunify proofs

  #1204·eponier opened Jun 16, 2025Contributor·

  ·
  2

• Safety assert2

  #1170·lyonel2017 opened May 27, 2025Collaborator·

  ·
  1

• Split large memory accesses in stack alloc

  arm
  #741·sarranz opened Feb 28, 2024Collaborator·

  ·
  7