Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Performative confessional condolences #48

Open
wants to merge 7 commits into
base: master
Choose a base branch
from
Open

Performative confessional condolences #48

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
7 commits
Select commit Hold shift + click to select a range
20d2c2e
flush dirty_lemmas.k.md
livnev Aug 23, 2019
0adf30d
dss.md: update cage-ilk to include par
livnev Sep 6, 2019
b467956
add live and cage() to Pot, add pot to End
livnev Sep 6, 2019
f4ca78f
dss.md: add rho check to Pot.join()
livnev Sep 6, 2019
bbd31ea
dss.md: at tick spec to Flopper
livnev Sep 6, 2019
201332f
src/dss.md: fix calls reference in Flopper.kick
livnev Sep 6, 2019
36a921a
dss: bump to latest master
livnev Sep 6, 2019
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion dss
Open in desktop
Submodule dss updated 7 files
+28 −15 src/end.sol
+5 −0 src/flop.sol
+0 −1 src/join.sol
+10 −0 src/pot.sol
+25 −0 src/test/end.t.sol
+53 −18 src/test/flop.t.sol
+32 −0 src/test/pot.t.sol
156 changes: 0 additions & 156 deletions src/dirty_lemmas.k.md
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,159 +1,3 @@
This is an example for rules that won't affect the proof hashes
this should be "flushed" once in a while to the real lemmas.k file

```k
rule WM[ N := #take(X, WS) ] => WM [ N := #asByteStackInWidth(#asWord(#take(X, WS)), X) ]

rule 0 -Word X => #unsigned(0 -Int X)
requires 0 <=Int X andBool X <=Int pow255
/*
proof:

1) rule W0 -Word W1 => chop( (W0 +Int pow256) -Int W1 ) requires W0 <Int W1
2) rule chop ( I:Int ) => I modInt pow256 [concrete, smt-lemma]
3) rule W0 -Word W1 => chop( W0 -Int W1 ) requires W0 >=Int W1

Assume X != 0:

0 < X : 0 -W X =(1)=> chop( pow256 - X )
0 < pow256 - X < pow256 : chop( pow256 - X ) =(2)=> pow256 - X

Assume X == 0:

0 == X : 0 -W 0 =(3)=> chop( 0 - 0 )
*/

rule #range(WS [ X := #padToWidth(32, Y) ], Z, 32, WSS) => #range(WS, Z, 32, WSS)
requires Z +Int 32 <Int X

// possibly wrong but i'll keep using it as a hack
rule #sizeWordStack(#range(WS, Y, Z, WSS), 0) => Z

//assume ecrec returns an address
rule maxUInt160 &Int #symEcrec(MSG, V, R, S) => #symEcrec(MSG, V, R, S)

rule 0 <=Int #symEcrec(MSG, V, R, S) => true
rule #symEcrec(MSG, V, R, S) <Int pow256 => true

rule A -Word B <=Int A => 0 <=Int A -Int B
requires #rangeUInt(256, A)
andBool #rangeUInt(256, B)

rule A <=Int chop(A +Int B) => A +Int B <=Int maxUInt256
requires #rangeUInt(256, A)
andBool #rangeUInt(256, B)

rule #sgnInterp(sgn(chop(A *Int #unsigned(B))) *Int -1, abs(chop(A *Int #unsigned(B))) /Int (pow256 -Int #unsigned(B))) ==K A => #rangeSInt(256, A *Int B)
requires #rangeUInt(256, A)
andBool #rangeSInt(256, B)
andBool B <Int 0

rule #sgnInterp(sgn(chop(A *Int #unsigned(B))), abs(chop(A *Int #unsigned(B))) /Int #unsigned(B)) ==K A => #rangeSInt(256, A *Int B)
requires #rangeUInt(256, A)
andBool #rangeSInt(256, B)
andBool 0 <Int B

// Lemmas for Vat_frob_fail
rule A +Int #unsigned(B) => A +Int B
requires #rangeUInt(256, A)
andBool #rangeUInt(256, B)
andBool #rangeUInt(256, A +Int B)

rule A +Int #unsigned(B) => A
requires B ==K 0

// lemma for Jug_drip
rule A -Word B => #unsigned(A -Int B)
requires #rangeSInt(256, A)
andBool #rangeSInt(256, B)
andBool 0 <=Int B
andBool 0 <=Int A

// lemmas for End_skim
rule (A +Int (0 -Int B)) => A -Int B
rule (A *Int (0 -Int B)) => (0 -Int (A *Int B))
rule (A -Int (0 -Int B)) => A +Int B
//lemmas for End_bail
rule (0 -Int A) <Int B => (0 -Int B) <Int A
requires (notBool #isConcrete(A))
andBool #isConcrete(B)
rule (0 -Int A) <=Int B => (0 -Int B) <=Int A
requires (notBool #isConcrete(A))
andBool #isConcrete(B)
rule A <=Int (0 -Int B) => B <=Int 0 -Int A
requires (notBool #isConcrete(B))
andBool #isConcrete(A)
rule A <Int (0 -Int B) => B <Int 0 -Int A
requires (notBool #isConcrete(B))
andBool #isConcrete(A)

// Lemmas dealing with stupid 0
rule (0 -Int X) *Int Y => 0 -Int (X *Int Y)
rule (0 -Int X) /Int Y => 0 -Int (X /Int Y)

rule #unsigned( X *Int Y ) /Int #unsigned( Y ) => X
requires #rangeSInt(256, X *Int Y)
andBool #rangeSInt(256, X)
andBool #rangeSInt(256, Y)
andBool 0 <=Int X
andBool 0 <Int Y

rule A +Int B => A
requires B ==K 0
andBool #isVariable(A)
andBool #isVariable(B)

rule A +Int B => B
requires A ==K 0
andBool #isVariable(A)
andBool #isVariable(B)

// lemma for Cat_bite-full to prevent unsigned(0 - X) devision
rule pow256 -Int #unsigned(0 -Int X) => X
requires X >Int 0


// lemma to deal with deep nested calls - gas stuff
rule X -Int (A1 +Int (A2 +Int (A3 +Int (A4 +Int (A5 +Int (A6 +Int (A7 +Int (A8 +Int (A9 +Int (A10 +Int (A11 +Int (A12 +Int (A13 +Int (A14 +Int (A15 +Int (A16 +Int (A17 +Int (X +Int AS)))))))))))))))))) => 0 -Int (A1 +Int (A2 +Int (A3 +Int (A4 +Int (A5 +Int (A6 +Int (A7 +Int (A8 +Int (A9 +Int (A10 +Int (A11 +Int (A12 +Int (A13 +Int (A14 +Int (A15 +Int (A16 +Int (A17 +Int AS)))))))))))))))))
rule X -Int (A1 +Int (A2 +Int (A3 +Int (A4 +Int (A5 +Int (A6 +Int (A7 +Int (A8 +Int (A9 +Int (A10 +Int (A11 +Int (A12 +Int (A13 +Int (A14 +Int (A15 +Int (A16 +Int (X +Int AS))))))))))))))))) => 0 -Int (A1 +Int (A2 +Int (A3 +Int (A4 +Int (A5 +Int (A6 +Int (A7 +Int (A8 +Int (A9 +Int (A10 +Int (A11 +Int (A12 +Int (A13 +Int (A14 +Int (A15 +Int (A16 +Int AS))))))))))))))))
rule X -Int (A1 +Int (A2 +Int (A3 +Int (A4 +Int (A5 +Int (A6 +Int (A7 +Int (A8 +Int (A9 +Int (A10 +Int (A11 +Int (A12 +Int (A13 +Int (A14 +Int (A15 +Int (X +Int AS)))))))))))))))) => 0 -Int (A1 +Int (A2 +Int (A3 +Int (A4 +Int (A5 +Int (A6 +Int (A7 +Int (A8 +Int (A9 +Int (A10 +Int (A11 +Int (A12 +Int (A13 +Int (A14 +Int (A15 +Int AS)))))))))))))))
rule X -Int (A1 +Int (A2 +Int (A3 +Int (A4 +Int (A5 +Int (A6 +Int (A7 +Int (A8 +Int (A9 +Int (A10 +Int (A11 +Int (A12 +Int (A13 +Int (A14 +Int (X +Int AS))))))))))))))) => 0 -Int (A1 +Int (A2 +Int (A3 +Int (A4 +Int (A5 +Int (A6 +Int (A7 +Int (A8 +Int (A9 +Int (A10 +Int (A11 +Int (A12 +Int (A13 +Int (A14 +Int AS))))))))))))))
rule X -Int (A1 +Int (A2 +Int (A3 +Int (A4 +Int (A5 +Int (A6 +Int (A7 +Int (A8 +Int (A9 +Int (A10 +Int (A11 +Int (A12 +Int (A13 +Int (X +Int AS)))))))))))))) => 0 -Int (A1 +Int (A2 +Int (A3 +Int (A4 +Int (A5 +Int (A6 +Int (A7 +Int (A8 +Int (A9 +Int (A10 +Int (A11 +Int (A12 +Int (A13 +Int AS)))))))))))))
rule X -Int (A1 +Int (A2 +Int (A3 +Int (A4 +Int (A5 +Int (A6 +Int (A7 +Int (A8 +Int (A9 +Int (A10 +Int (A11 +Int (A12 +Int (X +Int AS))))))))))))) => 0 -Int (A1 +Int (A2 +Int (A3 +Int (A4 +Int (A5 +Int (A6 +Int (A7 +Int (A8 +Int (A9 +Int (A10 +Int (A11 +Int (A12 +Int AS))))))))))))
rule X -Int (A1 +Int (A2 +Int (A3 +Int (A4 +Int (A5 +Int (A6 +Int (A7 +Int (A8 +Int (A9 +Int (A10 +Int (A11 +Int (X +Int AS)))))))))))) => 0 -Int (A1 +Int (A2 +Int (A3 +Int (A4 +Int (A5 +Int (A6 +Int (A7 +Int (A8 +Int (A9 +Int (A10 +Int (A11 +Int AS)))))))))))
rule X -Int (A1 +Int (A2 +Int (A3 +Int (A4 +Int (A5 +Int (A6 +Int (A7 +Int (A8 +Int (A9 +Int (A10 +Int (X +Int AS))))))))))) => 0 -Int (A1 +Int (A2 +Int (A3 +Int (A4 +Int (A5 +Int (A6 +Int (A7 +Int (A8 +Int (A9 +Int (A10 +Int AS))))))))))
rule X -Int (A1 +Int (A2 +Int (A3 +Int (A4 +Int (A5 +Int (A6 +Int (A7 +Int (A8 +Int (A9 +Int (X +Int AS)))))))))) => 0 -Int (A1 +Int (A2 +Int (A3 +Int (A4 +Int (A5 +Int (A6 +Int (A7 +Int (A8 +Int (A9 +Int AS)))))))))
rule X -Int (A1 +Int (A2 +Int (A3 +Int (A4 +Int (A5 +Int (A6 +Int (A7 +Int (A8 +Int (X +Int AS))))))))) => 0 -Int (A1 +Int (A2 +Int (A3 +Int (A4 +Int (A5 +Int (A6 +Int (A7 +Int (A8 +Int AS))))))))
rule X -Int (A1 +Int (A2 +Int (A3 +Int (A4 +Int (A5 +Int (A6 +Int (A7 +Int (X +Int AS)))))))) => 0 -Int (A1 +Int (A2 +Int (A3 +Int (A4 +Int (A5 +Int (A6 +Int (A7 +Int AS)))))))
rule X -Int (A1 +Int (A2 +Int (A3 +Int (A4 +Int (A5 +Int (A6 +Int (X +Int AS))))))) => 0 -Int (A1 +Int (A2 +Int (A3 +Int (A4 +Int (A5 +Int (A6 +Int AS))))))
rule X -Int (A1 +Int (A2 +Int (A3 +Int (A4 +Int (A5 +Int (X +Int AS)))))) => 0 -Int (A1 +Int (A2 +Int (A3 +Int (A4 +Int (A5 +Int AS)))))
rule X -Int (A1 +Int (A2 +Int (A3 +Int (A4 +Int (X +Int AS))))) => 0 -Int (A1 +Int (A2 +Int (A3 +Int (A4 +Int AS))))
rule X -Int (A1 +Int (A2 +Int (A3 +Int (X +Int AS)))) => 0 -Int (A1 +Int (A2 +Int (A3 +Int AS)))
rule X -Int (A1 +Int (A2 +Int (X +Int AS))) => 0 -Int (A1 +Int (A2 +Int AS))

// Vat_fork-same_fail lemma
rule X +Int (pow256 -Int #unsigned(Y)) => X -Int Y
requires Y <Int 0
andBool 0 <=Int X -Int Y

rule #unsigned(X) -Int (pow256 +Int X) => 0
requires X <Int 0

// Cat_bite_full_fail_rough lemma
// rule #sgnInterp(sgn(chop(A *Int #unsigned(0 -Int B))) *Int -1, abs(chop(A *Int #unsigned(0 -Int B))) /Int B) ==K A => #rangeSInt(256, A *Int (0 -Int B))
// requires #rangeUInt(256, A)
// andBool 0 <Int B
// andBool #rangeSInt(256, 0 -Int B)

// skim/bail Rate * Art <= pow255 (condition for grab)
rule #signed(chop((A *Int #unsigned((0 -Int B))))) <=Int 0 => #rangeSInt(256, 0 -Int (A *Int B))
requires #rangeUInt(256, A)
andBool 0 <Int B
andBool #rangeSInt(256, 0 -Int B)

rule chop(A *Int #unsigned(0 -Int B)) <=Int maxSInt256 andBool minSInt256 <=Int chop(A *Int #unsigned(0 -Int B)) => #rangeSInt(256, A *Int (0 -Int B))
requires #rangeUInt256(A)
andBool #rangeUInt256(A *Int B)
andBool 0 <Int B
andBool #rangeSInt(256, 0 -Int B)
```
101 changes: 98 additions & 3 deletions src/dss.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3099,6 +3099,27 @@ iff
returns Rho
```

#### system liveness flag

```act
behaviour live of Pot
interface live()

for all

Live : uint256

storage

live |-> Live

iff

VCallValue == 0

returns Live
```

### Mutators

#### adding and removing owners
Expand Down Expand Up @@ -3211,11 +3232,13 @@ storage

wards[CALLER_ID] |-> May
dsr |-> Dsr => (#if what == #string2Word("dsr") #then data #else Dsr #fi)
live |-> Live

iff

// act: caller is `. ? : not` authorised
May == 1
Live == 1
VCallValue == 0
```

Expand All @@ -3242,6 +3265,31 @@ iff
VCallValue == 0
```

#### freezing `dsr` upon global settlement

```act
behaviour cage of Pot
interface cage()

for all

May : uint256
Dsr : uint256
Live : uint256

storage

wards[CALLER_ID] |-> May
dsr |-> Dsr => #Ray
live |-> Live => 0

iff

// act: caller is `. ? : not` authorised
May == 1
VCallValue == 0
```

#### `rpow`

```act
Expand Down Expand Up @@ -3401,6 +3449,7 @@ for all
Pie_u : uint256
Pie_tot : uint256
Chi : uint256
Rho : uint256
Vat : address Vat
Can : uint256
Dai_u : uint256
Expand All @@ -3411,6 +3460,7 @@ storage
pie[CALLER_ID] |-> Pie_u => Pie_u + wad
Pie |-> Pie_tot => Pie_tot + wad
chi |-> Chi
rho |-> Rho
vat |-> Vat

storage Vat
Expand All @@ -3424,6 +3474,7 @@ iff
VCallValue == 0
VCallDepth < 1024
Can == 1
Rho == TIME

iff in range uint256

Expand Down Expand Up @@ -7361,7 +7412,37 @@ if
returns 1 + Kicks

calls
Flapper.addu48u48
Flopper.addu48u48
```

```act
behaviour tick of Flopper
interface tick(uint256 id)

for all
Ttl : uint48
Tau : uint48
Guy : address
Tic : uint48
End : uint48

storage
ttl_tau |-> #WordPackUInt48UInt48(Ttl, Tau)
bids[1 + Kicks].guy_tic_end |-> #WordPackAddrUInt48UInt48(Guy, Tic, End) => #WordPackAddrUInt48UInt48(Guy, Tic, TIME + Tau)

iff
VCallValue == 0
Tic == 0
End < TIME

iff in range uint48
TIME + Tau

if
#rangeUInt(48, TIME)

calls
Flopper.addu48u48
```

```act
Expand Down Expand Up @@ -7905,6 +7986,7 @@ for all
Vat : address
Cat : address
Vow : address
Pot : address
Spot : address

storage
Expand All @@ -7913,6 +7995,7 @@ storage
vat |-> Vat => (#if what == #string2Word("vat") #then data #else Vat #fi)
cat |-> Cat => (#if what == #string2Word("cat") #then data #else Cat #fi)
vow |-> Vow => (#if what == #string2Word("vow") #then data #else Vow #fi)
pot |-> Pot => (#if what == #string2Word("pot") #then data #else Pot #fi)
spot |-> Spot => (#if what == #string2Word("spot") #then data #else Spot #fi)

iff
Expand Down Expand Up @@ -8112,6 +8195,7 @@ for all
Vat : address Vat
Cat : address Cat
Vow : address Vow
Pot : address Pot
Flapper : address Flapper
Flopper : address Flopper
FlapVat : address
Expand All @@ -8123,13 +8207,15 @@ for all
VatLive : uint256
CatLive : uint256
VowLive : uint256
PotLive : uint256
FlapLive : uint256
FlopLive : uint256

CallerMay : uint256
EndMayVat : uint256
EndMayCat : uint256
EndMayVow : uint256
EndMayPot : uint256
VowMayFlap : uint256
VowMayFlop : uint256

Expand All @@ -8140,6 +8226,7 @@ for all
Vice : uint256
Sin : uint256
Ash : uint256
Dsr : uint256

storage

Expand Down Expand Up @@ -8176,6 +8263,12 @@ storage Vow
Sin |-> Sin => 0
Ash |-> Ash => 0

storage Pot

wards[ACCT_ID] |-> EndMayPot
dsr |-> Dsr => #Ray
live |-> PotLive => 0

storage Flapper

wards[Vow] |-> VowMayFlap
Expand Down Expand Up @@ -8476,6 +8569,7 @@ for all
Line_i : uint256
Dust_i : uint256
Mat_i : uint256
Par : uint256
Vat : address Vat
Spotter : address Spotter
DSValue : address DSValue
Expand All @@ -8488,11 +8582,12 @@ storage
vat |-> Vat
spot |-> Spotter
Art[ilk] |-> Art_i
tag[ilk] |-> Tag_i => (#Wad * #Ray) / Price
tag[ilk] |-> Tag_i => (#Wad * Par) / Price

storage Spotter
ilks[ilk].pip |-> DSValue
ilks[ilk].mat |-> Mat_i
ilks[ilk].par |-> Par

storage Vat
ilks[ilk].Art |-> Art_i
Expand All @@ -8514,7 +8609,7 @@ iff
Price =/= 0

iff in range uint256
#Wad * #Ray
#Wad * Par

calls
End.rdiv
Expand Down
Loading