Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Lean verification code generator #7180

Draft
wants to merge 50 commits into
base: main
Choose a base branch
from
+7,504 −5
Draft

Lean verification code generator #7180

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
50 commits
Select commit Hold shift + click to select a range
0c5c5c6
Generates signature of Lean specs.
yoavseginer Jun 20, 2023
3734870
Verification: auto spec generation.
yoavseginer Jun 28, 2023
fb112f4
Lean generation: added rebinding for variables.
yoavseginer Jul 3, 2023
95447d7
First steps of soundness proof generation.
yoavseginer Jul 5, 2023
68cf20a
Completed automatic generation of auto soundness theorem.
yoavseginer Jul 11, 2023
2dbee85
Numerous fixed to the Lean code generator.
yoavseginer Jul 18, 2023
fc6948e
Lean generator ignores tests which are not supported.
yoavseginer Jul 19, 2023
21497e4
WIP commit for supporting Lean 4 generated proofs
ccodel Aug 9, 2023
3d73f1c
WIP: first steps in handling guarantee destructors in libfunc tests.
yoavseginer Aug 15, 2023
2bc63ff
WIP: improvements to soundness generation for guarantee destruction.
yoavseginer Aug 16, 2023
bbfcc9a
Fix: extended the definition of an empty auxiliary information object.
yoavseginer Aug 16, 2023
b4f2b0c
Streamline lean 4 string generation, add command line switch
ccodel Aug 17, 2023
ab61f0c
Lean generator: unpack memory one by one and generate ap advance steps.
yoavseginer Sep 4, 2023
a48ecd2
Seperated lean code generation and output.
yoavseginer Sep 19, 2023
a08d001
Verification: new code unpacking and some sorrys replaced by generate…
yoavseginer Sep 20, 2023
66a04d1
Fixes after rebase.
yoavseginer Oct 10, 2023
b67b83e
Libfunc tests for soundness and removed Lean code from test files.
yoavseginer Oct 10, 2023
c4f08c6
Test without destructor for u256_guarantee_inv_mod_n and block arg ge…
yoavseginer Oct 16, 2023
5f7a393
WIP: split specs and proofs into blocks.
yoavseginer Oct 18, 2023
e42a05e
Verification: automatic generation of soundness blocks.
yoavseginer Oct 24, 2023
5d19b2e
Lean generation: improved argument and range check code generation.
yoavseginer Nov 1, 2023
ff8d5ab
Lean generation: better names for return variables.
yoavseginer Nov 1, 2023
7936e3c
false -> False for Lean 4
yoavseginer Nov 20, 2023
1466ddc
Lean generator: use new macro names, and some name and rw fixes.
yoavseginer Nov 21, 2023
fecc823
Lean generator: a few small bug fixes related to range checks.
yoavseginer Nov 21, 2023
a320129
Lean generator: imported changed from branch verification-dev-v2.4.0.
yoavseginer Apr 2, 2024
0137577
Lean generator fixes after rebase.
yoavseginer Apr 3, 2024
6b99f78
Verification WIP: completeness generation after Lean version update.
yoavseginer May 22, 2024
0edc2ad
Verification: completeness WIP.
yoavseginer May 29, 2024
172e851
Verification: correct generation of completeness for u256_guarantee_i…
yoavseginer Jun 4, 2024
2ce55a6
Verification: completeness spec is now modulo the prime.
yoavseginer Jun 4, 2024
2cc2227
Verification: removed Lean 3 generation code.
yoavseginer Jun 10, 2024
5117094
Small version changes.
yoavseginer Jun 18, 2024
1a2e6d2
Verification: fixed problem with rc deficit in soundness proofs.
yoavseginer Jun 18, 2024
18ca1f6
Lean generator: extended support for implicitly defined variables.
yoavseginer Jul 1, 2024
10f68a7
Verification: generation of Lean code for different versions of the s…
yoavseginer Jul 10, 2024
69f6027
Added namespaces to generated Lean files.
yoavseginer Sep 16, 2024
095e011
Lean generator: updates after Mathlib update and removed bogus argume…
yoavseginer Jan 6, 2025
5a5704c
Lean generator: fixes after rebase.
yoavseginer Jan 7, 2025
564ad6d
Made Lean code generation into a compilation feature ("lean").
yoavseginer Jan 7, 2025
8d3f9f0
Lean verification: fixed (most) test files which were modified.
yoavseginer Jan 8, 2025
15f8f9a
Separate variant of some libfunc tests for generating Lean code.
yoavseginer Jan 20, 2025
ea68ea9
Lean verification: separated auxiliary info code out of builder.
yoavseginer Jan 20, 2025
92a9ca8
Lean verification: extracted auxiliary info code from macros into fun…
yoavseginer Jan 21, 2025
030edfb
Fixed rust formatting.
yoavseginer Jan 21, 2025
a8ee198
Lean generator: removed dead code.
yoavseginer Jan 21, 2025
3d805e3
Lean verification: fixed typos.
yoavseginer Jan 21, 2025
31820af
Lean generator: first round of clippy fixes.
yoavseginer Jan 27, 2025
1339dbf
Lean verification: clippy and formatting fixes.
yoavseginer Jan 28, 2025
d52997d
Lean verification: small docs/dependency fixes to pass automatic tests.
yoavseginer Jan 28, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
14 changes: 14 additions & 0 deletions Cargo.lock
View file
Open in desktop

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

1 change: 1 addition & 0 deletions Cargo.toml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -34,6 +34,7 @@ members = [
"crates/cairo-lang-executable",
"crates/cairo-lang-filesystem",
"crates/cairo-lang-formatter",
"crates/cairo-lang-lean",
"crates/cairo-lang-lowering",
"crates/cairo-lang-parser",
"crates/cairo-lang-plugins",
Expand Down
1 change: 1 addition & 0 deletions crates/cairo-lang-casm/Cargo.toml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -30,3 +30,4 @@ std = ["cairo-lang-utils/std", "num-bigint/std", "num-traits/std", "serde?/std",
serde = ["dep:serde", "cairo-lang-utils/serde" ]
schemars = [ "std", "dep:schemars", "cairo-lang-utils/schemars"]
parity-scale-codec = ["dep:parity-scale-codec", "cairo-lang-utils/parity-scale-codec"]
lean = []
Loading
Loading