All pull requests

Pull requests

• Prove allocation size preparation and tail containment

  #3790·joshlf opened Oct 6, 2026Member·

  ·
  2

• Prove the concrete CastUnsized layout gate

  #3789·joshlf opened Oct 6, 2026Member·

  ·
  2

• Prove split lengths and non-overlapping numerical regions

  #3788·joshlf opened Oct 6, 2026Member·

  ·
  2

• Prove concrete pointer metadata operations

  #3787·joshlf opened Oct 6, 2026Member·

  ·
  2

• [anneal][v1] Preserve the Darwin native translation tool closure

  #3786·joshlf opened Oct 5, 2026Member·

  ·
  57

• [anneal][v1] Refresh stock Lean workers when local imports change

  #3784·joshlf opened Oct 5, 2026Member·

  ·
  140

• [anneal][v1] Bind stock editor and SDK source clients to the workspace

  #3785·joshlf opened Oct 5, 2026Member·

  ·
  81

• [anneal][v1] Generate and verify private SDK-bound workspaces

  #3783·joshlf opened Oct 5, 2026Member·

  ·
  54

• [anneal][v1] Bind private workspaces to one immutable Lean SDK

  #3782·joshlf opened Oct 5, 2026Member·

  ·
  122

• [anneal][v1] Publish a validated immutable Lean SDK view

  #3781·joshlf opened Oct 5, 2026Member·

  ·
  13

• [anneal][v1] Reject failed Lean processes and simplify output capture

  #3780·joshlf opened Oct 5, 2026Member·

  ·
  8

• Prove cast metadata composition against reference sizes

  #3777·joshlf opened Oct 5, 2026Member·

  ·
  2

• Prove numerical cast plan selection and metadata conversion

  #3776·joshlf opened Oct 5, 2026Member·

  ·
  2

• [byte_slice] Require deref stability across moves

  #3775·miguelcorderopamphile opened Oct 5, 2026·

  ·
  3

• Separate numerical cast planning from typed pointer projection

  #3774·joshlf opened Oct 5, 2026Member·

  ·
  2

• Move pointer cast implementation into its own source file

  #3773·joshlf opened Oct 5, 2026Member·

  ·
  4

• Prove cast validation and exact metadata inference

  #3755·joshlf opened Oct 2, 2026Member·

  ·
  2

• Prove byte advancement and padding sequence queries

  #3754·joshlf opened Oct 2, 2026Member·

  ·
  2

• Prove normalized layout padding and field extension

  #3753·joshlf opened Oct 2, 2026Member·

  ·
  2

• Prove exact trailing sizes, padding and capacity

  #3752·joshlf opened Oct 2, 2026Member·

  ·
  2

• Prove primitive layout constructors with recursive mathematical models

  #3751·joshlf opened Oct 2, 2026Member·

  ·
  2

• Compare nested DST sizes with a recursive Rust oracle

  #3749·joshlf opened Oct 2, 2026Member·

  ·
  2

• Model alignment and phase encoding as a bounded mathematical pair

  #3747·joshlf opened Oct 2, 2026Member·

  ·
  2

• Strengthen arithmetic specifications and prove arithmetic corollaries

  #3746·joshlf opened Oct 2, 2026Member·

  ·
  4

• Reuse Aeneas specifications for views and indexed loops

  #3745·joshlf opened Oct 2, 2026Member·

  ·
  2