search

runtimeverification / pyk

Python tools for the K Framework
BSD 3-Clause "New" or "Revised" License
13 stars 2 forks source link

Refactoring the branching mechanism #1072

Closed PetarMax closed 6 months ago

PetarMax commented 6 months ago

This is a very draft PR that uses branching information from the backend (for which support was enabled by runtimeverification/pyk#942) to simplify the branching mechanism, potentially making the extract_branches obsolete and only creating NDBranches in the presence of true non-determinism.

I've done a preliminary testing in Kontrol, more info in comments below.

PetarMax commented 6 months ago

As a first example, I have that the KCFG of the CSE execution of ArithmeticCallTest.test_double_add transforms from this

┌─ 1 (root, init)
│   k: #execute ~> CONTINUATION:K
│   pc: 0
│   callDepth: 0
│   statusCode: STATUSCODE:StatusCode
│
│  (1024 steps)
├─ 7 (split)
│   k: #execute ~> #return 128 32 ~> #pc [ STATICCALL ] ~> #execute ~> CONTINUATION:K
│   pc: 0
│   callDepth: 1
│   statusCode: STATUSCODE:StatusCode
┃
┃ (branch)
┣━━┓ constraint: ( maxUInt256 -Int VV1_y_114b9705:Int ) <Int VV0_x_114b9705:Int
┃  │
┃  ├─ 8
┃  │   k: #execute ~> #return 128 32 ~> #pc [ STATICCALL ] ~> #execute ~> CONTINUATION:K
┃  │   pc: 0
┃  │   callDepth: 1
┃  │   statusCode: STATUSCODE:StatusCode
┃  │
┃  │  (73 steps)
┃  └─ 10 (leaf, terminal)
┃      k: #halt ~> CONTINUATION:K
┃      pc: 2357
┃      callDepth: 0
┃      statusCode: EVMC_REVERT
┃
┗━━┓ constraint: VV0_x_114b9705:Int <=Int ( maxUInt256 -Int VV1_y_114b9705:Int )
   │
   ├─ 9
   │   k: #execute ~> #return 128 32 ~> #pc [ STATICCALL ] ~> #execute ~> CONTINUATION:K
   │   pc: 0
   │   callDepth: 1
   │   statusCode: STATUSCODE:StatusCode
   │
   │  (413 steps)
   ├─ 11
   │   k: #execute ~> #return 160 32 ~> #pc [ STATICCALL ] ~> #execute ~> CONTINUATION:K
   │   pc: 0
   │   callDepth: 1
   │   statusCode: EVMC_SUCCESS
   ┃
   ┃ (1 step)
   ┣━━┓
   ┃  │
   ┃  ├─ 12
   ┃  │   k: #halt ~> #return 160 32 ~> #pc [ STATICCALL ] ~> #execute ~> CONTINUATION:K
   ┃  │   pc: 550
   ┃  │   callDepth: 1
   ┃  │   statusCode: EVMC_REVERT
   ┃  │
   ┃  │  (72 steps)
   ┃  └─ 14 (leaf, terminal)
   ┃      k: #halt ~> CONTINUATION:K
   ┃      pc: 2474
   ┃      callDepth: 0
   ┃      statusCode: EVMC_REVERT
   ┃
   ┗━━┓
      │
      ├─ 13 (split)
      │   k: #halt ~> #return 160 32 ~> #pc [ STATICCALL ] ~> #execute ~> CONTINUATION:K
      │   pc: 128
      │   callDepth: 1
      │   statusCode: EVMC_SUCCESS
      ┃
      ┃ (branch)
      ┣━━┓ constraint: VV0_x_114b9705:Int <Int ( ( VV0_x_114b9705:Int +Int VV1_y_114b9705:Int ) +Int VV1_y_114b9705:Int )
      ┃  │
      ┃  ├─ 20
      ┃  │   k: #halt ~> #return 160 32 ~> #pc [ STATICCALL ] ~> #execute ~> CONTINUATION:K
      ┃  │   pc: 128
      ┃  │   callDepth: 1
      ┃  │   statusCode: EVMC_SUCCESS
      ┃  │
      ┃  │  (321 steps)
      ┃  ├─ 18 (terminal)
      ┃  │   k: #halt ~> CONTINUATION:K
      ┃  │   pc: 248
      ┃  │   callDepth: 0
      ┃  │   statusCode: EVMC_SUCCESS
      ┃  │
      ┃  ┊  constraint: true
      ┃  ┊  subst: OMITTED SUBST
      ┃  └─ 6 (leaf, target, terminal)
      ┃      k: #halt ~> CONTINUATION:K
      ┃      pc: PC_CELL_5d410f2a:Int
      ┃      callDepth: CALLDEPTH_CELL_5d410f2a:Int
      ┃      statusCode: STATUSCODE_FINAL:StatusCode
      ┃
      ┗━━┓ constraint: ( notBool VV0_x_114b9705:Int <Int ( ( VV0_x_114b9705:Int +Int VV1_y_114b9705:Int ) +Int VV1_y_114b9705:Int ) )
         │
         ├─ 21
         │   k: #halt ~> #return 160 32 ~> #pc [ STATICCALL ] ~> #execute ~> CONTINUATION:K
         │   pc: 128
         │   callDepth: 1
         │   statusCode: EVMC_SUCCESS
         │
         │  (331 steps)
         └─ 19 (leaf, terminal)
             k: #halt ~> CONTINUATION:K
             pc: 3736
             callDepth: 0
             statusCode: EVMC_REVERT

which is not great, and in which simultaneous applications of multiple specifications of the underlying functions cause non-deterministic branching, to this

┌─ 1 (root, init)
│   k: #execute ~> CONTINUATION:K
│   pc: 0
│   callDepth: 0
│   statusCode: STATUSCODE:StatusCode
│   src: test/ArithmeticCall.t.sol:6:33
│
│  (1024 steps)
├─ 7 (split)
│   k: #execute ~> #return 128 32 ~> #pc [ STATICCALL ] ~> #execute ~> CONTINUATION:K
│   pc: 0
│   callDepth: 1
│   statusCode: STATUSCODE:StatusCode
│   src: test/ArithmeticCall.t.sol:6:33
┃
┃ (branch)
┣━━┓ constraint: ( maxUInt256 -Int VV1_y_114b9705:Int ) <Int VV0_x_114b9705:Int
┃  │
┃  ├─ 9
┃  │   k: #execute ~> #return 128 32 ~> #pc [ STATICCALL ] ~> #execute ~> CONTINUATION:K
┃  │   pc: 0
┃  │   callDepth: 1
┃  │   statusCode: STATUSCODE:StatusCode
┃  │   src: test/ArithmeticCall.t.sol:6:33
┃  │
┃  │  (73 steps)
┃  └─ 11 (leaf, terminal)
┃      k: #halt ~> CONTINUATION:K
┃      pc: 2357
┃      callDepth: 0
┃      statusCode: EVMC_REVERT
┃
┣━━┓ constraints:
┃  ┃     ( VV0_x_114b9705:Int +Int VV1_y_114b9705:Int ) <Int pow256
┃  ┃     VV0_x_114b9705:Int <=Int ( maxUInt256 -Int VV1_y_114b9705:Int )
┃  ┃     ( maxUInt256 -Int VV1_y_114b9705:Int ) <Int ( VV0_x_114b9705:Int +Int VV1_y_114b9705:Int )
┃  │
┃  ├─ 21
┃  │   k: #execute ~> #return 128 32 ~> #pc [ STATICCALL ] ~> #execute ~> CONTINUATION:K
┃  │   pc: 0
┃  │   callDepth: 1
┃  │   statusCode: STATUSCODE:StatusCode
┃  │   src: test/ArithmeticCall.t.sol:6:33
┃  │
┃  │  (486 steps)
┃  └─ 15 (leaf, terminal)
┃      k: #halt ~> CONTINUATION:K
┃      pc: 2474
┃      callDepth: 0
┃      statusCode: EVMC_REVERT
┃
┣━━┓ constraints:
┃  ┃     ( VV0_x_114b9705:Int +Int VV1_y_114b9705:Int ) <Int pow256
┃  ┃     VV0_x_114b9705:Int <=Int ( maxUInt256 -Int VV1_y_114b9705:Int )
┃  ┃     VV0_x_114b9705:Int <Int ( ( VV0_x_114b9705:Int +Int VV1_y_114b9705:Int ) +Int VV1_y_114b9705:Int )
┃  ┃     ( VV0_x_114b9705:Int +Int VV1_y_114b9705:Int ) <=Int ( maxUInt256 -Int VV1_y_114b9705:Int )
┃  │
┃  ├─ 24
┃  │   k: #execute ~> #return 128 32 ~> #pc [ STATICCALL ] ~> #execute ~> CONTINUATION:K
┃  │   pc: 0
┃  │   callDepth: 1
┃  │   statusCode: STATUSCODE:StatusCode
┃  │   src: test/ArithmeticCall.t.sol:6:33
┃  │
┃  │  (735 steps)
┃  ├─ 18 (terminal)
┃  │   k: #halt ~> CONTINUATION:K
┃  │   pc: 248
┃  │   callDepth: 0
┃  │   statusCode: EVMC_SUCCESS
┃  │   src: test/ArithmeticCall.t.sol:9:12
┃  │
┃  ┊  constraint: true
┃  ┊  subst: OMITTED SUBST
┃  └─ 6 (leaf, target, terminal)
┃      k: #halt ~> CONTINUATION:K
┃      pc: PC_CELL_5d410f2a:Int
┃      callDepth: CALLDEPTH_CELL_5d410f2a:Int
┃      statusCode: STATUSCODE_FINAL:StatusCode
┃
┗━━┓ constraints:
   ┃     ( VV0_x_114b9705:Int +Int VV1_y_114b9705:Int ) <Int pow256
   ┃     VV0_x_114b9705:Int <=Int ( maxUInt256 -Int VV1_y_114b9705:Int )
   ┃     ( ( VV0_x_114b9705:Int +Int VV1_y_114b9705:Int ) +Int VV1_y_114b9705:Int ) <=Int VV0_x_114b9705:Int
   ┃     ( VV0_x_114b9705:Int +Int VV1_y_114b9705:Int ) <=Int ( maxUInt256 -Int VV1_y_114b9705:Int )
   │
   ├─ 25
   │   k: #execute ~> #return 128 32 ~> #pc [ STATICCALL ] ~> #execute ~> CONTINUATION:K
   │   pc: 0
   │   callDepth: 1
   │   statusCode: STATUSCODE:StatusCode
   │   src: test/ArithmeticCall.t.sol:6:33
   │
   │  (745 steps)
   └─ 19 (leaf, terminal)
       k: #halt ~> CONTINUATION:K
       pc: 3736
       callDepth: 0
       statusCode: EVMC_REVERT

where there are no non-deterministic branches and all branching conditions are present.

PetarMax commented 6 months ago

In a recent proof, also, the two branchings below were characterised as non-deterministic, but their constraints are now fully captured:

┃
┃ (branch)
┣━━┓ constraint: ( X:Int ==Int ( X:Int *Int Y:Int ) /Word Y:Int orBool Y:Int ==Int 0 )
┃  │
┃  ├─ 65
┃  │   k: JUMPI --- bool2Word ( ( X:Int ==Int ( X:Int *Int Y:Int ) /Word ...
┃  │   pc: ---
┃  │   callDepth: ---
┃  │   statusCode: EVMC_SUCCESS
┃  │
┃  ...
┃  ┃
┃  ┃ (branch)
┃  ┣━━┓ constraint: ( Z:Int ==Int ( Z:Int *Int T:Int ) /Word T:Int orBool T:Int ==Int 0 )
┃  ┃  │
┃  ┃  └─ 75 (leaf, refuted)
┃  ┃      k: JUMPI --- bool2Word ( ( Z:Int ==Int ( Z:Int *Int T:Int ) /Word ...
┃  ┃      pc: ---
┃  ┃      callDepth: ---
┃  ┃      statusCode: EVMC_SUCCESS
┃  ┃
┃  ┗━━┓ constraints:
┃     ┃     ( notBool T:Int ==K 0 )
┃     ┃     ( notBool Z:Int ==K ( Z:Int *Int T:Int ) /Word T:Int )
┃     │
┃     ...
┃
┗━━┓ constraints:
     ┃     ( notBool Y:Int ==K 0 )
     ┃     ( notBool X:Int ==K ( X:Int *Int Y:Int ) /Word Y:Int )
     │
     ├─ 66
     │   k: JUMPI --- bool2Word ( ( X:Int ==Int ( X:Int *Int Y:Int ) /Word ...
     │   pc: ---
     │   callDepth: ---
     │   statusCode: EVMC_SUCCESS
     │
     ...
Baltoli commented 6 months ago

https://github.com/runtimeverification/k/pull/4248