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

Show file tree
Hide file tree
Changes from 1 commit
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
5 changes: 5 additions & 0 deletions kwasm-lemmas.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -21,6 +21,11 @@ Basic logic
Basic arithmetic
----------------

```k
rule #signed(_, 0) => 0 [simplification]
rule #signed(_, X -Int Y) => X -Int Y [simplification]
Copy link
Member

Choose a reason for hiding this comment

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

This isn't true. Consider the definition of #signed (in data.md)

    rule #signed(ITYPE, N) => N                  requires 0            <=Int N andBool N <Int #pow1(ITYPE) 
    rule #signed(ITYPE, N) => N -Int #pow(ITYPE) requires #pow1(ITYPE) <=Int N andBool N <Int #pow (ITYPE)

So if we have that notBool (0 <=Int X -Int Y andBool X - Int Y <Int #pow1(ITYPE)), and we also have that #pow1(ITYPE) <=Int X -Int Y andBool X -Int Y <Int #pow(ITYPE), we should be returning (X -Int Y) -Int #pow(ITYPE), but your simplification rule returns X -Int Y.

Copy link
Member

Choose a reason for hiding this comment

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

You can add a requires clause to your second rule which says 0 <=Int X -Int Y andBool X -Int Y <Int #pow1(ITYPE), but that would be saying the same thing as the original rule in the semantics.

So instead, we should make it so the prover can know that 0 <=Int X -Int Y andBool X -Int Y <Int #pow1(ITYPE) is true. Which proof is this lemma needed for?

```

// TODO: Upstream the lemmas in this section into K.

### Modular Arithmetic
Expand Down
59 changes: 59 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,59 @@
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 . sub ~>
ITYPE:IValType . const 0 ~>
ITYPE:IValType . ge_s ~>
#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) andBool
#inUnsignedRange(ITYPE, X -Int 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