Skip to content

Commit

Permalink
Use KRun for wasm initialization
Browse files Browse the repository at this point in the history
  • Loading branch information
@virgil-serbanuta
virgil-serbanuta committed Sep 13, 2023
1 parent bab9234 commit a9e9c64
Show file tree
Hide file tree
Showing 19 changed files with 556 additions and 146 deletions.
10 changes: 8 additions & 2 deletions kmxwasm/k-src/ceils-syntax.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -8,10 +8,12 @@ module CEILS-SYNTAX
syntax Bool ::= definedReplaceAtBytes(dest: Bytes, index: Int, src: Bytes) [function, total]
syntax Bool ::= definedPadRightBytes(Bytes, length: Int, value: Int) [function, total]
syntax Bool ::= definedModInt(Int, Int) [function, total]
syntax Bool ::= definedDivInt(Int, Int) [function, total]
syntax Bool ::= definedShlInt(Int, Int) [function, total]
syntax Bool ::= definedShrInt(Int, Int) [function, total]
syntax Bool ::= definedPowInt(Int, Int) [function, total]
syntax Bool ::= definedDivInt(Int, Int) [function, total]
syntax Bool ::= definedTModInt(Int, Int) [function, total]
syntax Bool ::= definedTDivInt(Int, Int) [function, total]
syntax Bool ::= definedLog2Int(Int) [function, total]
syntax Bool ::= definedProjectBytes(KItem) [function, total]
syntax Bool ::= definedProjectInt(KItem) [function, total]
Expand All @@ -30,14 +32,18 @@ module CEILS-SYNTAX
[function, total, klabel(padRightBytesTotal), symbol, no-evaluators]
syntax Int ::= Int "modIntTotal" Int
[function, total, klabel(modIntTotal), symbol, no-evaluators, smt-hook(mod)]
syntax Int ::= Int "divIntTotal" Int
[function, total, klabel(divIntTotal), symbol, no-evaluators, smt-hook(div)]
syntax Int ::= Int "<<IntTotal" Int
[function, total, klabel(shlIntTotal), symbol, no-evaluators]
syntax Int ::= Int ">>IntTotal" Int
[function, total, klabel(shrIntTotal), symbol, no-evaluators]
syntax Int ::= Int "^IntTotal" Int
[function, total, klabel(powIntTotal), symbol, no-evaluators]
syntax Int ::= Int "%IntTotal" Int
[function, total, klabel(tModIntTotal), symbol, no-evaluators, smtlib(tModInt)]
syntax Int ::= Int "/IntTotal" Int
[function, total, klabel(divIntTotal), symbol, no-evaluators, smt-hook(div)]
[function, total, klabel(tDivIntTotal), symbol, no-evaluators, smtlib(tDivInt)]
syntax Int ::= log2IntTotal(Int)
[ function, total, klabel(log2IntTotal), symbol, no-evaluators,
smtlib(log2IntTotal)
Expand Down
78 changes: 65 additions & 13 deletions kmxwasm/k-src/ceils.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -141,15 +141,33 @@ module CEILS
requires definedModInt(Arg0, Arg1)
[symbolic(Arg1), simplification]

// rule Arg0:Int modInt Arg1:Int
// => normalizeModIntTotalHelper(Arg0, Arg1) modIntTotal Arg1 // Arg0 modIntTotal Arg1
// requires definedModInt(Arg0, Arg1)
// [symbolic(Arg0), simplification]
//----------------------------------


rule definedDivInt (_:Int, X:Int) => X =/=Int 0

rule #Ceil(@Arg0:Int divInt @Arg1:Int)
=> (({ definedDivInt(@Arg0, @Arg1) #Equals true }
#And #Ceil(@Arg0))
#And #Ceil(@Arg1))
[simplification]

rule _ divIntTotal 0 => 0

rule Arg0:Int divIntTotal Arg1:Int
=> Arg0 divInt Arg1
requires definedDivInt(Arg0, Arg1)
[concrete, simplification]

rule Arg0:Int divInt Arg1:Int
=> Arg0 divIntTotal Arg1
requires definedDivInt(Arg0, Arg1)
[symbolic(Arg0), simplification]

// rule Arg0:Int modInt Arg1:Int
// => normalizeModIntTotalHelper(Arg0, Arg1) modIntTotal Arg1 // Arg0 modIntTotal Arg1
// requires definedModInt(Arg0, Arg1)
// [symbolic(Arg1), simplification]
rule Arg0:Int divInt Arg1:Int
=> Arg0 divIntTotal Arg1
requires definedDivInt(Arg0, Arg1)
[symbolic(Arg1), simplification]

//----------------------------------

Expand Down Expand Up @@ -220,27 +238,54 @@ module CEILS
//-------------------------------------


rule definedDivInt(_:Int, Y:Int) => Y =/=Int 0
rule definedTModInt(_:Int, Y:Int) => Y =/=Int 0

rule #Ceil(@Arg0:Int %Int @Arg1:Int)
=> (({ definedTModInt(@Arg0, @Arg1) #Equals true }
#And #Ceil(@Arg0))
#And #Ceil(@Arg1))
[simplification]

rule Arg0:Int %IntTotal Arg1:Int
=> Arg0 %Int Arg1
requires definedTModInt(Arg0, Arg1)
[concrete, simplification]

rule Arg0:Int %Int Arg1:Int
=> Arg0 %IntTotal Arg1
requires definedTModInt(Arg0, Arg1)
[symbolic(Arg0), simplification]

rule Arg0:Int %Int Arg1:Int
=> Arg0 %IntTotal Arg1
requires definedTModInt(Arg0, Arg1)
[symbolic(Arg1), simplification]


//-------------------------------------


rule definedTDivInt(_:Int, Y:Int) => Y =/=Int 0

rule #Ceil(@Arg0:Int /Int @Arg1:Int)
=> (({ definedDivInt(@Arg0, @Arg1) #Equals true }
=> (({ definedTDivInt(@Arg0, @Arg1) #Equals true }
#And #Ceil(@Arg0))
#And #Ceil(@Arg1))
[simplification]

rule Arg0:Int /IntTotal Arg1:Int
=> Arg0 /Int Arg1
requires definedDivInt(Arg0, Arg1)
requires definedTDivInt(Arg0, Arg1)
[concrete, simplification]

rule Arg0:Int /Int Arg1:Int
=> Arg0 /IntTotal Arg1
requires definedDivInt(Arg0, Arg1)
requires definedTDivInt(Arg0, Arg1)
[symbolic(Arg0), simplification]

rule Arg0:Int /Int Arg1:Int
=> Arg0 /IntTotal Arg1
requires definedDivInt(Arg0, Arg1)
requires definedTDivInt(Arg0, Arg1)
[symbolic(Arg1), simplification]


Expand Down Expand Up @@ -389,4 +434,11 @@ module CEILS
#And #Ceil(@N)
[simplification]

// -----------------------------------
// Other stuff
// -----------------------------------

rule I /IntTotal J => I divIntTotal J requires 0 <Int J
rule I %IntTotal J => I modIntTotal J requires 0 <Int J

endmodule
30 changes: 20 additions & 10 deletions kmxwasm/k-src/elrond-lemmas.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,8 @@ module ELROND-LEMMAS
imports private SET
imports private WASM-TEXT
rule size(_:List) >=Int 0 => true [simplification, smt-lemma]
rule ( size ( _L:List ) >=Int 0 => true )
[simplification(), smt-lemma()]
rule Bytes2Int(#getBytesRange(_:Bytes, _:Int, N:Int), _:Endianness, _:Signedness) <Int M:Int
=> true
Expand All @@ -31,8 +32,8 @@ module ELROND-LEMMAS
requires 0 <=Int Value
[simplification]
rule { b"" #Equals Int2Bytes(Len:Int, _Value:Int, _:Endianness)} => #Bottom
requires Len >Int 0
rule { b"" #Equals Int2Bytes(Len:Int, _Value:Int, _E:Endianness)}:Bool
=> {0 #Equals Len}
[simplification]
rule 0 <=Int A +Int B => true
Expand Down Expand Up @@ -308,8 +309,23 @@ module ELROND-LEMMAS
requires B =/=Int 0
[simplification(50)]
rule A:Int <Int 2 ^IntTotal ((( log2IntTotal(A) +Int 8) /IntTotal 8) *Int 8)
// log2IntTotal(X) is the index of the highest bit. This means that
// X < 2^(log2IntTotal(X) + 1) since the highest bit of the right term
// has a higher index.
// We need
// 2^(log2IntTotal(X) + 1) <= 2 ^IntTotal (((log2IntTotal(X) +Int 8) divIntTotal 8) *Int 8)
// which is equivalent to
// log2IntTotal(X) + 1 <= ((log2IntTotal(X) +Int 8) divIntTotal 8) *Int 8.
// Let us denote log2IntTotal(X) by Y >= 0
// Y + 1 <= (Y divIntTotal 8 + 1) *Int 8.
// Y + 1 <= (Y divIntTotal 8) *Int 8 + 8.
// Y <= (Y divIntTotal 8) *Int 8 + 7.
// Let A be Y divIntTotal 8
// Let B be Y modIntTotal 8.
// A * 8 + B <= A * 8 + 7, which is obviously true.
rule A:Int <Int 2 ^IntTotal ((( log2IntTotal(A) +Int 8) divIntTotal 8) *Int 8)
=> true
requires 0 <Int A
[simplification]
rule 0 <=Int #bool ( _B ) => true
Expand All @@ -327,12 +343,6 @@ module ELROND-LEMMAS
rule { 1 #Equals #bool ( B:Bool ) } => { true #Equals B:Bool }
[simplification()]
rule X:Int <=Int maxInt ( Y:Int , Z:Int ) => true
requires ( X:Int <=Int Y:Int
orBool ( X:Int <=Int Z:Int
))
[simplification()]
rule X:Int <Int maxInt ( Y:Int , Z:Int ) => true
requires ( X:Int <Int Y:Int
orBool ( X:Int <Int Z:Int
Expand Down
2 changes: 1 addition & 1 deletion kmxwasm/k-src/elrond-semantics
Submodule elrond-semantics updated from 58ccff to 1c0c21
22 changes: 22 additions & 0 deletions kmxwasm/k-src/specification-lemmas.md
View file
Original file line number Diff line number Diff line change
@@ -1,5 +1,6 @@
```k
module SPECIFICATION-LEMMAS
imports private CEILS-SYNTAX
imports private INT
imports private LIST
Expand All @@ -16,5 +17,26 @@ module SPECIFICATION-LEMMAS
rule minInt(A:Int, B:Int) => A requires A <=Int B
[simplification]
// Y > 0
rule X /IntTotal Y => 0
requires 0 <=Int X andBool X <Int Y
[simplification]
rule X /IntTotal Y => 1 +Int ((X -Int Y) /IntTotal Y)
requires 0 <Int Y andBool Y <=Int X
[simplification]
rule X /IntTotal Y => ((X +Int Y) /IntTotal Y) -Int 1
requires 0 <Int Y andBool X <Int 0
[simplification]
// Y < 0
rule X /IntTotal Y => 0
requires Y <Int X andBool X <=Int 0
[simplification]
rule X /IntTotal Y => 1 +Int ((X -Int Y) /IntTotal Y)
requires X <=Int Y andBool Y <Int 0
[simplification]
rule X /IntTotal Y => ((X +Int Y) /IntTotal Y) -Int 1
requires Y <Int 0 andBool 0 <Int X
[simplification]
endmodule
```
Loading

0 comments on commit a9e9c64

Please sign in to comment.