Skip to content

Pre post #2

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

Open
parisaF163 wants to merge 5 commits into
base: main
Choose a base branch
from
Open

Pre post #2

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
df99173
support for pre and post conditions
pFathololumi Dec 15, 2023
9248018
merge main into pre-post
pFathololumi Jan 21, 2024
f0e3864
merge GCommute with Commute statement
pFathololumi Apr 30, 2024
84a2d60
new examples
Jan 27, 2025
e1f64d6
issue with hoare triple proof
parisaF163 Feb 24, 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
4 changes: 3 additions & 1 deletion .vscode/settings.json
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,8 @@
{
"files.associations": {
"*.smtlib2": "smt-lib",
"*.vcy": "c",
"random": "c"
"random": "c",
"fetchandadd": "c"
}
}
2 changes: 1 addition & 1 deletion README.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -26,7 +26,7 @@ opam switch create 4.12.0mc 4.12.0+domains+effects --repositories=multicore=git+
opam switch 4.12.0mc
eval $(opam env)

opam install sexplib ppxlib.0.22.0+effect-syntax ppx_deriving_yaml
opam install sexplib ppxlib.0.22.0+effect-syntax ppx_deriving_yaml ounit2 menhir
eval $(opam env)
```

Expand Down
97 changes: 97 additions & 0 deletions benchmarks/inferred/auction1.vcy
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,97 @@

int main(int argc, string[] argv) {

int[] bids = new int[100];

int msg_sender = int_of_string(argv[1]);
int highestBindingBid = int_of_string(argv[2]);
int highestBidder = int_of_string(argv[3]);
int msg_value = int_of_string(argv[4]);
int minimumBidValue = int_of_string(argv[5]);
int bidIncrement = int_of_string(argv[6]);

int bidIncrementWei_arg = int_of_string(argv[7]);
int minimumBidValue_arg = int_of_string(argv[8]);
int startBlock = int_of_string(argv[9]);
int endBlock = int_of_string(argv[10]);
string ipfsHash = int_of_string(argv[11]);
int block_number = int_of_string(argv[12]);
int blocksGenerated = int_of_string(argv[13]);

int auctionState = 0;
int state_started = 1;
int state_running = 2;
int state_ended = 3;
int state_canceled = 4;

int currentBid = 0;
int a = 0;
int b = 0;
int c = 0;

commute _ {
{
/* placeBid */
assume(auctionState == state_running);
assume(msg_value >= minimumBidValue);
currentBid = bids[msg_sender] + msg_value;
assume(currentBid >= highestBindingBid);
bids[msg_sender] = currentBid;
b = bids[highestBidder];
if(currentBid <= b){
a = currentBid + bidIncrement;
if(a <= b){
highestBindingBid = a;
}
else{
highestBindingBid = b;
}
return 0;
}

if(currentBid > b){
c = bids[highestBidder];
c = c + bidIncrement;
if(currentBid <= c){
highestBindingBid = currentBid;
}
else{
highestBindingBid = c;
}
highestBidder = msg_sender;
}
}
{
/* placeBid */
assume(auctionState == state_running);
assume(msg_value >= minimumBidValue);
currentBid = bids[msg_sender] + msg_value;
assume(currentBid >= highestBindingBid);
bids[msg_sender] = currentBid;
b = bids[highestBidder];
if(currentBid <= b){
a = currentBid + bidIncrement;
if(a <= b){
highestBindingBid = a;
}
else{
highestBindingBid = b;
}
return 0;
}

if(currentBid > b){
c = bids[highestBidder];
c = c + bidIncrement;
if(currentBid <= c){
highestBindingBid = currentBid;
}
else{
highestBindingBid = c;
}
highestBidder = msg_sender;
}
}
}
return 0;
}
79 changes: 79 additions & 0 deletions benchmarks/inferred/auction2.vcy
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,79 @@
int min(int a, int b){
if(a<=b){
return a;
}else {
return b;
}
}

int main(int argc, string[] argv) {

int[] bids = new int[100];

int msg_sender = int_of_string(argv[1]);
int highestBindingBid = int_of_string(argv[2]);
int highestBidder = int_of_string(argv[3]);
int msg_value = int_of_string(argv[4]);
int minimumBidValue = int_of_string(argv[5]);
int bidIncrement = int_of_string(argv[6]);

int bidIncrementWei_arg = int_of_string(argv[7]);
int minimumBidValue_arg = int_of_string(argv[8]);
int startBlock = int_of_string(argv[9]);
int endBlock = int_of_string(argv[10]);
string ipfsHash = int_of_string(argv[11]);
int block_number = int_of_string(argv[12]);
int blocksGenerated = int_of_string(argv[13]);

int auctionState = 0;
int state_started = 1;
int state_running = 2;
int state_ended = 3;
int state_canceled = 4;

int currentBid = 0;
int a = 0;
int b = 0;
int c = 0;


commute _ {
{
/* cancelAuction */
auctionState = state_canceled;

}
{
/* placeBid */
assume(auctionState == state_running);
assume(msg_value >= minimumBidValue);
currentBid = bids[msg_sender] + msg_value;
assume(currentBid >= highestBindingBid);
bids[msg_sender] = currentBid;
b = bids[highestBidder];
if(currentBid <= b){
a = currentBid + bidIncrement;
if(a <= b){
highestBindingBid = a;
}
else{
highestBindingBid = b;
}
return 0;
}

if(currentBid > b) {
c = bids[highestBidder];
c = c + bidIncrement;
if(currentBid <= c){
highestBindingBid = currentBid;
}
else{
highestBindingBid = c;
}
highestBidder = msg_sender;
}
}
}
return 0;
}
63 changes: 63 additions & 0 deletions benchmarks/inferred/auction3.vcy
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,63 @@

int main(int argc, string[] argv) {

int[] bids = new int[100];

int msg_sender = int_of_string(argv[1]);
int highestBindingBid = int_of_string(argv[2]);
int highestBidder = int_of_string(argv[3]);
int msg_value = int_of_string(argv[4]);
int minimumBidValue = int_of_string(argv[5]);
int bidIncrement = int_of_string(argv[6]);

int bidIncrementWei_arg = int_of_string(argv[7]);
int minimumBidValue_arg = int_of_string(argv[8]);
int startBlock = int_of_string(argv[9]);
int endBlock = int_of_string(argv[10]);
string ipfsHash = int_of_string(argv[11]);
int block_number = int_of_string(argv[12]);
int blocksGenerated = int_of_string(argv[13]);

int auctionState = 0;
int state_started = 1;
int state_running = 2;
int state_ended = 3;
int state_canceled = 4;

int currentBid = 0;
int a = 0;
int b = 0;


commute _ {
{
/* startNewBid */
assume (auctionState == state_started);
startBlock = block_number;
endBlock = startBlock + blocksGenerated;
auctionState = state_running;
ipfsHash = "";
bidIncrement = bidIncrementWei_arg;
minimumBidValue = minimumBidValue_arg;
}
{
/* placeBid */
assume(auctionState == state_running);
assume(msg_value >= minimumBidValue);
currentBid = bids[msg_sender] + msg_value;
assume(currentBid >= highestBindingBid);
bids[msg_sender] = currentBid;
b = bids[highestBidder];
if(currentBid <= b){
a = currentBid + bidIncrement;
if(a <= b){
highestBindingBid = a;
}
else{
highestBindingBid = b;
}
}
}
}
return 0;
}
78 changes: 78 additions & 0 deletions benchmarks/inferred/auction4.vcy
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,78 @@

int main(int argc, string[] argv) {

int[] bids = new int[100];

int msg_sender = int_of_string(argv[1]);
int highestBindingBid = int_of_string(argv[2]);
int highestBidder = int_of_string(argv[3]);
int msg_value = int_of_string(argv[4]);
int minimumBidValue = int_of_string(argv[5]);
int bidIncrement = int_of_string(argv[6]);

int bidIncrementWei_arg = int_of_string(argv[7]);
int minimumBidValue_arg = int_of_string(argv[8]);
int startBlock = int_of_string(argv[9]);
int endBlock = int_of_string(argv[10]);
string ipfsHash = int_of_string(argv[11]);
int block_number = int_of_string(argv[12]);
int blocksGenerated = int_of_string(argv[13]);

int auctionState = 0;
int state_started = 1;
int state_running = 2;
int state_ended = 3;
int state_canceled = 4;

int currentBid = 0;
int a = 0;
int b = 0;
int c = 0;


commute _ {
{
/* startNewBid */
assume (auctionState == state_started);
startBlock = block_number;
endBlock = startBlock + blocksGenerated;
auctionState = state_running;
ipfsHash = "";
bidIncrement = bidIncrementWei_arg;
minimumBidValue = minimumBidValue_arg;
}
{
/* placeBid */
assume(auctionState == state_running);
assume(msg_value >= minimumBidValue);
currentBid = bids[msg_sender] + msg_value;
assume(currentBid >= highestBindingBid);
bids[msg_sender] = currentBid;
b = bids[highestBidder];
if(currentBid <= b){
a = currentBid + bidIncrement;
if(a <= b){
highestBindingBid = a;
}
else{
highestBindingBid = b;
}
return 0;
}

if(currentBid > b){
c = bids[highestBidder];
c = c + bidIncrement;
if(currentBid <= c){
highestBindingBid = currentBid;
}
else{
highestBindingBid = c;
}
highestBidder = msg_sender;
}

}
}
return 0;
}
37 changes: 37 additions & 0 deletions benchmarks/inferred/pullPayment.vcy
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,37 @@

int main(int argc, string[] argv) {

int[] payments = new int[10];

int msg_sender = int_of_string(argv[1]);
int dest = int_of_string(argv[2]);
int amount = int_of_string(argv[3]);
int balance = int_of_string(argv[4]);
int flag = 1;
int payee = 0;
int payment = 0;

commute _ {
{
/* asyncSend */
payments[dest] = payments[dest] + amount;
}
{
/* withdrawPayments */
payee = msg_sender;
payment = payments[payee];

if (payment == 0){
flag = 0;
return 0;
}
if (balance < payment){
flag = 0;
return 0;
}
payments[payee] = 0;
/* if(!payee.send(payment)) throw */
}
}
return 0;
}
Loading