Uncaught exception thrown of type MatchError

[norbeyandresg]

I was trying to prove a simple algorithm like the sumToN from the KEVM 1.0 technical report, but when I run the line ./kevm prove get the error

~/evm-semantics$ ./kevm prove tests/proofs/resources/pow-of-two-spec.k
[Error] Internal: Uncaught exception thrown of type MatchError.
Please rerun your program with the --debug flag to generate a stack trace, and
file a bug report at https://github.com/kframework/k/issues (null)

When I try to run it in debug mode get an error in the name of the module.

~/evm-semantics$ ./kevm debug tests/proofs/resources/pow-of-two-spec.k
== debugging: tests/proofs/resources/pow-of-two-spec.k
[Error] Critical: Parser returned a non-zero exit code: 113
Stdout:

Stderr:
[Error] Inner Parser: Scanner error: unexpected character sequence '-'.
        Source(/home/ngallego/evm-semantics/./tests/proofs/resources/pow-of-two-spec.k)
        Location(3,11,3,12)

pow-verification.k

module VERIFICATION
  imports EDSL
  imports LEMMAS

  syntax Map ::= "powOfTwo" "(" Int ")"   [function]
  //----------------------------------------------------

  rule powOfTwo(N)
    => #asMapOpCodes( PUSH(1,1); PUSH(N,1)                    // y - 1, x = N
                    ; JUMPDEST                                // label:loop
                    ; DUP(1); ISZERO; PUSH(1,55); JUMPI       // if n == 0, jump to end
                    ; SWAP(1); PUSH(1,1); SWAP(1); SUB        // x = x - 1
                    ; SWAP(1); SWAP(5); DUP(1); SUM           // y = y + y
                    ; SWAP(1); SWAP(3); PSUH(1,35); JUMP      // jump to loop
                    ; JUMPDEST                                // label:end
                    ; .OpCodes
                    )   [macro]
endmodule

pow-of-two-speck.k

requires "pow-verification.k"

module POW-OF-TWO-SPEC
  imports ETHEREUM-SIMULATION
  imports VERIFICATION

  //powOfTwo
  rule <k> #execute... </k>
       <mode> NORMAL </mode>
       <schedule> DEFAULT </schedule>
       <callStack> .List </callStack>
       <memoryUsed> 0 </memoryUsed>
       <localMem> .Map </localMem>
       <previousGas>  _ => _ </previousGas>
       <program> powOfTwo(N) </program>

       <pc>        0 => 56                           </pc>
       <wordStack> WS => 0 : 2 ^Int N : WS           </wordStack>
       <gas>       G  => G -Int (52 *Int N +Int 27)  </gas>

       requires N >=Int 0
       andBool  N <=Int 340282366920938463463374607431768211455
       andBool  #sizeWordStack(WS) <Int 1021
       andBool G >=Int 55 *Int N +Int 27

  rule <k> #execute... </k>
       <mode> NORMAL </mode>
       <schedule> DEFAULT </schedule>
       <callStack> .List </callStack>
       <memoryUsed> 0 </memoryUsed>
       <localMem> .Map </localMem>
       <previousGas>  _ => _ </previousGas>
       <program> powOfTwo(N) </program>

       <pc>        35 => 56                           </pc>
       <gas>       G  => G -Int (52 *Int N +Int 27)   </gas>
       <wordStack> I : S         : WS
                => 0 : S +Int S  : WS                 </wordStack>

       requires I >=Int 0
       andBool  S >=Int 0
       andBool  S +Int S <=Int pow256
       andBool  #sizeWordStack(WS) <Int 1021
       andBool G >=Int 55 *Int N +Int 27
endmodule

[ehildenb]

./kevm help indicates that you cannot run ./kevm debug on a *-spec.k file, it must be on an individual program, not a specification file.

Did you try running ./kevm prove tests/proofs/resources/pow-of-two-spec.k with the --debug flag as it suggests?

Please post the output of:

./kevm prove tests/proofs/resources/pow-of-two-spec.k --debug

[norbeyandresg]

I try it but I get the same error

~/evm-semantics$ ./kevm prove tests/proofs/resources/pow-of-two-spec.k --debug
[Error] Internal: Uncaught exception thrown of type MatchError.
Please rerun your program with the --debug flag to generate a stack trace, and
file a bug report at https://github.com/kframework/k/issues (null)

[ehildenb]

I see in your pow-verification.k two potential typos, one is the opcode SUM, on is the opcode PSUH. Does your local file actually contain those typos?

[norbeyandresg]

I corrected the opcodes and it worked.
thanks