hm, I'm getting "failed to generate a model" for this too:

    function prove_assert_false() public pure {
        assert(false);
    }

Running functions: ['\''src%unsafe%1tx-abstract%AssertFalse.prove_assert_false()'\'']
PROOF FAILED: src%unsafe%1tx-abstract%AssertFalse.prove_assert_false():0
1 Failure nodes. (0 pending and 1 failing)

Failing nodes:

  Node id: 5
  Failure reason:
    Implication check failed, the following is the remaining implication:
    ( ( { true #Equals 0 <=Int CALLER_ID:Int }
    #And ( { true #Equals 0 <=Int ORIGIN_ID:Int }
    #And ( { true #Equals 0 <=Int NUMBER_CELL:Int }
    #And ( { true #Equals CALLER_ID:Int <Int pow160 }
    #And ( { true #Equals ORIGIN_ID:Int <Int pow160 }
    #And { true #Equals NUMBER_CELL:Int <=Int maxSInt256 } ) ) ) ) ) #Implies { true #Equals foundry_success ( ... statusCode: EVMC_REVERT , failed: #lookup ( .Map , 46308022326495007027972728677917914892729792999299745830475596687180801507328 ) , revertExpected: false , opcodeExpected: false , recordEventExpected: false , eventExpected: false ) } )
  Path condition:
    #Top
  Failed to generate a model.

In reply to @xvwx:matrix.dapp.org.uk
do you know of any examples where it can produce a model? or like some example output of a model? Just so I can write a regex that can detect if it has managed to produce a model?

Hey @dxo! Thanks for all your work on the benchmark repo and integrating Kontrol there!

To produce a model, you can execute the same prove_sub_comm(uint x, uint y) test you've been using:

    function prove_sub_comm(uint x, uint y) public pure {
        unchecked {
            assert(x - y == y - x);
        }
    }

but please add a --counterexample-information option to kontrol prove:

❯ kontrol prove --match-test prove_sub_comm --counterexample-information

...

Failing nodes:

  Node id: 11
  Failure reason:
    Implication check failed, the following is the remaining implication:
    ( ( { true #Equals 0 <=Int CALLER_ID:Int }
    #And ( { true #Equals 0 <=Int ORIGIN_ID:Int }
    #And ( { true #Equals 0 <=Int NUMBER_CELL:Int }
    #And ( { true #Equals 0 <=Int VV0_x_114b9705:Int }
    #And ( { true #Equals 0 <=Int VV1_y_114b9705:Int }
    #And ( { true #Equals CALLER_ID:Int <Int pow160 }
    #And ( { true #Equals ORIGIN_ID:Int <Int pow160 }
    #And ( { true #Equals NUMBER_CELL:Int <=Int maxSInt256 }
    #And ( { true #Equals VV0_x_114b9705:Int <Int pow256 }
    #And ( { true #Equals VV1_y_114b9705:Int <Int pow256 }
    #And #Not ( { chop ( ( VV0_x_114b9705:Int -Int VV1_y_114b9705:Int ) ) #Equals chop ( ( VV1_y_114b9705:Int -Int VV0_x_114b9705:Int ) ) } ) ) ) ) ) ) ) ) ) ) ) #Implies { true #Equals foundry_success ( ... statusCode: EVMC_REVERT , failed: #lookup ( .Map , 46308022326495007027972728677917914892729792999299745830475596687180801507328 ) , revertExpected: false , opcodeExpected: false , recordEventExpected: false , eventExpected: false ) } )
  Path condition:
    { true #Equals ( notBool chop ( ( VV0_x_114b9705:Int -Int VV1_y_114b9705:Int ) ) ==Int chop ( ( VV1_y_114b9705:Int -Int VV0_x_114b9705:Int ) ) ) }
  Model:
    NUMBER_CELL = 0
    VV1_y_114b9705 = maxUInt256
    ORIGIN_ID = maxUInt160
    CALLER_ID = 0
    VV0_x_114b9705 = 57896044618658097711785492504343953926634992332820282019728792003956564819966

In reply to @xvwx:matrix.dapp.org.uk
do you know of any examples where it can produce a model? or like some example output of a model? Just so I can write a regex that can detect if it has managed to produce a model?

Hey dxo ! Thanks for all your work on the benchmark repo and integrating Kontrol there!

To produce a model, you can execute the same prove_sub_comm(uint x, uint y) test you've been using:

    function prove_sub_comm(uint x, uint y) public pure {
        unchecked {
            assert(x - y == y - x);
        }
    }

but please add a --counterexample-information option to kontrol prove:

❯ kontrol prove --match-test prove_sub_comm --counterexample-information

...

Failing nodes:

  Node id: 11
  Failure reason:
    Implication check failed, the following is the remaining implication:
    ( ( { true #Equals 0 <=Int CALLER_ID:Int }
    #And ( { true #Equals 0 <=Int ORIGIN_ID:Int }
    #And ( { true #Equals 0 <=Int NUMBER_CELL:Int }
    #And ( { true #Equals 0 <=Int VV0_x_114b9705:Int }
    #And ( { true #Equals 0 <=Int VV1_y_114b9705:Int }
    #And ( { true #Equals CALLER_ID:Int <Int pow160 }
    #And ( { true #Equals ORIGIN_ID:Int <Int pow160 }
    #And ( { true #Equals NUMBER_CELL:Int <=Int maxSInt256 }
    #And ( { true #Equals VV0_x_114b9705:Int <Int pow256 }
    #And ( { true #Equals VV1_y_114b9705:Int <Int pow256 }
    #And #Not ( { chop ( ( VV0_x_114b9705:Int -Int VV1_y_114b9705:Int ) ) #Equals chop ( ( VV1_y_114b9705:Int -Int VV0_x_114b9705:Int ) ) } ) ) ) ) ) ) ) ) ) ) ) #Implies { true #Equals foundry_success ( ... statusCode: EVMC_REVERT , failed: #lookup ( .Map , 46308022326495007027972728677917914892729792999299745830475596687180801507328 ) , revertExpected: false , opcodeExpected: false , recordEventExpected: false , eventExpected: false ) } )
  Path condition:
    { true #Equals ( notBool chop ( ( VV0_x_114b9705:Int -Int VV1_y_114b9705:Int ) ) ==Int chop ( ( VV1_y_114b9705:Int -Int VV0_x_114b9705:Int ) ) ) }
  Model:
    NUMBER_CELL = 0
    VV1_y_114b9705 = maxUInt256
    ORIGIN_ID = maxUInt160
    CALLER_ID = 0
    VV0_x_114b9705 = 57896044618658097711785492504343953926634992332820282019728792003956564819966

In reply to @xvwx:matrix.dapp.org.uk
Is there a way to tell kontrol to start with a fully abstract storage?

We have a cheatcode for that, but it's contract-specific. You can install cheatcodes as a forge library in your project:

forge install runtimeverification/kontrol-cheatcodes

and then use it as follows:

    function testSymbolicStorage(uint256 slot) public {
         address addr = 0xEA674fdDe714fd979de3EdF0F56AA9716B898ec8;
         kevm.symbolicStorage(addr);
         // the storage for addr is symbolic
         // ...
    }

In reply to @xvwx:matrix.dapp.org.uk
Is there a way to tell kontrol to start with a fully abstract storage?

We have a cheatcode for that, but it's contract-specific. You can install cheatcodes as a forge library in your project:

forge install runtimeverification/kontrol-cheatcodes

and then use it as follows:

    function testSymbolicStorage(uint256 slot) public {
         address addr = 0xEA674fdDe714fd979de3EdF0F56AA9716B898ec8;
         kevm.symbolicStorage(addr);
         // the storage for addr is symbolic
         // ...
    }