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

Jump to bottom

[move] essential formal verification tests on transfers #94

Merged
merged 33 commits into from
Nov 11, 2023
Merged

[move] essential formal verification tests on transfers #94

merged 33 commits into from
Nov 11, 2023

Conversation

0o-de-lally
Copy link
Contributor

@0o-de-lally 0o-de-lally commented Nov 9, 2023 •
edited
Loading

Essential Move Prover test for to prove essential policies can't be circumvented.

  • remove .freeze field from coin object in vendor code (!)
  • create FV test for ol_account::withdraw
  • create FV test for main slow_wallet.move functions
  • create FV test for all sacred_cows.move functions (especially epoch boundary)
  • add CI workflow formal.yaml

@0o-de-lally
fixup cargo.lock
7d6996f
@0o-de-lally
patch formal
7a47505
@0o-de-lally
publish
b99d794
@0o-de-lally
clean
065fa99
@0o-de-lally
test publish
73c5340
@0o-de-lally
slow wallet epoch boundary prover test passing
5819f3a
@0o-de-lally
replace dev setup with Diem
37b563a
@0o-de-lally
update dev_setup
ed5ebee
@0o-de-lally
docs
d106074
@0o-de-lally
update dev setup to include libgmp
34ff006
@0o-de-lally
update formal yaml
2a141ab
@0o-de-lally
patch
cf76d34
@0o-de-lally
Squashed commit of the following:
47b557e 
commit e0d57cf
Author: 0o-de-lally <[email protected]>
Date:   Thu Nov 9 20:41:36 2023 +0000

    simplify

commit 2b4f3df
Author: 0o-de-lally <[email protected]>
Date:   Thu Nov 9 20:38:58 2023 +0000

    try hardcoding env

commit 99b44db
Author: 0o-de-lally <[email protected]>
Date:   Thu Nov 9 20:29:35 2023 +0000

    try updating profile

commit c8b659c
Author: 0o-de-lally <[email protected]>
Date:   Thu Nov 9 20:23:25 2023 +0000

    patch yaml

commit 819708d
Author: 0o-de-lally <[email protected]>
Date:   Thu Nov 9 20:21:52 2023 +0000

    try diem exec
@0o-de-lally
cleanup ci yaml
9a89bf2
@0o-de-lally
patch
eca187e
@0o-de-lally
patch slow wallet test
0e9aa27
@0o-de-lally
sacred cows init proved
ea27330
@0o-de-lally
sacred cows full abort coverage with aborts_if_is_strict
9cfdf5e
@0o-de-lally
accounts should not have a frozen bit
7f1ef80
@0o-de-lally
critical tests for ol_account, slow, sacred, written and passing
8791f4f
@0o-de-lally 0o-de-lally changed the title [move] basic formal verification tests [move] essential formal verification tests on transfers Nov 10, 2023
@0o-de-lally
patch cargo.toml version
bc54f7f
@0o-de-lally
framework build
1524664
@0o-de-lally
update gas coin rust struct after .frozen was removed
cba694e
@0o-de-lally
fmt
b00051a
@0o-de-lally
Squashed commit of the following:
ccc9bda 
commit 52b3024
Author: 0o-de-lally <[email protected]>
Date:   Fri Nov 10 16:53:24 2023 -0500

    [move] various account state patches from testnet (0LNetworkCommunity#96)

commit 2c0838b
Author: 0o-de-lally <[email protected]>
Date:   Fri Nov 10 18:05:00 2023 +0000

    patch fullnode downloads url

commit 2ef4734
Author: zoz <[email protected]>
Date:   Sat Nov 11 03:37:06 2023 +1100

    [tools] update fullnode-init command (0LNetworkCommunity#95)

commit 1319077
Author: 0o-de-lally <[email protected]>
Date:   Fri Nov 10 11:07:53 2023 -0500

    [ci] publish ubuntu bins for CI use (0LNetworkCommunity#91)

commit b6477bb
Author: 0o-de-lally <[email protected]>
Date:   Fri Nov 10 11:07:36 2023 -0500

    [tools] better env setup tools util/dev_setup.sh (0LNetworkCommunity#93)
@0o-de-lally
trigger ci build
36d9172
@0o-de-lally 0o-de-lally marked this pull request as ready for review November 11, 2023 00:05
@0o-de-lally 0o-de-lally merged commit 8389cd6 into 0LNetworkCommunity:main Nov 11, 2023
11 checks passed
0o-de-lally added a commit that referenced this pull request Aug 8, 2024
@0o-de-lally @hemulin
[move] essential formal verification tests on transfers (#94)
b438f32 
Co-authored-by: Yotam Katznelson <[email protected]>
0o-de-lally added a commit that referenced this pull request Aug 8, 2024
@0o-de-lally @hemulin
[move] essential formal verification tests on transfers (#94)
b600b08 
Co-authored-by: Yotam Katznelson <[email protected]>
0o-de-lally added a commit to 0o-de-lally/libra-framework that referenced this pull request Aug 17, 2024
@0o-de-lally @hemulin
[move] essential formal verification tests on transfers (0LNetworkCom…
21a2df7 
…munity#94)

Co-authored-by: Yotam Katznelson <[email protected]>
0o-de-lally added a commit to 0o-de-lally/libra-framework that referenced this pull request Aug 17, 2024
@0o-de-lally @hemulin
[move] essential formal verification tests on transfers (0LNetworkCom…
44c82ca 
…munity#94)

Co-authored-by: Yotam Katznelson <[email protected]>
0o-de-lally added a commit to 0o-de-lally/libra-framework that referenced this pull request Aug 17, 2024
@0o-de-lally @hemulin
[move] essential formal verification tests on transfers (0LNetworkCom…
2c65076 
…munity#94)

Co-authored-by: Yotam Katznelson <[email protected]>
0o-de-lally added a commit to 0o-de-lally/libra-framework that referenced this pull request Aug 17, 2024
@0o-de-lally @hemulin
[move] essential formal verification tests on transfers (0LNetworkCom…
ef16b6a 
…munity#94)

Co-authored-by: Yotam Katznelson <[email protected]>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@0xzoz 0xzoz 0xzoz approved these changes

Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
3 participants
@0o-de-lally @0xzoz @hemulin