removing chop reasoning that has been upstreamed

runtimeverification · Sep 11, 2024 · a5ca5c5 · a5ca5c5
1 parent 8838e67
commit a5ca5c5
Show file tree

Hide file tree

Showing 2 changed files with 0 additions and 42 deletions.
diff --git a/src/kontrol/kdist/kontrol_lemmas.md b/src/kontrol/kdist/kontrol_lemmas.md
@@ -33,16 +33,6 @@ module KONTROL-AUX-LEMMAS
     rule ethUpperBound => 2 ^Int ethMaxWidth
  // ----------------------------------------
 
-    // chop and +Int
-    rule [chop-plus]: chop (A +Int B) ==Int 0 => A ==Int (-1) *Int B
-      requires #rangeUInt(256, A) andBool #rangeUInt(256, (-1) *Int B)
-      [concrete(B), simplification, comm]
-
-    // chop and -Int
-    rule [chop-zero-minus]: chop (0 -Int A) ==Int B => A ==Int (pow256 -Int B) modInt pow256
-      requires #rangeUInt(256, A) andBool #rangeUInt(256, B)
-      [concrete(B), simplification, comm, preserves-definedness]
-
     // ==Int
     rule [int-eq-refl]: X ==Int X => true [simplification]
 
@@ -208,21 +198,6 @@ module KONTROL-AUX-LEMMAS
      andBool log2Int(X +Int 1) <=Int log2Int(Y)
      [simplification, concrete(X, Y), preserves-definedness]
 
-    rule chop ( X *Int Y ) => X *Int Y
-      requires 0 <=Int X andBool X <Int ethUpperBound
-       andBool 0 <=Int Y andBool Y <Int 2 ^Int ( 256 -Int ethMaxWidth )
-       [simplification]
-
-    rule [mul-overflow-check]:
-      X ==Int chop ( X *Int Y ) /Int Y => X *Int Y <Int pow256
-      requires #rangeUInt(256, X) andBool 0 <Int Y
-      [simplification, comm, preserves-definedness]
-
-    rule [mul-overflow-check-ML]:
-      { X #Equals chop ( X *Int Y ) /Int Y } => { true #Equals X *Int Y <Int pow256 }
-      requires #rangeUInt(256, X) andBool 0 <Int Y
-      [simplification, preserves-definedness]
-
     rule [mul-cancel-10-le]:
       A *Int B <=Int C *Int D => (A /Int 10) *Int B <=Int (C /Int 10) *Int D
       requires 0 <=Int A andBool 0 <=Int C andBool A modInt 10 ==Int 0 andBool C modInt 10 ==Int 0
@@ -244,12 +219,6 @@ module KONTROL-AUX-LEMMAS
     rule X <Int A +Int B => true requires X <=Int 0 andBool 0 <=Int A andBool 0  <Int B [concrete(X), simplification]
     rule X <Int A *Int B => true requires X <=Int 0 andBool 0  <Int A andBool 0  <Int B [concrete(X), simplification]
 
-    rule [chop-no-overflow-add-l]: X:Int <=Int chop ( X +Int Y:Int ) => X +Int Y <Int pow256 requires #rangeUInt(256, X) andBool #rangeUInt(256, Y)             [simplification]
-    rule [chop-no-overflow-add-r]: X:Int <=Int chop ( Y +Int X:Int ) => X +Int Y <Int pow256 requires #rangeUInt(256, X) andBool #rangeUInt(256, Y)             [simplification]
-    rule [chop-no-overflow-mul-l]: X:Int <=Int chop ( X *Int Y:Int ) => X *Int Y <Int pow256 requires #rangeUInt(256, X) andBool #rangeUInt(256, Y)             [simplification]
-    rule [chop-no-overflow-mul-r]: X:Int <=Int chop ( Y *Int X:Int ) => X *Int Y <Int pow256 requires #rangeUInt(256, X) andBool #rangeUInt(256, Y)             [simplification]
-    rule [chop-no-overflow-div]:   X:Int <=Int chop ( X /Int Y:Int ) => X /Int Y <Int pow256 requires #rangeUInt(256, X) andBool 0 <Int Y andBool Y <Int pow256 [simplification]
-
     //
     // #lookup
     //
@@ -265,12 +234,6 @@ module KONTROL-AUX-LEMMAS
         requires #rangeUInt(256, VALUE)
         [simplification]
 
-    rule chop ( X -Int Y ) => X -Int Y
-        requires #rangeUInt(256, X)
-         andBool #rangeUInt(256, Y)
-         andBool Y <=Int X
-        [simplification]
-
     rule X -Int Y <=Int Z => true
         requires X <=Int Z
          andBool 0 <=Int Y

diff --git a/src/tests/integration/test-data/cse-lemmas.k b/src/tests/integration/test-data/cse-lemmas.k
@@ -14,11 +14,6 @@ module CSE-LEMMAS
       requires #rangeUInt ( 256 , X )
       [simplification]
 
-    // for-loop chop
-    rule chop ( ( X:Int +Int Y:Int ) ) ==Int 0 => X ==Int pow256 -Int (Y modInt pow256)
-      requires #rangeUInt(256, X) andBool 0 <=Int Y
-      [simplification, concrete(Y)]
-
     // Set equality needed for discharging `#Not ( #Exists ( ... )` on `<accessedAccounts>` unification
     rule { S1:Set #Equals S2:Set |Set SetItem ( X ) } =>
          { X in S1 } #And