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

Generalized lemma broadcast, implements #37 #1022

Merged
merged 37 commits into from
Mar 27, 2024
Merged

Generalized lemma broadcast, implements #37 #1022

Show file tree
Hide file tree
Changes from 30 commits
Commits
Show all changes
37 commits
Select commit Hold shift + click to select a range
aecbadd
Add groups of broadcast_forall (and other revealable things)
Chris-Hawblitzel Feb 15, 2024
00ed369
Minor reveal_group fixes
Chris-Hawblitzel Feb 15, 2024
6e5b1ec
Merge branch 'main' into reveal_group
Chris-Hawblitzel Feb 16, 2024
164d95d
Merge branch 'main' into reveal_group
Chris-Hawblitzel Feb 16, 2024
5dc7bf3
Add attributes to reveal_group to express defaults and pruning
Chris-Hawblitzel Feb 16, 2024
eb0e6c2
Emit fuel id for all broadcast_forall functions
Chris-Hawblitzel Feb 16, 2024
5bb9e79
Add reveal_groups to call graph
Chris-Hawblitzel Feb 16, 2024
86122fd
Handle reveal_group in get_callee
Chris-Hawblitzel Feb 16, 2024
c7f4cf9
Fix broadcast_forall check of external_body
Chris-Hawblitzel Feb 17, 2024
c4fc203
Merge reveal_group member axioms into single axiom
Chris-Hawblitzel Feb 17, 2024
797c031
Merge branch 'main' into reveal_group
Chris-Hawblitzel Feb 17, 2024
05d5964
Merge branch 'main' into reveal_group
utaal-b Feb 18, 2024
b7174b1
add support for reveal_group in impl, add tests
utaal-b Feb 19, 2024
8513bba
parse item-level reveals (which will apply to the entire module)
utaal-b Feb 19, 2024
b45e56f
add module-level reveals to function call graph
utaal-b Feb 25, 2024
ac26752
emit module-level reveal axioms
utaal-b Feb 26, 2024
f01ac92
Merge branch 'main' into reveal_group
utaal-b Feb 26, 2024
b46a0f4
add test for reveal group in generic impl
utaal-b Feb 27, 2024
68fb0d1
Merge branch 'main' into generalized-broadcast
utaal-b Mar 3, 2024
e5e9596
add support for broadcast group syntax
utaal-b Mar 3, 2024
1ac4f0c
deprecate explicit verifier attribute for broadcast_forall
utaal-b Mar 3, 2024
e24d57e
add support for `broadcast proof fn` syntax
utaal-b Mar 3, 2024
879e2cb
replace the broadcast_forall attribute with the new `broadcast proof …
utaal-b Mar 3, 2024
cb1fb0b
change module-level `reveal` to `broadcast use`
utaal-b Mar 3, 2024
33e7b0e
allow `broadcast use` as statement-level item
utaal-b Mar 3, 2024
d1f5b24
distinguish between `broadcast` and `reveal`
utaal-b Mar 3, 2024
492d1f8
fully distinguish between `broadcast` and `reveal`, clean up error me…
utaal-b Mar 3, 2024
c101328
do not completely erase a broadcast group fn if it is public
utaal-b Mar 3, 2024
f442fa1
rename broadcast_use_by_default_when_this_crate_is_imported for consi…
utaal-b Mar 4, 2024
852db35
broadcast use in a method body is automatically proof mode
utaal-b Mar 4, 2024
7eb36ff
rename #[verifier::hidden_unless_this_module_is_used] to #[verifier::…
utaal-b Mar 12, 2024
6fc8a9d
be more specific in unsupported error
utaal-b Mar 12, 2024
2d0de16
Merge branch 'main' into generalized-broadcast
utaal-b Mar 13, 2024
e45435d
Merge branch 'main' into generalized-broadcast
utaal-b Mar 27, 2024
443e8f1
apply candidate verusfmt
utaal-b Mar 27, 2024
8c6b5da
Merge branch 'main' into generalized-broadcast
utaal-b Mar 27, 2024
6fc22fa
bump minimum verusfmt version
utaal-b Mar 27, 2024
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
28 changes: 28 additions & 0 deletions dependencies/syn/src/gen/clone.rs
View file
Open in desktop

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

40 changes: 40 additions & 0 deletions dependencies/syn/src/gen/debug.rs
View file
Open in desktop

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

38 changes: 31 additions & 7 deletions dependencies/syn/src/gen/eq.rs
View file
Open in desktop

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

53 changes: 53 additions & 0 deletions dependencies/syn/src/gen/fold.rs
View file
Open in desktop

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

35 changes: 35 additions & 0 deletions dependencies/syn/src/gen/hash.rs
View file
Open in desktop

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

Loading