Note: refer to the following branch of k-dss for latest work https://github.com/makerdao/k-dss/tree/pot-rpow
So far I've only looked at the rpow proofs in the Pot contract.
First, I updated the pc values in Pot.rpow-loop, which passes without any issue.
Latest pc values:
// 13af => 13f3
pc
5039 => 5107
pc values at last pass:
// 0e01 => 0e45
pc
3585 => 3653
Then, I ran the Pot.rpow proof, which depends on the loop lemma.
This failed--seems to either be stuck or just running forever. Probably the lemma is not getting applied, but hard to tell.
Branching behavior from klab debug:
├ 0 (((0 < (VGas - (82 + #if_#then_#else_#fi_K-EQUAL((ABI_n ==K 0), 0, 10))))) AND (ABI_x ==K 0))
│ ├ 0 (((0 < (VGas - 82))) AND (((num1(0) >= 0)) AND (((num0(0) >= 0)) AND (ABI_n ==K 0))))
│ └ 1 ((ABI_n ==K 0) ==K false)
└ 1 ((ABI_x ==K 0) ==K false)
├ 0 (_modInt_(ABI_n, 2) ==K 0)
└ 1 ((_modInt_(ABI_n, 2) ==K 0) ==K false)
Other info: I notice that a z3 process is consuming most of my CPU when the proof enters its "stuck" phase.
Last known pass: https://dapp.ci/k-dss/1bf8c47b9f7afa2c89ca/#Pot_rpow(uint256,uint256,uint256)
Bytecode of Pot contract as last known passing run: 0x608060405234801561001057600080fd5b50600436106100f55760003560e01c8063626cb3c5116100975780639f678cca116100665780639f678cca1461035c578063bf353dbb14610366578063c92aecc4146103be578063d4e8be83146103dc576100f5565b8063626cb3c51461025c57806365fae35e146102a65780637f8661a1146102ea5780639c52a7f114610318576100f5565b806329ae8114116100d357806329ae81141461019e5780632c69ed58146101d657806336569e77146101f4578063487bf0821461023e576100f5565b8063049878f3146100fa5780630bebac861461012857806320aba08b14610180575b600080fd5b6101266004803603602081101561011057600080fd5b810190808035906020019092919050505061042a565b005b61016a6004803603602081101561013e57600080fd5b81019080803573ffffffffffffffffffffffffffffffffffffffff1690602001909291905050506105fe565b6040518082815260200191505060405180910390f35b610188610616565b6040518082815260200191505060405180910390f35b6101d4600480360360408110156101b457600080fd5b81019080803590602001909291908035906020019092919050505061061c565b005b6101de6106ce565b6040518082815260200191505060405180910390f35b6101fc6106d4565b604051808273ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200191505060405180910390f35b6102466106fa565b6040518082815260200191505060405180910390f35b610264610700565b604051808273ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200191505060405180910390f35b6102e8600480360360208110156102bc57600080fd5b81019080803573ffffffffffffffffffffffffffffffffffffffff169060200190929190505050610726565b005b6103166004803603602081101561030057600080fd5b81019080803590602001909291905050506107eb565b005b61035a6004803603602081101561032e57600080fd5b81019080803573ffffffffffffffffffffffffffffffffffffffff1690602001909291905050506109bf565b005b610364610a84565b005b6103a86004803603602081101561037c57600080fd5b81019080803573ffffffffffffffffffffffffffffffffffffffff169060200190929190505050610c3b565b6040518082815260200191505060405180910390f35b6103c6610c53565b6040518082815260200191505060405180910390f35b610428600480360360408110156103f257600080fd5b8101908080359060200190929190803573ffffffffffffffffffffffffffffffffffffffff169060200190929190505050610c59565b005b610473600160003373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1681526020019081526020016000205482610d45565b600160003373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff168152602001908152602001600020819055506104c260025482610d45565b600281905550600560009054906101000a900473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1663bb35783b333061051460045486610d5f565b6040518463ffffffff1660e01b8152600401808473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1681526020018373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1681526020018281526020019350505050600060405180830381600087803b1580156105b057600080fd5b505af11580156105c4573d6000803e3d6000fd5b505050505961012081016040526020815260e0602082015260e0600060408301376024356004353360003560e01c60e01b61012085a45050565b60016020528060005260406000206000915090505481565b60075481565b60016000803373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff168152602001908152602001600020541461066757600080fd5b7f647372000000000000000000000000000000000000000000000000000000000082141561069757806003819055505b5961012081016040526020815260e0602082015260e0600060408301376024356004353360003560e01c60e01b61012085a4505050565b60025481565b600560009054906101000a900473ffffffffffffffffffffffffffffffffffffffff1681565b60035481565b600660009054906101000a900473ffffffffffffffffffffffffffffffffffffffff1681565b60016000803373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff168152602001908152602001600020541461077157600080fd5b60016000808373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff168152602001908152602001600020819055505961012081016040526020815260e0602082015260e0600060408301376024356004353360003560e01c60e01b61012085a45050565b610834600160003373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1681526020019081526020016000205482610d8b565b600160003373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1681526020019081526020016000208190555061088360025482610d8b565b600281905550600560009054906101000a900473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1663bb35783b30336108d560045486610d5f565b6040518463ffffffff1660e01b8152600401808473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1681526020018373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1681526020018281526020019350505050600060405180830381600087803b15801561097157600080fd5b505af1158015610985573d6000803e3d6000fd5b505050505961012081016040526020815260e0602082015260e0600060408301376024356004353360003560e01c60e01b61012085a45050565b60016000803373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1681526020019081526020016000205414610a0a57600080fd5b60008060008373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff168152602001908152602001600020819055505961012081016040526020815260e0602082015260e0600060408301376024356004353360003560e01c60e01b61012085a45050565b600754421015610a9357600080fd5b6000610ac8610ac0610ab860035460075442036b033b2e3c9fd0803ce8000000610da5565b600454610e6b565b600454610d8b565b9050610ad660045482610d45565b60048190555042600781905550600560009054906101000a900473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1663f24e23eb600660009054906101000a900473ffffffffffffffffffffffffffffffffffffffff1630610b5160025486610d5f565b6040518463ffffffff1660e01b8152600401808473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1681526020018373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1681526020018281526020019350505050600060405180830381600087803b158015610bed57600080fd5b505af1158015610c01573d6000803e3d6000fd5b50505050505961012081016040526020815260e0602082015260e0600060408301376024356004353360003560e01c60e01b61012085a450565b60006020528060005260406000206000915090505481565b60045481565b60016000803373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1681526020019081526020016000205414610ca457600080fd5b7f766f770000000000000000000000000000000000000000000000000000000000821415610d0e5780600660006101000a81548173ffffffffffffffffffffffffffffffffffffffff021916908373ffffffffffffffffffffffffffffffffffffffff1602179055505b5961012081016040526020815260e0602082015260e0600060408301376024356004353360003560e01c60e01b61012085a4505050565b6000828284019150811015610d5957600080fd5b92915050565b600080821480610d7c5750828283850292508281610d7957fe5b04145b610d8557600080fd5b92915050565b6000828284039150811115610d9f57600080fd5b92915050565b60008360008114610e4b576002840660008114610dc457859250610dc8565b8392505b50600283046002850494505b8415610e45578586028687820414610deb57600080fd5b81810181811015610dfb57600080fd5b85810497506002870615610e38578785028589820414158915151615610e2057600080fd5b83810181811015610e3057600080fd5b878104965050505b5050600285049450610dd4565b50610e63565b8360008114610e5d5760009250610e61565b8392505b505b509392505050565b60006b033b2e3c9fd0803ce8000000610e848484610d5f565b81610e8b57fe5b0490509291505056fea265627a7a723058200d0f28f3e2fe83bf3db10418bb2fb854157eef54ce68904167437e4746b2f2ee64736f6c63430005090032
Current (failing) Pot bytecode: 0x608060405234801561001057600080fd5b506004361061010b5760003560e01c806365fae35e116100a25780639c52a7f1116100715780639c52a7f1146103565780639f678cca1461039a578063bf353dbb146103b8578063c92aecc414610410578063d4e8be831461042e5761010b565b806365fae35e146102bc57806369245009146103005780637f8661a11461030a578063957aa58c146103385761010b565b80632c69ed58116100de5780632c69ed58146101ec57806336569e771461020a578063487bf08214610254578063626cb3c5146102725761010b565b8063049878f3146101105780630bebac861461013e57806320aba08b1461019657806329ae8114146101b4575b600080fd5b61013c6004803603602081101561012657600080fd5b810190808035906020019092919050505061047c565b005b6101806004803603602081101561015457600080fd5b81019080803573ffffffffffffffffffffffffffffffffffffffff1690602001909291905050506106c7565b6040518082815260200191505060405180910390f35b61019e6106df565b6040518082815260200191505060405180910390f35b6101ea600480360360408110156101ca57600080fd5b8101908080359060200190929190803590602001909291905050506106e5565b005b6101f4610961565b6040518082815260200191505060405180910390f35b610212610967565b604051808273ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200191505060405180910390f35b61025c61098d565b6040518082815260200191505060405180910390f35b61027a610993565b604051808273ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200191505060405180910390f35b6102fe600480360360208110156102d257600080fd5b81019080803573ffffffffffffffffffffffffffffffffffffffff1690602001909291905050506109b9565b005b610308610ae7565b005b6103366004803603602081101561032057600080fd5b8101908080359060200190929190505050610beb565b005b610340610dbf565b6040518082815260200191505060405180910390f35b6103986004803603602081101561036c57600080fd5b81019080803573ffffffffffffffffffffffffffffffffffffffff169060200190929190505050610dc5565b005b6103a2610ef3565b6040518082815260200191505060405180910390f35b6103fa600480360360208110156103ce57600080fd5b81019080803573ffffffffffffffffffffffffffffffffffffffff16906020019092919050505061110e565b6040518082815260200191505060405180910390f35b610418611126565b6040518082815260200191505060405180910390f35b61047a6004803603604081101561044457600080fd5b8101908080359060200190929190803573ffffffffffffffffffffffffffffffffffffffff16906020019092919050505061112c565b005b60075442146104f3576040517f08c379a00000000000000000000000000000000000000000000000000000000081526004018080602001828103825260138152602001807f506f742f72686f2d6e6f742d757064617465640000000000000000000000000081525060200191505060405180910390fd5b61053c600160003373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200190815260200160002054826112f3565b600160003373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1681526020019081526020016000208190555061058b600254826112f3565b600281905550600560009054906101000a900473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1663bb35783b33306105dd6004548661130d565b6040518463ffffffff1660e01b8152600401808473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1681526020018373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1681526020018281526020019350505050600060405180830381600087803b15801561067957600080fd5b505af115801561068d573d6000803e3d6000fd5b505050505961012081016040526020815260e0602082015260e0600060408301376024356004353360003560e01c60e01b61012085a45050565b60016020528060005260406000206000915090505481565b60075481565b60016000803373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1681526020019081526020016000205414610799576040517f08c379a00000000000000000000000000000000000000000000000000000000081526004018080602001828103825260128152602001807f506f742f6e6f742d617574686f72697a6564000000000000000000000000000081525060200191505060405180910390fd5b600160085414610811576040517f08c379a000000000000000000000000000000000000000000000000000000000815260040180806020018281038252600c8152602001807f506f742f6e6f742d6c697665000000000000000000000000000000000000000081525060200191505060405180910390fd5b6007544214610888576040517f08c379a00000000000000000000000000000000000000000000000000000000081526004018080602001828103825260138152602001807f506f742f72686f2d6e6f742d757064617465640000000000000000000000000081525060200191505060405180910390fd5b7f64737200000000000000000000000000000000000000000000000000000000008214156108bc578060038190555061092a565b6040517f08c379a000000000000000000000000000000000000000000000000000000000815260040180806020018281038252601b8152602001807f506f742f66696c652d756e7265636f676e697a65642d706172616d000000000081525060200191505060405180910390fd5b5961012081016040526020815260e0602082015260e0600060408301376024356004353360003560e01c60e01b61012085a4505050565b60025481565b600560009054906101000a900473ffffffffffffffffffffffffffffffffffffffff1681565b60035481565b600660009054906101000a900473ffffffffffffffffffffffffffffffffffffffff1681565b60016000803373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1681526020019081526020016000205414610a6d576040517f08c379a00000000000000000000000000000000000000000000000000000000081526004018080602001828103825260128152602001807f506f742f6e6f742d617574686f72697a6564000000000000000000000000000081525060200191505060405180910390fd5b60016000808373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff168152602001908152602001600020819055505961012081016040526020815260e0602082015260e0600060408301376024356004353360003560e01c60e01b61012085a45050565b60016000803373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1681526020019081526020016000205414610b9b576040517f08c379a00000000000000000000000000000000000000000000000000000000081526004018080602001828103825260128152602001807f506f742f6e6f742d617574686f72697a6564000000000000000000000000000081525060200191505060405180910390fd5b60006008819055506b033b2e3c9fd0803ce80000006003819055505961012081016040526020815260e0602082015260e0600060408301376024356004353360003560e01c60e01b61012085a450565b610c34600160003373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1681526020019081526020016000205482611339565b600160003373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200190815260200160002081905550610c8360025482611339565b600281905550600560009054906101000a900473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1663bb35783b3033610cd56004548661130d565b6040518463ffffffff1660e01b8152600401808473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1681526020018373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1681526020018281526020019350505050600060405180830381600087803b158015610d7157600080fd5b505af1158015610d85573d6000803e3d6000fd5b505050505961012081016040526020815260e0602082015260e0600060408301376024356004353360003560e01c60e01b61012085a45050565b60085481565b60016000803373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1681526020019081526020016000205414610e79576040517f08c379a00000000000000000000000000000000000000000000000000000000081526004018080602001828103825260128152602001807f506f742f6e6f742d617574686f72697a6564000000000000000000000000000081525060200191505060405180910390fd5b60008060008373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff168152602001908152602001600020819055505961012081016040526020815260e0602082015260e0600060408301376024356004353360003560e01c60e01b61012085a45050565b6000600754421015610f6d576040517f08c379a000000000000000000000000000000000000000000000000000000000815260040180806020018281038252600f8152602001807f506f742f696e76616c69642d6e6f77000000000000000000000000000000000081525060200191505060405180910390fd5b610f95610f8d60035460075442036b033b2e3c9fd0803ce8000000611353565b600454611419565b90506000610fa582600454611339565b90508160048190555042600781905550600560009054906101000a900473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1663f24e23eb600660009054906101000a900473ffffffffffffffffffffffffffffffffffffffff16306110236002548661130d565b6040518463ffffffff1660e01b8152600401808473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1681526020018373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1681526020018281526020019350505050600060405180830381600087803b1580156110bf57600080fd5b505af11580156110d3573d6000803e3d6000fd5b50505050505961012081016040526020815260e0602082015260e0600060408301376024356004353360003560e01c60e01b61012085a45090565b60006020528060005260406000206000915090505481565b60045481565b60016000803373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200190815260200160002054146111e0576040517f08c379a00000000000000000000000000000000000000000000000000000000081526004018080602001828103825260128152602001807f506f742f6e6f742d617574686f72697a6564000000000000000000000000000081525060200191505060405180910390fd5b7f766f77000000000000000000000000000000000000000000000000000000000082141561124e5780600660006101000a81548173ffffffffffffffffffffffffffffffffffffffff021916908373ffffffffffffffffffffffffffffffffffffffff1602179055506112bc565b6040517f08c379a000000000000000000000000000000000000000000000000000000000815260040180806020018281038252601b8152602001807f506f742f66696c652d756e7265636f676e697a65642d706172616d000000000081525060200191505060405180910390fd5b5961012081016040526020815260e0602082015260e0600060408301376024356004353360003560e01c60e01b61012085a4505050565b600082828401915081101561130757600080fd5b92915050565b60008082148061132a575082828385029250828161132757fe5b04145b61133357600080fd5b92915050565b600082828403915081111561134d57600080fd5b92915050565b600083600081146113f957600284066000811461137257859250611376565b8392505b50600283046002850494505b84156113f357858602868782041461139957600080fd5b818101818110156113a957600080fd5b858104975060028706156113e65787850285898204141589151516156113ce57600080fd5b838101818110156113de57600080fd5b878104965050505b5050600285049450611382565b50611411565b836000811461140b576000925061140f565b8392505b505b509392505050565b60006b033b2e3c9fd0803ce8000000611432848461130d565b8161143957fe5b0490509291505056fea265627a7a7231582081eb75c1aefafc732ccf1dedb24c8a4616012d610da18eefbc3b92cb3b71830464736f6c634300050c0032
36d6fef8d451cbc67480ab5d4e13fb99.json
{"format":"KAST","version":1,"term":{"node":"KRewrite","lhs":{"node":"KApply","label":"","variable":false,"arity":5,"args":[{"node":"KApply","label":"","variable":false,"arity":1,"args":[{"node":"KApply","label":"#KSequence","variable":false,"arity":2,"args":[{"node":"KApply","label":"____EVM","variable":false,"arity":3,"args":[{"node":"KApply","label":"EQ_EVM","variable":false,"arity":0,"args":[]},{"node":"KVariable","name":"W0","originalName":"W0"},{"node":"KVariable","name":"W1","originalName":"W1"}]},{"node":"KVariable","name":"DotVar1","originalName":"DotVar1"}]}]},{"node":"KVariable","name":"_0","originalName":"_0"},{"node":"KVariable","name":"_1","originalName":"_1"},{"node":"KVariable","name":"_2","originalName":"_2"},{"node":"KVariable","name":"3","originalName":"3"}]},"rhs":{"node":"KApply","label":"","variable":false,"arity":5,"args":[{"node":"KApply","label":"","variable":false,"arity":1,"args":[{"node":"KApply","label":"#KSequence","variable":false,"arity":2,"args":[{"node":"KApply","label":"bool2Word","variable":false,"arity":1,"args":[{"node":"KApply","label":"==K","variable":false,"arity":2,"args":[{"node":"KVariable","name":"W0","originalName":"W0"},{"node":"KVariable","name":"W1","originalName":"W1"}]}]},{"node":"KApply","label":"#KSequence","variable":false,"arity":2,"args":[{"node":"KApply","label":"#push_EVM","variable":false,"arity":0,"args":[]},{"node":"KVariable","name":"DotVar1","originalName":"DotVar1"}]}]}]},{"node":"KVariable","name":"_0","originalName":"_0"},{"node":"KVariable","name":"_1","originalName":"_1"},{"node":"KVariable","name":"_2","originalName":"_2"},{"node":"KVariable","name":"_3","originalName":"_3"}]},"att":"[contentStartColumn(8) contentStartLine(508) org.kframework.attributes.Location(Location(508,8,508,64)) org.kframework.attributes.Source(Source(/home/kurt/makerdao/k-dss/out/rules.k)) org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions) symbol()]) specification() trusted()]"}}