diff --git a/dss b/dss
index b5e9bc071..f2dfa2a24 160000
--- a/dss
+++ b/dss
@@ -1 +1 @@
-Subproject commit b5e9bc0717defffae73cd4f4e7f30fb84843c200
+Subproject commit f2dfa2a244db059b3a37183ea73b2aea417858ba
diff --git a/src/dirty_lemmas.k.md b/src/dirty_lemmas.k.md
index 95c3227af..8b411c6d0 100644
--- a/src/dirty_lemmas.k.md
+++ b/src/dirty_lemmas.k.md
@@ -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)
-```
diff --git a/src/dss.md b/src/dss.md
index 73c69681f..845f6436d 100644
--- a/src/dss.md
+++ b/src/dss.md
@@ -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
@@ -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
 ```
 
@@ -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
@@ -3401,6 +3449,7 @@ for all
     Pie_u   : uint256
     Pie_tot : uint256
     Chi     : uint256
+    Rho     : uint256
     Vat     : address Vat
     Can     : uint256
     Dai_u   : uint256
@@ -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
@@ -3424,6 +3474,7 @@ iff
     VCallValue == 0
     VCallDepth < 1024
     Can == 1
+    Rho == TIME
 
 iff in range uint256
 
@@ -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
@@ -7905,6 +7986,7 @@ for all
     Vat  : address
     Cat  : address
     Vow  : address
+    Pot  : address
     Spot : address
 
 storage
@@ -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
@@ -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
@@ -8123,6 +8207,7 @@ for all
     VatLive  : uint256
     CatLive  : uint256
     VowLive  : uint256
+    PotLive  : uint256
     FlapLive : uint256
     FlopLive : uint256
 
@@ -8130,6 +8215,7 @@ for all
     EndMayVat : uint256
     EndMayCat : uint256
     EndMayVow : uint256
+    EndMayPot : uint256
     VowMayFlap : uint256
     VowMayFlop : uint256
 
@@ -8140,6 +8226,7 @@ for all
     Vice  : uint256
     Sin   : uint256
     Ash   : uint256
+    Dsr   : uint256
 
 storage
 
@@ -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
@@ -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
@@ -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
@@ -8514,7 +8609,7 @@ iff
   Price =/= 0
 
 iff in range uint256
-  #Wad * #Ray
+  #Wad * Par
 
 calls
   End.rdiv
diff --git a/src/lemmas.k.md b/src/lemmas.k.md
index 18857c642..30ac77c9a 100644
--- a/src/lemmas.k.md
+++ b/src/lemmas.k.md
@@ -481,3 +481,162 @@ rule (#sgnInterp(sgn(chop(A *Int #unsigned(B))) *Int sgn(#unsigned(B)), abs(chop
   andBool #rangeSInt(256, B)
   andBool B =/=Int 0
 ```
+
+from `dirty_lemmas.k.md` on 23/08/2019:
+
+```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)
+```
diff --git a/src/storage.k.md b/src/storage.k.md
index fc99e4bf2..7c971e480 100644
--- a/src/storage.k.md
+++ b/src/storage.k.md
@@ -645,71 +645,77 @@ syntax Int ::= "#End.vow" [function]
 // act:
 rule #End.vow => 3
 
+syntax Int ::= "#End.pot" [function]
+// ---------------------------------
+// doc: `Pot` that this `End` points to
+// act:
+rule #End.spot => 4
+
 syntax Int ::= "#End.spot" [function]
 // ---------------------------------
 // doc: `Spot` that this `End` points to
 // act:
-rule #End.spot => 4
+rule #End.spot => 5
 
 syntax Int ::= "#End.live" [function]
 // ----------------------------------
 // doc: system liveness
 // act:
-rule #End.live => 5
+rule #End.live => 6
 
 syntax Int ::= "#End.when" [function]
 // ----------------------------------
 // doc: time of cage
 // act:
-rule #End.when => 6
+rule #End.when => 7
 
 syntax Int ::= "#End.wait" [function]
 // ----------------------------------
 // doc: processing period
 // act:
-rule #End.wait => 7
+rule #End.wait => 8
 
 syntax Int ::= "#End.debt" [function]
 // ----------------------------------
 // doc: total outstanding debt following processing
 // act:
-rule #End.debt => 8
+rule #End.debt => 9
 
 syntax Int ::= "#End.tag" "[" Int "]" [function]
 // -----------------------------------------------
 // doc: the cage price of ilk `$0`
 // act:
-rule #End.tag[Ilk] => #hashedLocation("Solidity", 9, Ilk)
+rule #End.tag[Ilk] => #hashedLocation("Solidity", 10, Ilk)
 
 syntax Int ::= "#End.gap" "[" Int "]" [function]
 // -----------------------------------------------
 // doc: the collateral shortfall of ilk `$0`
 // act:
-rule #End.gap[Ilk] => #hashedLocation("Solidity", 10, Ilk)
+rule #End.gap[Ilk] => #hashedLocation("Solidity", 11, Ilk)
 
 syntax Int ::= "#End.Art" "[" Int "]" [function]
 // -----------------------------------------------
 // doc: the total debt of ilk `$0`
 // act:
-rule #End.Art[Ilk] => #hashedLocation("Solidity", 11, Ilk)
+rule #End.Art[Ilk] => #hashedLocation("Solidity", 12, Ilk)
 
 syntax Int ::= "#End.fix" "[" Int "]" [function]
 // -----------------------------------------------
 // doc: the final cash price of ilk `$0`
 // act:
-rule #End.fix[Ilk] => #hashedLocation("Solidity", 12, Ilk)
+rule #End.fix[Ilk] => #hashedLocation("Solidity", 13, Ilk)
 
 syntax Int ::= "#End.bag" "[" Int "]" [function]
 // -----------------------------------------------
 // doc: the packed dai of user `$0`
 // act:
-rule #End.bag[Usr] => #hashedLocation("Solidity", 13, Usr)
+rule #End.bag[Usr] => #hashedLocation("Solidity", 14, Usr)
 
 syntax Int ::= "#End.out" "[" Int "][" Int "]" [function]
 // ---------------------------------------------
 // doc: cashed collateral of ilk `$0` assigned to `$1`
 // act:
-rule #End.out[Ilk][Usr] => #hashedLocation("Solidity", 14, Ilk Usr)
+rule #End.out[Ilk][Usr] => #hashedLocation("Solidity", 15, Ilk Usr)
 ```
 
 ### Pot
@@ -762,6 +768,12 @@ syntax Int ::= "#Pot.rho" [function]
 // doc:
 // act:
 rule #Pot.rho => 7
+
+syntax Int ::= "#Pot.live" [function]
+// ----------------------------------
+// doc:
+// act:
+rule #Pot.rho => 8
 ```
 ### DSToken