Skip to content

Commit

Permalink
dexter: fix unused variable warnings
Browse files Browse the repository at this point in the history
  • Loading branch information
@sskeirik
sskeirik committed Aug 4, 2021
1 parent 24b97b8 commit 5194d31
Showing 1 changed file with 36 additions and 33 deletions.
69 changes: 36 additions & 33 deletions tests/proofs/dexter/dexter-spec.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -170,7 +170,7 @@ module DEXTER-ADDLIQUIDITY-NEGATIVE-SPEC
<tokenPool> TokenAmount </tokenPool>
<currentContract> DexterAddress </currentContract>
<contracts>
<contract> <address> DexterAddress </address> <entrypoints> DexterEntrypoints </entrypoints> ... </contract>
<contract> <address> DexterAddress </address> <entrypoints> _DexterEntrypoints </entrypoints> ... </contract>
</contracts>
requires notBool IsFA2
andBool ( IsUpdating
Expand All @@ -191,7 +191,7 @@ module DEXTER-ADDLIQUIDITY-NEGATIVE-SPEC
<tokenPool> TokenAmount </tokenPool>
<currentContract> DexterAddress </currentContract>
<contracts>
<contract> <address> DexterAddress </address> <entrypoints> DexterEntrypoints </entrypoints> ... </contract>
<contract> <address> DexterAddress </address> <entrypoints> _DexterEntrypoints </entrypoints> ... </contract>
</contracts>
requires IsFA2
andBool ( IsUpdating
Expand Down Expand Up @@ -244,6 +244,7 @@ module DEXTER-REMOVELIQUIDITY-POSITIVE-SPEC
<contract> <address> DexterAddress </address> <entrypoints> DexterEntrypoints </entrypoints> ... </contract>
<contract> <address> TokenAddress </address> <entrypoints> TokenEntrypoints </entrypoints> ... </contract>
<contract> <address> LqtAddress </address> <entrypoints> LqtEntrypoints </entrypoints> ... </contract>
<contract> <address> To </address> <entrypoints> ToEntrypoints </entrypoints> ... </contract>
</contracts>
<operations> _
=> [ Transfer_tokens (Pair (0 -Int LqtBurned) Sender) #Mutez(0) LqtAddress . %mintOrBurn Nonce ] ;;
Expand Down Expand Up @@ -282,15 +283,15 @@ module DEXTER-REMOVELIQUIDITY-NEGATIVE-SPEC
<selfIsUpdatingTokenPool> true </selfIsUpdatingTokenPool>
<currentContract> DexterAddress </currentContract>
<contracts>
<contract> <address> DexterAddress </address> <entrypoints> DexterEntrypoints </entrypoints> ... </contract>
<contract> <address> DexterAddress </address> <entrypoints> _DexterEntrypoints </entrypoints> ... </contract>
</contracts>
claim <k> #runProof(_IsFA2, RemoveLiquidity(_, _, _, _, _)) => Aborted(?_, ?_, ?_, ?_) </k>
<stack> .Stack => ( Failed ?_ ) </stack>
<myamount> #Mutez(Amount) </myamount>
<currentContract> DexterAddress </currentContract>
<contracts>
<contract> <address> DexterAddress </address> <entrypoints> DexterEntrypoints </entrypoints> ... </contract>
<contract> <address> DexterAddress </address> <entrypoints> _DexterEntrypoints </entrypoints> ... </contract>
</contracts>
requires Amount >Int 0
Expand All @@ -299,7 +300,7 @@ module DEXTER-REMOVELIQUIDITY-NEGATIVE-SPEC
<mynow> #Timestamp(CurrentTime) </mynow>
<currentContract> DexterAddress </currentContract>
<contracts>
<contract> <address> DexterAddress </address> <entrypoints> DexterEntrypoints </entrypoints> ... </contract>
<contract> <address> DexterAddress </address> <entrypoints> _DexterEntrypoints </entrypoints> ... </contract>
</contracts>
requires CurrentTime >=Int Deadline
Expand All @@ -308,7 +309,7 @@ module DEXTER-REMOVELIQUIDITY-NEGATIVE-SPEC
<lqtTotal> OldLqt </lqtTotal>
<currentContract> DexterAddress </currentContract>
<contracts>
<contract> <address> DexterAddress </address> <entrypoints> DexterEntrypoints </entrypoints> ... </contract>
<contract> <address> DexterAddress </address> <entrypoints> _DexterEntrypoints </entrypoints> ... </contract>
</contracts>
requires OldLqt ==Int 0
orBool OldLqt <Int LqtBurned
Expand All @@ -319,7 +320,7 @@ module DEXTER-REMOVELIQUIDITY-NEGATIVE-SPEC
<xtzPool> #Mutez(XtzAmount) </xtzPool>
<currentContract> DexterAddress </currentContract>
<contracts>
<contract> <address> DexterAddress </address> <entrypoints> DexterEntrypoints </entrypoints> ... </contract>
<contract> <address> DexterAddress </address> <entrypoints> _DexterEntrypoints </entrypoints> ... </contract>
</contracts>
requires MinXtzWithdrawn >Int (LqtBurned *Int XtzAmount) /Int OldLqt
Expand Down Expand Up @@ -348,7 +349,7 @@ The contract sets its manager to the provided manager address if the following c
<senderaddr> Sender </senderaddr>
<currentContract> DexterAddress </currentContract>
<contracts>
<contract> <address> DexterAddress </address> <entrypoints> DexterEntrypoints </entrypoints> ... </contract>
<contract> <address> DexterAddress </address> <entrypoints> _DexterEntrypoints </entrypoints> ... </contract>
</contracts>
requires Amount ==Int 0
```
Expand All @@ -364,7 +365,7 @@ If any of the conditions are not satisfied, the call fails.
<senderaddr> Sender </senderaddr>
<currentContract> DexterAddress </currentContract>
<contracts>
<contract> <address> DexterAddress </address> <entrypoints> DexterEntrypoints </entrypoints> ... </contract>
<contract> <address> DexterAddress </address> <entrypoints> _DexterEntrypoints </entrypoints> ... </contract>
</contracts>
requires Amount >Int 0
orBool Sender =/=K CurrentManager
Expand Down Expand Up @@ -400,7 +401,7 @@ The contract sets its delegate to the value of `baker` (and optionally freezes t
<nonce> #Nonce(N => N +Int 1) </nonce>
<currentContract> DexterAddress </currentContract>
<contracts>
<contract> <address> DexterAddress </address> <entrypoints> DexterEntrypoints </entrypoints> ... </contract>
<contract> <address> DexterAddress </address> <entrypoints> _DexterEntrypoints </entrypoints> ... </contract>
</contracts>
<operations> _ => [ Set_delegate Baker N:Int ] ;; .InternalList </operations>
requires Amount ==Int 0
Expand All @@ -418,7 +419,7 @@ If any of the conditions are not satisfied, the call fails.
<freezeBaker> FreezeBaker </freezeBaker>
<currentContract> DexterAddress </currentContract>
<contracts>
<contract> <address> DexterAddress </address> <entrypoints> DexterEntrypoints </entrypoints> ... </contract>
<contract> <address> DexterAddress </address> <entrypoints> _DexterEntrypoints </entrypoints> ... </contract>
</contracts>
requires Amount >Int 0
orBool IsUpdating
Expand Down Expand Up @@ -454,7 +455,7 @@ The contract sets its liquidity pool adddress to the provided address if the fol
<lqtAddress> LQTAddress => NewLQTAddress </lqtAddress>
<currentContract> DexterAddress </currentContract>
<contracts>
<contract> <address> DexterAddress </address> <entrypoints> DexterEntrypoints </entrypoints> ... </contract>
<contract> <address> DexterAddress </address> <entrypoints> _DexterEntrypoints </entrypoints> ... </contract>
</contracts>
requires Amount ==Int 0
andBool LQTAddress ==K #Address("tz1Ke2h7sDdakHJQh8WX4Z372du1KChsksyU")
Expand All @@ -472,7 +473,7 @@ If any of the conditions are not satisfied, the call fails.
<lqtAddress> LQTAddress </lqtAddress>
<currentContract> DexterAddress </currentContract>
<contracts>
<contract> <address> DexterAddress </address> <entrypoints> DexterEntrypoints </entrypoints> ... </contract>
<contract> <address> DexterAddress </address> <entrypoints> _DexterEntrypoints </entrypoints> ... </contract>
</contracts>
requires Amount >Int 0
orBool IsUpdating
Expand Down Expand Up @@ -539,6 +540,7 @@ NOTE: The failure conditions are split into two claims with identical configurat
<currentContract> DexterAddress </currentContract>
<contracts>
<contract> <address> DexterAddress </address> <entrypoints> DexterEntrypoints </entrypoints> ... </contract>
<contract> <address> TokenAddress </address> <entrypoints> TokenEntrypoints </entrypoints> ... </contract>
</contracts>
requires ( Amount >Int 0
orBool (notBool #EntrypointExists(TokenEntrypoints, #if IsFA2 #then %balance_of #else %getBalance #fi, #TokenBalanceEntrypointType(IsFA2)))
Expand All @@ -547,6 +549,7 @@ NOTE: The failure conditions are split into two claims with identical configurat
)
andBool #EntrypointExists(DexterEntrypoints, %updateTokenPoolInternal, #Type(#DexterVersionSpecificParamType(IsFA2)))
andBool #EntrypointExists(DexterEntrypoints, %default, unit)
andBool #EntrypointExists(TokenEntrypoints, #if IsFA2 #then %balance_of #else %getBalance #fi, #TokenBalanceEntrypointType(IsFA2))
```

```k
Expand All @@ -573,7 +576,7 @@ Adds more money to the xtz reserves if the following conditions are satisifed:
<xtzPool> #Mutez(XtzPool => XtzPool +Int Amount) </xtzPool>
<currentContract> DexterAddress </currentContract>
<contracts>
<contract> <address> DexterAddress </address> <entrypoints> DexterEntrypoints </entrypoints> ... </contract>
<contract> <address> DexterAddress </address> <entrypoints> _DexterEntrypoints </entrypoints> ... </contract>
</contracts>
requires #IsLegalMutezValue(XtzPool +Int Amount)
```
Expand All @@ -588,7 +591,7 @@ If any of the conditions are not satisfied, the call fails.
<xtzPool> #Mutez(XtzPool) </xtzPool>
<currentContract> DexterAddress </currentContract>
<contracts>
<contract> <address> DexterAddress </address> <entrypoints> DexterEntrypoints </entrypoints> ... </contract>
<contract> <address> DexterAddress </address> <entrypoints> _DexterEntrypoints </entrypoints> ... </contract>
</contracts>
requires IsUpdating
orBool notBool #IsLegalMutezValue(XtzPool +Int Amount)
Expand Down Expand Up @@ -622,7 +625,7 @@ Summary: The underlying token contract updates the Dexter contract's view of its
<senderaddr> TokenAddress </senderaddr>
<currentContract> DexterAddress </currentContract>
<contracts>
<contract> <address> DexterAddress </address> <entrypoints> DexterEntrypoints </entrypoints> ... </contract>
<contract> <address> DexterAddress </address> <entrypoints> _DexterEntrypoints </entrypoints> ... </contract>
</contracts>
```

Expand All @@ -638,7 +641,7 @@ In the FA2, UpdateTokenPoolInternal ignores all balances additional balances pas
<senderaddr> TokenAddress </senderaddr>
<currentContract> DexterAddress </currentContract>
<contracts>
<contract> <address> DexterAddress </address> <entrypoints> DexterEntrypoints </entrypoints> ... </contract>
<contract> <address> DexterAddress </address> <entrypoints> _DexterEntrypoints </entrypoints> ... </contract>
</contracts>
```

Expand Down Expand Up @@ -667,7 +670,7 @@ The following claims cover these cases:
<senderaddr> Sender </senderaddr>
<currentContract> DexterAddress </currentContract>
<contracts>
<contract> <address> DexterAddress </address> <entrypoints> DexterEntrypoints </entrypoints> ... </contract>
<contract> <address> DexterAddress </address> <entrypoints> _DexterEntrypoints </entrypoints> ... </contract>
</contracts>
requires Amount >Int 0
andBool IsUpdating
Expand All @@ -683,7 +686,7 @@ The following claims cover these cases:
<senderaddr> _Sender </senderaddr>
<currentContract> DexterAddress </currentContract>
<contracts>
<contract> <address> DexterAddress </address> <entrypoints> DexterEntrypoints </entrypoints> ... </contract>
<contract> <address> DexterAddress </address> <entrypoints> _DexterEntrypoints </entrypoints> ... </contract>
</contracts>
requires (notBool IsUpdating)
```
Expand All @@ -697,7 +700,7 @@ The following claims cover these cases:
<senderaddr> Sender </senderaddr>
<currentContract> DexterAddress </currentContract>
<contracts>
<contract> <address> DexterAddress </address> <entrypoints> DexterEntrypoints </entrypoints> ... </contract>
<contract> <address> DexterAddress </address> <entrypoints> _DexterEntrypoints </entrypoints> ... </contract>
</contracts>
requires TokenAddress =/=K Sender
```
Expand All @@ -723,7 +726,7 @@ The following claims cover these cases:
<senderaddr> #Address(_Sender) </senderaddr>
<currentContract> DexterAddress </currentContract>
<contracts>
<contract> <address> DexterAddress </address> <entrypoints> DexterEntrypoints </entrypoints> ... </contract>
<contract> <address> DexterAddress </address> <entrypoints> _DexterEntrypoints </entrypoints> ... </contract>
</contracts>
requires (notBool IsUpdating)
```
Expand All @@ -737,7 +740,7 @@ The following claims cover these cases:
<senderaddr> #Address(Sender) </senderaddr>
<currentContract> DexterAddress </currentContract>
<contracts>
<contract> <address> DexterAddress </address> <entrypoints> DexterEntrypoints </entrypoints> ... </contract>
<contract> <address> DexterAddress </address> <entrypoints> _DexterEntrypoints </entrypoints> ... </contract>
</contracts>
requires TokenAddress =/=K Sender
```
Expand All @@ -751,7 +754,7 @@ The following claims cover these cases:
<senderaddr> #Address(Sender) </senderaddr>
<currentContract> DexterAddress </currentContract>
<contracts>
<contract> <address> DexterAddress </address> <entrypoints> DexterEntrypoints </entrypoints> ... </contract>
<contract> <address> DexterAddress </address> <entrypoints> _DexterEntrypoints </entrypoints> ... </contract>
</contracts>
requires TokenAddress ==K Sender
andBool BalanceOfResult ==K .InternalList
Expand All @@ -766,7 +769,7 @@ The following claims cover these cases:
<senderaddr> #Address(Sender) </senderaddr>
<currentContract> DexterAddress </currentContract>
<contracts>
<contract> <address> DexterAddress </address> <entrypoints> DexterEntrypoints </entrypoints> ... </contract>
<contract> <address> DexterAddress </address> <entrypoints> _DexterEntrypoints </entrypoints> ... </contract>
</contracts>
requires Amount >Int 0
andBool IsUpdating
Expand Down Expand Up @@ -841,17 +844,17 @@ The following claims prove the negative case:
```k
module DEXTER-TOKENTOXTZ-FA12-NEGATIVE-1-SPEC
imports DEXTER-VERIFICATION
claim <k> #runProof(IsFA2, TokenToXtz(_To, _TokensSold, #Mutez(_MinXtzBought), #Timestamp(Deadline))) => Aborted(?_, ?_, ?_, ?_) </k>
claim <k> #runProof(IsFA2, TokenToXtz(To, _TokensSold, #Mutez(_MinXtzBought), #Timestamp(Deadline))) => Aborted(?_, ?_, ?_, ?_) </k>
<stack> .Stack => ?_:FailedStack </stack>
<selfIsUpdatingTokenPool> IsUpdating </selfIsUpdatingTokenPool>
<mynow> #Timestamp(CurrentTime) </mynow>
<myamount> #Mutez(Amount) </myamount>
<tokenAddress> _TokenAddress:Address </tokenAddress>
<tokenAddress> TokenAddress:Address </tokenAddress>
<currentContract> DexterAddress </currentContract>
<contracts>
<contract> <address> DexterAddress </address> <entrypoints> DexterEntrypoints </entrypoints> ... </contract>
<contract> <address> TokenAddress </address> <entrypoints> TokenEntrypoints </entrypoints> ... </contract>
<contract> <address> To </address> <entrypoints> ToEntrypoints </entrypoints> ... </contract>
<contract> <address> DexterAddress </address> <entrypoints> _DexterEntrypoints </entrypoints> ... </contract>
<contract> <address> TokenAddress </address> <entrypoints> _TokenEntrypoints </entrypoints> ... </contract>
<contract> <address> To </address> <entrypoints> _ToEntrypoints </entrypoints> ... </contract>
</contracts>
requires notBool IsFA2
andBool ( IsUpdating
Expand Down Expand Up @@ -1290,7 +1293,7 @@ A buyer sends tokens to the Dexter contract, converts its to xtz, and then immed
<contracts>
<contract> <address> DexterAddress </address> <entrypoints> DexterEntrypoints </entrypoints> ... </contract>
<contract> <address> TokenAddress </address> <entrypoints> TokenEntrypoints </entrypoints> ... </contract>
<contract> <address> OutputDexterContract </address> <entrypoints> OuptutDexterEntrypoints </entrypoints> ... </contract>
<contract> <address> OutputDexterContract </address> <entrypoints> OutputDexterEntrypoints </entrypoints> ... </contract>
</contracts>
<operations> _
=> [ Transfer_tokens #TokenTransferData(IsFA2, Sender, DexterAddress, TokenID, TokensSold) #Mutez(0) TokenAddress . %transfer N ]
Expand Down Expand Up @@ -1326,7 +1329,7 @@ A buyer sends tokens to the Dexter contract, converts its to xtz, and then immed
<contracts>
<contract> <address> DexterAddress </address> <entrypoints> DexterEntrypoints </entrypoints> ... </contract>
<contract> <address> TokenAddress </address> <entrypoints> TokenEntrypoints </entrypoints> ... </contract>
<contract> <address> OutputDexterContract </address> <entrypoints> OuptutDexterEntrypoints </entrypoints> ... </contract>
<contract> <address> OutputDexterContract </address> <entrypoints> OutputDexterEntrypoints </entrypoints> ... </contract>
</contracts>
<operations> _
=> [ Transfer_tokens #TokenTransferData(IsFA2, Sender, DexterAddress, TokenID, TokensSold) #Mutez(0) TokenAddress . %transfer N ]
Expand Down Expand Up @@ -1373,7 +1376,7 @@ module DEXTER-TOKENTOTOKEN-NEGATIVE-SPEC
<contracts>
<contract> <address> DexterAddress </address> <entrypoints> DexterEntrypoints </entrypoints> ... </contract>
<contract> <address> TokenAddress </address> <entrypoints> TokenEntrypoints </entrypoints> ... </contract>
<contract> <address> OutputDexterContract </address> <entrypoints> OuptutDexterEntrypoints </entrypoints> ... </contract>
<contract> <address> OutputDexterContract </address> <entrypoints> OutputDexterEntrypoints </entrypoints> ... </contract>
</contracts>
<operations> _ </operations>
requires notBool IsFA2
Expand Down Expand Up @@ -1408,7 +1411,7 @@ module DEXTER-TOKENTOTOKEN-NEGATIVE-SPEC
<contracts>
<contract> <address> DexterAddress </address> <entrypoints> DexterEntrypoints </entrypoints> ... </contract>
<contract> <address> TokenAddress </address> <entrypoints> TokenEntrypoints </entrypoints> ... </contract>
<contract> <address> OutputDexterContract </address> <entrypoints> OuptutDexterEntrypoints </entrypoints> ... </contract>
<contract> <address> OutputDexterContract </address> <entrypoints> OutputDexterEntrypoints </entrypoints> ... </contract>
</contracts>
<operations> _ </operations>
requires IsFA2
Expand Down

0 comments on commit 5194d31

Please sign in to comment.