Skip to content

Generate lemmas and prove them#50

Open
petros-marko wants to merge 2 commits intomasterfrom
petros-marko/proofs
Open

Generate lemmas and prove them#50
petros-marko wants to merge 2 commits intomasterfrom
petros-marko/proofs

Conversation

@petros-marko
Copy link
Collaborator

Pull Request Overview

  • Marks previously trusted lemmas as proven_externally
  • Proves the generated theorems
  • Fixes some overflow checking issues that came up from running flux with pointer-width=32

Testing Strategy

WIP; I don't think I'm merging this anytime soon, I just wanted to be able to point to the changes

@ranjitjhala @nilehmann @vrindisbacher

@petros-marko petros-marko self-assigned this Oct 6, 2025
@ranjitjhala
Copy link

This is super exciting -- well done @petros-marko !!!

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants