From 8c4291ad7aad7eeb190f9ef7aa25079c2d4e3a64 Mon Sep 17 00:00:00 2001 From: Calin Nicolau Date: Tue, 28 Sep 2021 13:36:45 +0300 Subject: [PATCH 1/4] Add simple example proofs --- kwasm-lemmas.md | 5 ++++ tests/proofs/simple-spec.k | 59 ++++++++++++++++++++++++++++++++++++++ 2 files changed, 64 insertions(+) create mode 100644 tests/proofs/simple-spec.k diff --git a/kwasm-lemmas.md b/kwasm-lemmas.md index e05f317c4..f3450b92f 100644 --- a/kwasm-lemmas.md +++ b/kwasm-lemmas.md @@ -21,6 +21,11 @@ Basic logic Basic arithmetic ---------------- +```k + rule #signed(_, 0) => 0 [simplification] + rule #signed(_, X -Int Y) => X -Int Y [simplification] +``` + // TODO: Upstream the lemmas in this section into K. ### Modular Arithmetic diff --git a/tests/proofs/simple-spec.k b/tests/proofs/simple-spec.k new file mode 100644 index 000000000..490c00357 --- /dev/null +++ b/tests/proofs/simple-spec.k @@ -0,0 +1,59 @@ +requires "kwasm-lemmas.md" + +module SIMPLE-SPEC + imports KWASM-LEMMAS + + // forall X Y : Nat, X = Y -> X - Y = 0 + claim + + ITYPE:IValType . const X ~> + ITYPE:IValType . const Y ~> + ITYPE:IValType . sub + => . + ... + + S => < ITYPE > 0 : S + requires #inUnsignedRange(ITYPE, X) andBool X ==Int Y + + // forall X Y : Nat, X <= max X Y && Y <= max X Y + claim + + 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, _) + => . + ... + + S => < ITYPE > ?MAX : S + 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 + + ITYPE:IValType . const X:Int ~> + ITYPE:IValType . const Y:Int ~> + ITYPE . add => . + ... + + S:ValStack => < ITYPE > Z : S + requires + 0 <=Int X andBool + 0 <=Int Y andBool + 0 <=Int Z andBool + Z ==Int (X +Int Y) andBool + Z Date: Thu, 7 Oct 2021 13:24:24 +0300 Subject: [PATCH 2/4] Fix proof --- kwasm-lemmas.md | 5 ----- tests/proofs/simple-spec.k | 4 +--- 2 files changed, 1 insertion(+), 8 deletions(-) diff --git a/kwasm-lemmas.md b/kwasm-lemmas.md index f3450b92f..e05f317c4 100644 --- a/kwasm-lemmas.md +++ b/kwasm-lemmas.md @@ -21,11 +21,6 @@ Basic logic Basic arithmetic ---------------- -```k - rule #signed(_, 0) => 0 [simplification] - rule #signed(_, X -Int Y) => X -Int Y [simplification] -``` - // TODO: Upstream the lemmas in this section into K. ### Modular Arithmetic diff --git a/tests/proofs/simple-spec.k b/tests/proofs/simple-spec.k index 490c00357..b7ee8d2ec 100644 --- a/tests/proofs/simple-spec.k +++ b/tests/proofs/simple-spec.k @@ -20,9 +20,7 @@ module SIMPLE-SPEC ITYPE:IValType . const X ~> ITYPE:IValType . const Y ~> - ITYPE:IValType . sub ~> - ITYPE:IValType . const 0 ~> - ITYPE:IValType . ge_s ~> + ITYPE:IValType . ge_u ~> #if([ITYPE:IValType .ValTypes], ITYPE:IValType.const X, ITYPE:IValType.const Y, _) => . ... From 85d747c4700e6d7ee957db411a6867a7d280bd73 Mon Sep 17 00:00:00 2001 From: Calin Nicolau Date: Thu, 7 Oct 2021 13:28:28 +0300 Subject: [PATCH 3/4] Remove #inUnsignedRange for subtraction --- tests/proofs/simple-spec.k | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/tests/proofs/simple-spec.k b/tests/proofs/simple-spec.k index b7ee8d2ec..abee240a1 100644 --- a/tests/proofs/simple-spec.k +++ b/tests/proofs/simple-spec.k @@ -28,8 +28,7 @@ module SIMPLE-SPEC S => < ITYPE > ?MAX : S requires #inUnsignedRange(ITYPE, X) andBool - #inUnsignedRange(ITYPE, Y) andBool - #inUnsignedRange(ITYPE, X -Int Y) + #inUnsignedRange(ITYPE, Y) ensures #inUnsignedRange(ITYPE, ?MAX) andBool X <=Int ?MAX andBool From 669f7dd8c23e7dce30dab72ca4a9473b6ba34b0b Mon Sep 17 00:00:00 2001 From: Calin Nicolau Date: Mon, 11 Oct 2021 12:18:18 +0300 Subject: [PATCH 4/4] Fix format --- tests/proofs/simple-spec.k | 78 ++++++++++++++++++-------------------- 1 file changed, 37 insertions(+), 41 deletions(-) diff --git a/tests/proofs/simple-spec.k b/tests/proofs/simple-spec.k index abee240a1..197e16e4b 100644 --- a/tests/proofs/simple-spec.k +++ b/tests/proofs/simple-spec.k @@ -4,53 +4,49 @@ module SIMPLE-SPEC imports KWASM-LEMMAS // forall X Y : Nat, X = Y -> X - Y = 0 - claim - - ITYPE:IValType . const X ~> - ITYPE:IValType . const Y ~> - ITYPE:IValType . sub - => . - ... - + claim ITYPE:IValType . const X + ~> ITYPE:IValType . const Y + ~> ITYPE:IValType . sub + => . + ... + S => < ITYPE > 0 : S - requires #inUnsignedRange(ITYPE, X) andBool X ==Int Y + requires #inUnsignedRange(ITYPE, X) + andBool X ==Int Y // forall X Y : Nat, X <= max X Y && Y <= max X Y - claim - - ITYPE:IValType . const X ~> - ITYPE:IValType . const Y ~> - ITYPE:IValType . ge_u ~> - #if([ITYPE:IValType .ValTypes], ITYPE:IValType.const X, ITYPE:IValType.const Y, _) - => . - ... + claim ITYPE:IValType . const X + ~> ITYPE:IValType . const Y + ~> ITYPE:IValType . ge_u + ~> #if([ITYPE:IValType .ValTypes], + ITYPE:IValType.const X, + ITYPE:IValType.const Y, + _ + ) + => . + ... S => < ITYPE > ?MAX : S - requires - #inUnsignedRange(ITYPE, X) andBool - #inUnsignedRange(ITYPE, Y) - ensures - #inUnsignedRange(ITYPE, ?MAX) andBool - X <=Int ?MAX andBool - Y <=Int ?MAX + 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 - - ITYPE:IValType . const X:Int ~> - ITYPE:IValType . const Y:Int ~> - ITYPE . add => . - ... + claim ITYPE:IValType . const X:Int + ~> ITYPE:IValType . const Y:Int + ~> ITYPE:IValType . add + => . + ... - S:ValStack => < ITYPE > Z : S - requires - 0 <=Int X andBool - 0 <=Int Y andBool - 0 <=Int Z andBool - Z ==Int (X +Int Y) andBool - Z S:ValStack => < ITYPE:IValType > Z : S + requires 0 <=Int X + andBool 0 <=Int Y + andBool 0 <=Int Z + andBool Z ==Int (X +Int Y) + andBool Z