search

Pi-Squared-Inc / solidity-demo-semantics

Demonstration Solidity Semantics in K
2 stars 2 forks source link

performed modifications after adding sqrt computation #26

Closed ovatman closed 2 months ago

ovatman commented 2 months ago

Changes include:

dwightguth commented 2 months ago

I will happily investigate the failures in the semantics if there are any, but now that we have a working version of the semantics on one version of the contract, changes to the contract need to only go through if they don't break the semantics.

dwightguth commented 2 months ago

Also, just fyi, auto formatting a file in the same PR that you make other modifications to that file is a bad idea; it makes it vastly more difficult to review the code.

mariaKt commented 2 months ago

I tried this version of Uniswap locally, and it does not run. It fails insetUp (https://github.com/Pi-Squared-Inc/solidity-demo-semantics/blob/ca576a1fbbd9a7285831d16a1c08140f510a6e2e/test/examples/swaps/UniswapV2Swap.sol#L673). Looking very briefly, it seems that is attempts to create a UniswapV2Swap using two different constructors. https://github.com/Pi-Squared-Inc/solidity-demo-semantics/blob/ca576a1fbbd9a7285831d16a1c08140f510a6e2e/test/examples/swaps/UniswapV2Swap.sol#L677 and https://github.com/Pi-Squared-Inc/solidity-demo-semantics/blob/ca576a1fbbd9a7285831d16a1c08140f510a6e2e/test/examples/swaps/UniswapV2Swap.sol#L689 Only the one with 3 parameters exists though.

ovatman commented 2 months ago

@mariaKt I have addressed the issue below; Uniswap is compiling now.

I tried this version of Uniswap locally, and it does not run. It fails insetUp (

https://github.com/Pi-Squared-Inc/solidity-demo-semantics/blob/ca576a1fbbd9a7285831d16a1c08140f510a6e2e/test/examples/swaps/UniswapV2Swap.sol#L673 ). Looking very briefly, it seems that is attempts to create a UniswapV2Swap using two different constructors.

https://github.com/Pi-Squared-Inc/solidity-demo-semantics/blob/ca576a1fbbd9a7285831d16a1c08140f510a6e2e/test/examples/swaps/UniswapV2Swap.sol#L677

and

https://github.com/Pi-Squared-Inc/solidity-demo-semantics/blob/ca576a1fbbd9a7285831d16a1c08140f510a6e2e/test/examples/swaps/UniswapV2Swap.sol#L689

Only the one with 3 parameters exists though.

ovatman commented 2 months ago

@dwightguth last commit performs this synchronization.

Please also make sure you are applying the same modifications to the version of the contract in test/regression/swaps.sol. The two files differ slightly, but we want to keep them enough in sync that they are running the same computations. Also, that version is the only version that is currently being regression tested.

ovatman commented 2 months ago

@dwightguth @mariaKt as far as I can see current state of semantics don't work well with the sqrt() related modifications. I believe it should be possible to keep the older version but still add sqrt() related functionality. However, I'm not certain how it will work with retesteth related stuff.

dwightguth commented 2 months ago

Can you show me what the change to the contract and the resulting stuck configuration were?

mariaKt commented 2 months ago

@dwightguth if you meant me: I made no changes to the contract, and simply added the transaction

txn(1, 2, 0, 1724300000, testRouterAddLiquidity, )

after the others (so it is similar to the UniswapTest.txn file in this PR). Here is the stuck configuration. conf.txt

ovatman commented 2 months ago

@dwightguth @mariaKt I went over the error and performed necessary modifications. krun progressed when I replaced integer literals in the addLiquidity() call with local variables keeping the same values.

I have also updated the reference output accordingly, I wasn't able to see any problems with the output reference please check if you can see anything odd.