section‹Constant Folding› theory Constant_Folding imports Solidity_Main begin text‹ The following function optimizes expressions w.r.t. gas consumption. › primrec eupdate :: "E ⇒ E" and lupdate :: "L ⇒ L" where "lupdate (Id i) = Id i" | "lupdate (Ref i exp) = Ref i (map eupdate exp)" | "eupdate (E.INT b v) = (if (b∈vbits) then if v ≥ 0 then E.INT b (-(2^(b-1)) + (v+2^(b-1)) mod (2^b)) else E.INT b (2^(b-1) - (-v+2^(b-1)-1) mod (2^b) - 1) else E.INT b v)" | "eupdate (UINT b v) = (if (b∈vbits) then UINT b (v mod (2^b)) else UINT b v)" | "eupdate (ADDRESS a) = ADDRESS a" | "eupdate (BALANCE a) = BALANCE a" | "eupdate THIS = THIS" | "eupdate SENDER = SENDER" | "eupdate VALUE = VALUE" | "eupdate TRUE = TRUE" | "eupdate FALSE = FALSE" | "eupdate (LVAL l) = LVAL (lupdate l)" | "eupdate (PLUS ex1 ex2) = (case (eupdate ex1) of E.INT b1 v1 ⇒ if b1 ∈ vbits then (case (eupdate ex2) of E.INT b2 v2 ⇒ if b2∈vbits then let v=v1+v2 in if v ≥ 0 then E.INT (max b1 b2) (-(2^((max b1 b2)-1)) + (v+2^((max b1 b2)-1)) mod (2^(max b1 b2))) else E.INT (max b1 b2) (2^((max b1 b2)-1) - (-v+2^((max b1 b2)-1)-1) mod (2^(max b1 b2)) - 1) else (PLUS (E.INT b1 v1) (E.INT b2 v2)) | UINT b2 v2 ⇒ if b2∈vbits ∧ b2 < b1 then let v=v1+v2 in if v ≥ 0 then E.INT b1 (-(2^(b1-1)) + (v+2^(b1-1)) mod (2^b1)) else E.INT b1 (2^(b1-1) - (-v+2^(b1-1)-1) mod (2^b1) - 1) else PLUS (E.INT b1 v1) (UINT b2 v2) | _ ⇒ PLUS (E.INT b1 v1) (eupdate ex2)) else PLUS (E.INT b1 v1) (eupdate ex2) | UINT b1 v1 ⇒ if b1 ∈ vbits then (case (eupdate ex2) of UINT b2 v2 ⇒ if b2 ∈ vbits then UINT (max b1 b2) ((v1 + v2) mod (2^(max b1 b2))) else (PLUS (UINT b1 v1) (UINT b2 v2)) | E.INT b2 v2 ⇒ if b2∈vbits ∧ b1 < b2 then let v=v1+v2 in if v ≥ 0 then E.INT b2 (-(2^(b2-1)) + (v+2^(b2-1)) mod (2^b2)) else E.INT b2 (2^(b2-1) - (-v+2^(b2-1)-1) mod (2^b2) - 1) else PLUS (UINT b1 v1) (E.INT b2 v2) | _ ⇒ PLUS (UINT b1 v1) (eupdate ex2)) else PLUS (UINT b1 v1) (eupdate ex2) | _ ⇒ PLUS (eupdate ex1) (eupdate ex2))" | "eupdate (MINUS ex1 ex2) = (case (eupdate ex1) of E.INT b1 v1 ⇒ if b1 ∈ vbits then (case (eupdate ex2) of E.INT b2 v2 ⇒ if b2∈vbits then let v=v1-v2 in if v ≥ 0 then E.INT (max b1 b2) (-(2^((max b1 b2)-1)) + (v+2^((max b1 b2)-1)) mod (2^(max b1 b2))) else E.INT (max b1 b2) (2^((max b1 b2)-1) - (-v+2^((max b1 b2)-1)-1) mod (2^(max b1 b2)) - 1) else (MINUS (E.INT b1 v1) (E.INT b2 v2)) | UINT b2 v2 ⇒ if b2∈vbits ∧ b2 < b1 then let v=v1-v2 in if v ≥ 0 then E.INT b1 (-(2^(b1-1)) + (v+2^(b1-1)) mod (2^b1)) else E.INT b1 (2^(b1-1) - (-v+2^(b1-1)-1) mod (2^b1) - 1) else MINUS (E.INT b1 v1) (UINT b2 v2) | _ ⇒ MINUS (E.INT b1 v1) (eupdate ex2)) else MINUS (E.INT b1 v1) (eupdate ex2) | UINT b1 v1 ⇒ if b1 ∈ vbits then (case (eupdate ex2) of UINT b2 v2 ⇒ if b2 ∈ vbits then UINT (max b1 b2) ((v1 - v2) mod (2^(max b1 b2))) else (MINUS (UINT b1 v1) (UINT b2 v2)) | E.INT b2 v2 ⇒ if b2∈vbits ∧ b1 < b2 then let v=v1-v2 in if v ≥ 0 then E.INT b2 (-(2^(b2-1)) + (v+2^(b2-1)) mod (2^b2)) else E.INT b2 (2^(b2-1) - (-v+2^(b2-1)-1) mod (2^b2) - 1) else MINUS (UINT b1 v1) (E.INT b2 v2) | _ ⇒ MINUS (UINT b1 v1) (eupdate ex2)) else MINUS (UINT b1 v1) (eupdate ex2) | _ ⇒ MINUS (eupdate ex1) (eupdate ex2))" | "eupdate (EQUAL ex1 ex2) = (case (eupdate ex1) of E.INT b1 v1 ⇒ if b1 ∈ vbits then (case (eupdate ex2) of E.INT b2 v2 ⇒ if b2∈vbits then if v1 = v2 then TRUE else FALSE else EQUAL (E.INT b1 v1) (E.INT b2 v2) | UINT b2 v2 ⇒ if b2∈vbits ∧ b2 < b1 then if v1 = v2 then TRUE else FALSE else EQUAL (E.INT b1 v1) (UINT b2 v2) | _ ⇒ EQUAL (E.INT b1 v1) (eupdate ex2)) else EQUAL (E.INT b1 v1) (eupdate ex2) | UINT b1 v1 ⇒ if b1 ∈ vbits then (case (eupdate ex2) of UINT b2 v2 ⇒ if b2 ∈ vbits then if v1 = v2 then TRUE else FALSE else EQUAL (E.INT b1 v1) (UINT b2 v2) | E.INT b2 v2 ⇒ if b2∈vbits ∧ b1 < b2 then if v1 = v2 then TRUE else FALSE else EQUAL (UINT b1 v1) (E.INT b2 v2) | _ ⇒ EQUAL (UINT b1 v1) (eupdate ex2)) else EQUAL (UINT b1 v1) (eupdate ex2) | _ ⇒ EQUAL (eupdate ex1) (eupdate ex2))" | "eupdate (LESS ex1 ex2) = (case (eupdate ex1) of E.INT b1 v1 ⇒ if b1 ∈ vbits then (case (eupdate ex2) of E.INT b2 v2 ⇒ if b2∈vbits then if v1 < v2 then TRUE else FALSE else LESS (E.INT b1 v1) (E.INT b2 v2) | UINT b2 v2 ⇒ if b2∈vbits ∧ b2 < b1 then if v1 < v2 then TRUE else FALSE else LESS (E.INT b1 v1) (UINT b2 v2) | _ ⇒ LESS (E.INT b1 v1) (eupdate ex2)) else LESS (E.INT b1 v1) (eupdate ex2) | UINT b1 v1 ⇒ if b1 ∈ vbits then (case (eupdate ex2) of UINT b2 v2 ⇒ if b2 ∈ vbits then if v1 < v2 then TRUE else FALSE else LESS (E.INT b1 v1) (UINT b2 v2) | E.INT b2 v2 ⇒ if b2∈vbits ∧ b1 < b2 then if v1 < v2 then TRUE else FALSE else LESS (UINT b1 v1) (E.INT b2 v2) | _ ⇒ LESS (UINT b1 v1) (eupdate ex2)) else LESS (UINT b1 v1) (eupdate ex2) | _ ⇒ LESS (eupdate ex1) (eupdate ex2))" | "eupdate (AND ex1 ex2) = (case (eupdate ex1) of TRUE ⇒ (case (eupdate ex2) of TRUE ⇒ TRUE | FALSE ⇒ FALSE | _ ⇒ AND TRUE (eupdate ex2)) | FALSE ⇒ (case (eupdate ex2) of TRUE ⇒ FALSE | FALSE ⇒ FALSE | _ ⇒ AND FALSE (eupdate ex2)) | _ ⇒ AND (eupdate ex1) (eupdate ex2))" | "eupdate (OR ex1 ex2) = (case (eupdate ex1) of TRUE ⇒ (case (eupdate ex2) of TRUE ⇒ TRUE | FALSE ⇒ TRUE | _ ⇒ OR TRUE (eupdate ex2)) | FALSE ⇒ (case (eupdate ex2) of TRUE ⇒ TRUE | FALSE ⇒ FALSE | _ ⇒ OR FALSE (eupdate ex2)) | _ ⇒ OR (eupdate ex1) (eupdate ex2))" | "eupdate (NOT ex1) = (case (eupdate ex1) of TRUE ⇒ FALSE | FALSE ⇒ TRUE | _ ⇒ NOT (eupdate ex1))" | "eupdate (CALL i xs) = CALL i xs" | "eupdate (ECALL e i xs r) = ECALL e i xs r" value "eupdate (UINT 8 250)" lemma "eupdate (UINT 8 250) =UINT 8 250" by(simp) lemma "eupdate (UINT 8 500) = UINT 8 244" by(simp) lemma "eupdate (E.INT 8 (-100)) = E.INT 8 (- 100)" by(simp) lemma "eupdate (E.INT 8 (-150)) = E.INT 8 106" by(simp) lemma "eupdate (PLUS (UINT 8 100) (UINT 8 100)) = UINT 8 200" by(simp) lemma "eupdate (PLUS (UINT 8 257) (UINT 16 100)) = UINT 16 101" by(simp) lemma "eupdate (PLUS (E.INT 8 100) (UINT 8 250)) = PLUS (E.INT 8 100) (UINT 8 250)" by(simp) lemma "eupdate (PLUS (E.INT 8 250) (UINT 8 500)) = PLUS (E.INT 8 (- 6)) (UINT 8 244)" by(simp) lemma "eupdate (PLUS (E.INT 16 250) (UINT 8 500)) = E.INT 16 494" by(simp) lemma "eupdate (EQUAL (UINT 16 250) (UINT 8 250)) = TRUE" by(simp) lemma "eupdate (EQUAL (E.INT 16 100) (UINT 8 100)) = TRUE" by(simp) lemma "eupdate (EQUAL (E.INT 8 100) (UINT 8 100)) = EQUAL (E.INT 8 100) (UINT 8 100)" by(simp) lemma update_bounds_int: assumes "eupdate ex = (E.INT b v)" and "b∈vbits" shows "(v < 2^(b-1)) ∧ v ≥ -(2^(b-1))" proof (cases ex) case (INT b' v') then show ?thesis proof cases assume "b'∈vbits" show ?thesis proof cases let ?x="-(2^(b'-1)) + (v'+2^(b'-1)) mod 2^b'" assume "v'≥0" with `b'∈vbits` have "eupdate (E.INT b' v') = E.INT b' ?x" by simp with assms have "b=b'" and "v=?x" using INT by (simp,simp) moreover from `b'∈vbits` have "b'>0" by auto hence "?x < 2 ^(b'-1)" using upper_bound2[of b' "(v' + 2 ^ (b' - 1)) mod 2^b'"] by simp moreover have "?x ≥ -(2^(b'-1))" by simp ultimately show ?thesis by simp next let ?x="2^(b'-1) - (-v'+2^(b'-1)-1) mod (2^b') - 1" assume "¬v'≥0" with `b'∈vbits` have "eupdate (E.INT b' v') = E.INT b' ?x" by simp with assms have "b=b'" and "v=?x" using INT by (simp,simp) moreover have "(-v'+2^(b'-1)-1) mod (2^b')≥0" by simp hence "?x < 2 ^(b'-1)" by arith moreover from `b'∈vbits` have "b'>0" by auto hence "?x ≥ -(2^(b'-1))" using lower_bound2[of b' v'] by simp ultimately show ?thesis by simp qed next assume "¬ b'∈vbits" with assms show ?thesis using INT by simp qed next case (UINT b' v') with assms show ?thesis proof cases assume "b'∈vbits" with assms show ?thesis using UINT by simp next assume "¬ b'∈vbits" with assms show ?thesis using UINT by simp qed next case (ADDRESS x3) with assms show ?thesis by simp next case (BALANCE x4) with assms show ?thesis by simp next case THIS with assms show ?thesis by simp next case SENDER with assms show ?thesis by simp next case VALUE with assms show ?thesis by simp next case TRUE with assms show ?thesis by simp next case FALSE with assms show ?thesis by simp next case (LVAL x7) with assms show ?thesis by simp next case p: (PLUS e1 e2) show ?thesis proof (cases "eupdate e1") case i: (INT b1 v1) show ?thesis proof cases assume "b1∈vbits" show ?thesis proof (cases "eupdate e2") case i2: (INT b2 v2) then show ?thesis proof cases let ?v="v1+v2" assume "b2∈vbits" show ?thesis proof cases let ?x="-(2^((max b1 b2)-1)) + (?v+2^((max b1 b2)-1)) mod 2^(max b1 b2)" assume "?v≥0" with `b1∈vbits` `b2∈vbits` i i2 have "eupdate (PLUS e1 e2) = E.INT (max b1 b2) ?x" by simp with assms have "b=max b1 b2" and "v=?x" using p by (simp,simp) moreover from `b1∈vbits` have "max b1 b2>0" by auto hence "?x < 2 ^(max b1 b2 - 1)" using upper_bound2[of "max b1 b2" "(?v + 2 ^ (max b1 b2 - 1)) mod 2^max b1 b2"] by simp moreover have "?x ≥ -(2^(max b1 b2-1))" by simp ultimately show ?thesis by simp next let ?x="2^((max b1 b2)-1) - (-?v+2^((max b1 b2)-1)-1) mod (2^(max b1 b2)) - 1" assume "¬?v≥0" with `b1∈vbits` `b2∈vbits` i i2 have "eupdate (PLUS e1 e2) = E.INT (max b1 b2) ?x" by simp with assms have "b=max b1 b2" and "v=?x" using p by (simp,simp) moreover have "(-?v+2^(max b1 b2-1)-1) mod (2^max b1 b2)≥0" by simp hence "?x < 2 ^(max b1 b2-1)" by arith moreover from `b1∈vbits` have "max b1 b2>0" by auto hence "?x ≥ -(2^(max b1 b2-1))" using lower_bound2[of "max b1 b2" ?v] by simp ultimately show ?thesis by simp qed next assume "b2∉vbits" with p i i2 `b1∈vbits` show ?thesis using assms by simp qed next case u: (UINT b2 v2) then show ?thesis proof cases let ?v="v1+v2" assume "b2∈vbits" show ?thesis proof cases assume "b2<b1" then show ?thesis proof cases let ?x="(-(2^(b1-1)) + (?v+2^(b1-1)) mod (2^b1))" assume "?v≥0" with `b1∈vbits` `b2∈vbits` `b2<b1` i u have "eupdate (PLUS e1 e2) = E.INT b1 ?x" by simp with assms have "b=b1" and "v=?x" using p by (simp,simp) moreover from `b1∈vbits` have "b1>0" by auto hence "?x < 2 ^(b1 - 1)" using upper_bound2[of b1] by simp moreover have "?x ≥ -(2^(b1-1))" by simp ultimately show ?thesis by simp next let ?x="2^(b1-1) - (-?v+2^(b1-1)-1) mod (2^b1) - 1" assume "¬?v≥0" with `b1∈vbits` `b2∈vbits` `b2<b1` i u have "eupdate (PLUS e1 e2) = E.INT b1 ?x" by simp with assms have "b=b1" and "v=?x" using p i u by (simp,simp) moreover have "(-?v+2^(b1-1)-1) mod 2^b1≥0" by simp hence "?x < 2 ^(b1-1)" by arith moreover from `b1∈vbits` have "b1>0" by auto hence "?x ≥ -(2^(b1-1))" using lower_bound2[of b1 ?v] by simp ultimately show ?thesis by simp qed next assume "¬ b2<b1" with p i u `b1∈vbits` show ?thesis using assms by simp qed next assume "b2∉vbits" with p i u `b1∈vbits` show ?thesis using assms by simp qed next case (ADDRESS x3) with p i `b1∈vbits` show ?thesis using assms by simp next case (BALANCE x4) with p i `b1∈vbits` show ?thesis using assms by simp next case THIS with p i `b1∈vbits` show ?thesis using assms by simp next case SENDER with p i `b1∈vbits` show ?thesis using assms by simp next case VALUE with p i `b1∈vbits` show ?thesis using assms by simp next case TRUE with p i `b1∈vbits` show ?thesis using assms by simp next case FALSE with p i `b1∈vbits` show ?thesis using assms by simp next case (LVAL x7) with p i `b1∈vbits` show ?thesis using assms by simp next case (PLUS x81 x82) with p i `b1∈vbits` show ?thesis using assms by simp next case (MINUS x91 x92) with p i `b1∈vbits` show ?thesis using assms by simp next case (EQUAL x101 x102) with p i `b1∈vbits` show ?thesis using assms by simp next case (LESS x111 x112) with p i `b1∈vbits` show ?thesis using assms by simp next case (AND x121 x122) with p i `b1∈vbits` show ?thesis using assms by simp next case (OR x131 x132) with p i `b1∈vbits` show ?thesis using assms by simp next case (NOT x131) with p i `b1∈vbits` show ?thesis using assms by simp next case (CALL x181 x182) with p i `b1∈vbits` show ?thesis using assms by simp next case (ECALL x191 x192 x193 x194) with p i `b1∈vbits` show ?thesis using assms by simp qed next assume "¬ b1∈vbits" with p i show ?thesis using assms by simp qed next case u: (UINT b1 v1) show ?thesis proof cases assume "b1∈vbits" show ?thesis proof (cases "eupdate e2") case i: (INT b2 v2) then show ?thesis proof cases let ?v="v1+v2" assume "b2∈vbits" show ?thesis proof cases assume "b1<b2" then show ?thesis proof cases let ?x="(-(2^(b2-1)) + (?v+2^(b2-1)) mod (2^b2))" assume "?v≥0" with `b1∈vbits` `b2∈vbits` `b1<b2` i u have "eupdate (PLUS e1 e2) = E.INT b2 ?x" by simp with assms have "b=b2" and "v=?x" using p by (simp,simp) moreover from `b2∈vbits` have "b2>0" by auto hence "?x < 2 ^(b2 - 1)" using upper_bound2[of b2] by simp moreover have "?x ≥ -(2^(b2-1))" by simp ultimately show ?thesis by simp next let ?x="2^(b2-1) - (-?v+2^(b2-1)-1) mod (2^b2) - 1" assume "¬?v≥0" with `b1∈vbits` `b2∈vbits` `b1<b2` i u have "eupdate (PLUS e1 e2) = E.INT b2 ?x" by simp with assms have "b=b2" and "v=?x" using p i u by (simp,simp) moreover have "(-?v+2^(b2-1)-1) mod 2^b2≥0" by simp hence "?x < 2 ^(b2-1)" by arith moreover from `b2∈vbits` have "b2>0" by auto hence "?x ≥ -(2^(b2-1))" using lower_bound2[of b2 ?v] by simp ultimately show ?thesis by simp qed next assume "¬ b1<b2" with p i u `b1∈vbits` show ?thesis using assms by simp qed next assume "b2∉vbits" with p i u `b1∈vbits` show ?thesis using assms by simp qed next case u2: (UINT b2 v2) then show ?thesis proof cases assume "b2∈vbits" with `b1∈vbits` u u2 p show ?thesis using assms by simp next assume "¬b2∈vbits" with p u u2 `b1∈vbits` show ?thesis using assms by simp qed next case (ADDRESS x3) with p u `b1∈vbits` show ?thesis using assms by simp next case (BALANCE x4) with p u `b1∈vbits` show ?thesis using assms by simp next case THIS with p u `b1∈vbits` show ?thesis using assms by simp next case SENDER with p u `b1∈vbits` show ?thesis using assms by simp next case VALUE with p u `b1∈vbits` show ?thesis using assms by simp next case TRUE with p u `b1∈vbits` show ?thesis using assms by simp next case FALSE with p u `b1∈vbits` show ?thesis using assms by simp next case (LVAL x7) with p u `b1∈vbits` show ?thesis using assms by simp next case (PLUS x81 x82) with p u `b1∈vbits` show ?thesis using assms by simp next case (MINUS x91 x92) with p u `b1∈vbits` show ?thesis using assms by simp next case (EQUAL x101 x102) with p u `b1∈vbits` show ?thesis using assms by simp next case (LESS x111 x112) with p u `b1∈vbits` show ?thesis using assms by simp next case (AND x121 x122) with p u `b1∈vbits` show ?thesis using assms by simp next case (OR x131 x132) with p u `b1∈vbits` show ?thesis using assms by simp next case (NOT x131) with p u `b1∈vbits` show ?thesis using assms by simp next case (CALL x181 x182) with p u `b1∈vbits` show ?thesis using assms by simp next case (ECALL x191 x192 x193 x194) with p u `b1∈vbits` show ?thesis using assms by simp qed next assume "¬ b1∈vbits" with p u show ?thesis using assms by simp qed next case (ADDRESS x3) with p show ?thesis using assms by simp next case (BALANCE x4) with p show ?thesis using assms by simp next case THIS with p show ?thesis using assms by simp next case SENDER with p show ?thesis using assms by simp next case VALUE with p show ?thesis using assms by simp next case TRUE with p show ?thesis using assms by simp next case FALSE with p show ?thesis using assms by simp next case (LVAL x7) with p show ?thesis using assms by simp next case (PLUS x81 x82) with p show ?thesis using assms by simp next case (MINUS x91 x92) with p show ?thesis using assms by simp next case (EQUAL x101 x102) with p show ?thesis using assms by simp next case (LESS x111 x112) with p show ?thesis using assms by simp next case (AND x121 x122) with p show ?thesis using assms by simp next case (OR x131 x132) with p show ?thesis using assms by simp next case (NOT x131) with p show ?thesis using assms by simp next case (CALL x181 x182) with p show ?thesis using assms by simp next case (ECALL x191 x192 x193 x194) with p show ?thesis using assms by simp qed next case m: (MINUS e1 e2) show ?thesis proof (cases "eupdate e1") case i: (INT b1 v1) with m show ?thesis proof cases assume "b1∈vbits" show ?thesis proof (cases "eupdate e2") case i2: (INT b2 v2) then show ?thesis proof cases let ?v="v1-v2" assume "b2∈vbits" with `b1 ∈ vbits` have u_def: "eupdate (MINUS e1 e2) = (let v = v1 - v2 in if 0 ≤ v then E.INT (max b1 b2) (- (2 ^ (max b1 b2 - 1)) + (v + 2 ^ (max b1 b2 - 1)) mod 2 ^ max b1 b2) else E.INT (max b1 b2) (2 ^ (max b1 b2 - 1) - (- v + 2 ^ (max b1 b2 - 1) - 1) mod 2 ^ max b1 b2 - 1))" using i i2 eupdate.simps(11)[of e1 e2] by simp show ?thesis proof cases let ?x="-(2^((max b1 b2)-1)) + (?v+2^((max b1 b2)-1)) mod 2^(max b1 b2)" assume "?v≥0" with u_def have "eupdate (MINUS e1 e2) = E.INT (max b1 b2) ?x" by simp with assms have "b=max b1 b2" and "v=?x" using m by (simp,simp) moreover from `b1∈vbits` have "max b1 b2>0" by auto hence "?x < 2 ^(max b1 b2 - 1)" using upper_bound2[of "max b1 b2" "(?v + 2 ^ (max b1 b2 - 1)) mod 2^max b1 b2"] by simp moreover have "?x ≥ -(2^(max b1 b2-1))" by simp ultimately show ?thesis by simp next let ?x="2^((max b1 b2)-1) - (-?v+2^((max b1 b2)-1)-1) mod (2^(max b1 b2)) - 1" assume "¬?v≥0" with u_def have "eupdate (MINUS e1 e2) = E.INT (max b1 b2) ?x" using u_def by simp with assms have "b=max b1 b2" and "v=?x" using m by (simp,simp) moreover have "(-?v+2^(max b1 b2-1)-1) mod (2^max b1 b2)≥0" by simp hence "?x < 2 ^(max b1 b2-1)" by arith moreover from `b1∈vbits` have "max b1 b2>0" by auto hence "?x ≥ -(2^(max b1 b2-1))" using lower_bound2[of "max b1 b2" ?v] by simp ultimately show ?thesis by simp qed next assume "b2∉vbits" with m i i2 `b1∈vbits` show ?thesis using assms by simp qed next case u: (UINT b2 v2) then show ?thesis proof cases let ?v="v1-v2" assume "b2∈vbits" show ?thesis proof cases assume "b2<b1" with `b1 ∈ vbits` `b2 ∈ vbits` have u_def: "eupdate (MINUS e1 e2) = (let v = v1 - v2 in if 0 ≤ v then E.INT b1 (- (2 ^ (b1 - 1)) + (v + 2 ^ (b1 - 1)) mod 2 ^ b1) else E.INT b1 (2 ^ (b1 - 1) - (- v + 2 ^ (b1 - 1) - 1) mod 2 ^ b1 - 1))" using i u eupdate.simps(11)[of e1 e2] by simp then show ?thesis proof cases let ?x="(-(2^(b1-1)) + (?v+2^(b1-1)) mod (2^b1))" assume "?v≥0" with u_def have "eupdate (MINUS e1 e2) = E.INT b1 ?x" by simp with assms have "b=b1" and "v=?x" using m by (simp,simp) moreover from `b1∈vbits` have "b1>0" by auto hence "?x < 2 ^(b1 - 1)" using upper_bound2[of b1] by simp moreover have "?x ≥ -(2^(b1-1))" by simp ultimately show ?thesis by simp next let ?x="2^(b1-1) - (-?v+2^(b1-1)-1) mod (2^b1) - 1" assume "¬?v≥0" with u_def have "eupdate (MINUS e1 e2) = E.INT b1 ?x" by simp with assms have "b=b1" and "v=?x" using m i u by (simp,simp) moreover have "(-?v+2^(b1-1)-1) mod 2^b1≥0" by simp hence "?x < 2 ^(b1-1)" by arith moreover from `b1∈vbits` have "b1>0" by auto hence "?x ≥ -(2^(b1-1))" using lower_bound2[of b1 ?v] by simp ultimately show ?thesis by simp qed next assume "¬ b2<b1" with m i u `b1∈vbits` show ?thesis using assms by simp qed next assume "b2∉vbits" with m i u `b1∈vbits` show ?thesis using assms by simp qed next case (ADDRESS x3) with m i `b1∈vbits` show ?thesis using assms by simp next case (BALANCE x4) with m i `b1∈vbits` show ?thesis using assms by simp next case THIS with m i `b1∈vbits` show ?thesis using assms by simp next case SENDER with m i `b1∈vbits` show ?thesis using assms by simp next case VALUE with m i `b1∈vbits` show ?thesis using assms by simp next case TRUE with m i `b1∈vbits` show ?thesis using assms by simp next case FALSE with m i `b1∈vbits` show ?thesis using assms by simp next case (LVAL x7) with m i `b1∈vbits` show ?thesis using assms by simp next case (PLUS x81 x82) with m i `b1∈vbits` show ?thesis using assms by simp next case (MINUS x91 x92) with m i `b1∈vbits` show ?thesis using assms by simp next case (EQUAL x101 x102) with m i `b1∈vbits` show ?thesis using assms by simp next case (LESS x111 x112) with m i `b1∈vbits` show ?thesis using assms by simp next case (AND x121 x122) with m i `b1∈vbits` show ?thesis using assms by simp next case (OR x131 x132) with m i `b1∈vbits` show ?thesis using assms by simp next case (NOT x131) with m i `b1∈vbits` show ?thesis using assms by simp next case (CALL x181 x182) with m i `b1∈vbits` show ?thesis using assms by simp next case (ECALL x191 x192 x193 x194) with m i `b1∈vbits` show ?thesis using assms by simp qed next assume "¬ b1∈vbits" with m i show ?thesis using assms by simp qed next case u: (UINT b1 v1) show ?thesis proof cases assume "b1∈vbits" show ?thesis proof (cases "eupdate e2") case i: (INT b2 v2) then show ?thesis proof cases let ?v="v1-v2" assume "b2∈vbits" show ?thesis proof cases assume "b1<b2" with `b1 ∈ vbits` `b2 ∈ vbits` have u_def: "eupdate (MINUS e1 e2) = (let v = v1 - v2 in if 0 ≤ v then E.INT b2 (- (2 ^ (b2 - 1)) + (v + 2 ^ (b2 - 1)) mod 2 ^ b2) else E.INT b2 (2 ^ (b2 - 1) - (- v + 2 ^ (b2 - 1) - 1) mod 2 ^ b2 - 1))" using i u eupdate.simps(11)[of e1 e2] by simp then show ?thesis proof cases let ?x="(-(2^(b2-1)) + (?v+2^(b2-1)) mod (2^b2))" assume "?v≥0" with u_def have "eupdate (MINUS e1 e2) = E.INT b2 ?x" by simp with assms have "b=b2" and "v=?x" using m by (simp,simp) moreover from `b2∈vbits` have "b2>0" by auto hence "?x < 2 ^(b2 - 1)" using upper_bound2[of b2] by simp moreover have "?x ≥ -(2^(b2-1))" by simp ultimately show ?thesis by simp next let ?x="2^(b2-1) - (-?v+2^(b2-1)-1) mod (2^b2) - 1" assume "¬?v≥0" with u_def have "eupdate (MINUS e1 e2) = E.INT b2 ?x" by simp with assms have "b=b2" and "v=?x" using m i u by (simp,simp) moreover have "(-?v+2^(b2-1)-1) mod 2^b2≥0" by simp hence "?x < 2 ^(b2-1)" by arith moreover from `b2∈vbits` have "b2>0" by auto hence "?x ≥ -(2^(b2-1))" using lower_bound2[of b2 ?v] by simp ultimately show ?thesis by simp qed next assume "¬ b1<b2" with m i u `b1∈vbits` show ?thesis using assms by simp qed next assume "b2∉vbits" with m i u `b1∈vbits` show ?thesis using assms by simp qed next case u2: (UINT b2 v2) then show ?thesis proof cases assume "b2∈vbits" with `b1∈vbits` u u2 m show ?thesis using assms by simp next assume "¬b2∈vbits" with m u u2 `b1∈vbits` show ?thesis using assms by simp qed next case (ADDRESS x3) with m u `b1∈vbits` show ?thesis using assms by simp next case (BALANCE x4) with m u `b1∈vbits` show ?thesis using assms by simp next case THIS with m u `b1∈vbits` show ?thesis using assms by simp next case SENDER with m u `b1∈vbits` show ?thesis using assms by simp next case VALUE with m u `b1∈vbits` show ?thesis using assms by simp next case TRUE with m u `b1∈vbits` show ?thesis using assms by simp next case FALSE with m u `b1∈vbits` show ?thesis using assms by simp next case (LVAL x7) with m u `b1∈vbits` show ?thesis using assms by simp next case (PLUS x81 x82) with m u `b1∈vbits` show ?thesis using assms by simp next case (MINUS x91 x92) with m u `b1∈vbits` show ?thesis using assms by simp next case (EQUAL x101 x102) with m u `b1∈vbits` show ?thesis using assms by simp next case (LESS x111 x112) with m u `b1∈vbits` show ?thesis using assms by simp next case (AND x121 x122) with m u `b1∈vbits` show ?thesis using assms by simp next case (OR x131 x132) with m u `b1∈vbits` show ?thesis using assms by simp next case (NOT x131) with m u `b1∈vbits` show ?thesis using assms by simp next case (CALL x181 x182) with m u `b1∈vbits` show ?thesis using assms by simp next case (ECALL x191 x192 x193 x194) with m u `b1∈vbits` show ?thesis using assms by simp qed next assume "¬ b1∈vbits" with m u show ?thesis using assms by simp qed next case (ADDRESS x3) with m show ?thesis using assms by simp next case (BALANCE x4) with m show ?thesis using assms by simp next case THIS with m show ?thesis using assms by simp next case SENDER with m show ?thesis using assms by simp next case VALUE with m show ?thesis using assms by simp next case TRUE with m show ?thesis using assms by simp next case FALSE with m show ?thesis using assms by simp next case (LVAL x7) with m show ?thesis using assms by simp next case (PLUS x81 x82) with m show ?thesis using assms by simp next case (MINUS x91 x92) with m show ?thesis using assms by simp next case (EQUAL x101 x102) with m show ?thesis using assms by simp next case (LESS x111 x112) with m show ?thesis using assms by simp next case (AND x121 x122) with m show ?thesis using assms by simp next case (OR x131 x132) with m show ?thesis using assms by simp next case (NOT x131) with m show ?thesis using assms by simp next case (CALL x181 x182) with m show ?thesis using assms by simp next case (ECALL x191 x192 x193 x194) with m show ?thesis using assms by simp qed next case e: (EQUAL e1 e2) show ?thesis proof (cases "eupdate e1") case i: (INT b1 v1) show ?thesis proof cases assume "b1∈vbits" show ?thesis proof (cases "eupdate e2") case i2: (INT b2 v2) then show ?thesis proof cases assume "b2∈vbits" show ?thesis proof cases assume "v1=v2" with assms show ?thesis using e i i2 `b1∈vbits` `b2∈vbits` by simp next assume "¬ v1=v2" with assms show ?thesis using e i i2 `b1∈vbits` `b2∈vbits` by simp qed next assume "b2∉vbits" with e i i2 `b1∈vbits` show ?thesis using assms by simp qed next case u: (UINT b2 v2) then show ?thesis proof cases assume "b2∈vbits" show ?thesis proof cases assume "b2<b1" then show ?thesis proof cases assume "v1=v2" with assms show ?thesis using e i u `b1∈vbits` `b2∈vbits` `b2<b1` by simp next assume "¬ v1=v2" with assms show ?thesis using e i u `b1∈vbits` `b2∈vbits` `b2<b1` by simp qed next assume "¬ b2<b1" with e i u `b1∈vbits` show ?thesis using assms by simp qed next assume "b2∉vbits" with e i u `b1∈vbits` show ?thesis using assms by simp qed next case (ADDRESS x3) with e i `b1∈vbits` show ?thesis using assms by simp next case (BALANCE x4) with e i `b1∈vbits` show ?thesis using assms by simp next case THIS with e i `b1∈vbits` show ?thesis using assms by simp next case SENDER with e i `b1∈vbits` show ?thesis using assms by simp next case VALUE with e i `b1∈vbits` show ?thesis using assms by simp next case TRUE with e i `b1∈vbits` show ?thesis using assms by simp next case FALSE with e i `b1∈vbits` show ?thesis using assms by simp next case (LVAL x7) with e i `b1∈vbits` show ?thesis using assms by simp next case (PLUS x81 x82) with e i `b1∈vbits` show ?thesis using assms by simp next case (MINUS x91 x92) with e i `b1∈vbits` show ?thesis using assms by simp next case (EQUAL x101 x102) with e i `b1∈vbits` show ?thesis using assms by simp next case (LESS x111 x112) with e i `b1∈vbits` show ?thesis using assms by simp next case (AND x121 x122) with e i `b1∈vbits` show ?thesis using assms by simp next case (OR x131 x132) with e i `b1∈vbits` show ?thesis using assms by simp next case (NOT x131) with e i `b1∈vbits` show ?thesis using assms by simp next case (CALL x181 x182) with e i `b1∈vbits` show ?thesis using assms by simp next case (ECALL x191 x192 x193 x194) with e i `b1∈vbits` show ?thesis using assms by simp qed next assume "¬ b1∈vbits" with e i show ?thesis using assms by simp qed next case u: (UINT b1 v1) show ?thesis proof cases assume "b1∈vbits" show ?thesis proof (cases "eupdate e2") case i: (INT b2 v2) then show ?thesis proof cases assume "b2∈vbits" show ?thesis proof cases assume "b1<b2" then show ?thesis proof cases assume "v1=v2" with assms show ?thesis using e i u `b1∈vbits` `b2∈vbits` `b1<b2` by simp next assume "¬ v1=v2" with assms show ?thesis using e i u `b1∈vbits` `b2∈vbits` `b1<b2` by simp qed next assume "¬ b1<b2" with e i u `b1∈vbits` show ?thesis using assms by simp qed next assume "b2∉vbits" with e i u `b1∈vbits` show ?thesis using assms by simp qed next case u2: (UINT b2 v2) then show ?thesis proof cases assume "b2∈vbits" show ?thesis proof cases assume "v1=v2" with assms show ?thesis using e u u2 `b1∈vbits` `b2∈vbits` by simp next assume "¬ v1=v2" with assms show ?thesis using e u u2 `b1∈vbits` `b2∈vbits` by simp qed next assume "¬b2∈vbits" with e u u2 `b1∈vbits` show ?thesis using assms by simp qed next case (ADDRESS x3) with e u `b1∈vbits` show ?thesis using assms by simp next case (BALANCE x4) with e u `b1∈vbits` show ?thesis using assms by simp next case THIS with e u `b1∈vbits` show ?thesis using assms by simp next case SENDER with e u `b1∈vbits` show ?thesis using assms by simp next case VALUE with e u `b1∈vbits` show ?thesis using assms by simp next case TRUE with e u `b1∈vbits` show ?thesis using assms by simp next case FALSE with e u `b1∈vbits` show ?thesis using assms by simp next case (LVAL x7) with e u `b1∈vbits` show ?thesis using assms by simp next case (PLUS x81 x82) with e u `b1∈vbits` show ?thesis using assms by simp next case (MINUS x91 x92) with e u `b1∈vbits` show ?thesis using assms by simp next case (EQUAL x101 x102) with e u `b1∈vbits` show ?thesis using assms by simp next case (LESS x111 x112) with e u `b1∈vbits` show ?thesis using assms by simp next case (AND x121 x122) with e u `b1∈vbits` show ?thesis using assms by simp next case (OR x131 x132) with e u `b1∈vbits` show ?thesis using assms by simp next case (NOT x131) with e u `b1∈vbits` show ?thesis using assms by simp next case (CALL x181 x182) with e u `b1∈vbits` show ?thesis using assms by simp next case (ECALL x191 x192 x193 x194) with e u `b1∈vbits` show ?thesis using assms by simp qed next assume "¬ b1∈vbits" with e u show ?thesis using assms by simp qed next case (ADDRESS x3) with e show ?thesis using assms by simp next case (BALANCE x4) with e show ?thesis using assms by simp next case THIS with e show ?thesis using assms by simp next case SENDER with e show ?thesis using assms by simp next case VALUE with e show ?thesis using assms by simp next case TRUE with e show ?thesis using assms by simp next case FALSE with e show ?thesis using assms by simp next case (LVAL x7) with e show ?thesis using assms by simp next case (PLUS x81 x82) with e show ?thesis using assms by simp next case (MINUS x91 x92) with e show ?thesis using assms by simp next case (EQUAL x101 x102) with e show ?thesis using assms by simp next case (LESS x111 x112) with e show ?thesis using assms by simp next case (AND x121 x122) with e show ?thesis using assms by simp next case (OR x131 x132) with e show ?thesis using assms by simp next case (NOT x131) with e show ?thesis using assms by simp next case (CALL x181 x182) with e show ?thesis using assms by simp next case (ECALL x191 x192 x193 x194) with e show ?thesis using assms by simp qed next case l: (LESS e1 e2) show ?thesis proof (cases "eupdate e1") case i: (INT b1 v1) show ?thesis proof cases assume "b1∈vbits" show ?thesis proof (cases "eupdate e2") case i2: (INT b2 v2) then show ?thesis proof cases assume "b2∈vbits" show ?thesis proof cases assume "v1<v2" with assms show ?thesis using l i i2 `b1∈vbits` `b2∈vbits` by simp next assume "¬ v1<v2" with assms show ?thesis using l i i2 `b1∈vbits` `b2∈vbits` by simp qed next assume "b2∉vbits" with l i i2 `b1∈vbits` show ?thesis using assms by simp qed next case u: (UINT b2 v2) then show ?thesis proof cases assume "b2∈vbits" show ?thesis proof cases assume "b2<b1" then show ?thesis proof cases assume "v1<v2" with assms show ?thesis using l i u `b1∈vbits` `b2∈vbits` `b2<b1` by simp next assume "¬ v1<v2" with assms show ?thesis using l i u `b1∈vbits` `b2∈vbits` `b2<b1` by simp qed next assume "¬ b2<b1" with l i u `b1∈vbits` show ?thesis using assms by simp qed next assume "b2∉vbits" with l i u `b1∈vbits` show ?thesis using assms by simp qed next case (ADDRESS x3) with l i `b1∈vbits` show ?thesis using assms by simp next case (BALANCE x4) with l i `b1∈vbits` show ?thesis using assms by simp next case THIS with l i `b1∈vbits` show ?thesis using assms by simp next case SENDER with l i `b1∈vbits` show ?thesis using assms by simp next case VALUE with l i `b1∈vbits` show ?thesis using assms by simp next case TRUE with l i `b1∈vbits` show ?thesis using assms by simp next case FALSE with l i `b1∈vbits` show ?thesis using assms by simp next case (LVAL x7) with l i `b1∈vbits` show ?thesis using assms by simp next case (PLUS x81 x82) with l i `b1∈vbits` show ?thesis using assms by simp next case (MINUS x91 x92) with l i `b1∈vbits` show ?thesis using assms by simp next case (EQUAL x101 x102) with l i `b1∈vbits` show ?thesis using assms by simp next case (LESS x111 x112) with l i `b1∈vbits` show ?thesis using assms by simp next case (AND x121 x122) with l i `b1∈vbits` show ?thesis using assms by simp next case (OR x131 x132) with l i `b1∈vbits` show ?thesis using assms by simp next case (NOT x131) with l i `b1∈vbits` show ?thesis using assms by simp next case (CALL x181 x182) with l i `b1∈vbits` show ?thesis using assms by simp next case (ECALL x191 x192 x193 x194) with l i `b1∈vbits` show ?thesis using assms by simp qed next assume "¬ b1∈vbits" with l i show ?thesis using assms by simp qed next case u: (UINT b1 v1) show ?thesis proof cases assume "b1∈vbits" show ?thesis proof (cases "eupdate e2") case i: (INT b2 v2) then show ?thesis proof cases assume "b2∈vbits" show ?thesis proof cases assume "b1<b2" then show ?thesis proof cases assume "v1<v2" with assms show ?thesis using l i u `b1∈vbits` `b2∈vbits` `b1<b2` by simp next assume "¬ v1<v2" with assms show ?thesis using l i u `b1∈vbits` `b2∈vbits` `b1<b2` by simp qed next assume "¬ b1<b2" with l i u `b1∈vbits` show ?thesis using assms by simp qed next assume "b2∉vbits" with l i u `b1∈vbits` show ?thesis using assms by simp qed next case u2: (UINT b2 v2) then show ?thesis proof cases assume "b2∈vbits" show ?thesis proof cases assume "v1<v2" with assms show ?thesis using l u u2 `b1∈vbits` `b2∈vbits` by simp next assume "¬ v1<v2" with assms show ?thesis using l u u2 `b1∈vbits` `b2∈vbits` by simp qed next assume "¬b2∈vbits" with l u u2 `b1∈vbits` show ?thesis using assms by simp qed next case (ADDRESS x3) with l u `b1∈vbits` show ?thesis using assms by simp next case (BALANCE x4) with l u `b1∈vbits` show ?thesis using assms by simp next case THIS with l u `b1∈vbits` show ?thesis using assms by simp next case SENDER with l u `b1∈vbits` show ?thesis using assms by simp next case VALUE with l u `b1∈vbits` show ?thesis using assms by simp next case TRUE with l u `b1∈vbits` show ?thesis using assms by simp next case FALSE with l u `b1∈vbits` show ?thesis using assms by simp next case (LVAL x7) with l u `b1∈vbits` show ?thesis using assms by simp next case (PLUS x81 x82) with l u `b1∈vbits` show ?thesis using assms by simp next case (MINUS x91 x92) with l u `b1∈vbits` show ?thesis using assms by simp next case (EQUAL x101 x102) with l u `b1∈vbits` show ?thesis using assms by simp next case (LESS x111 x112) with l u `b1∈vbits` show ?thesis using assms by simp next case (AND x121 x122) with l u `b1∈vbits` show ?thesis using assms by simp next case (OR x131 x132) with l u `b1∈vbits` show ?thesis using assms by simp next case (NOT x131) with l u `b1∈vbits` show ?thesis using assms by simp next case (CALL x181 x182) with l u `b1∈vbits` show ?thesis using assms by simp next case (ECALL x191 x192 x193 x194) with l u `b1∈vbits` show ?thesis using assms by simp qed next assume "¬ b1∈vbits" with l u show ?thesis using assms by simp qed next case (ADDRESS x3) with l show ?thesis using assms by simp next case (BALANCE x4) with l show ?thesis using assms by simp next case THIS with l show ?thesis using assms by simp next case SENDER with l show ?thesis using assms by simp next case VALUE with l show ?thesis using assms by simp next case TRUE with l show ?thesis using assms by simp next case FALSE with l show ?thesis using assms by simp next case (LVAL x7) with l show ?thesis using assms by simp next case (PLUS x81 x82) with l show ?thesis using assms by simp next case (MINUS x91 x92) with l show ?thesis using assms by simp next case (EQUAL x101 x102) with l show ?thesis using assms by simp next case (LESS x111 x112) with l show ?thesis using assms by simp next case (AND x121 x122) with l show ?thesis using assms by simp next case (OR x131 x132) with l show ?thesis using assms by simp next case (NOT x131) with l show ?thesis using assms by simp next case (CALL x181 x182) with l show ?thesis using assms by simp next case (ECALL x191 x192 x193 x194) with l show ?thesis using assms by simp qed next case a: (AND e1 e2) show ?thesis proof (cases "eupdate e1") case (INT x11 x12) with a show ?thesis using assms by simp next case (UINT x21 x22) with a show ?thesis using assms by simp next case (ADDRESS x3) with a show ?thesis using assms by simp next case (BALANCE x4) with a show ?thesis using assms by simp next case THIS with a show ?thesis using assms by simp next case SENDER with a show ?thesis using assms by simp next case VALUE with a show ?thesis using assms by simp next case t: TRUE show ?thesis proof (cases "eupdate e2") case (INT x11 x12) with a t show ?thesis using assms by simp next case (UINT x21 x22) with a t show ?thesis using assms by simp next case (ADDRESS x3) with a t show ?thesis using assms by simp next case (BALANCE x4) with a t show ?thesis using assms by simp next case THIS with a t show ?thesis using assms by simp next case SENDER with a t show ?thesis using assms by simp next case VALUE with a t show ?thesis using assms by simp next case TRUE with a t show ?thesis using assms by simp next case FALSE with a t show ?thesis using assms by simp next case (LVAL x7) with a t show ?thesis using assms by simp next case (PLUS x81 x82) with a t show ?thesis using assms by simp next case (MINUS x91 x92) with a t show ?thesis using assms by simp next case (EQUAL x101 x102) with a t show ?thesis using assms by simp next case (LESS x111 x112) with a t show ?thesis using assms by simp next case (AND x121 x122) with a t show ?thesis using assms by simp next case (OR x131 x132) with a t show ?thesis using assms by simp next case (NOT x131) with a t show ?thesis using assms by simp next case (CALL x181 x182) with a t show ?thesis using assms by simp next case (ECALL x191 x192 x193 x194) with a t show ?thesis using assms by simp qed next case f: FALSE show ?thesis proof (cases "eupdate e2") case (INT x11 x12) with a f show ?thesis using assms by simp next case (UINT x21 x22) with a f show ?thesis using assms by simp next case (ADDRESS x3) with a f show ?thesis using assms by simp next case (BALANCE x4) with a f show ?thesis using assms by simp next case THIS with a f show ?thesis using assms by simp next case SENDER with a f show ?thesis using assms by simp next case VALUE with a f show ?thesis using assms by simp next case TRUE with a f show ?thesis using assms by simp next case FALSE with a f show ?thesis using assms by simp next case (LVAL x7) with a f show ?thesis using assms by simp next case (PLUS x81 x82) with a f show ?thesis using assms by simp next case (MINUS x91 x92) with a f show ?thesis using assms by simp next case (EQUAL x101 x102) with a f show ?thesis using assms by simp next case (LESS x111 x112) with a f show ?thesis using assms by simp next case (AND x121 x122) with a f show ?thesis using assms by simp next case (OR x131 x132) with a f show ?thesis using assms by simp next case (NOT x131) with a f show ?thesis using assms by simp next case (CALL x181 x182) with a f show ?thesis using assms by simp next case (ECALL x191 x192 x193 x194) with a f show ?thesis using assms by simp qed next case (LVAL x7) with a show ?thesis using assms by simp next case (PLUS x81 x82) with a show ?thesis using assms by simp next case (MINUS x91 x92) with a show ?thesis using assms by simp next case (EQUAL x101 x102) with a show ?thesis using assms by simp next case (LESS x111 x112) with a show ?thesis using assms by simp next case (AND x121 x122) with a show ?thesis using assms by simp next case (OR x131 x132) with a show ?thesis using assms by simp next case (NOT x131) with a show ?thesis using assms by simp next case (CALL x181 x182) with a show ?thesis using assms by simp next case (ECALL x191 x192 x193 x194) with a show ?thesis using assms by simp qed next case o: (OR e1 e2) show ?thesis proof (cases "eupdate e1") case (INT x11 x12) with o show ?thesis using assms by simp next case (UINT x21 x22) with o show ?thesis using assms by simp next case (ADDRESS x3) with o show ?thesis using assms by simp next case (BALANCE x4) with o show ?thesis using assms by simp next case THIS with o show ?thesis using assms by simp next case SENDER with o show ?thesis using assms by simp next case VALUE with o show ?thesis using assms by simp next case t: TRUE show ?thesis proof (cases "eupdate e2") case (INT x11 x12) with o t show ?thesis using assms by simp next case (UINT x21 x22) with o t show ?thesis using assms by simp next case (ADDRESS x3) with o t show ?thesis using assms by simp next case (BALANCE x4) with o t show ?thesis using assms by simp next case THIS with o t show ?thesis using assms by simp next case SENDER with o t show ?thesis using assms by simp next case VALUE with o t show ?thesis using assms by simp next case TRUE with o t show ?thesis using assms by simp next case FALSE with o t show ?thesis using assms by simp next case (LVAL x7) with o t show ?thesis using assms by simp next case (PLUS x81 x82) with o t show ?thesis using assms by simp next case (MINUS x91 x92) with o t show ?thesis using assms by simp next case (EQUAL x101 x102) with o t show ?thesis using assms by simp next case (LESS x111 x112) with o t show ?thesis using assms by simp next case (AND x121 x122) with o t show ?thesis using assms by simp next case (OR x131 x132) with o t show ?thesis using assms by simp next case (NOT x131) with o t show ?thesis using assms by simp next case (CALL x181 x182) with o t show ?thesis using assms by simp next case (ECALL x191 x192 x193 x194) with o t show ?thesis using assms by simp qed next case f: FALSE show ?thesis proof (cases "eupdate e2") case (INT x11 x12) with o f show ?thesis using assms by simp next case (UINT x21 x22) with o f show ?thesis using assms by simp next case (ADDRESS x3) with o f show ?thesis using assms by simp next case (BALANCE x4) with o f show ?thesis using assms by simp next case THIS with o f show ?thesis using assms by simp next case SENDER with o f show ?thesis using assms by simp next case VALUE with o f show ?thesis using assms by simp next case TRUE with o f show ?thesis using assms by simp next case FALSE with o f show ?thesis using assms by simp next case (LVAL x7) with o f show ?thesis using assms by simp next case (PLUS x81 x82) with o f show ?thesis using assms by simp next case (MINUS x91 x92) with o f show ?thesis using assms by simp next case (EQUAL x101 x102) with o f show ?thesis using assms by simp next case (LESS x111 x112) with o f show ?thesis using assms by simp next case (AND x121 x122) with o f show ?thesis using assms by simp next case (OR x131 x132) with o f show ?thesis using assms by simp next case (NOT x131) with o f show ?thesis using assms by simp next case (CALL x181 x182) with o f show ?thesis using assms by simp next case (ECALL x191 x192 x193 x194) with o f show ?thesis using assms by simp qed next case (LVAL x7) with o show ?thesis using assms by simp next case (PLUS x81 x82) with o show ?thesis using assms by simp next case (MINUS x91 x92) with o show ?thesis using assms by simp next case (EQUAL x101 x102) with o show ?thesis using assms by simp next case (LESS x111 x112) with o show ?thesis using assms by simp next case (AND x121 x122) with o show ?thesis using assms by simp next case (OR x131 x132) with o show ?thesis using assms by simp next case (NOT x131) with o show ?thesis using assms by simp next case (CALL x181 x182) with o show ?thesis using assms by simp next case (ECALL x191 x192 x193 x194) with o show ?thesis using assms by simp qed next case o: (NOT e1) show ?thesis proof (cases "eupdate e1") case (INT x11 x12) with o show ?thesis using assms by simp next case (UINT x21 x22) with o show ?thesis using assms by simp next case (ADDRESS x3) with o show ?thesis using assms by simp next case (BALANCE x4) with o show ?thesis using assms by simp next case THIS with o show ?thesis using assms by simp next case SENDER with o show ?thesis using assms by simp next case VALUE with o show ?thesis using assms by simp next case t: TRUE with o show ?thesis using assms by simp next case f: FALSE with o show ?thesis using assms by simp next case (LVAL x7) with o show ?thesis using assms by simp next case (PLUS x81 x82) with o show ?thesis using assms by simp next case (MINUS x91 x92) with o show ?thesis using assms by simp next case (EQUAL x101 x102) with o show ?thesis using assms by simp next case (LESS x111 x112) with o show ?thesis using assms by simp next case (AND x121 x122) with o show ?thesis using assms by simp next case (OR x131 x132) with o show ?thesis using assms by simp next case (NOT x131) with o show ?thesis using assms by simp next case (CALL x181 x182) with o show ?thesis using assms by simp next case (ECALL x191 x192 x193 x194) with o show ?thesis using assms by simp qed next case (CALL x181 x182) with assms show ?thesis by simp next case (ECALL x191 x192 x193 x194) with assms show ?thesis by simp qed lemma update_bounds_uint: assumes "eupdate ex = UINT b v" and "b∈vbits" shows "v < 2^b ∧ v ≥ 0" proof (cases ex) case (INT b' v') with assms show ?thesis proof cases assume "b'∈vbits" show ?thesis proof cases assume "v'≥0" with INT show ?thesis using assms `b'∈vbits` by simp next assume "¬ v'≥0" with INT show ?thesis using assms `b'∈vbits` by simp qed next assume "¬ b'∈vbits" with INT show ?thesis using assms by simp qed next case (UINT b' v') then show ?thesis proof cases assume "b'∈vbits" with UINT show ?thesis using assms by auto next assume "¬ b'∈vbits" with UINT show ?thesis using assms by auto qed next case (ADDRESS x3) with assms show ?thesis by simp next case (BALANCE x4) with assms show ?thesis by simp next case THIS with assms show ?thesis by simp next case SENDER with assms show ?thesis by simp next case VALUE with assms show ?thesis by simp next case TRUE with assms show ?thesis by simp next case FALSE with assms show ?thesis by simp next case (LVAL x7) with assms show ?thesis by