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

Add some simple proofs #437

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

Add some simple proofs #437

Changes from 3 commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
8c4291a
Add simple example proofs
calin1304 Sep 28, 2021
0a3b1d0
Fix proof
calin1304 Oct 7, 2021
85d747c
Remove #inUnsignedRange for subtraction
calin1304 Oct 7, 2021
669f7dd
Fix format
calin1304 Oct 11, 2021
0da3e27
Merge branch 'master' into simple-claims
hjorthjort Mar 21, 2023
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
56 changes: 56 additions & 0 deletions tests/proofs/simple-spec.k
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,56 @@
requires "kwasm-lemmas.md"
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

For #signed(ITYPE, 0), it probably can't tell that 0 <Int #pow1(ITYPE), even though ITYPE can only be i32 or i64.

rule 0 <Int #pow1(_) => true [simplification]

and see if this works on Ana's branch.

Make sure to check the defniition of #pow1 and make sure this is true.


module SIMPLE-SPEC
imports KWASM-LEMMAS

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Write a functional spec:

claim <instrs> run(#signed(ITYPE, X -Int Y)) => done(X -Int Y) ... </k> requires #inUnsignedRange(ITYPE, X -Int Y)

// forall X Y : Nat, X = Y -> X - Y = 0
claim
<instrs>
ITYPE:IValType . const X ~>
ITYPE:IValType . const Y ~>
ITYPE:IValType . sub
=> .
...
</instrs>
<valstack> S => < ITYPE > 0 : S </valstack>
requires #inUnsignedRange(ITYPE, X) andBool X ==Int Y

// forall X Y : Nat, X <= max X Y && Y <= max X Y
claim
<instrs>
ITYPE:IValType . const X ~>
ITYPE:IValType . const Y ~>
ITYPE:IValType . ge_u ~>
#if([ITYPE:IValType .ValTypes], ITYPE:IValType.const X, ITYPE:IValType.const Y, _)
=> .
...
</instrs>
<valstack> S => < ITYPE > ?MAX : S </valstack>
requires
#inUnsignedRange(ITYPE, X) andBool
#inUnsignedRange(ITYPE, Y)
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
requires
#inUnsignedRange(ITYPE, X) andBool
#inUnsignedRange(ITYPE, Y)
requires #inUnsignedRange(ITYPE, X)
andBool #inUnsignedRange(ITYPE, Y)

ensures
#inUnsignedRange(ITYPE, ?MAX) andBool
X <=Int ?MAX andBool
Y <=Int ?MAX

// forall X Y : Nat, even X -> even Y -> even (X + Y)
claim
<instrs>
ITYPE:IValType . const X:Int ~>
ITYPE:IValType . const Y:Int ~>
ITYPE . add => .
...
</instrs>
<valstack> S:ValStack => < ITYPE > Z : S </valstack>
requires
0 <=Int X andBool
0 <=Int Y andBool
0 <=Int Z andBool
Z ==Int (X +Int Y) andBool
Z <Int #pow(ITYPE) andBool
X modInt 2 ==Int 0 andBool
Y modInt 2 ==Int 0
ensures
Z modInt 2 ==Int 0
endmodule