From d7422935319e674198edb42350f11f70d8195ff6 Mon Sep 17 00:00:00 2001 From: Guillaume Claret Date: Wed, 11 Dec 2024 15:21:29 +0100 Subject: [PATCH] coq-of-solidity: remove the submodule for coq-evm and use copy and paste instead --- .github/workflows/coq.yml | 7 - .gitmodules | 3 - coq/CoqOfSolidity/CoqEvm/Arith/Nibble.v | 626 ++++++++++++++++ coq/CoqOfSolidity/CoqEvm/Arith/SInt.v | 427 +++++++++++ coq/CoqOfSolidity/CoqEvm/Arith/UInt.v | 458 ++++++++++++ coq/CoqOfSolidity/CoqEvm/Arith/UInt63.v | 223 ++++++ coq/CoqOfSolidity/CoqEvm/Arith/UInt64.v | 668 ++++++++++++++++++ .../CoqEvm/Containers/Tuplevector.v | 247 +++++++ coq/CoqOfSolidity/CoqEvm/Containers/Vec16.v | 290 ++++++++ coq/CoqOfSolidity/CoqEvm/Containers/Vec8.v | 67 ++ coq/CoqOfSolidity/CoqEvm/Crypto/BLAKE2b.v | 133 ++++ coq/CoqOfSolidity/CoqEvm/Crypto/Keccak.v | 419 +++++++++++ coq/CoqOfSolidity/CoqEvm/Crypto/RIPEMD160.v | 239 +++++++ coq/CoqOfSolidity/CoqEvm/Crypto/SHA256.v | 282 ++++++++ coq/CoqOfSolidity/CoqEvm/Instructions.v | 660 +++++++++++++++++ coq/CoqOfSolidity/CoqEvm/JumpDest.v | 247 +++++++ coq/CoqOfSolidity/CoqEvm/LICENSE | 201 ++++++ coq/CoqOfSolidity/CoqEvm/Lib2/Arith2.v | 530 ++++++++++++++ coq/CoqOfSolidity/CoqEvm/Lib2/List2.v | 37 + coq/CoqOfSolidity/CoqEvm/Lib2/ListSet2.v | 332 +++++++++ coq/CoqOfSolidity/CoqEvm/Lib2/Logic2.v | 37 + coq/CoqOfSolidity/CoqEvm/Lib2/QArith2.v | 33 + coq/CoqOfSolidity/CoqEvm/Lib2/Vector2.v | 39 + coq/CoqOfSolidity/CoqEvm/README.md | 25 + coq/CoqOfSolidity/blacklist.txt | 3 +- coq/CoqOfSolidity/simulations/CoqOfSolidity.v | 8 +- coq/third-party/coq-evm | 1 - 27 files changed, 6226 insertions(+), 16 deletions(-) create mode 100644 coq/CoqOfSolidity/CoqEvm/Arith/Nibble.v create mode 100644 coq/CoqOfSolidity/CoqEvm/Arith/SInt.v create mode 100644 coq/CoqOfSolidity/CoqEvm/Arith/UInt.v create mode 100644 coq/CoqOfSolidity/CoqEvm/Arith/UInt63.v create mode 100644 coq/CoqOfSolidity/CoqEvm/Arith/UInt64.v create mode 100644 coq/CoqOfSolidity/CoqEvm/Containers/Tuplevector.v create mode 100644 coq/CoqOfSolidity/CoqEvm/Containers/Vec16.v create mode 100644 coq/CoqOfSolidity/CoqEvm/Containers/Vec8.v create mode 100644 coq/CoqOfSolidity/CoqEvm/Crypto/BLAKE2b.v create mode 100644 coq/CoqOfSolidity/CoqEvm/Crypto/Keccak.v create mode 100644 coq/CoqOfSolidity/CoqEvm/Crypto/RIPEMD160.v create mode 100644 coq/CoqOfSolidity/CoqEvm/Crypto/SHA256.v create mode 100644 coq/CoqOfSolidity/CoqEvm/Instructions.v create mode 100644 coq/CoqOfSolidity/CoqEvm/JumpDest.v create mode 100644 coq/CoqOfSolidity/CoqEvm/LICENSE create mode 100644 coq/CoqOfSolidity/CoqEvm/Lib2/Arith2.v create mode 100644 coq/CoqOfSolidity/CoqEvm/Lib2/List2.v create mode 100644 coq/CoqOfSolidity/CoqEvm/Lib2/ListSet2.v create mode 100644 coq/CoqOfSolidity/CoqEvm/Lib2/Logic2.v create mode 100644 coq/CoqOfSolidity/CoqEvm/Lib2/QArith2.v create mode 100644 coq/CoqOfSolidity/CoqEvm/Lib2/Vector2.v create mode 100644 coq/CoqOfSolidity/CoqEvm/README.md delete mode 160000 coq/third-party/coq-evm diff --git a/.github/workflows/coq.yml b/.github/workflows/coq.yml index 09b4d11c27df..83ce3f6ac9ff 100644 --- a/.github/workflows/coq.yml +++ b/.github/workflows/coq.yml @@ -38,13 +38,6 @@ jobs: startGroup "Check that the diff is empty (excluding submodules)" git -c color.ui=always diff --exit-code --ignore-submodules=dirty endGroup - startGroup "Install Coq dependencies" - cd coq/third-party/coq-evm - ./configure - make - make install - cd ../../.. - endGroup startGroup "Compile Coq project" cd coq/CoqOfSolidity make diff --git a/.gitmodules b/.gitmodules index 6aefecf97dfb..47bcbb4fde94 100644 --- a/.gitmodules +++ b/.gitmodules @@ -7,6 +7,3 @@ [submodule "deps/fmtlib"] path = deps/fmtlib url = https://github.com/fmtlib/fmt.git -[submodule "coq/third-party/coq-evm"] - path = coq/third-party/coq-evm - url = https://github.com/formal-land/coq-evm.git diff --git a/coq/CoqOfSolidity/CoqEvm/Arith/Nibble.v b/coq/CoqOfSolidity/CoqEvm/Arith/Nibble.v new file mode 100644 index 000000000000..f10dd098481b --- /dev/null +++ b/coq/CoqOfSolidity/CoqEvm/Arith/Nibble.v @@ -0,0 +1,626 @@ +From Coq Require Import Ascii. +From Coq Require Import NArith. +From Coq Require Import ZArith. +From Coq Require Import Uint63. +From Coq Require Import Lia. +From Coq Require String Ascii. + +From CoqOfSolidity Require Import UInt63 Arith2. + +Inductive nibble := Nibble (x3 x2 x1 x0: bool). +Inductive hex_digit := +| x0 | x1 | x2 | x3 +| x4 | x5 | x6 | x7 +| x8 | x9 | xA | xB +| xC | xD | xE | xF. + +Definition ascii_of_hex_digit (digit: hex_digit) (lower: bool) +: ascii +:= match digit with + | x0 => "0" + | x1 => "1" + | x2 => "2" + | x3 => "3" + | x4 => "4" + | x5 => "5" + | x6 => "6" + | x7 => "7" + | x8 => "8" + | x9 => "9" + | xA => if lower then "a" else "A" + | xB => if lower then "b" else "B" + | xC => if lower then "c" else "C" + | xD => if lower then "d" else "D" + | xE => if lower then "e" else "E" + | xF => if lower then "f" else "F" + end. + +Definition hex_digit_of_ascii (a: ascii) +: option hex_digit +:= match a with + | "0" => Some x0 + | "1" => Some x1 + | "2" => Some x2 + | "3" => Some x3 + | "4" => Some x4 + | "5" => Some x5 + | "6" => Some x6 + | "7" => Some x7 + | "8" => Some x8 + | "9" => Some x9 + | "a" | "A" => Some xA + | "b" | "B" => Some xB + | "c" | "C" => Some xC + | "d" | "D" => Some xD + | "e" | "E" => Some xE + | "f" | "F" => Some xF + | _ => None + end%char. + +Definition is_hex_digit (a: ascii) +:= match hex_digit_of_ascii a with + | Some _ => true + | None => false + end. + +Lemma hex_digit_of_ascii_of_hex_digit (h: hex_digit) (lower: bool): + hex_digit_of_ascii (ascii_of_hex_digit h lower) = Some h. +Proof. +destruct lower; destruct h; trivial. +Qed. + +Lemma is_hex_digit_true (a: ascii): + is_hex_digit a = true -> hex_digit_of_ascii a <> None. +Proof. +unfold is_hex_digit. now destruct hex_digit_of_ascii. +Qed. + +Definition hex_digit_of_ascii' (a: ascii) (ok: is_hex_digit a = true) +: hex_digit +:= match hex_digit_of_ascii a as h return _ = h -> _ with + | Some x => fun _ => x + | None => fun E => False_rect _ (is_hex_digit_true a ok E) + end eq_refl. + +Lemma hex_digit_of_ascii_of_hex_digit' (h: hex_digit) (lower: bool) + (ok: is_hex_digit (ascii_of_hex_digit h lower) = true): + hex_digit_of_ascii' (ascii_of_hex_digit h lower) ok = h. +Proof. +destruct lower; destruct h; trivial. +Qed. + +Definition nibble_of_hex_digit (digit: hex_digit) +: nibble +:= match digit with + | x0 => Nibble false false false false + | x1 => Nibble false false false true + | x2 => Nibble false false true false + | x3 => Nibble false false true true + | x4 => Nibble false true false false + | x5 => Nibble false true false true + | x6 => Nibble false true true false + | x7 => Nibble false true true true + | x8 => Nibble true false false false + | x9 => Nibble true false false true + | xA => Nibble true false true false + | xB => Nibble true false true true + | xC => Nibble true true false false + | xD => Nibble true true false true + | xE => Nibble true true true false + | xF => Nibble true true true true + end. + +Definition hex_digit_of_nibble (n: nibble) +: hex_digit +:= match n with + | Nibble false false false false => x0 + | Nibble false false false true => x1 + | Nibble false false true false => x2 + | Nibble false false true true => x3 + | Nibble false true false false => x4 + | Nibble false true false true => x5 + | Nibble false true true false => x6 + | Nibble false true true true => x7 + | Nibble true false false false => x8 + | Nibble true false false true => x9 + | Nibble true false true false => xA + | Nibble true false true true => xB + | Nibble true true false false => xC + | Nibble true true false true => xD + | Nibble true true true false => xE + | Nibble true true true true => xF + end. + +Lemma hex_digit_of_nibble_of_hex_digit (d: hex_digit): + hex_digit_of_nibble (nibble_of_hex_digit d) = d. +Proof. +destruct d; easy. +Qed. + +Lemma nibble_of_hex_digit_of_nibble (n: nibble): + nibble_of_hex_digit (hex_digit_of_nibble n) = n. +Proof. +destruct n as (a3, a2, a1, a0). +destruct a3; destruct a2; destruct a1; destruct a0; easy. +Qed. + +Definition N_of_hex_digit (digit: hex_digit) +: N +:= match digit with + | x0 => 0 + | x1 => 1 + | x2 => 2 + | x3 => 3 + | x4 => 4 + | x5 => 5 + | x6 => 6 + | x7 => 7 + | x8 => 8 + | x9 => 9 + | xA => 10 + | xB => 11 + | xC => 12 + | xD => 13 + | xE => 14 + | xF => 15 + end. + +Lemma N_of_hex_digit_ub (digit: hex_digit): + (N_of_hex_digit digit < 16)%N. +Proof. + destruct digit; cbn; rewrite<- N.ltb_lt; trivial. +Qed. + +Definition N_of_nibble (n: nibble) +: N +:= let f (a: bool) := if a then xI else xO in + match n with + | Nibble true a2 a1 a0 => Npos (f a0 (f a1 (f a2 xH))) + | Nibble false true a1 a0 => Npos (f a0 (f a1 xH)) + | Nibble false false true a0 => Npos (f a0 xH) + | Nibble false false false true => Npos xH + | Nibble false false false false => N0 + end. + +Lemma N_of_nibble_bound (n: nibble): + (N_of_nibble n < 16)%N. +Proof. + destruct n as (a3, a2, a1, a0); destruct a3; destruct a2; destruct a1; destruct a0; easy. +Qed. + +Lemma hex_digit_to_N_via_nibble (d: hex_digit): + N_of_nibble (nibble_of_hex_digit d) = N_of_hex_digit d. +Proof. + destruct d; easy. +Qed. + +Lemma nibble_to_N_via_hex_digit (n: nibble): + N_of_hex_digit (hex_digit_of_nibble n) = N_of_nibble n. +Proof. + destruct n as (a3, a2, a1, a0); destruct a3; destruct a2; destruct a1; destruct a0; easy. +Qed. + +Definition push_bit (n: N) (bit: bool) +: N +:= match n with + | N0 => if bit then 1 else 0 + | Npos p => Npos ((if bit then xI else xO) p) + end. + +Lemma push_bit_arith (n: N) (bit: bool): + push_bit n bit = (2 * n + if bit then 1 else 0)%N. +Proof. +destruct bit; now destruct n. +Qed. + +Definition last_bit (n: N) +: bool +:= match n with + | N0 | Npos (xO _) => false + | Npos xH | Npos (xI _) => true + end. + +Lemma last_bit_odd (n: N): + last_bit n = N.odd n. +Proof. +destruct n. { trivial. } +destruct p; easy. +Qed. + +Lemma push_bit_then_shr1 (n: N) (bit: bool): + N.div2 (push_bit n bit) = n. +Proof. + destruct n; destruct bit; easy. +Qed. + +Lemma last_of_push_bit (n: N) (bit: bool): + last_bit (push_bit n bit) = bit. +Proof. + destruct n; destruct bit; easy. +Qed. + +Lemma push_last_bit (n: N): + push_bit (N.div2 n) (last_bit n) = n. +Proof. + destruct n. easy. + destruct p; easy. +Qed. + +Definition push_nibble (n: N) (nib: nibble) +: N +:= match nib with + | Nibble a3 a2 a1 a0 => push_bit (push_bit (push_bit (push_bit n a3) a2) a1) a0 + end. + +Lemma push_nibble_arith (n: N) (nib: nibble): + push_nibble n nib = (16 * n + N_of_nibble nib)%N. +Proof. +destruct nib as (a3, a2, a1, a0). +unfold push_nibble. +repeat rewrite push_bit_arith. +repeat rewrite N.mul_add_distr_l. +repeat rewrite<- N.add_assoc. +f_equal. +{ now repeat rewrite N.mul_assoc. } +destruct a3; destruct a2; destruct a1; destruct a0; easy. +Qed. + +Definition pop_nibble (n: N) +: N * nibble +:= let a0 := last_bit n in + let n1 := N.div2 n in + let a1 := last_bit n1 in + let n2 := N.div2 n1 in + let a2 := last_bit n2 in + let n3 := N.div2 n2 in + let a3 := last_bit n3 in + let n4 := N.div2 n3 in + (n4, Nibble a3 a2 a1 a0). + +Lemma push_nibble_then_pop (n: N) (nib: nibble): + pop_nibble (push_nibble n nib) = (n, nib). +Proof. + destruct nib as (a3, a2, a1, a0). unfold pop_nibble. cbn. + repeat rewrite push_bit_then_shr1. + now repeat rewrite last_of_push_bit. +Qed. + +Lemma pop_nibble_then_push (n: N): + push_nibble (fst (pop_nibble n)) (snd (pop_nibble n)) = n. +Proof. + destruct n. easy. + unfold pop_nibble. unfold fst. unfold snd. + unfold push_nibble. + now repeat rewrite push_last_bit. +Qed. + +Definition nibble_of_N (n: N) +: nibble +:= snd (pop_nibble n). + +Lemma N_of_nibble_of_N (n: N) (B: (n < 16)%N): + N_of_nibble (nibble_of_N n) = n. +Proof. +assert(P := pop_nibble_then_push n). +rewrite push_nibble_arith in P. +unfold nibble_of_N. +remember (N_of_nibble _) as k. clear Heqk. +remember (fst _) as z. clear Heqz. +lia. +Qed. + +Definition pop_nibble_arith (a b: N) (B: (b < 16)%N): + pop_nibble (16 * a + b) = (a, nibble_of_N b). +Proof. +enough (E: push_nibble a (nibble_of_N b) = (16 * a + b)%N). +{ rewrite<- E. apply push_nibble_then_pop. } +rewrite push_nibble_arith. +f_equal. apply N_of_nibble_of_N. +assumption. +Qed. + +Definition pop_nibble_arith_small (b: N) (B: (b < 16)%N): + pop_nibble b = (0%N, nibble_of_N b). +Proof. +rewrite<- (pop_nibble_arith _ _ B). +f_equal. +Qed. + +Definition nibble_of_uint63 (i: int) +:= Nibble (0 + ((if a8 then 8%uint63 else 0%uint63) + lor + (if a4 then 4%uint63 else 0%uint63) + lor + (if a2 then 2%uint63 else 0%uint63) + lor + (if a1 then 1%uint63 else 0%uint63))%uint63 + end. + +Lemma nibble_of_uint63_of_nibble (n: nibble): + nibble_of_uint63 (uint63_of_nibble n) = n. +Proof. +destruct n as (a3, a2, a1, a0). +destruct a3; destruct a2; destruct a1; destruct a0; easy. +Qed. + +(** A direct conversion from a native int to a hex digit via an if cascade. *) +Definition hex_digit_of_uint63 (i: int) +:= if (0 Nibble a3 a2 a1 a0 + end. + +Definition high_nibble (b: byte) +: nibble +:= match b with + | Byte a7 a6 a5 a4 _ _ _ _ => Nibble a7 a6 a5 a4 + end. + +Definition byte_of_nibbles (high low: nibble) +: byte +:= match high with + | Nibble a7 a6 a5 a4 => + match low with + | Nibble a3 a2 a1 a0 => + Byte a7 a6 a5 a4 a3 a2 a1 a0 + end + end. + +Lemma low_nibble_ok (high low: nibble): + low_nibble (byte_of_nibbles high low) = low. +Proof. + destruct low. destruct high. easy. +Qed. + +Lemma high_nibble_ok (high low: nibble): + high_nibble (byte_of_nibbles high low) = high. +Proof. + destruct low. destruct high. easy. +Qed. + +Lemma byte_of_nibbles_ok (b: byte): + byte_of_nibbles (high_nibble b) (low_nibble b) = b. +Proof. + now destruct b. +Qed. + +Definition byte_of_hex_digits (high low: hex_digit) +: byte +:= byte_of_nibbles (nibble_of_hex_digit high) (nibble_of_hex_digit low). + +Definition hex_digits_of_byte (b: byte) +: hex_digit * hex_digit +:= (hex_digit_of_nibble (high_nibble b), + hex_digit_of_nibble (low_nibble b)). + +Definition N_of_byte (b: byte) +: N +:= let f (a: bool) := if a then xI else xO in + match b with + | Byte true a6 a5 a4 a3 a2 a1 a0 => Npos (f a0 (f a1 (f a2 (f a3 (f a4 (f a5 (f a6 xH))))))) + | Byte false true a5 a4 a3 a2 a1 a0 => Npos (f a0 (f a1 (f a2 (f a3 (f a4 (f a5 xH)))))) + | Byte false false true a4 a3 a2 a1 a0 => Npos (f a0 (f a1 (f a2 (f a3 (f a4 xH))))) + | Byte false false false true a3 a2 a1 a0 => Npos (f a0 (f a1 (f a2 (f a3 xH)))) + | Byte false false false false true a2 a1 a0 => Npos (f a0 (f a1 (f a2 xH))) + | Byte false false false false false true a1 a0 => Npos (f a0 (f a1 xH)) + | Byte false false false false false false true a0 => Npos (f a0 xH) + | Byte false false false false false false false true => Npos xH + | Byte false false false false false false false false => N0 + end. + +Definition pop_byte (n: N) +: N * byte +:= let (n1, x) := pop_nibble n in + let (n2, y) := pop_nibble n1 in + (n2, byte_of_nibbles y x). + +Definition byte_of_N (n: N) +: byte +:= snd (pop_byte n). + +Lemma byte_of_N_arith (high low: N) + (H16: (high < 16)%N) + (L16: (low < 16)%N): + byte_of_N (16 * high + low) = byte_of_nibbles (nibble_of_N high) (nibble_of_N low). +Proof. +unfold byte_of_N. unfold pop_byte. +rewrite (pop_nibble_arith _ _ L16). +remember (nibble_of_N low) as nib. clear Heqnib low L16. +rewrite (pop_nibble_arith_small _ H16). +trivial. +Qed. + +Lemma byte_of_N_of_byte (b: byte): + byte_of_N (N_of_byte b) = b. +Proof. +destruct b as (a7, a6, a5, a4, a3, a2, a1, a0). +destruct a7; destruct a6; destruct a5; destruct a4; +destruct a3; destruct a2; destruct a1; destruct a0; trivial. +Qed. + +Definition byte_of_int (i: int) +:= Byte (0 + (let a7 := if b7 then 128 else 0 in + let a6 := if b6 then 64 lor a7 else a7 in + let a5 := if b5 then 32 lor a6 else a6 in + let a4 := if b4 then 16 lor a5 else a5 in + let a3 := if b3 then 8 lor a4 else a4 in + let a2 := if b2 then 4 lor a3 else a3 in + let a1 := if b1 then 2 lor a2 else a2 in + if b0 then 1 lor a1 else a1)%uint63 + end. + +Lemma byte_of_int_of_byte (b: byte): + byte_of_int (int_of_byte b) = b. +Proof. +destruct b as (a7, a6, a5, a4, a3, a2, a1, a0). +destruct a7; destruct a6; destruct a5; destruct a4; +destruct a3; destruct a2; destruct a1; destruct a0; trivial. +Qed. + +Fixpoint hex_of_bytes (b: list byte) (lower: bool) +: String.string +:= match b with + | nil => String.EmptyString + | (h :: t)%list => + let (hi, lo) := hex_digits_of_byte h in + String.String (ascii_of_hex_digit hi lower) + (String.String (ascii_of_hex_digit lo lower) + (hex_of_bytes t lower)) + end. + +Definition byte_of_ascii (a: ascii) +:= let (b0, b1, b2, b3, b4, b5, b6, b7) := a in Byte b7 b6 b5 b4 b3 b2 b1 b0. + +Fixpoint bytes_of_string (s: String.string) +: list byte +:= match s with + | String.EmptyString => nil + | String.String h t => byte_of_ascii h :: bytes_of_string t + end. + +(* TODO: to Str *) +Fixpoint string_forallb (f: ascii -> bool) (s: String.string) +: bool +:= match s with + | String.EmptyString => true + | String.String h t => f h && string_forallb f t + end. + +Lemma string_forallb_iff (f: ascii -> bool) (s: String.string): + string_forallb f s = List.forallb f (String.list_ascii_of_string s). +Proof. +induction s; cbn. { trivial. } +f_equal. exact IHs. +Qed. + +Definition is_hex_string (s: String.string) +: bool +:= Nat.even (String.length s) + && + string_forallb is_hex_digit s. + +Fixpoint bytes_of_hex (s: String.string) + (ok: is_hex_string s = true) +: list byte. +Proof. +refine(match s as s' return s = s' -> _ with + | String.EmptyString => fun _ => nil + | String.String h String.EmptyString => fun E => _ + | String.String hi (String.String lo rest) => fun E => + (byte_of_hex_digits (hex_digit_of_ascii' hi _) (hex_digit_of_ascii' lo _) + :: + bytes_of_hex rest _)%list + end eq_refl); + unfold is_hex_string in ok; unfold string_forallb in ok; subst; cbn in *; + repeat (rewrite Bool.andb_true_iff in *); try easy. +fold string_forallb in ok. unfold is_hex_string. +rewrite Bool.andb_true_iff. +tauto. +Defined. + +Lemma ascii_of_hex_digit_is_hex_digit (h: hex_digit) (lower: bool): + is_hex_digit (ascii_of_hex_digit h lower) = true. +Proof. +unfold is_hex_digit. now rewrite hex_digit_of_ascii_of_hex_digit. +Qed. + +Lemma hex_of_bytes_is_hex_string (b: list byte) (lower: bool) +: is_hex_string (hex_of_bytes b lower) = true. +Proof. +unfold is_hex_string. repeat (rewrite Bool.andb_true_iff). +split; induction b; try easy. +cbn. repeat rewrite ascii_of_hex_digit_is_hex_digit. +rewrite IHb. trivial. +Qed. + +Lemma bytes_of_hex_of_bytes (b: list byte) (lower: bool): + let hex := hex_of_bytes b lower in + forall ok: is_hex_string hex = true, + bytes_of_hex hex ok = b. +Proof. +induction b. { easy. } +cbn zeta in *. intro ok. +cbn. f_equal. +{ + unfold byte_of_hex_digits. + repeat rewrite hex_digit_of_ascii_of_hex_digit'. + repeat rewrite nibble_of_hex_digit_of_nibble. + apply byte_of_nibbles_ok. +} +apply IHb. +Qed. diff --git a/coq/CoqOfSolidity/CoqEvm/Arith/SInt.v b/coq/CoqOfSolidity/CoqEvm/Arith/SInt.v new file mode 100644 index 000000000000..4b4b574176fc --- /dev/null +++ b/coq/CoqOfSolidity/CoqEvm/Arith/SInt.v @@ -0,0 +1,427 @@ +(* Ethereum instructions that deal with signed ints: SDIV SMOD SIGNEXTEND SLT SGT SAR *) + +From Coq Require Import NArith ZArith Lia. + +Require Import UInt. +Require Import Arith2. + +Local Open Scope Z_scope. + +Definition sint (width: N) := bound_int (- 2 ^ (Z.of_N width - 1)) + ( 2 ^ (Z.of_N width - 1)). + +Definition Z_of_sint {width: N} (z: sint width): Z := Z_of_bound_int z. + +Local Lemma uint_of_sint_pos_spec {width : N} + (a: sint width) + (p: positive) + (E: Z_of_sint a = Z.pos p): + (N.pos p < 2 ^ width)%N. +Proof. +assert (B := bound_int_upper a). +unfold Z_of_sint in E. rewrite E in B. +clear E a. +apply N2Z.inj_lt. +rewrite N2Z.inj_pow. +cbn. +apply (Z.lt_trans _ _ _ B). +apply Z.pow_lt_mono_r. { now rewrite<- Z.ltb_lt. } +{ apply N2Z.is_nonneg. } +apply Z.lt_pred_l. +Qed. + +Local Lemma uint_of_sint_neg_spec {width : N} + (a: sint width) + (p: positive) + (E: Z_of_sint a = Z.neg p): + (2 ^ width - N.pos p < 2 ^ width)%N. +Proof. +assert (B := bound_int_lower a). unfold Z_of_sint in E. +rewrite E in B. clear E a. +apply N.sub_lt. 2:{ now apply N_ne_0_gt_0. } +apply N2Z.inj_le. +rewrite N2Z.inj_pow. +cbn. +rewrite Z.opp_le_mono in B. +cbn in B. rewrite Z.opp_involutive in B. +apply (Z.le_trans _ _ _ B). +apply Z.pow_le_mono_r. { now rewrite<- Z.ltb_lt. } +apply Z.lt_le_incl. +apply Z.lt_pred_l. +Qed. + +(** Convert an uint to a sint in a usual way: + split the range of uints in half and + map the higher half into the negatives. + *) + +Definition uint_of_sint {width: N} (a: sint width) +: uint width +:= let z := Z_of_sint a in + match z as z' return z = z' -> _ with + | Z0 => fun _ => uint_0 width + | Zpos p => fun E => uint_of_N (Npos p) (uint_of_sint_pos_spec a p E) + | Zneg p => fun E => uint_of_N (2^width - Npos p)%N (uint_of_sint_neg_spec a p E) + end eq_refl. (* I don't like this ^ subtraction in N but it's too late *) + + +Lemma Z_of_uint_of_sint {width: N} (a: sint width): + Z_of_uint (uint_of_sint a) = + let z := Z_of_sint a in + match z with + | Z0 | Zpos _ => z + | Zneg p => (z + 2^(Z.of_N width))%Z + end. +Proof. +unfold Z_of_uint. +unfold uint_of_sint. +remember (fun p (E : Z_of_sint a = Z.pos p) => uint_of_N (N.pos p) (uint_of_sint_pos_spec a p E)) + as branch_pos. +remember (fun p (E : Z_of_sint a = Z.neg p) => + uint_of_N (2 ^ width - N.pos p) (uint_of_sint_neg_spec a p E)) + as branch_neg. +assert(PosOk: forall p E, Z_of_bound_int (branch_pos p E) = Zpos p). +{ intros. subst. trivial. } +assert(NegOk: forall p E, Z_of_bound_int (branch_neg p E) = Zneg p + 2^(Z.of_N width)). +{ + intros. subst. cbn. clear PosOk. + assert (P: 0 < 2 ^ Z.of_N width). { apply Z_0_lt_pow2. apply N2Z.is_nonneg. } + remember (2 ^ Z.of_N width) as m. + destruct m. { now apply Z.lt_irrefl in P. } + 2:{ exfalso. rewrite<- Z.ltb_lt in P. cbn in P. discriminate. } + clear P. + unfold Z_of_sint in E. + rewrite<- Pos2Z.add_pos_neg. + rewrite Heqm. clear Heqm. + assert (U := bound_int_lower a). + assert (Q: (N.pos p <= 2 ^ width)%N). + { + rewrite E in U. + rewrite<- (Pos2Z.opp_pos p) in U. + rewrite<- Z.opp_le_mono in U. + rewrite N2Z.inj_le. + rewrite N2Z.inj_pow. cbn. + apply (Z.le_trans _ _ _ U). + apply Z.pow_le_mono_r. { now rewrite<- Z.ltb_lt. } + apply Z.le_pred_l. + } + rewrite N2Z.inj_sub; try assumption. + rewrite N2Z.inj_pow. cbn. + rewrite<- (Pos2Z.opp_pos p). rewrite Z.add_opp_r. trivial. +} +clear Heqbranch_pos Heqbranch_neg. +destruct (Z_of_sint a); easy. +Qed. + +Local Lemma sint_of_uint_high {width: positive} + (z: Z) + (H : (Z.ones (Zpos width - 1) _ + then fun H => bound_int_of_Z_conj (z - 2^(Zpos width)) + (sint_of_uint_high z H (bound_int_upper a)) + else fun L => bound_int_of_Z_conj z + (sint_of_uint_low z L (bound_int_lower a))) + eq_refl. + +(* Same but without proofs: *) +Lemma Z_of_sint_of_uint {width: positive} (a: uint (Npos width)): + Z_of_sint (sint_of_uint a) = + let z := Z_of_uint a in + if (Z.ones (Zpos width - 1) + bound_int_of_Z_conj (Z_of_uint a - 2 ^ Z.pos width) + (sint_of_uint_high (Z_of_uint a) H (bound_int_upper a))) + as high_branch. +remember (fun L : (Z.ones (Z.pos width - 1) + bound_int_of_Z_conj (Z_of_uint a) (sint_of_uint_low (Z_of_uint a) L (bound_int_lower a))) + as low_branch. +assert(HighOk: forall H, Z_of_bound_int (high_branch H) = Z_of_uint a - 2 ^ Z.pos width). +{ intro. subst. trivial. } +assert(LowOk: forall L, Z_of_bound_int (low_branch L) = Z_of_uint a). +{ intro. subst. trivial. } +clear Heqhigh_branch Heqlow_branch. +destruct (Z.ones (Z.pos width - 1) _ + then fun _ => a + else fun E => bound_int_of_Z_conj (sdiv (Z_of_sint a) (Z_of_sint b)) + (sint_sdiv_bound a b E)) + eq_refl. + +(*************************************************************************) + +(* This is Ethereum's smod: the sign of b is ignored. *) +Definition smod (a b: Z) := Z.sgn a * (Z.abs a mod Z.abs b). +Lemma smod_0_r (a: Z): + smod a 0 = 0. +Proof. +unfold smod. cbn. rewrite Zmod_0_r. now rewrite Z.mul_0_r. +Qed. + +Lemma sint_smod_bound {width: positive} (a b: sint (Npos width)): + - 2 ^ (Z.of_N (N.pos width) - 1) <= smod (Z_of_sint a) (Z_of_sint b) < 2 ^ (Z.of_N (N.pos width) - 1). +Proof. +assert(AL := bound_int_lower a). +assert(AU := bound_int_upper a). +assert(BL := bound_int_lower b). +assert(BU := bound_int_upper b). +unfold Z_of_sint in *. +remember (Z_of_bound_int a) as n. clear Heqn. +remember (Z_of_bound_int b) as m. clear Heqm. +assert(M: m = 0 \/ 0 < Z.abs m) by lia. +case M; intro MZ. { subst. rewrite smod_0_r. apply (bound_int_both (sint_0 width)). } +clear M. +unfold smod. +assert (B := Z.mod_pos_bound (Z.abs n) (Z.abs m) MZ). +enough(- 2 ^ (Z.of_N (N.pos width) - 1) < Z.sgn n * (Z.abs n mod Z.abs m) < 2 ^ (Z.of_N (N.pos width) - 1)) by lia. +apply Z.abs_lt. rewrite Z_abs_sgn. +enough (Z.abs (Z.abs n mod Z.abs m) < 2 ^ (Z.of_N (N.pos width) - 1)) by now destruct n. +lia. +Qed. + +Definition sint_smod {width: positive} (a b: sint (Npos width)) +: sint (Npos width) +:= bound_int_of_Z_conj (smod (Z_of_sint a) (Z_of_sint b)) + (sint_smod_bound a b). \ No newline at end of file diff --git a/coq/CoqOfSolidity/CoqEvm/Arith/UInt.v b/coq/CoqOfSolidity/CoqEvm/Arith/UInt.v new file mode 100644 index 000000000000..5fe0c19d5c8d --- /dev/null +++ b/coq/CoqOfSolidity/CoqEvm/Arith/UInt.v @@ -0,0 +1,458 @@ +(** This is an implementation of finite integers using Z with constraints. + Warning: proof terms may blow up during computation. + *) + +From Coq Require Import NArith ZArith. +From Coq Require Import Bool Eqdep_dec. +From Coq Require Import Lia. + +From CoqOfSolidity Require Import Logic2 Arith2. + +Local Open Scope Z_scope. + +Definition bound_int (lower upper: Z) := { a: Z | ((lower <=? a) && (a a + | p~0%positive => let x := uint_pow_pos a p in uint_mul x x + | p~1%positive => let x := uint_pow_pos a p in uint_mul a (uint_mul x x) + end. + +Lemma uint_pow_pos_ok {width: N} (a: uint width) (b: positive): + uint_pow_pos a b = uint_of_Z_mod width (Z_of_uint a ^ Z.pos b)%Z. +Proof. +induction b. +{ + replace (Z.pos b~1) with (2 * Z.pos b + 1) by trivial. + rewrite Z.pow_add_r; try lia. + rewrite Z.pow_1_r. + rewrite Z.pow_twice_r. + cbn. unfold uint_mul. + apply bound_int_irrel. + cbn. repeat rewrite Z.land_ones; try apply N2Z.is_nonneg. + rewrite IHb. + repeat rewrite Z_of_uint_of_Z_mod. + clear IHb. rewrite Z.pow_pos_fold. + remember (Z_of_uint a) as n. remember (Z.pos b) as p. remember (2 ^ Z.of_N width) as m. + rewrite<- Zmult_mod. + rewrite<- Z.mul_assoc. + rewrite<- Z.mul_comm. + rewrite Zmult_mod_idemp_l. + now rewrite<- Z.mul_assoc. +} +{ + replace (Z.pos b~0) with (2 * Z.pos b) by trivial. + rewrite Z.pow_twice_r. + cbn. unfold uint_mul. + apply bound_int_irrel. + cbn. repeat rewrite Z.land_ones; try apply N2Z.is_nonneg. + rewrite IHb. + repeat rewrite Z_of_uint_of_Z_mod. + clear IHb. rewrite Z.pow_pos_fold. + remember (Z_of_uint a) as n. remember (Z.pos b) as p. remember (2 ^ Z.of_N width) as m. + now rewrite<- Zmult_mod. +} +cbn. apply bound_int_irrel. +cbn. rewrite Z.land_ones; try apply N2Z.is_nonneg. +rewrite Z.mul_1_r. +rewrite Z.mod_small. { trivial. } +exact (bound_int_both a). +Qed. + +Definition uint_pow_N {width: positive} (a: uint (Npos width)) (b: N) +: uint (Npos width) +:= match b with + | 0%N => uint_1 width + | Npos p => uint_pow_pos a p + end. + +Lemma uint_pow_N_ok {width: positive} (a: uint (Npos width)) (b: N): + uint_pow_N a b = uint_of_Z_mod (Npos width) (Z_of_uint a ^ Z.of_N b)%Z. +Proof. +destruct b. 2:{ apply uint_pow_pos_ok. } +cbn. apply bound_int_irrel. +replace Z_of_bound_int with (@Z_of_uint (N.pos width)) by trivial. +rewrite Z_of_uint_of_Z_mod. +cbn. +rewrite Z.pow_pos_fold. +symmetry. apply Z.mod_small. +split. { now rewrite<- Z.leb_le. } +replace 1 with (2 ^ 0) by trivial. +apply Z.pow_lt_mono_r; lia. +Qed. + +Definition uint_pow {width: positive} (a b: uint (Npos width)) +: uint (Npos width) +:= uint_pow_N a (N_of_uint b). + +Lemma uint_pow_ok {width: positive} (a b: uint (Npos width)): + uint_pow a b = uint_pow_ideal a b. +Proof. +unfold uint_pow. rewrite uint_pow_N_ok. +unfold uint_pow_ideal. +now rewrite Z_of_N_of_uint. +Qed. diff --git a/coq/CoqOfSolidity/CoqEvm/Arith/UInt63.v b/coq/CoqOfSolidity/CoqEvm/Arith/UInt63.v new file mode 100644 index 000000000000..f801083a604f --- /dev/null +++ b/coq/CoqOfSolidity/CoqEvm/Arith/UInt63.v @@ -0,0 +1,223 @@ +(** + This file continues theories/Numbers/Cyclic/Int63/Int63.v from the standard library of Coq. + *) + +From Coq Require Import Uint63 NArith ZArith Lia. + +From CoqOfSolidity Require Import Logic2 Arith2. + +Definition uint63 := int. +Definition Z_of_uint63 := to_Z. +Definition uint63_of_Z := of_Z. + +Ltac rewrite_Z_of_uint63 +:= repeat (rewrite lsl_spec + || rewrite lsr_spec + || rewrite land_spec' + || rewrite lor_spec' + || rewrite lxor_spec' + || rewrite add_spec + || rewrite sub_spec + || rewrite mul_spec + || rewrite div_spec + || rewrite mod_spec + || rewrite ltb_spec + || rewrite leb_spec). + +Definition N_of_uint63 (i: uint63): N +:= Z.to_N (to_Z i). +Definition uint63_of_N (n: N): uint63 +:= of_Z (Z.of_N n). + +Definition nat_of_uint63 (i: uint63): nat +:= N.to_nat (N_of_uint63 i). + +Definition uint63_of_nat (n: nat): uint63 +:= uint63_of_N (N.of_nat n). + + +Lemma Z_of_uint63_nonneg (i: uint63): + (0 <= to_Z i)%Z. +Proof. +assert(B := to_Z_bounded i). +tauto. +Qed. + +Lemma uint63_ltb_Z (x y: uint63): + (x iff_refl _) Z.ltb_lt). +apply ltb_spec. +Qed. + +Lemma uint63_leb_Z (x y: uint63): + (x <=? y)%uint63 = (to_Z x <=? to_Z y)%Z. +Proof. +apply (relation_quad (fun x y => iff_refl _) Z.leb_le). +apply leb_spec. +Qed. + +Lemma uint63_ltb_N (x y: uint63): + (x rewrite<- (of_to_Z lhs); rewrite<- (of_to_Z rhs) +end. +f_equal. +rewrite lsl_spec. +rewrite to_Z_1. rewrite to_Z_0. +rewrite Z.mul_1_l. +rewrite uint63_leb_Z in B. +replace (to_Z 63%uint63) with 63%Z in B. 2:{ trivial. } +remember (to_Z k) as n. clear i k Heqn. +remember (n - 63)%Z as m. +assert (Q: n = (m + 63)%Z). { subst. lia. } +subst n. +rewrite Z.pow_add_r; rewrite Z.leb_le in B; [ | lia | lia ]. +apply Z_mod_mult. +Qed. + +Lemma uint63_testbit_Z (i k: uint63): + get_digit i k = Z.testbit (to_Z i) (to_Z k). +Proof. +remember (k Uint63.to_Z n + | (true , n) => Uint63.to_Z n + Uint63.wB + end. + +Definition Z_of_uint64_lor (a: uint64) +:= match a with + | (false, n) => Uint63.to_Z n + | (true , n) => Z.lor (Uint63.to_Z n) Uint63.wB + end. + +Lemma Z_of_uint64_lor_ok (a: uint64): + Z_of_uint64_lor a = Z_of_uint64 a. +Proof. +unfold Z_of_uint64_lor. +destruct a as (b, n). +rewrite<- Arith2.Z_add_nocarry_lor. { trivial. } +apply Arith2.Z_land_pow2_small. { apply to_Z_bounded. } +apply Nat2Z.is_nonneg. +Qed. + +Definition Z_of_uint64_lxor (a: uint64) +:= match a with + | (false, n) => Uint63.to_Z n + | (true , n) => Z.lxor (Uint63.to_Z n) Uint63.wB + end. + +Lemma Z_of_uint64_lxor_ok (a: uint64): + Z_of_uint64_lxor a = Z_of_uint64 a. +Proof. +unfold Z_of_uint64_lxor. +destruct a as (b, n). +rewrite<- Z.add_nocarry_lxor. { trivial. } +apply Arith2.Z_land_pow2_small. { apply to_Z_bounded. } +apply Nat2Z.is_nonneg. +Qed. + +Lemma Z_of_uint64_lower (a: uint64): + 0 <= Z_of_uint64 a. +Proof. +destruct a as (hi, lo). +assert(B := Uint63.to_Z_bounded lo). +destruct B as (L, H). +destruct hi; unfold Z_of_uint64; lia. +Qed. + +Lemma Z_of_uint64_upper (a: uint64): + Z_of_uint64 a < 2^64. +Proof. +destruct a as (hi, lo). +assert(B := Uint63.to_Z_bounded lo). +destruct B as (_, H). +assert (E: Uint63.wB = 2^63). { unfold Uint63.wB. f_equal. } +destruct hi; unfold Z_of_uint64; lia. +Qed. + +Definition Z_of_uint64' (a: uint64) +:= let (b, n) := a in + Uint63.to_Z n + (if b then 1 else 0) * Uint63.wB. + +Lemma Z_of_uint64_alt (a: uint64): + Z_of_uint64' a = Z_of_uint64 a. +Proof. +unfold Z_of_uint64'. unfold Z_of_uint64. +destruct a as (b, n). destruct b; lia. +Qed. + +Definition Z_of_uint64_lor' (a: uint64) +:= let (b, n) := a in + Z.lor (Uint63.to_Z n) ((if b then 1 else 0) * Uint63.wB). + +Lemma Z_of_uint64_lor'_ok (a: uint64): + Z_of_uint64_lor' a = Z_of_uint64' a. +Proof. +unfold Z_of_uint64_lor'. +destruct a as (b, n). +rewrite<- Arith2.Z_add_nocarry_lor. { trivial. } +destruct b. +{ + rewrite Z.mul_1_l. apply Arith2.Z_land_pow2_small. + { apply to_Z_bounded. } apply Nat2Z.is_nonneg. +} +rewrite Z.mul_0_l. rewrite Z.land_0_r. trivial. +Qed. + +Definition uint64_of_Z (z: Z) + (lower: 0 <= z) + (upper: z < 2^64) +: uint64 +:= (2^63 <=? z, Uint63.of_Z z). + +Lemma uint64_of_Z_of_uint64 (a: uint64): + uint64_of_Z (Z_of_uint64 a) (Z_of_uint64_lower a) (Z_of_uint64_upper a) = a. +Proof. +assert (E: Uint63.wB = 2^63). { unfold Uint63.wB. f_equal. } +destruct a as (hi, lo). +assert(B := Uint63.to_Z_bounded lo). +destruct hi; unfold Z_of_uint64; unfold uint64_of_Z. +{ + rewrite E. f_equal. + { rewrite Z.leb_le. lia. } + rewrite<- E. clear E. + apply Uint63.to_Z_inj. rewrite Uint63.of_Z_spec. + rewrite Z.add_comm. + rewrite<- Zplus_mod_idemp_l. + rewrite Z_mod_same_full. + rewrite Z.add_0_l. + remember (Uint63.to_Z lo) as n. clear Heqn. + exact (Z.mod_small _ _ B). +} +rewrite<- E. +f_equal. { rewrite Z.leb_gt. tauto. } +apply Uint63.of_to_Z. +Qed. + +Lemma Z_of_uint64_of_Z (z: Z) + (lower: 0 <= z) + (upper: z < 2^64): + Z_of_uint64 (uint64_of_Z z lower upper) = z. +Proof. +assert (E: Uint63.wB = 2^63). { unfold Uint63.wB. f_equal. } +unfold Z_of_uint64. unfold uint64_of_Z. +remember (2 ^ 63 <=? z) as is_high. +rewrite Uint63.of_Z_spec. +symmetry in Heqis_high. +destruct is_high. +{ + rewrite Z.leb_le in Heqis_high. + rewrite E. clear E. + remember (z - 2^63) as y. + assert (YL: 0 <= y) by lia. + assert (YU: y < 2^63) by lia. + assert (R: z mod 2^63 = y mod 2^63). + { + subst. + rewrite<- Zminus_mod_idemp_r. + rewrite Z_mod_same_full. + rewrite Z.sub_0_r. + trivial. + } + rewrite R. + rewrite (Z.mod_small _ _ (conj YL YU)). + lia. +} +rewrite Z.leb_gt in Heqis_high. +apply Z.mod_small. tauto. +Qed. + +Definition uint64_of_Z_mod (z: Z) +: uint64 +:= (Z.testbit z 63, Uint63.of_Z z). + +Lemma uint64_mod_pos_bound (a: Z): + 0 <= a mod 2^64 < 2^64. +Proof. +apply Z.mod_pos_bound. +rewrite<- Z.ltb_lt. +trivial. +Qed. + +Lemma uint64_of_Z_mod_ok (z: Z): + uint64_of_Z_mod z = uint64_of_Z (z mod 2^64) + (proj1 (uint64_mod_pos_bound z)) + (proj2 (uint64_mod_pos_bound z)). +Proof. +unfold uint64_of_Z. unfold uint64_of_Z_mod. +f_equal. +{ + rewrite<- (Z.mod_pow2_bits_low z 64 63) by now rewrite<- Z.ltb_lt. + assert (B := uint64_mod_pos_bound z). + remember (z mod 2 ^ 64) as x. clear Heqx. + rewrite (Z.testbit_odd x 63). + rewrite Z.shiftr_div_pow2 by now rewrite<- Z.leb_le. + remember (2 ^ 63 <=? x) as f. symmetry in Heqf. + destruct f. + { + rewrite Z.leb_le in Heqf. + assert(L: 1 <= x / 2 ^ 63). + { + rewrite<- (Z.div_same (2^63)) by discriminate. + apply Z.div_le_mono. { rewrite<- Z.ltb_lt. trivial. } + assumption. + } + assert (U: x / 2^63 <= (2 ^ 64 - 1) / 2 ^ 63). + { + apply Z.div_le_mono. { rewrite<- Z.ltb_lt. trivial. } + lia. + } + replace ((2 ^ 64 - 1) / 2 ^ 63) with 1 in U by trivial. + assert (E: x / 2 ^ 63 = 1) by lia. + now rewrite E. + } + rewrite (Logic2.b_false (Z.leb_le _ _)) in Heqf. + apply Z.nle_gt in Heqf. + replace (x / 2 ^ 63) with 0. 2:{ symmetry. apply Z.div_small. tauto. } + trivial. +} +apply to_Z_inj. +repeat rewrite of_Z_spec. +apply Znumtheory.Zmod_div_mod; try rewrite<- Z.ltb_lt; trivial. +replace (2^64) with (2 * wB) by trivial. +apply Z.divide_factor_r. +Qed. + +Lemma Z_of_uint64_of_Z_mod (z: Z): + Z_of_uint64 (uint64_of_Z_mod z) = z mod 2^64. +Proof. +rewrite uint64_of_Z_mod_ok. +rewrite Z_of_uint64_of_Z. +trivial. +Qed. + +Definition uint64_0: uint64 := (false, 0%uint63). +Lemma uint64_0_ok: + Z_of_uint64 uint64_0 = 0. +Proof. trivial. Qed. +Definition uint64_1: uint64 := (false, 1%uint63). +Lemma uint64_1_ok: + Z_of_uint64 uint64_1 = 1. +Proof. trivial. Qed. +Definition uint64_max_value: uint64 := (true, max_int). +Lemma uint64_max_value_ok: + Z_of_uint64 uint64_max_value = 2^64 - 1. +Proof. trivial. Qed. + +(*******************************************************************************) + +Definition add (a b: uint64) +: uint64 +:= let (ha, la) := a in + let (hb, lb) := b in + let x := xorb ha hb in + match Uint63.addc la lb with + | DoubleType.C0 c => (x, c) + | DoubleType.C1 c => (negb x, c) + end. + +Ltac wB_up +:= repeat (rewrite (Z.add_comm _ Uint63.wB) + || rewrite (Z.add_comm _ (_ * Uint63.wB))); + repeat rewrite Z.add_assoc; + repeat rewrite<- Z.mul_add_distr_r. + +Lemma mod_wB (x: Z): + (x * Uint63.wB) mod 2 ^ 64 = if Z.odd x then Uint63.wB else 0. +Proof. +remember (Z.odd x) as last_bit. +rewrite (Zdiv2_odd_eqn x). subst. +rewrite Z.mul_add_distr_r. +replace (2 * Z.div2 x) with (Z.div2 x * 2) by apply Z.mul_comm. +rewrite<- Z.mul_assoc. +replace (2 * Uint63.wB) with (2 ^ 64)%Z by trivial. +rewrite Z.add_comm. rewrite Z.mod_add by discriminate. +now destruct (Z.odd x). +Qed. + +Lemma add_ok (a b: uint64): + Z_of_uint64 (add a b) = ((Z_of_uint64 a + Z_of_uint64 b) mod 2^64). +Proof. +assert (L := Z_of_uint64_lower (add a b)). +assert (U := Z_of_uint64_upper (add a b)). +repeat rewrite<- Z_of_uint64_alt in *. +rewrite<- (Z.mod_small (Z_of_uint64' (add a b)) (2 ^ 64)) by tauto. +unfold add. destruct a as (ha, la). destruct b as (hb, lb). +assert (R := Uint63.addc_spec la lb). +cbn in L. cbn in U. +unfold DoubleType.interp_carry in R. +remember (Uint63.addc la lb) as x. clear Heqx. +unfold Z_of_uint64'. +destruct x; + [rewrite R | try rewrite Z.mul_1_l in R; + replace (Uint63.to_Z i) with (Uint63.to_Z la + Uint63.to_Z lb + (-1) * Uint63.wB) by lia]; + wB_up; wB_up; repeat rewrite<- Z.add_assoc; + apply Z_mod_add_r; + destruct ha, hb; rewrite mod_wB; trivial. +Qed. + +(*******************************************************************************) + +Definition shr_uint63 (a: uint64) (sh: uint63) +: uint64 +:= if (sh =? 0)%uint63 + then a + else let (hi, lo) := a in + (false, if hi + then (((1 << 62) >> (sh - 1)) lor (lo >> sh))%uint63 + else lsr lo sh). + +Lemma shr_uint63_ok (a: uint64) (sh: uint63): + Z_of_uint64 (shr_uint63 a sh) = Z.shiftr (Z_of_uint64 a) (Uint63.to_Z sh). +Proof. +unfold shr_uint63. +remember ((sh =? 0)%uint63) as sh0 eqn:Sh0. symmetry in Sh0. destruct sh0. +{ rewrite Uint63.eqb_spec in Sh0. now subst. } +assert(BS := to_Z_bounded sh). remember (to_Z sh) as s. +assert(SPos: 0 < s). +{ + enough (s <> 0) by lia. + intro H. subst. + replace 0 with (to_Z 0) in H by trivial. + apply to_Z_inj in H. + apply eqb_spec in H. + rewrite H in Sh0. + discriminate. +} +destruct a as (hi, lo). +destruct hi; unfold Z_of_uint64. +2:{ + (* low case *) + rewrite Uint63.lsr_spec. + rewrite Z.shiftr_div_pow2 by tauto. + now subst. +} +(* high case *) +rewrite Uint63.lor_spec'. +rewrite Uint63.lsr_spec. +rewrite Uint63.lsr_spec. +rewrite Uint63.lsl_spec. +rewrite Uint63.sub_spec. +replace (to_Z 1) with 1 by trivial. +replace (to_Z 62) with 62 by trivial. +rewrite<- Heqs. +clear Sh0 Heqs. +assert(BN := to_Z_bounded lo). remember (to_Z lo) as n. clear Heqn. +rewrite Z.mul_1_l. rewrite Z.shiftr_div_pow2 by tauto. +replace (2 ^ 62 mod wB) with (2 ^ 62) by trivial. +replace ((s - 1) mod wB) with (s - 1). 2:{ symmetry. apply Z.mod_small. lia. } +assert (CS: 64 <= s \/ s <= 63) by lia. +case CS; clear CS; intro CS. +{ + (* large shift, everything is 0 *) + replace (n / 2 ^ s) with 0. + 2:{ + symmetry. apply Z.div_small. + split. { tauto. } + replace Uint63.wB with (2 ^ 63) in * by trivial. + apply (Z.lt_trans n (2^63) (2^s)). { tauto. } + apply Z.pow_lt_mono_r; lia. + } + rewrite Z.lor_0_r. + rewrite Z.div_small. + 2:{ + split. { lia. } + apply Z.pow_lt_mono_r; lia. + } + rewrite Z.div_small. { trivial. } + split. { lia. } + apply (Z.lt_le_trans _ (2^64) (2^s)). + { replace (2 ^ 64) with (wB + wB) by trivial. lia. } + apply Z.pow_le_mono_r; lia. +} +replace (2 ^ 62 / 2 ^ (s - 1)) with (2 ^ 63 / 2 ^ s). +2:{ + replace (2 ^ 63) with (2 * (2 ^ 62)) by trivial. + replace (2 ^ s) with ((2 ^ (1 + (s - 1)))) by now replace (1 + (s - 1)) with s by lia. + rewrite Z.pow_add_r; try lia. + rewrite Z.div_mul_cancel_l; lia. +} +repeat rewrite<- Z.shiftr_div_pow2 by tauto. +rewrite<- Z.shiftr_lor. +f_equal. +rewrite<- Arith2.Z_add_nocarry_lor. { apply Z.add_comm. } +rewrite Z.land_comm. +apply Arith2.Z_land_pow2_small. { tauto. } +now rewrite<- Z.leb_le. +Qed. + +(*******************************************************************************) + +Definition shl_uint63 (a: uint64) (sh: uint63) +: uint64 +:= if (sh =? 0)%uint63 + then a + else let (hi, lo) := a in + (get_digit lo (63 - sh), lsl lo sh). + +Lemma shl_uint63_ok (a: uint64) (sh: uint63): + Z_of_uint64 (shl_uint63 a sh) = (Z.shiftl (Z_of_uint64 a) (Uint63.to_Z sh) mod 2^64)%Z. +Proof. +repeat rewrite<- Z_of_uint64_alt. repeat rewrite<- Z_of_uint64_lor'_ok. +unfold shl_uint63. +remember ((sh =? 0)%uint63) as sh0 eqn:Sh0. symmetry in Sh0. destruct sh0. +{ + rewrite Uint63.eqb_spec in Sh0. subst. rewrite Z.shiftl_0_r. + symmetry. apply Z.mod_small. + rewrite Z_of_uint64_lor'_ok. + rewrite Z_of_uint64_alt. + split. { apply Z_of_uint64_lower. } apply Z_of_uint64_upper. +} +assert(BS := to_Z_bounded sh). remember (to_Z sh) as s. +assert(SPos: 0 < s). +{ + enough (s <> 0) by lia. + intro H. subst. + replace 0 with (to_Z 0) in H by trivial. + apply to_Z_inj in H. + apply eqb_spec in H. + rewrite H in Sh0. + discriminate. +} +destruct a as (hi, lo). +rewrite uint63_testbit_Z. +unfold Z_of_uint64_lor'. +rewrite Uint63.lsl_spec. +apply Z.bits_inj'. intros k Knonneg. +rewrite Z.lor_spec. +rewrite<- Z.shiftl_mul_pow2 by now subst. +rewrite<- Heqs. +assert (BN := to_Z_bounded lo). remember (to_Z lo) as n. +rewrite Z.shiftl_lor. +replace wB with (2^63) by trivial. +repeat rewrite<- Z.land_ones. +rewrite Z.land_lor_distr_l. +replace (Z.land (Z.shiftl ((if hi then 1 else 0) * 2 ^ 63) s) (Z.ones 64)) with 0. +3-4: now rewrite<- Z.leb_le. +2:{ + destruct hi. 2:{ rewrite Z.mul_0_l. rewrite Z.shiftl_0_l. rewrite Z.land_0_l. trivial. } + symmetry. + rewrite Z.mul_1_l. + rewrite Z.shiftl_mul_pow2 by tauto. + rewrite Z.land_ones by now rewrite<- Z.leb_le. + rewrite<- Z.pow_add_r; try lia. + replace (2 ^ (63 + s)) with (2^(s - 1) * 2^64). + 2:{ rewrite<- Z.pow_add_r; try f_equal; lia. } + apply Z_mod_mult. +} +rewrite Z.lor_0_r. +repeat rewrite Z.land_spec. +repeat rewrite Z.testbit_ones_nonneg; try lia. +remember (Z.testbit (Z.shiftl n s) k) as x. +assert (CK: k <> 63 \/ k = 63) by lia. +case CK; clear CK; intro CK. +{ + replace (Z.testbit ((if Z.testbit n (to_Z (63 - sh)%uint63) then 1 else 0) * 2 ^ 63) k) with false. + 2:{ + symmetry. + destruct (Z.testbit n (to_Z (63 - sh)%uint63)); [ rewrite Z.mul_1_l | rewrite Z.mul_0_l ]. + { apply Z.pow2_bits_false. lia. } + apply Z.bits_0. + } + rewrite Bool.orb_false_r. + f_equal. + rewrite Arith2.Z_ltb_lt_quad. split; lia. +} +subst k x. +replace (63 0) by discriminate. + assert(D := Z.div_mod (63 - s) wB WBNZ). + assert(WBPos: 0 < wB) by lia. + assert(BQ := Z.mod_pos_bound (63 - s) wB WBPos). + remember ((63 - s) mod wB) as q. + clear Heqq. + assert (L: -1 <= (63 - s) / wB) by nia. + assert (U: (63 - s) / wB <= 0) by nia. + assert (T: (63 - s) / wB = 0 \/ (63 - s) / wB = -1) by lia. + case T; clear T; intro T; lia. +} +case Q; clear Q; intro Q. { now rewrite Q. } +assert (S63: 63 < s). +{ + apply Z.nle_gt. intro H. + replace ((63 - s) mod wB) with (63 - s) in *. + 2:{ + rewrite Z.mod_small. { trivial. } + lia. + } + lia. +} +rewrite (Z.testbit_neg_r n (63 - s)) by lia. +apply Arith2.Z_testbit_small. { tauto. } +refine (Z.lt_trans n wB _ _ _). { tauto. } +replace wB with (2^63) by trivial. +apply Z.pow_lt_mono_r; try lia. +apply Z.mod_pos_bound. +trivial. apply Q. +Qed. + +(*******************************************************************************) + +Definition bitwise_or (a b: uint64) +: uint64 +:= ((fst a || fst b)%bool, Uint63.lor (snd a) (snd b)). + +Lemma bitwise_or_ok (a b: uint64): + Z_of_uint64 (bitwise_or a b) = (Z.lor (Z_of_uint64 a) (Z_of_uint64 b)). +Proof. +repeat rewrite<- Z_of_uint64_lor_ok. +destruct a as (a_hi, a_lo). +destruct b as (b_hi, b_lo). +unfold Z_of_uint64_lor. unfold bitwise_or. +destruct a_hi, b_hi; + match goal with + |- (if ?cond then _ else _) = ?rhs => remember cond as c; cbn in Heqc; subst + end; + repeat rewrite lor_spec'; + replace (snd (_, a_lo)) with a_lo by trivial; + replace (snd (_, b_lo)) with b_lo by trivial; + remember (to_Z a_lo) as x; + remember (to_Z b_lo) as y; + repeat rewrite Z.lor_assoc; trivial. +{ + (* goal: Z.lor (Z.lor x y) wB = Z.lor (Z.lor (Z.lor x wB) y) wB *) + repeat rewrite<- Z.lor_assoc. f_equal. + rewrite Z.lor_comm. + rewrite Z.lor_assoc. + now replace (Z.lor wB wB) with wB by trivial. +} +(* goal: Z.lor (Z.lor x y) wB = Z.lor (Z.lor x wB) y *) +repeat rewrite<- Z.lor_assoc. f_equal. +apply Z.lor_comm. +Qed. + +(*******************************************************************************) + +Definition bitwise_xor (a b: uint64) +: uint64 +:= (xorb (fst a) (fst b), Uint63.lxor (snd a) (snd b)). + +Lemma bitwise_xor_ok (a b: uint64): + Z_of_uint64 (bitwise_xor a b) = (Z.lxor (Z_of_uint64 a) (Z_of_uint64 b)). +Proof. +repeat rewrite<- Z_of_uint64_lxor_ok. +destruct a as (a_hi, a_lo). +destruct b as (b_hi, b_lo). +unfold Z_of_uint64_lxor. unfold bitwise_xor. +destruct a_hi, b_hi; + match goal with + |- (if ?cond then _ else _) = ?rhs => remember cond as c; cbn in Heqc; subst + end; + repeat rewrite lxor_spec'; + replace (snd (_, a_lo)) with a_lo by trivial; + replace (snd (_, b_lo)) with b_lo by trivial; + remember (to_Z a_lo) as x; + remember (to_Z b_lo) as y; + repeat rewrite Z.lxor_assoc; trivial. +{ + (* goal: Z.lxor x y = Z.lxor x (Z.lxor wB (Z.lxor y wB)) *) + rewrite (Z.lxor_comm y wB). f_equal. + rewrite<- Z.lxor_assoc. + now replace (Z.lor wB wB) with wB by trivial. +} +f_equal. apply Z.lxor_comm. +Qed. + +(*******************************************************************************) + +Definition bitwise_and (a b: uint64) +: uint64 +:= ((fst a && fst b)%bool, Uint63.land (snd a) (snd b)). + +Lemma bitwise_and_ok (a b: uint64): + Z_of_uint64 (bitwise_and a b) = (Z.land (Z_of_uint64 a) (Z_of_uint64 b)). +Proof. +repeat rewrite<- Z_of_uint64_lor_ok. +destruct a as (a_hi, a_lo). +destruct b as (b_hi, b_lo). +unfold Z_of_uint64_lor. unfold bitwise_and. +destruct a_hi, b_hi; + match goal with + |- (if ?cond then _ else _) = ?rhs => remember cond as c; cbn in Heqc; subst + end; + repeat rewrite land_spec'; + replace (snd (_, a_lo)) with a_lo by trivial; + replace (snd (_, b_lo)) with b_lo by trivial; + remember (to_Z a_lo) as x; + remember (to_Z b_lo) as y; + repeat rewrite Z.land_assoc; trivial. +{ apply Z.lor_land_distr_l. } +{ + rewrite Z.land_lor_distr_l. + replace (Z.land wB y) with 0. { now rewrite Z.lor_0_r. } + symmetry. rewrite Z.land_comm. apply Arith2.Z_land_pow2_small. + { subst. apply to_Z_bounded. } + rewrite<- Z.leb_le. trivial. +} +rewrite Z.land_lor_distr_r. +replace (Z.land x wB) with 0. { now rewrite Z.lor_0_r. } +symmetry. apply Arith2.Z_land_pow2_small. +{ subst. apply to_Z_bounded. } +rewrite<- Z.leb_le. trivial. +Qed. + +(*******************************************************************************) + +Definition bitwise_not (a: uint64) +: uint64 +:= (negb (fst a), Uint63.lxor (snd a) (of_Z (-1))). + +Lemma bitwise_not_via_xor (a: uint64): + bitwise_not a = bitwise_xor a uint64_max_value. +Proof. +trivial. +Qed. + +Lemma bitwise_not_ok (a: uint64): + Z_of_uint64 (bitwise_not a) = (Z.lnot (Z_of_uint64 a)) mod 2^64. +Proof. +rewrite bitwise_not_via_xor. rewrite bitwise_xor_ok. +rewrite<- Z.lxor_m1_r. rewrite<- Z.land_ones. 2: { now rewrite<- Z.leb_le. } +assert (L := Z_of_uint64_lower a). +assert (U := Z_of_uint64_upper a). +remember (Z_of_uint64 a) as x. clear Heqx. +rewrite uint64_max_value_ok. +replace (2 ^ 64 - 1) with (Z.ones 64) by trivial. +rewrite Z_land_lxor_distr_l. +f_equal. +symmetry. apply Z.land_ones_low. { assumption. } +apply Arith2.Z_log2_lt_pow2; try assumption. +now rewrite<- Z.ltb_lt. +Qed. + +(*******************************************************************************) + +Definition uint64_of_be_bytes (b: byte * byte * byte * byte * byte * byte * byte * byte) +: uint64 +:= match b with + | (b7, b6, b5, b4, b3, b2, b1, b0) => + bitwise_or (shl_uint63 (false, int_of_byte b7) 56%uint63) + (false, ((int_of_byte b6 << 48) lor (int_of_byte b5 << 40) lor (int_of_byte b4 << 32) + lor (int_of_byte b3 << 24) lor (int_of_byte b2 << 16) lor (int_of_byte b1 << 8) + lor int_of_byte b0)%uint63) + end. + +Definition uint64_to_be_bytes (a: uint64) +: byte * byte * byte * byte * byte * byte * byte * byte +:= let (f, i) := a in + (byte_of_int (snd (shr_uint63 a 56)), + byte_of_int (i >> 48), + byte_of_int (i >> 40), + byte_of_int (i >> 32), + byte_of_int (i >> 24), + byte_of_int (i >> 16), + byte_of_int (i >> 8), + byte_of_int i)%uint63. + +Definition uint64_to_le_bytes (a: uint64) +: byte * byte * byte * byte * byte * byte * byte * byte +:= let (f, i) := a in + (byte_of_int i, + byte_of_int (i >> 8), + byte_of_int (i >> 16), + byte_of_int (i >> 24), + byte_of_int (i >> 32), + byte_of_int (i >> 40), + byte_of_int (i >> 48), + byte_of_int (snd (shr_uint63 a 56)))%uint63. diff --git a/coq/CoqOfSolidity/CoqEvm/Containers/Tuplevector.v b/coq/CoqOfSolidity/CoqEvm/Containers/Tuplevector.v new file mode 100644 index 000000000000..f5d208af54cb --- /dev/null +++ b/coq/CoqOfSolidity/CoqEvm/Containers/Tuplevector.v @@ -0,0 +1,247 @@ +From Coq Require Import Arith. +From Coq Require List. + +(** A tuplevector is a tuple containing items of the same type. *) +Fixpoint t (T: Type) (n: nat) +: Type +:= match n with + | O => unit + | 1%nat => T + | S k => (t T k * T)%type + end. + +(** The tuplevector type simply expands to a power of its base type: *) +Local Example type_example: t nat 3 = (nat * nat * nat)%type. +Proof. trivial. Qed. + +(** Coq already has a notation for a tuplevector. The type needs to be supplied though. *) +Local Example example_tuple_5: t nat 5 := (10, 20, 30, 40, 50). + +(** As an exception, a tuple with one item is just the item itself. + In Lisp terms, a tuple is an improper list (also backwards, that is, + the head is in the rightmost position). + *) +Local Example example_tuple_1: t nat 1 := 10. + +(** Let can destructure a tuplevector with an apostrophe: *) +Local Example destructuring_example: + (let tuple := (10, 20, 30, 40, 50): t nat 5 in + let '(a, b, c, d, e) := tuple in + a) + = + 10. +Proof. trivial. Qed. + +(** [snoc] is a term from Haskell, it means cons backwards. *) +Definition snoc {T n} (tv: t T n) (last: T) +: t T (S n) +:= match n, tv with + | 0, _ => last + | S _, x => (x, last) + end. + +Local Example snoc_example: + snoc ((10, 20, 30): t nat 3) 40 = (10, 20, 30, 40). +Proof. trivial. Qed. + +Definition last {T n} (tv: t T (S n)) +: T +:= match n, tv with + | 0, x => x + | S _, (_, x) => x + end. + +Lemma last_of_snoc {T n} (tv: t T n) (x: T): + last (snoc tv x) = x. +Proof. +destruct n; easy. +Qed. + +Definition but_last {T n} (tv: t T (S n)) +: t T n +:= match n, tv with + | 0, x => tt + | S k, (rest, x) => rest + end. + +Lemma but_last_of_snoc {T n} (tv: t T n) (x: T): + but_last (snoc tv x) = tv. +Proof. +destruct n. { now destruct tv. } +destruct n; easy. +Qed. + +Lemma snoc_ok {T n} (tv: t T (S n)): + snoc (but_last tv) (last tv) = tv. +Proof. +destruct n. { easy. } +now destruct tv. +Qed. + +Fixpoint app_to_list {T n} (tv: t T n) (l: list T) +: list T +:= match n as n' return (t T n' -> list T) with + | 0 => fun _ => l + | S k => fun tv' => app_to_list (but_last tv') (last tv' :: l)%list + end tv. + +Local Example app_to_list_example: + app_to_list ((5, 15): t _ 2) (10 :: 20 :: 30 :: nil)%list = (5 :: 15 :: 10 :: 20 :: 30 :: nil)%list. +Proof. trivial. Qed. + +Lemma app_to_list_length {T n} (tv: t T n) (l: list T): + length (app_to_list tv l) = n + length l. +Proof. +revert l. +induction n. { easy. } +cbn. intros. rewrite IHn. cbn. +symmetry. apply plus_n_Sm. +Qed. + +Fixpoint prepend {T: Type} {n: nat} (new: T) (tv: t T n) +: t T (S n) +:= match n, tv with + | 0, _ => new + | S _, x => (prepend new (but_last x), last x) + end. + +Local Example prepend_example: + prepend 5 ((2, 3, 4): t nat 3) = (5, 2, 3, 4). +Proof. trivial. Qed. + +Fixpoint rev {T: Type} {n: nat} (tv: t T n) +: t T n +:= match n, tv with + | 0, _ => tt + | S _, x => prepend (last x) (rev (but_last x)) + end. + +Local Example rev_example: + rev ((1, 2, 3, 4): t nat 4) = (4, 3, 2, 1). +Proof. trivial. Qed. + +(************************************************) + +Local Lemma take_from_list_helper {T k} {head: T} {tail: list T} + (H: S k <= length (head :: tail)%list): + k <= length tail. +Proof. +apply le_S_n. apply H. +Qed. + +Fixpoint take_from_list_rev {T n} (l: list T) (ok: n <= length l) +: t T n * list T +:= match n as n' return n' <= length l -> t T n' * list T with + | O => fun _ => (tt, l) + | S k => + match l as l' return S k <= length l' -> t T (S k) * list T with + | nil => fun X => False_rect _ (Nat.nle_succ_0 k X) + | (head :: tail)%list => fun X => + let (prefix, rest) := take_from_list_rev tail (take_from_list_helper X) in + (snoc prefix head, rest) + end + end ok. + +Fixpoint to_list_backwards {T n} (tv: t T n) +: list T +:= match n, tv with + | 0, _ => nil + | S _, x => last x :: to_list_backwards (but_last x) + end. + +Local Example to_list_backwards_example: + to_list_backwards ((1, 2, 3, 4): t nat 4) = (4 :: 3 :: 2 :: 1 :: nil)%list. +Proof. trivial. Qed. + +Lemma take_from_list_rev_firstn {T n} (l: list T) (ok: n <= length l): + to_list_backwards (fst (take_from_list_rev l ok)) = List.firstn n l. +Proof. +revert l ok. induction n, l; try easy. intros. +cbn. +assert (M := IHn l (take_from_list_helper ok)). +remember (take_from_list_rev l (take_from_list_helper ok)) as pq. destruct pq as (p, q). +cbn in *. +rewrite last_of_snoc. rewrite but_last_of_snoc. f_equal. +exact M. +Qed. + +Lemma take_from_list_rev_skipn {T n} (l: list T) (ok: n <= length l): + snd (take_from_list_rev l ok) = List.skipn n l. +Proof. +revert l ok. induction n, l; try easy. intros. +cbn. +assert (M := IHn l (take_from_list_helper ok)). +remember (take_from_list_rev l (take_from_list_helper ok)) as pq. destruct pq as (p, q). +cbn in *. exact M. +Qed. + +(** This function fixes the flip of take_from_list_rev by applying rev. + The name reflects the opinion that this function should be avoided + because rev is quadratic. + *) +Definition take_from_list_slow {T n} (l: list T) (ok: n <= length l) +: t T n * list T +:= let (prefix, rest) := take_from_list_rev l ok + in (rev prefix, rest). + +(**********************************************************************************) + +Local Lemma gather_helper_nil {T} {x: T} {l: list T} {block_len}: + ~ (length (x :: l) = 0 * block_len). +Proof. discriminate. Qed. + +Local Lemma gather_helper_block_len {T} (k block_len: nat) (l: list T) + (E : length l = S k * block_len): + block_len <= length l. +Proof. +rewrite E. +rewrite<- Nat.mul_1_l at 1. +apply Nat.mul_le_mono_r. +apply le_n_S. +apply Nat.le_0_l. +Qed. + +Definition take_from_list_rev_dep_skipn {T n} (l: list T) (ok: n <= length l) +: { x: t T n * list T | snd x = List.skipn n l } +:= exist _ (take_from_list_rev l ok) (take_from_list_rev_skipn l ok). + +Local Lemma gather_helper_skipn {T k block_len l} + (ok: length l = S k * block_len) + (p: {x : t T block_len * list T | snd x = List.skipn block_len l}): + length (snd (proj1_sig p)) = k * block_len. +Proof. +assert (P := proj2_sig p). cbn in P. rewrite P. +rewrite List.skipn_length. +rewrite ok. +cbn. +rewrite Nat.add_comm. +rewrite Nat.add_sub. +trivial. +Qed. + +Fixpoint gather {T} (l: list T) (n block_len: nat) (ok: length l = n * block_len) +{struct n} +: list (t T block_len) +:= match n as n' return length l = n' * block_len -> list (t T block_len) with + | O => match l as l' return length l' = 0 * block_len -> _ with + | nil => fun _ => nil + | cons _ _ => fun ok' => False_rect _ (gather_helper_nil ok') + end + | S k => fun ok' => + let p := take_from_list_rev_dep_skipn l (gather_helper_block_len k block_len l ok') in + (fst (proj1_sig p) :: gather (snd (proj1_sig p)) k block_len + (gather_helper_skipn ok' p))%list + end ok. + +Example gather_example: + gather (1 :: 2 :: 3 :: 4 :: 5 :: 6 :: 7 :: 8 :: 9 :: 10 :: nil)%list 5 2 eq_refl + = + ((2, 1) :: (4, 3) :: (6, 5) :: (8, 7) :: (10, 9) :: nil)%list. +Proof. trivial. Qed. + +Lemma gather_length {T} (l: list T) (n block_len: nat) (ok: length l = n * block_len): + List.length (gather l n block_len ok) = n. +Proof. +revert l ok. induction n; intros; destruct l; cbn; + trivial; try easy; f_equal; apply IHn. +Qed. \ No newline at end of file diff --git a/coq/CoqOfSolidity/CoqEvm/Containers/Vec16.v b/coq/CoqOfSolidity/CoqEvm/Containers/Vec16.v new file mode 100644 index 000000000000..41651603ab3d --- /dev/null +++ b/coq/CoqOfSolidity/CoqEvm/Containers/Vec16.v @@ -0,0 +1,290 @@ +From Coq Require Import Uint63. +From CoqOfSolidity Require Import Nibble UInt63. + +Inductive vec16 (T: Type) +:= Vec16 (v0 v1 v2 v3 v4 v5 v6 v7 v8 v9 va vb vc vd ve vf: T). +Arguments Vec16 {_}. + +Local Generalizable Variable T. + +Definition t := vec16. + +Definition to_list `(v: vec16 T) +: list T +:= match v with + | Vec16 v0 v1 v2 v3 v4 v5 v6 v7 v8 v9 va vb vc vd ve vf => + v0 :: v1 :: v2 :: v3 :: v4 :: v5 :: v6 :: v7 :: + v8 :: v9 :: va :: vb :: vc :: vd :: ve :: vf :: nil + end. + +Definition fill `(x: T) +: vec16 T +:= Vec16 x x x x x x x x x x x x x x x x. + +Definition fill_but_first {T: Type} (x first: T) +: vec16 T +:= Vec16 first x x x x x x x x x x x x x x x. + +Definition get_by_hex `(v: vec16 T) (h: hex_digit) +: T +:= match v with + | Vec16 v0 v1 v2 v3 v4 v5 v6 v7 v8 v9 va vb vc vd ve vf => + match h with + | x0 => v0 + | x1 => v1 + | x2 => v2 + | x3 => v3 + | x4 => v4 + | x5 => v5 + | x6 => v6 + | x7 => v7 + | x8 => v8 + | x9 => v9 + | xA => va + | xB => vb + | xC => vc + | xD => vd + | xE => ve + | xF => vf + end + end. + +Definition get_by_int `(v: vec16 T) (i: uint63) +: T +:= match v with + | Vec16 v0 v1 v2 v3 v4 v5 v6 v7 v8 v9 va vb vc vd ve vf => + if (0 + match h with + | x0 => Vec16 XX v1 v2 v3 v4 v5 v6 v7 v8 v9 va vb vc vd ve vf + | x1 => Vec16 v0 XX v2 v3 v4 v5 v6 v7 v8 v9 va vb vc vd ve vf + | x2 => Vec16 v0 v1 XX v3 v4 v5 v6 v7 v8 v9 va vb vc vd ve vf + | x3 => Vec16 v0 v1 v2 XX v4 v5 v6 v7 v8 v9 va vb vc vd ve vf + | x4 => Vec16 v0 v1 v2 v3 XX v5 v6 v7 v8 v9 va vb vc vd ve vf + | x5 => Vec16 v0 v1 v2 v3 v4 XX v6 v7 v8 v9 va vb vc vd ve vf + | x6 => Vec16 v0 v1 v2 v3 v4 v5 XX v7 v8 v9 va vb vc vd ve vf + | x7 => Vec16 v0 v1 v2 v3 v4 v5 v6 XX v8 v9 va vb vc vd ve vf + | x8 => Vec16 v0 v1 v2 v3 v4 v5 v6 v7 XX v9 va vb vc vd ve vf + | x9 => Vec16 v0 v1 v2 v3 v4 v5 v6 v7 v8 XX va vb vc vd ve vf + | xA => Vec16 v0 v1 v2 v3 v4 v5 v6 v7 v8 v9 XX vb vc vd ve vf + | xB => Vec16 v0 v1 v2 v3 v4 v5 v6 v7 v8 v9 va XX vc vd ve vf + | xC => Vec16 v0 v1 v2 v3 v4 v5 v6 v7 v8 v9 va vb XX vd ve vf + | xD => Vec16 v0 v1 v2 v3 v4 v5 v6 v7 v8 v9 va vb vc XX ve vf + | xE => Vec16 v0 v1 v2 v3 v4 v5 v6 v7 v8 v9 va vb vc vd XX vf + | xF => Vec16 v0 v1 v2 v3 v4 v5 v6 v7 v8 v9 va vb vc vd ve XX + end + end. + +Definition set_by_int `(v: vec16 T) (i: uint63) (XX: T) +: vec16 T +:= match v with + | Vec16 v0 v1 v2 v3 v4 v5 v6 v7 v8 v9 va vb vc vd ve vf => + if (0 + match v with + | Vec16 v0 v1 v2 v3 v4 v5 v6 v7 v8 v9 va vb vc vd ve vf => + match h with + | x0 => Vec16 v0 v1 v2 v3 v4 v5 v6 v7 v8 v9 va vb vc vd ve vf + | x1 => Vec16 uf v0 v1 v2 v3 v4 v5 v6 v7 v8 v9 va vb vc vd ve + | x2 => Vec16 ue uf v0 v1 v2 v3 v4 v5 v6 v7 v8 v9 va vb vc vd + | x3 => Vec16 ud ue uf v0 v1 v2 v3 v4 v5 v6 v7 v8 v9 va vb vc + | x4 => Vec16 uc ud ue uf v0 v1 v2 v3 v4 v5 v6 v7 v8 v9 va vb + | x5 => Vec16 ub uc ud ue uf v0 v1 v2 v3 v4 v5 v6 v7 v8 v9 va + | x6 => Vec16 ua ub uc ud ue uf v0 v1 v2 v3 v4 v5 v6 v7 v8 v9 + | x7 => Vec16 u9 ua ub uc ud ue uf v0 v1 v2 v3 v4 v5 v6 v7 v8 + | x8 => Vec16 u8 u9 ua ub uc ud ue uf v0 v1 v2 v3 v4 v5 v6 v7 + | x9 => Vec16 u7 u8 u9 ua ub uc ud ue uf v0 v1 v2 v3 v4 v5 v6 + | xA => Vec16 u6 u7 u8 u9 ua ub uc ud ue uf v0 v1 v2 v3 v4 v5 + | xB => Vec16 u5 u6 u7 u8 u9 ua ub uc ud ue uf v0 v1 v2 v3 v4 + | xC => Vec16 u4 u5 u6 u7 u8 u9 ua ub uc ud ue uf v0 v1 v2 v3 + | xD => Vec16 u3 u4 u5 u6 u7 u8 u9 ua ub uc ud ue uf v0 v1 v2 + | xE => Vec16 u2 u3 u4 u5 u6 u7 u8 u9 ua ub uc ud ue uf v0 v1 + | xF => Vec16 u1 u2 u3 u4 u5 u6 u7 u8 u9 ua ub uc ud ue uf v0 + end + end + end. + +Definition update_by_hex `(v: vec16 T) (h: hex_digit) (f: T -> T) +: vec16 T +:= match v with + | Vec16 v0 v1 v2 v3 v4 v5 v6 v7 v8 v9 va vb vc vd ve vf => + match h with + | x0 => Vec16(f v0) v1 v2 v3 v4 v5 v6 v7 v8 v9 va vb vc vd ve vf + | x1 => Vec16 v0(f v1) v2 v3 v4 v5 v6 v7 v8 v9 va vb vc vd ve vf + | x2 => Vec16 v0 v1(f v2) v3 v4 v5 v6 v7 v8 v9 va vb vc vd ve vf + | x3 => Vec16 v0 v1 v2(f v3) v4 v5 v6 v7 v8 v9 va vb vc vd ve vf + | x4 => Vec16 v0 v1 v2 v3(f v4) v5 v6 v7 v8 v9 va vb vc vd ve vf + | x5 => Vec16 v0 v1 v2 v3 v4(f v5) v6 v7 v8 v9 va vb vc vd ve vf + | x6 => Vec16 v0 v1 v2 v3 v4 v5(f v6) v7 v8 v9 va vb vc vd ve vf + | x7 => Vec16 v0 v1 v2 v3 v4 v5 v6(f v7) v8 v9 va vb vc vd ve vf + | x8 => Vec16 v0 v1 v2 v3 v4 v5 v6 v7(f v8) v9 va vb vc vd ve vf + | x9 => Vec16 v0 v1 v2 v3 v4 v5 v6 v7 v8(f v9) va vb vc vd ve vf + | xA => Vec16 v0 v1 v2 v3 v4 v5 v6 v7 v8 v9(f va) vb vc vd ve vf + | xB => Vec16 v0 v1 v2 v3 v4 v5 v6 v7 v8 v9 va(f vb) vc vd ve vf + | xC => Vec16 v0 v1 v2 v3 v4 v5 v6 v7 v8 v9 va vb(f vc) vd ve vf + | xD => Vec16 v0 v1 v2 v3 v4 v5 v6 v7 v8 v9 va vb vc(f vd) ve vf + | xE => Vec16 v0 v1 v2 v3 v4 v5 v6 v7 v8 v9 va vb vc vd(f ve) vf + | xF => Vec16 v0 v1 v2 v3 v4 v5 v6 v7 v8 v9 va vb vc vd ve(f vf) + end + end. + +Lemma set_via_update_by_hex `(v: vec16 T) (h: hex_digit) (new_value: T): + set_by_hex v h new_value = update_by_hex v h (fun _ => new_value). +Proof. +now destruct h. +Qed. + +Lemma get_of_update_by_hex `(v: vec16 T) (h: hex_digit) (f: T -> T): + get_by_hex (update_by_hex v h f) h = f (get_by_hex v h). +Proof. +now destruct v, h. +Qed. + +Lemma get_of_set_by_hex `(v: vec16 T) (h: hex_digit) (new_value: T): + get_by_hex (set_by_hex v h new_value) h = new_value. +Proof. +now destruct v, h. +Qed. + +Lemma get_of_update_ne_by_hex `(v: vec16 T) + (h h': hex_digit) + (NE: h <> h') + (f: T -> T): + get_by_hex (update_by_hex v h' f) h = get_by_hex v h. +Proof. +now destruct v, h, h'. +Qed. + +Lemma get_of_set_ne_by_hex `(v: vec16 T) + (h h': hex_digit) + (NE: h <> h') + (new_value: T): + get_by_hex (set_by_hex v h' new_value) h = get_by_hex v h. +Proof. +rewrite set_via_update_by_hex. +now apply get_of_update_ne_by_hex. +Qed. + +Definition fold_left {A B: Type} (f: A -> B -> A) (v: vec16 B) (init: A) +: A +:= match v with + | Vec16 v0 v1 v2 v3 v4 v5 v6 v7 v8 v9 va vb vc vd ve vf => + f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f init + v0) v1) v2) v3) v4) v5) v6) v7) v8) v9) va) vb) vc) vd) ve) vf + end. + +Lemma fold_left_ok {A B: Type} (f: A -> B -> A) (v: vec16 B) (init: A): + fold_left f v init = List.fold_left f (to_list v) init. +Proof. now destruct v. Qed. + +Definition fold_right {A B: Type} (f: B -> A -> A) (init: A) (v: vec16 B) +: A +:= match v with + | Vec16 v0 v1 v2 v3 v4 v5 v6 v7 v8 v9 va vb vc vd ve vf => + f v0 (f v1 (f v2 (f v3 + (f v4 (f v5 (f v6 (f v7 + (f v8 (f v9 (f va (f vb + (f vc (f vd (f ve (f vf init))))))))))))))) + end. + +Lemma fold_right_ok {A B: Type} (f: B -> A -> A) (init: A) (v: vec16 B): + fold_right f init v = List.fold_right f init (to_list v). +Proof. now destruct v. Qed. \ No newline at end of file diff --git a/coq/CoqOfSolidity/CoqEvm/Containers/Vec8.v b/coq/CoqOfSolidity/CoqEvm/Containers/Vec8.v new file mode 100644 index 000000000000..2385f43b079b --- /dev/null +++ b/coq/CoqOfSolidity/CoqEvm/Containers/Vec8.v @@ -0,0 +1,67 @@ +From Coq Require Import Uint63. + +Inductive vec8 (T: Type) +:= Vec8 (a b c d e f g h: T). +Arguments Vec8 {_}. + +Definition t := vec8. + +Definition map {A B: Type} (F: A -> B) (v: vec8 A) +: vec8 B +:= match v with + | Vec8 a b c d + e f g h => Vec8 (F a) (F b) (F c) (F d) + (F e) (F f) (F g) (F h) + end. + + +Definition to_list {T: Type} (v: vec8 T) +: list T +:= match v with + | Vec8 a b c d + e f g h => (a :: b :: c :: d :: e :: f :: g :: h :: nil)%list + end. + +Definition get {T: Type} (v: vec8 T) (i: int) +: T +:= match v with + | Vec8 v0 v1 v2 v3 v4 v5 v6 v7 => + if (0 + if (0 > y" := (UInt64.shr_uint63 x y). +Local Notation "x | y" := (UInt64.bitwise_or x y) (at level 30). (* dangerous! messes up match! *) +Local Notation "x & y" := (UInt64.bitwise_and x y) (at level 30). +Local Notation "x + y" := (UInt64.add x y). +Local Notation "~ x" := (UInt64.bitwise_not x). +Definition rot x k := ((x >> k) | (x << (64 - k)%uint63)). +Local Notation "x >>> y" := (rot x y) (at level 30). + + +(** 2.1 Parameters. *) + +(** G rotation *) +Definition R1 := 32%uint63. +Definition R2 := 24%uint63. +Definition R3 := 16%uint63. +Definition R4 := 63%uint63. + +Definition G (v: Vec16.t UInt64.t) (a b c d: Uint63.int) (x y: UInt64.t) +: Vec16.t UInt64.t +:= let ua := (Vec16.get_by_int v a) + (Vec16.get_by_int v b) + x in + let ud := ((Vec16.get_by_int v d) ^ ua) >>> R1 in + let uc := (Vec16.get_by_int v c) + ud in + let ub := ((Vec16.get_by_int v b) ^ uc) >>> R2 in + let wa := ua + ub + y in + let wd := (ud ^ wa) >>> R3 in + let wc := uc + wd in + let wb := (ub ^ wc) >>> R4 in + let va := Vec16.set_by_int v a wa in + let vb := Vec16.set_by_int va b wb in + let vc := Vec16.set_by_int vb c wc in + Vec16.set_by_int vc d wd. + +End MixingFunctionG. + + +Definition f_round (v m: Vec16.t UInt64.t) (s: Vec16.t Uint63.int) +: Vec16.t UInt64.t +:= let ms i := Vec16.get_by_int m (Vec16.get_by_int s i) in + (let v1 := G v 0 4 8 12 (ms 0) (ms 1) in + let v2 := G v1 1 5 9 13 (ms 2) (ms 3) in + let v3 := G v2 2 6 10 14 (ms 4) (ms 5) in + let v4 := G v3 3 7 11 15 (ms 6) (ms 7) in + let v5 := G v4 0 5 10 15 (ms 8) (ms 9) in + let v6 := G v5 1 6 11 12 (ms 10) (ms 11) in + let v7 := G v6 2 7 8 13 (ms 12) (ms 13) in + G v7 3 4 9 14 (ms 14) (ms 15))%uint63. + +Definition sigma +: Vec16.t (Vec16.t Uint63.int) +:= (let z := Vec16.fill 0 in + Vec16.Vec16 (Vec16.Vec16 0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15) + (Vec16.Vec16 14 10 4 8 9 15 13 6 1 12 0 2 11 7 5 3) + (Vec16.Vec16 11 8 12 0 5 2 15 13 10 14 3 6 7 1 9 4) + (Vec16.Vec16 7 9 3 1 13 12 11 14 2 6 5 10 4 0 15 8) + (Vec16.Vec16 9 0 5 7 2 4 10 15 14 1 11 12 6 8 3 13) + (Vec16.Vec16 2 12 6 10 0 11 8 3 4 13 7 5 15 14 1 9) + (Vec16.Vec16 12 5 1 15 14 13 4 10 0 7 6 3 9 2 8 11) + (Vec16.Vec16 13 11 7 14 12 1 3 9 5 0 15 4 8 6 2 10) + (Vec16.Vec16 6 15 14 9 11 3 0 8 12 2 13 7 1 4 10 5) + (Vec16.Vec16 10 2 8 4 7 6 1 5 15 11 9 14 3 12 13 0) + z z z z z z)%uint63. + +Fixpoint do_f_rounds_rec (v m: Vec16.t UInt64.t) (rounds_left: nat) (round_digit: Uint63.int) +{struct rounds_left} +: Vec16.t UInt64.t +:= match rounds_left with + | O => v + | S k => do_f_rounds_rec (f_round v m (Vec16.get_by_int sigma round_digit)) + m + k + (if round_digit + match b with + | (b16, b15, b14, b13, b12, b11, b10, b9, b8, b7, b6, b5, b4, b3, b2, b1, b0) => + Vec25 ( a0 ^ b0) (a1 ^ b1) (a2 ^ b2) (a3 ^ b3) (a4 ^ b4) + ( a5 ^ b5) (a6 ^ b6) (a7 ^ b7) (a8 ^ b8) (a9 ^ b9) + (a10 ^ b10) (a11 ^ b11) (a12 ^ b12) (a13 ^ b13) (a14 ^ b14) + (a15 ^ b15) (a16 ^ b16) a17 a18 a19 + a20 a21 a22 a23 a24 + end + end. + +Local Notation "x << y" := (UInt64.shl_uint63 x y). +Local Notation "x >> y" := (UInt64.shr_uint63 x y). +Local Notation "x | y" := (UInt64.bitwise_or x y) (at level 30). (* dangerous! messes up match! *) +Local Notation "x & y" := (UInt64.bitwise_and x y) (at level 30). +Local Notation "~ x" := (UInt64.bitwise_not x). + +Definition rot x k := ((x << k) | (x >> (64 - k)%uint63)). + +Definition round (rc: uint64) (a: vec25 uint64) (b: vec25 uint64) +: vec25 uint64 +:= match a, b with + | Vec25 a0 a1 a2 a3 a4 + a5 a6 a7 a8 a9 + a10 a11 a12 a13 a14 + a15 a16 a17 a18 a19 + a20 a21 a22 a23 a24, + Vec25 b0 b1 b2 b3 b4 + b5 b6 b7 b8 b9 + b10 b11 b12 b13 b14 + b15 b16 b17 b18 b19 + b20 b21 b22 b23 b24 => + + let bc0 := a0 ^ a5 ^ a10 ^ a15 ^ a20 in + let bc1 := a1 ^ a6 ^ a11 ^ a16 ^ a21 in + let bc2 := a2 ^ a7 ^ a12 ^ a17 ^ a22 in + let bc3 := a3 ^ a8 ^ a13 ^ a18 ^ a23 in + let bc4 := a4 ^ a9 ^ a14 ^ a19 ^ a24 in + + let d0 := bc4 ^ rot bc1 1%uint63 in + let d1 := bc0 ^ rot bc2 1%uint63 in + let d2 := bc1 ^ rot bc3 1%uint63 in + let d3 := bc2 ^ rot bc4 1%uint63 in + let d4 := bc3 ^ rot bc0 1%uint63 in + + let p0 := b0 ^ d0 in + let p1 := rot (b1 ^ d1) 44%uint63 in + let p2 := rot (b2 ^ d2) 43%uint63 in + let p3 := rot (b3 ^ d3) 21%uint63 in + let p4 := rot (b4 ^ d4) 14%uint63 in + + let z0 := p0 ^ (p2 & ~ p1) ^ rc in + let z1 := p1 ^ (p3 & ~ p2) in + let z2 := p2 ^ (p4 & ~ p3) in + let z3 := p3 ^ (p0 & ~ p4) in + let z4 := p4 ^ (p1 & ~ p0) in + + let q2 := rot (b5 ^ d0) 3%uint63 in + let q3 := rot (b6 ^ d1) 45%uint63 in + let q4 := rot (b7 ^ d2) 61%uint63 in + let q0 := rot (b8 ^ d3) 28%uint63 in + let q1 := rot (b9 ^ d4) 20%uint63 in + + let z5 := q0 ^ (q2 & ~ q1) in + let z6 := q1 ^ (q3 & ~ q2) in + let z7 := q2 ^ (q4 & ~ q3) in + let z8 := q3 ^ (q0 & ~ q4) in + let z9 := q4 ^ (q1 & ~ q0) in + + let r4 := rot (b10 ^ d0) 18%uint63 in + let r0 := rot (b11 ^ d1) 1%uint63 in + let r1 := rot (b12 ^ d2) 6%uint63 in + let r2 := rot (b13 ^ d3) 25%uint63 in + let r3 := rot (b14 ^ d4) 8%uint63 in + + let z10 := r0 ^ (r2 & ~ r1) in + let z11 := r1 ^ (r3 & ~ r2) in + let z12 := r2 ^ (r4 & ~ r3) in + let z13 := r3 ^ (r0 & ~ r4) in + let z14 := r4 ^ (r1 & ~ r0) in + + let s1 := rot (b15 ^ d0) 36%uint63 in + let s2 := rot (b16 ^ d1) 10%uint63 in + let s3 := rot (b17 ^ d2) 15%uint63 in + let s4 := rot (b18 ^ d3) 56%uint63 in + let s0 := rot (b19 ^ d4) 27%uint63 in + + let z15 := s0 ^ (s2 & ~ s1) in + let z16 := s1 ^ (s3 & ~ s2) in + let z17 := s2 ^ (s4 & ~ s3) in + let z18 := s3 ^ (s0 & ~ s4) in + let z19 := s4 ^ (s1 & ~ s0) in + + let t3 := rot (b20 ^ d0) 41%uint63 in + let t4 := rot (b21 ^ d1) 2%uint63 in + let t0 := rot (b22 ^ d2) 62%uint63 in + let t1 := rot (b23 ^ d3) 55%uint63 in + let t2 := rot (b24 ^ d4) 39%uint63 in + + let z20 := t0 ^ (t2 & ~ t1) in + let z21 := t1 ^ (t3 & ~ t2) in + let z22 := t2 ^ (t4 & ~ t3) in + let z23 := t3 ^ (t0 & ~ t4) in + let z24 := t4 ^ (t1 & ~ t0) in + + Vec25 z0 z1 z2 z3 z4 + z5 z6 z7 z8 z9 + z10 z11 z12 z13 z14 + z15 z16 z17 z18 z19 + z20 z21 z22 z23 z24 + end. + +Definition permute1 {T} (a: vec25 T) +:= match a with + | Vec25 a0 a1 a2 a3 a4 + a5 a6 a7 a8 a9 + a10 a11 a12 a13 a14 + a15 a16 a17 a18 a19 + a20 a21 a22 a23 a24 => + Vec25 a0 a11 a22 a8 a19 + a15 a1 a12 a23 a9 + a5 a16 a2 a13 a24 + a20 a6 a17 a3 a14 + a10 a21 a7 a18 a4 + end. +Definition permute2 {T} (a: vec25 T) +:= match a with + | Vec25 a0 a1 a2 a3 a4 + a5 a6 a7 a8 a9 + a10 a11 a12 a13 a14 + a15 a16 a17 a18 a19 + a20 a21 a22 a23 a24 => + Vec25 a0 a16 a7 a23 a14 + a20 a11 a2 a18 a9 + a15 a6 a22 a13 a4 + a10 a1 a17 a8 a24 + a5 a21 a12 a3 a19 + end. +Definition permute3 {T} (a: vec25 T) +:= match a with + | Vec25 a0 a1 a2 a3 a4 + a5 a6 a7 a8 a9 + a10 a11 a12 a13 a14 + a15 a16 a17 a18 a19 + a20 a21 a22 a23 a24 => + Vec25 a0 a6 a12 a18 a24 + a10 a16 a22 a3 a9 + a20 a1 a7 a13 a19 + a5 a11 a17 a23 a4 + a15 a21 a2 a8 a14 + end. +Lemma permute1_of_permute3 {T} (a: vec25 T): + permute1 (permute3 a) = a. +Proof. now destruct a. Qed. +Lemma permute3_of_permute1 {T} (a: vec25 T): + permute3 (permute1 a) = a. +Proof. now destruct a. Qed. +Lemma permute2_of_permute2 {T} (a: vec25 T): + permute2 (permute2 a) = a. +Proof. now destruct a. Qed. + + +Definition quad_round (a: vec25 uint64) (rcs: Tuplevector.t uint64 4) +: vec25 uint64 +:= match rcs with + | (rc4, rc3, rc2, rc1) => + let a1 := permute1 (round rc1 a (permute3 a)) in + let a2 := permute2 (round rc2 a1 (permute2 a1)) in + let a3 := permute3 (round rc3 a2 (permute1 a2)) in + round rc4 a3 a3 + end. + +Definition F1600 := fold_left quad_round rc_quads_backwards. + +End Permutation. + +(* Create padding of the given length (of the padding, not of the data). *) +Definition padding (len: positive) (start: int) (* start is 1 for Ethereum's Keccak, otherwise 6 *) +: list byte +:= match len with + | 1%positive => byte_of_int (128 lor start)%uint63 :: nil + | _ => (byte_of_int start) :: repeat (byte_of_int 0) (N.to_nat (N.pos len - 2)) ++ + byte_of_int 128 :: nil + end. + +(* The padding has the requested length *) +Lemma padding_ok (len: positive) (start: int): + List.length (padding len start) = Pos.to_nat len. +Proof. +unfold padding. +remember (byte_of_int start :: + repeat (byte_of_int 0) (N.to_nat (N.pos len - 2)) ++ + byte_of_int 128 :: + nil) as l. +assert (cons_length: forall {T} h (t: list T), List.length (h :: t) = S (List.length t)) by easy. +destruct len; cbn; subst; + repeat (rewrite List.app_length || rewrite List.repeat_length || rewrite cons_length); + replace (List.length (@nil byte)) with 0 by trivial; lia. +Qed. + +(** Calculate the padding length given the data length. *) +Definition padding_length (data_length: N) (rate: positive) +: positive +:= match (data_length mod N.pos rate)%N with + | 0%N => rate + | Npos p => rate - p + end. + +Lemma padding_length_ok (data_length: N) (rate: positive): + ((data_length + N.pos (padding_length data_length rate)) mod N.pos rate = 0)%N. +Proof. +unfold padding_length. +remember (data_length mod N.pos rate)%N as m. +destruct m; rewrite N.Div0.add_mod by discriminate; rewrite<- Heqm. +{ rewrite N.add_0_l. rewrite N.Div0.mod_same by discriminate. apply N.Div0.mod_0_l. } +assert(L: (N.pos p < N.pos rate)%N). +{ rewrite Heqm. apply N.mod_upper_bound. discriminate. } +replace (N.pos (rate - p) mod N.pos rate)%N with (N.pos (rate - p)). +2:{ symmetry. apply N.mod_small. lia. } +replace (N.pos p + N.pos (rate - p))%N with (N.pos rate) by lia. +apply N.Div0.mod_same. +Qed. + +Definition pad (unpadded_data: list byte) (rate: positive) (start: int) +: list byte +:= (unpadded_data ++ padding (padding_length (N.of_nat (List.length unpadded_data)) rate) start)%list. + +Lemma pad_ok_mod (data: list byte) (rate: positive) (start: int): + (N.of_nat (List.length (pad data rate start)) mod N.pos rate = 0)%N. +Proof. +unfold pad. rewrite List.app_length. rewrite Nat2N.inj_add. +remember (List.length data) as n. rewrite padding_ok. +rewrite positive_nat_N. rewrite padding_length_ok. +trivial. +Qed. + +Lemma pad_ok (data: list byte) (rate: positive) (start: int): + let d := List.length (pad data rate start) / Pos.to_nat rate in + List.length (pad data rate start) = d * Pos.to_nat rate. +Proof. +apply Nat2N.inj. +assert (M := pad_ok_mod data rate start). +remember (List.length _) as len. clear Heqlen. +match goal with |- ?lhs = ?rhs => rewrite<- (N.add_0_r rhs) end. +rewrite<- M. +rewrite Nat.mul_comm. +rewrite Nat2N.inj_mul. +rewrite Arith2.Nat2N_inj_div. +remember (Pos.to_nat rate) as r. +assert (R: N.pos rate = N.of_nat r). +{ subst. symmetry. apply positive_nat_N. } +rewrite R. rewrite R in M. +apply N.div_mod. +subst. assert(P := Pos2Nat.is_pos rate). +destruct (Pos.to_nat rate). +{ now apply Nat.lt_irrefl in P. } +discriminate. +Qed. + +Local Lemma can_gather_by_8 (n: nat): + n = n / 136 * 136 -> n = (n / 136 * 17) * 8. +Proof. +now rewrite<- Nat.mul_assoc. +Qed. + +Definition pad_by_136_and_gather_into_uint64s (data: list byte) (padding_start: int) +:= let padded := pad data 136%positive padding_start in + let PadOk := pad_ok data 136%positive padding_start in + List.map UInt64.uint64_of_be_bytes + (Tuplevector.gather padded _ 8 (can_gather_by_8 _ PadOk)). + +Lemma pad_by_136_and_gather_into_uint64s_length (data: list byte) (s: int): + List.length (pad_by_136_and_gather_into_uint64s data s) + = + (List.length (pad data 136 s)) / 136 * 17. +Proof. +unfold pad_by_136_and_gather_into_uint64s. +rewrite List.map_length. +apply (Tuplevector.gather_length (pad data 136 s) + (Datatypes.length (pad data 136 s) / 136 * 17) 8 + (can_gather_by_8 (Datatypes.length (pad data 136 s)) (pad_ok data 136 s))). +Qed. + +Definition blocks (data: list byte) (padding_start: int) +:= Tuplevector.gather (pad_by_136_and_gather_into_uint64s data padding_start) + _ 17 + (pad_by_136_and_gather_into_uint64s_length data padding_start). + +Definition absorb (data: list byte) (padding_start: int) +:= fold_left (fun state block => F1600 (vec25_xor_tuple17_backwards state block)) + (blocks data padding_start) + vec25_zeros. + +Definition squeeze_256 (a: vec25 uint64) +:= match a with + | Vec25 a0 a1 a2 a3 _ + _ _ _ _ _ + _ _ _ _ _ + _ _ _ _ _ + _ _ _ _ _ => + let eights: list (Tuplevector.t byte 8) + := map UInt64.uint64_to_le_bytes (a0 :: a1 :: a2 :: a3 :: nil) + in fold_right Tuplevector.app_to_list nil eights + end. + +Definition keccak_256 (data: list byte): list byte := squeeze_256 (absorb data 1). +Definition sha3_256 (data: list byte): list byte := squeeze_256 (absorb data 6). + +Definition keccak_256_of_string (s: String.string) +:= keccak_256 (bytes_of_string s). +Definition sha3_256_of_string (s: String.string) +:= sha3_256 (bytes_of_string s). + +Definition keccak_256_hex (data: list byte) +: String.string +:= hex_of_bytes (keccak_256 data) true. +Definition sha3_256_hex (data: list byte) +: String.string +:= hex_of_bytes (sha3_256 data) true. + +Definition keccak_256_hex_of_string (s: String.string) +: String.string +:= hex_of_bytes (keccak_256_of_string s) true. +Definition sha3_256_hex_of_string (s: String.string) +: String.string +:= hex_of_bytes (sha3_256_of_string s) true. + +(* This test is from Go's sha3_test.go. *) +Example keccak_256_smoke_test: + keccak_256_hex_of_string "abc" + = + "4e03657aea45a94fc7d47ba826c8d667c0d1e6e33a64a036ec44f58fa12d6c45". +Proof. trivial. Qed. + +(* A byte-long test from XKCP's ShortMsgKAT_SHA3-256.txt. *) +Example sha3_256_test_CC: + sha3_256_hex (byte_of_N (HexString.to_N "0xCC") :: nil) + = + "677035391cd3701293d385f037ba32796252bb7ce180b00b582dd9b20aaad7f0". +Proof. trivial. Qed. diff --git a/coq/CoqOfSolidity/CoqEvm/Crypto/RIPEMD160.v b/coq/CoqOfSolidity/CoqEvm/Crypto/RIPEMD160.v new file mode 100644 index 000000000000..28c2f85128d1 --- /dev/null +++ b/coq/CoqOfSolidity/CoqEvm/Crypto/RIPEMD160.v @@ -0,0 +1,239 @@ +From Coq Require Import NArith ZArith Uint63 String. +From Coq Require HexString. + +From CoqOfSolidity Require Import Nibble. +From CoqOfSolidity Require Vec16. +From CoqOfSolidity Require SHA256. + + +(** This is a port of Go's golang.org/x/crypto/ripemd160. *) +(** See also: + https://homes.esat.kuleuven.be/~bosselae/ripemd160.html + and + https://en.bitcoin.it/wiki/RIPEMD-160 +*) + + +Local Open Scope int63_scope. +Local Open Scope string_scope. + +(* This is almost the same as SHA256 padding but the length is little-endian. *) +Definition pad (data: list byte) +: list byte +:= let len := N.of_nat (List.length data) in + let len_in_bits := N.shiftl len 3 in + data + ++ + SHA256.padding (SHA256.padding_length len) + ++ + Tuplevector.app_to_list + (UInt64.uint64_to_le_bytes + (UInt64.uint64_of_Z_mod + (Z.of_N len_in_bits)): Tuplevector.t _ 8) + nil. + +(* This is exactly the same as its SHA256 counterpart. *) +Lemma pad_ok_mod (data: list byte): + ((N.of_nat (List.length (pad data))) mod 64 = 0)%N. +Proof. +unfold pad. +repeat rewrite List.app_length. +rewrite Tuplevector.app_to_list_length. +repeat rewrite Nat2N.inj_add. +rewrite N.add_assoc. +rewrite N.Div0.add_mod by discriminate. +cbn. +remember (N.of_nat (List.length data)) as n. +rewrite SHA256.padding_ok. +rewrite SHA256.padding_length_ok. +trivial. +Qed. + +Lemma pad_ok (data: list byte): + let d := (List.length (pad data) / 64)%nat in + (List.length (pad data) = d * 64)%nat. +Proof. +apply Nat2N.inj. +assert (M := pad_ok_mod data). +remember (List.length _) as len. clear Heqlen. +match goal with |- ?lhs = ?rhs => rewrite<- (N.add_0_r rhs) end. +rewrite<- M. +rewrite Nat.mul_comm. +rewrite Nat2N.inj_mul. +rewrite Arith2.Nat2N_inj_div. +apply N.div_mod. +subst. discriminate. +Qed. + +Definition int_of_4_be_bytes (b: byte * byte * byte * byte) +: int +:= let '(b3, b2, b1, b0) := b in + ((int_of_byte b3 << 24) lor + (int_of_byte b2 << 16) lor + (int_of_byte b1 << 8) lor + (int_of_byte b0))%uint63. + +Definition pad_and_gather_into_uint32s (data: list byte) +:= let padded := pad data in + let PadOk := pad_ok data in + List.map int_of_4_be_bytes (* gather flips the tuples *) + (Tuplevector.gather padded _ 4 (SHA256.can_gather_by_4 _ PadOk)). + +Lemma pad_and_gather_into_uint32s_length (data: list byte): + let d := (List.length (pad data) / 64)%nat in + (List.length (pad_and_gather_into_uint32s data) = d * 16)%nat. +Proof. +unfold pad_and_gather_into_uint32s. +rewrite List.map_length. +apply (Tuplevector.gather_length (pad data) (Datatypes.length (pad data) / 64 * 16) 4 + (SHA256.can_gather_by_4 (Datatypes.length (pad data)) (pad_ok data))). +Qed. + +Definition block_of_tuple (block: Tuplevector.t int 16) +: Vec16.t int +:= let '(bF, bE, bD, bC, bB, bA, b9, b8, b7, b6, b5, b4, b3, b2, b1, b0) := block in + Vec16.Vec16 b0 b1 b2 b3 b4 b5 b6 b7 b8 b9 bA bB bC bD bE bF. + +Definition blocks (data: list byte) +: list (Vec16.t int) +:= List.map block_of_tuple + (Tuplevector.gather (pad_and_gather_into_uint32s data) + _ 16 + (pad_and_gather_into_uint32s_length data)). + +(*************************************************************************) + +Inductive vec5 (T: Type) +:= Vec5 (a b c d e: T). +Arguments Vec5 {_}. + +Definition vec5_to_list {T: Type} (v: vec5 T) +: list T +:= let 'Vec5 a b c d e := v in + a :: b :: c :: d :: e :: nil. + +Definition vec5_map {A B: Type} (f: A -> B) (v: vec5 A) +: vec5 B +:= let 'Vec5 a b c d e := v in + Vec5 (f a) (f b) (f c) (f d) (f e). + +(* ripemd160block.go *) +Local Definition _n1: Vec16.t int := Vec16.Vec16 0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15. +Local Definition _n2: Vec16.t int := Vec16.Vec16 7 4 13 1 10 6 15 3 12 0 9 5 2 14 11 8. +Local Definition _n3: Vec16.t int := Vec16.Vec16 3 10 14 4 9 15 8 1 2 7 0 6 13 11 5 12. +Local Definition _n4: Vec16.t int := Vec16.Vec16 1 9 11 10 0 8 12 4 13 3 7 15 14 5 6 2. +Local Definition _n5: Vec16.t int := Vec16.Vec16 4 0 5 9 7 12 2 10 14 1 3 8 11 6 15 13. + +Local Definition _r1: Vec16.t int := Vec16.Vec16 11 14 15 12 5 8 7 9 11 13 14 15 6 7 9 8. +Local Definition _r2: Vec16.t int := Vec16.Vec16 7 6 8 13 11 9 7 15 7 12 15 9 11 7 13 12. +Local Definition _r3: Vec16.t int := Vec16.Vec16 11 13 6 7 14 9 13 15 14 8 13 6 5 12 7 5. +Local Definition _r4: Vec16.t int := Vec16.Vec16 11 12 14 15 14 15 9 8 9 14 5 6 8 6 5 12. +Local Definition _r5: Vec16.t int := Vec16.Vec16 9 15 5 11 6 8 13 12 5 12 13 14 11 8 5 6. + +Local Definition n_1: Vec16.t int := Vec16.Vec16 5 14 7 0 9 2 11 4 13 6 15 8 1 10 3 12. +Local Definition n_2: Vec16.t int := Vec16.Vec16 6 11 3 7 0 13 5 10 14 15 8 12 4 9 1 2. +Local Definition n_3: Vec16.t int := Vec16.Vec16 15 5 1 3 7 14 6 9 11 8 12 2 10 0 4 13. +Local Definition n_4: Vec16.t int := Vec16.Vec16 8 6 4 1 3 11 15 0 5 12 2 13 9 7 10 14. +Local Definition n_5: Vec16.t int := Vec16.Vec16 12 15 10 4 1 5 8 7 6 2 13 14 0 3 9 11. + +Local Definition r_1: Vec16.t int := Vec16.Vec16 8 9 9 11 13 15 15 5 7 7 8 11 14 14 12 6. +Local Definition r_2: Vec16.t int := Vec16.Vec16 9 13 15 7 12 8 9 11 7 7 12 7 6 15 13 11. +Local Definition r_3: Vec16.t int := Vec16.Vec16 9 7 15 11 8 6 6 14 12 13 5 14 13 13 7 5. +Local Definition r_4: Vec16.t int := Vec16.Vec16 15 5 8 11 14 14 6 14 6 9 12 9 12 5 15 8. +Local Definition r_5: Vec16.t int := Vec16.Vec16 8 5 12 9 12 5 14 6 8 13 6 5 15 13 11 11. + +Definition uint32_mask: int := (1 << 32) - 1. +Definition uint32_not (i: int) := (uint32_mask lxor i)%uint63. + +(* Rotate an int left as if it was uint32. *) +Definition rot x k := ((x << k) lor ((x land uint32_mask) >> (32 - k)))%uint63. + +Definition f1 (x y z: int): int := x lxor y lxor z. +Definition f2 (x y z: int): int := (x land y) lor (uint32_not x land z). +Definition f3 (x y z: int): int := (x lor uint32_not y) lxor z. +Definition f4 (x y z: int): int := (x land z) lor (y land uint32_not z). +Definition f5 (x y z: int): int := x lxor (y lor uint32_not z). + +Definition round (n r: Vec16.t int) (const: int) (f: int -> int -> int -> int) + (x: Vec16.t int) (s: vec5 int) (i: int) +: vec5 int +:= let 'Vec5 a b c d e := s in + let alpha := (a + + f b c d + + Vec16.get_by_int x (Vec16.get_by_int n i) + + const)%uint63 in + let alpha' := (rot alpha (Vec16.get_by_int r i) + e)%uint63 in + let beta := rot c 10 in + Vec5 e alpha' b beta d. + +Definition int_of_hex (s: string) := Uint63.of_Z (HexString.to_Z s). + +Definition iota: Vec16.t int := Vec16.Vec16 0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15. + +Definition round1a x := Vec16.fold_left (round _n1 _r1 (int_of_hex "0x0") f1 x) iota. +Definition round2a x := Vec16.fold_left (round _n2 _r2 (int_of_hex "0x5a827999") f2 x) iota. +Definition round3a x := Vec16.fold_left (round _n3 _r3 (int_of_hex "0x6ed9eba1") f3 x) iota. +Definition round4a x := Vec16.fold_left (round _n4 _r4 (int_of_hex "0x8f1bbcdc") f4 x) iota. +Definition round5a x := Vec16.fold_left (round _n5 _r5 (int_of_hex "0xa953fd4e") f5 x) iota. +Definition round1b x := Vec16.fold_left (round n_1 r_1 (int_of_hex "0x50a28be6") f5 x) iota. +Definition round2b x := Vec16.fold_left (round n_2 r_2 (int_of_hex "0x5c4dd124") f4 x) iota. +Definition round3b x := Vec16.fold_left (round n_3 r_3 (int_of_hex "0x6d703ef3") f3 x) iota. +Definition round4b x := Vec16.fold_left (round n_4 r_4 (int_of_hex "0x7a6d76e9") f2 x) iota. +Definition round5b x := Vec16.fold_left (round n_5 r_5 (int_of_hex "0x0") f1 x) iota. + +Local Definition init_hex: vec5 string +:= Vec5 "0x67452301" + "0xefcdab89" + "0x98badcfe" + "0x10325476" + "0xc3d2e1f0". +Local Definition init: vec5 int := vec5_map int_of_hex init_hex. + +Definition rounds_a x s := round5a x (round4a x (round3a x (round2a x (round1a x s)))). +Definition rounds_b x s := round5b x (round4b x (round3b x (round2b x (round1b x s)))). + +Definition absorb_block (s: vec5 int) (x: Vec16.t int) +: vec5 int +:= let 'Vec5 s0 s1 s2 s3 s4 := s in + let 'Vec5 a0 a1 a2 a3 a4 := rounds_a x s in + let 'Vec5 b0 b1 b2 b3 b4 := rounds_b x s in + Vec5 (s1 + a2 + b3)%uint63 + (s2 + a3 + b4)%uint63 + (s3 + a4 + b0)%uint63 + (s4 + a0 + b1)%uint63 + (s0 + a1 + b2)%uint63. + +Definition absorb (data: list byte) +:= List.fold_left absorb_block (blocks data) init. + +Definition le_4_bytes_of_int (i: int) +:= (byte_of_int i + :: byte_of_int (i >> 8) + :: byte_of_int (i >> 16) + :: byte_of_int (i >> 24) :: nil)%list%uint63. + +Definition squeeze (state: vec5 int) +:= List.concat (List.map le_4_bytes_of_int (vec5_to_list state)). + +Definition ripemd160 (data: list byte) +: list byte +:= squeeze (absorb data). + +Definition ripemd160_of_string (s: String.string) +:= ripemd160 (bytes_of_string s). + +Definition ripemd160_hex (data: list byte) +: String.string +:= hex_of_bytes (ripemd160 data) true. + +Definition ripemd160_hex_of_string (s: String.string) +: String.string +:= hex_of_bytes (ripemd160_of_string s) true. + +(* From https://homes.esat.kuleuven.be/~bosselae/ripemd160.html *) +Example smoke_test: + ripemd160_hex_of_string + "abcdefghijklmnopqrstuvwxyz" + = + "f71c27109c692c1b56bbdceb5b9d2865b3708dbc"%string. +Proof. trivial. Qed. \ No newline at end of file diff --git a/coq/CoqOfSolidity/CoqEvm/Crypto/SHA256.v b/coq/CoqOfSolidity/CoqEvm/Crypto/SHA256.v new file mode 100644 index 000000000000..12bcbaed6b27 --- /dev/null +++ b/coq/CoqOfSolidity/CoqEvm/Crypto/SHA256.v @@ -0,0 +1,282 @@ +(** This is a port of Go's crypto/sha256. *) + +From Coq Require Import NArith ZArith Lia Uint63. +From Coq Require Import String HexString. + +From CoqOfSolidity Require Import Nibble UInt64. +From CoqOfSolidity Require Tuplevector Vec8. + +Definition output_size := 32. +Definition block_size := 64. + + +Definition vec8_add (a b: Vec8.t int) +:= let 'Vec8.Vec8 a0 a1 a2 a3 a4 a5 a6 a7 := a in + let 'Vec8.Vec8 b0 b1 b2 b3 b4 b5 b6 b7 := b in + (Vec8.Vec8 (a0 + b0) (a1 + b1) (a2 + b2) (a3 + b3) + (a4 + b4) (a5 + b5) (a6 + b6) (a7 + b7))%uint63. + +Definition init_hex: Vec8.t string +:= (Vec8.Vec8 "0x6A09E667" + "0xBB67AE85" + "0x3C6EF372" + "0xA54FF53A" + "0x510E527F" + "0x9B05688C" + "0x1F83D9AB" + "0x5BE0CD19")%string. + +Definition init := Vec8.map Uint63.of_Z (Vec8.map HexString.to_Z init_hex). + +Definition K_hex: Vec8.t (Vec8.t string) +:= (Vec8.Vec8 (Vec8.Vec8 "0x428a2f98" "0x71374491" "0xb5c0fbcf" "0xe9b5dba5" + "0x3956c25b" "0x59f111f1" "0x923f82a4" "0xab1c5ed5") + (Vec8.Vec8 "0xd807aa98" "0x12835b01" "0x243185be" "0x550c7dc3" + "0x72be5d74" "0x80deb1fe" "0x9bdc06a7" "0xc19bf174") + (Vec8.Vec8 "0xe49b69c1" "0xefbe4786" "0x0fc19dc6" "0x240ca1cc" + "0x2de92c6f" "0x4a7484aa" "0x5cb0a9dc" "0x76f988da") + (Vec8.Vec8 "0x983e5152" "0xa831c66d" "0xb00327c8" "0xbf597fc7" + "0xc6e00bf3" "0xd5a79147" "0x06ca6351" "0x14292967") + (Vec8.Vec8 "0x27b70a85" "0x2e1b2138" "0x4d2c6dfc" "0x53380d13" + "0x650a7354" "0x766a0abb" "0x81c2c92e" "0x92722c85") + (Vec8.Vec8 "0xa2bfe8a1" "0xa81a664b" "0xc24b8b70" "0xc76c51a3" + "0xd192e819" "0xd6990624" "0xf40e3585" "0x106aa070") + (Vec8.Vec8 "0x19a4c116" "0x1e376c08" "0x2748774c" "0x34b0bcb5" + "0x391c0cb3" "0x4ed8aa4a" "0x5b9cca4f" "0x682e6ff3") + (Vec8.Vec8 "0x748f82ee" "0x78a5636f" "0x84c87814" "0x8cc70208" + "0x90befffa" "0xa4506ceb" "0xbef9a3f7" "0xc67178f2"))%string. +Definition K := Vec8.map (Vec8.map (fun hex => Uint63.of_Z (HexString.to_Z hex))) K_hex. + + +(** Calculate the padding length given the data length. *) +Definition padding_length (data_length: N) +: N +:= let m := (data_length mod 64)%N in + if (m 0%N. +Proof. +unfold padding_length. +remember (_ 0)%N) by discriminate. +assert (B := N.mod_upper_bound len 64 F). +lia. +Qed. + +Lemma padding_length_ok (len: N): + ((len + padding_length len) mod 64 = 56)%N. +Proof. +unfold padding_length. +assert (F: (64 <> 0)%N) by discriminate. +assert (B := N.mod_upper_bound len 64 F). +rewrite N.Div0.add_mod by discriminate. +rewrite N.Div0.add_mod_idemp_r by discriminate. +remember (len mod 64)%N as n. +remember (_ nil + | S k => (byte_of_int 128 :: List.repeat (byte_of_int 0) k)%list + end. + +Lemma padding_ok (len: N): + N.of_nat (List.length (padding len)) = len. +Proof. +unfold padding. +destruct len. { easy. } +rewrite positive_N_nat. +assert (P := Pos2Nat.is_pos p). +rewrite<- positive_nat_N. +remember (Pos.to_nat p) as n. +destruct n. { now apply Nat.lt_irrefl in P. } +cbn. now rewrite List.repeat_length. +Qed. + +Definition pad (data: list byte) +: list byte +:= let len := N.of_nat (List.length data) in + let len_in_bits := N.shiftl len 3 in + data + ++ + padding (padding_length len) + ++ + Tuplevector.app_to_list + (uint64_to_be_bytes + (uint64_of_Z_mod + (Z.of_N len_in_bits)): Tuplevector.t _ 8) + nil. + +Lemma pad_ok_mod (data: list byte): + ((N.of_nat (List.length (pad data))) mod 64 = 0)%N. +Proof. +unfold pad. +repeat rewrite List.app_length. +rewrite Tuplevector.app_to_list_length. +repeat rewrite Nat2N.inj_add. +rewrite N.add_assoc. +rewrite N.Div0.add_mod by discriminate. +cbn. +remember (N.of_nat (List.length data)) as n. +rewrite padding_ok. +rewrite padding_length_ok. +trivial. +Qed. + +Lemma pad_ok (data: list byte): + let d := (List.length (pad data) / 64)%nat in + (List.length (pad data) = d * 64)%nat. +Proof. +apply Nat2N.inj. +assert (M := pad_ok_mod data). +remember (List.length _) as len. clear Heqlen. +match goal with |- ?lhs = ?rhs => rewrite<- (N.add_0_r rhs) end. +rewrite<- M. +rewrite Nat.mul_comm. +rewrite Nat2N.inj_mul. +rewrite Arith2.Nat2N_inj_div. +apply N.div_mod. +subst. discriminate. +Qed. + +Lemma can_gather_by_4 (n: nat): + (n = n / 64 * 64 -> n = (n / 64 * 16) * 4)%nat. +Proof. +now rewrite<- Nat.mul_assoc. +Qed. + +Definition int_of_4_le_bytes (b: byte * byte * byte * byte) +: int +:= let '(b0, b1, b2, b3) := b in + ((int_of_byte b3 << 24) lor + (int_of_byte b2 << 16) lor + (int_of_byte b1 << 8) lor + (int_of_byte b0))%uint63. + +Definition pad_and_gather_into_uint32s (data: list byte) +:= let padded := pad data in + let PadOk := pad_ok data in + List.map int_of_4_le_bytes (* gather flips the tuples *) + (Tuplevector.gather padded _ 4 (can_gather_by_4 _ PadOk)). + +Lemma pad_and_gather_into_uint32s_length (data: list byte): + let d := (List.length (pad data) / 64)%nat in + (List.length (pad_and_gather_into_uint32s data) = d * 16)%nat. +Proof. +unfold pad_and_gather_into_uint32s. +rewrite List.map_length. +apply (Tuplevector.gather_length (pad data) (Datatypes.length (pad data) / 64 * 16) 4 + (can_gather_by_4 (Datatypes.length (pad data)) (pad_ok data))). +Qed. + +Definition vec64 (T: Type) := Vec8.t (Vec8.t T). + +Definition block_of_tuple (block: Tuplevector.t int 16) +: vec64 int +:= let z := (Vec8.Vec8 0 0 0 0 0 0 0 0)%uint63 in + let '(bF, bE, bD, bC, bB, bA, b9, b8, b7, b6, b5, b4, b3, b2, b1, b0) := block in + Vec8.Vec8 (Vec8.Vec8 b0 b1 b2 b3 b4 b5 b6 b7) (Vec8.Vec8 b8 b9 bA bB bC bD bE bF) z z z z z z. + +Definition blocks (data: list byte) +: list (vec64 int) +:= List.map block_of_tuple + (Tuplevector.gather (pad_and_gather_into_uint32s data) + _ 16 + (pad_and_gather_into_uint32s_length data)). + +Definition vec64_get {T: Type} (v: vec64 T) (i: int) +:= Vec8.get (Vec8.get v (i >> 3)%uint63) i. + +Definition vec64_set {T: Type} (v: vec64 T) (i: int) (new: T) +:= let hi := (i >> 3)%uint63 in + Vec8.set v hi (Vec8.set (Vec8.get v hi) i new). + +Definition uint32_mask := ((1 << 32) - 1)%uint63. + +Definition shr (i sh: int) := ((i land uint32_mask) >> sh)%uint63. +Definition rot (i sh: int) := (shr i sh lor (i << (32 - sh)))%uint63. + +Fixpoint calc_w_rec (n: nat) (start: vec64 int) +:= match n with + | O => start + | S k => (let w := calc_w_rec k start in + let i := Uint63.of_Z (Z.of_nat n + 15)%Z in + let v1 := vec64_get w (i - 2)%uint63 in + let t1 := (rot v1 17) lxor (rot v1 19) lxor (shr v1 10) in + let v2 := vec64_get w (i - 15)%uint63 in + let t2 := (rot v2 7) lxor (rot v2 18) lxor (shr v2 3) in + vec64_set w i (t1 + vec64_get w (i-7) + t2 + vec64_get w (i-16)))%uint63 + end. +Definition calc_w (w: vec64 int) := calc_w_rec 48 w. + +Fixpoint do_block_rec (n: nat) (initial_state: Vec8.t int) (w_after_calc: vec64 int) +: Vec8.t int +:= match n with + | O => initial_state + | S k => let state := do_block_rec k initial_state w_after_calc in + let i := Uint63.of_Z (Z.of_nat k) in + let 'Vec8.Vec8 a b c d e f g h := state in + (let t1 := h + ((rot e 6) lxor (rot e 11) lxor (rot e 25)) + + ((e land f) lxor ((e lxor uint32_mask) land g)) + + vec64_get K i + + vec64_get w_after_calc i in + let t2 := ((rot a 2) lxor (rot a 13) lxor (rot a 22)) + + ((a land b) lxor (a land c) lxor (b land c)) in + Vec8.Vec8 (t1 + t2) a b c (d + t1) e f g)%uint63 + end. +Definition do_block (state: Vec8.t int) (w: vec64 int) +:= do_block_rec 64 state w. + +Definition absorb_block (state: Vec8.t int) (w: vec64 int) +:= vec8_add state (do_block state (calc_w w)). + +Definition absorb (data: list byte) +:= List.fold_left absorb_block (blocks data) init. + +Definition be_4_bytes_of_int (i: int) +:= (byte_of_int (i >> 24) + :: byte_of_int (i >> 16) + :: byte_of_int (i >> 8) + :: byte_of_int i :: nil)%list%uint63. + +Definition squeeze (state: Vec8.t int) +:= List.concat (List.map be_4_bytes_of_int (Vec8.to_list state)). + +Definition sha256 (data: list byte) +: list byte +:= squeeze (absorb data). + +Definition sha256_of_string (s: String.string) +:= sha256 (bytes_of_string s). + +Definition sha256_hex (data: list byte) +: String.string +:= hex_of_bytes (sha256 data) true. + +Definition sha256_hex_of_string (s: String.string) +: String.string +:= hex_of_bytes (sha256_of_string s) true. + +(* This test is from Go's sha256_test.go. *) +Example smoke_test: + sha256_hex_of_string + "For every action there is an equal and opposite government program." + = + "23b1018cd81db1d67983c5f7417c44da9deb582459e378d7a068552ea649dc9f"%string. +Proof. trivial. Qed. \ No newline at end of file diff --git a/coq/CoqOfSolidity/CoqEvm/Instructions.v b/coq/CoqOfSolidity/CoqEvm/Instructions.v new file mode 100644 index 000000000000..acec777125ee --- /dev/null +++ b/coq/CoqOfSolidity/CoqEvm/Instructions.v @@ -0,0 +1,660 @@ +From Coq Require Import Arith NArith ZArith String. +From Coq Require Import Lia Bool. +From Coq Require Import Eqdep_dec. +From Coq Require Import Uint63. + +Require Import Nibble. +Local Open Scope N_scope. + +Inductive instruction := +(* 0x00 *) +| STOP +| ADD +| MUL +| SUB +| DIV +| SDIV +| MOD +| SMOD +| ADDMOD +| MULMOD +| EXP +| SIGNEXTEND + +(* 0x10 *) +| LT +| GT +| SLT +| SGT +| EQ +| ISZERO +| AND +| OR +| XOR +| NOT +| BYTE +| SHL +| SHR +| SAR + +(* 0x20 *) +| SHA3 + +(* 0x30 *) +| ADDRESS +| BALANCE +| ORIGIN +| CALLER +| CALLVALUE +| CALLDATALOAD +| CALLDATASIZE +| CALLDATACOPY +| CODESIZE +| CODECOPY +| GASPRICE +| EXTCODESIZE +| EXTCODECOPY +| RETURNDATASIZE +| RETURNDATACOPY +| EXTCODEHASH + +(* 0x40 *) +| BLOCKHASH +| COINBASE +| TIMESTAMP +| NUMBER +| DIFFICULTY +| GASLIMIT +| CHAINID (* https://eips.ethereum.org/EIPS/eip-1344 *) +| SELFBALANCE + +(* 0x50 *) +| POP +| MLOAD +| MSTORE +| MSTORE8 +| SLOAD +| SSTORE +| JUMP +| JUMPI +| PC +| MSIZE +| GAS +| JUMPDEST + +(* 0x60 *) +| PUSH (n: N) (ok: andb (0 x x0 x0 + | ADD => x x0 x1 + | MUL => x x0 x2 + | SUB => x x0 x3 + | DIV => x x0 x4 + | SDIV => x x0 x5 + | MOD => x x0 x6 + | SMOD => x x0 x7 + | ADDMOD => x x0 x8 + | MULMOD => x x0 x9 + | EXP => x x0 xA + | SIGNEXTEND => x x0 xB + + (* 0x10 *) + | LT => x x1 x0 + | GT => x x1 x1 + | SLT => x x1 x2 + | SGT => x x1 x3 + | EQ => x x1 x4 + | ISZERO => x x1 x5 + | AND => x x1 x6 + | OR => x x1 x7 + | XOR => x x1 x8 + | NOT => x x1 x9 + | BYTE => x x1 xA + | SHL => x x1 xB + | SHR => x x1 xC + | SAR => x x1 xD + + (* 0x20 *) + | SHA3 => x x2 x0 + + (* 0x30 *) + | ADDRESS => x x3 x0 + | BALANCE => x x3 x1 + | ORIGIN => x x3 x2 + | CALLER => x x3 x3 + | CALLVALUE => x x3 x4 + | CALLDATALOAD => x x3 x5 + | CALLDATASIZE => x x3 x6 + | CALLDATACOPY => x x3 x7 + | CODESIZE => x x3 x8 + | CODECOPY => x x3 x9 + | GASPRICE => x x3 xA + | EXTCODESIZE => x x3 xB + | EXTCODECOPY => x x3 xC + | RETURNDATASIZE => x x3 xD + | RETURNDATACOPY => x x3 xE + | EXTCODEHASH => x x3 xF + + (* 0x40 *) + | BLOCKHASH => x x4 x0 + | COINBASE => x x4 x1 + | TIMESTAMP => x x4 x2 + | NUMBER => x x4 x3 + | DIFFICULTY => x x4 x4 + | GASLIMIT => x x4 x5 + | CHAINID => x x4 x6 + | SELFBALANCE => x x4 x7 + + (* 0x50 *) + | POP => x x5 x0 + | MLOAD => x x5 x1 + | MSTORE => x x5 x2 + | MSTORE8 => x x5 x3 + | SLOAD => x x5 x4 + | SSTORE => x x5 x5 + | JUMP => x x5 x6 + | JUMPI => x x5 x7 + | PC => x x5 x8 + | MSIZE => x x5 x9 + | GAS => x x5 xA + | JUMPDEST => x x5 xB + + (* 0x60 *) + | PUSH n ok => opcode_of_push n ok + + (* 0x80 *) + | DUP n ok => opcode_of_dup n ok + + (* 0x90 *) + | SWAP n ok => opcode_of_swap n ok + + (* 0xa0 *) + | LOG n ok => opcode_of_log n ok + + (* 0xf0 *) + | CREATE => x xF x0 + | CALL => x xF x1 + | CALLCODE => x xF x2 + | RETURN => x xF x3 + | DELEGATECALL => x xF x4 + | CREATE2 => x xF x5 + | STATICCALL => x xF xA + | REVERT => x xF xD + | SELFDESTRUCT => x xF xF + end. + +Definition instruction_of_byte (b: byte) +: option instruction +:= let (high, low) := hex_digits_of_byte b in + match high with + | x0 => + match low with + | x0 => Some STOP + | x1 => Some ADD + | x2 => Some MUL + | x3 => Some SUB + | x4 => Some DIV + | x5 => Some SDIV + | x6 => Some MOD + | x7 => Some SMOD + | x8 => Some ADDMOD + | x9 => Some MULMOD + | xA => Some EXP + | xB => Some SIGNEXTEND + | _ => None + end + | x1 => + match low with + | x0 => Some LT + | x1 => Some GT + | x2 => Some SLT + | x3 => Some SGT + | x4 => Some EQ + | x5 => Some ISZERO + | x6 => Some AND + | x7 => Some OR + | x8 => Some XOR + | x9 => Some NOT + | xA => Some BYTE + | xB => Some SHL + | xC => Some SHR + | xD => Some SAR + | _ => None + end + | x2 => + match low with + | x0 => Some SHA3 + | _ => None + end + | x3 => + match low with + | x0 => Some ADDRESS + | x1 => Some BALANCE + | x2 => Some ORIGIN + | x3 => Some CALLER + | x4 => Some CALLVALUE + | x5 => Some CALLDATALOAD + | x6 => Some CALLDATASIZE + | x7 => Some CALLDATACOPY + | x8 => Some CODESIZE + | x9 => Some CODECOPY + | xA => Some GASPRICE + | xB => Some EXTCODESIZE + | xC => Some EXTCODECOPY + | xD => Some RETURNDATASIZE + | xE => Some RETURNDATACOPY + | xF => Some EXTCODEHASH + end + | x4 => + match low with + | x0 => Some BLOCKHASH + | x1 => Some COINBASE + | x2 => Some TIMESTAMP + | x3 => Some NUMBER + | x4 => Some DIFFICULTY + | x5 => Some GASLIMIT + | x6 => Some CHAINID + | x7 => Some SELFBALANCE + | _ => None + end + | x5 => + match low with + | x0 => Some POP + | x1 => Some MLOAD + | x2 => Some MSTORE + | x3 => Some MSTORE8 + | x4 => Some SLOAD + | x5 => Some SSTORE + | x6 => Some JUMP + | x7 => Some JUMPI + | x8 => Some PC + | x9 => Some MSIZE + | xA => Some GAS + | xB => Some JUMPDEST + | _ => None + end + | x6 => Some (x6_to_push low) + | x7 => Some (x7_to_push low) + | x8 => Some (x8_to_dup low) + | x9 => Some (x9_to_swap low) + | xA => + match low with + | x0 => Some (LOG 0 eq_refl) + | x1 => Some (LOG 1 eq_refl) + | x2 => Some (LOG 2 eq_refl) + | x3 => Some (LOG 3 eq_refl) + | x4 => Some (LOG 4 eq_refl) + | _ => None + end + | xF => + match low with + | x0 => Some CREATE + | x1 => Some CALL + | x2 => Some CALLCODE + | x3 => Some RETURN + | x4 => Some DELEGATECALL + | x5 => Some CREATE2 + (* 6-9 => None *) + | xA => Some STATICCALL + (* B,C => None *) + | xD => Some REVERT + (* E => None *) + | xF => Some SELFDESTRUCT + | _ => None + end + | _ => None + end. + +Lemma byte_of_instruction_of_byte (b: byte): + match instruction_of_byte b with + | Some op => byte_of_instruction op = b + | None => True + end. +Proof. +cbn. destruct b. +destruct a7; destruct a6; destruct a5; destruct a4; +destruct a3; destruct a2; destruct a1; destruct a0; easy. +Qed. + +Lemma instruction_irrel {bound: N} + (OP: forall n: N, (0 instruction) + {a b: N} + (OkA: (0 (0, 0) + | ADD => (2, 1) + | MUL => (2, 1) + | SUB => (2, 1) + | DIV => (2, 1) + | SDIV => (2, 1) + | MOD => (2, 1) + | SMOD => (2, 1) + | ADDMOD => (3, 1) + | MULMOD => (3, 1) + | EXP => (2, 1) + | SIGNEXTEND => (2, 1) + + (* 0x10 *) + | LT => (2, 1) + | GT => (2, 1) + | SLT => (2, 1) + | SGT => (2, 1) + | EQ => (2, 1) + | ISZERO => (1, 1) + | AND => (2, 1) + | OR => (2, 1) + | XOR => (2, 1) + | NOT => (1, 1) + | BYTE => (2, 1) + | SHL => (2, 1) + | SHR => (2, 1) + | SAR => (2, 1) + + (* 0x20 *) + | SHA3 => (2, 1) + + (* 0x30 *) + | ADDRESS => (0, 1) + | BALANCE => (1, 1) + | ORIGIN => (0, 1) + | CALLER => (0, 1) + | CALLVALUE => (0, 1) + | CALLDATALOAD => (1, 1) + | CALLDATASIZE => (0, 1) + | CALLDATACOPY => (3, 0) + | CODESIZE => (0, 1) + | CODECOPY => (3, 0) + | GASPRICE => (0, 1) + | EXTCODESIZE => (1, 1) + | EXTCODECOPY => (4, 0) + | RETURNDATASIZE => (0, 1) + | RETURNDATACOPY => (3, 0) + | EXTCODEHASH => (1, 1) + + (* 0x40 *) + | BLOCKHASH => (1, 1) + | COINBASE => (0, 1) + | TIMESTAMP => (0, 1) + | NUMBER => (0, 1) + | DIFFICULTY => (0, 1) + | GASLIMIT => (0, 1) + | CHAINID => (0, 1) + | SELFBALANCE => (0, 1) + + (* 0x50 *) + | POP => (1, 0) + | MLOAD => (1, 1) + | MSTORE => (2, 0) + | MSTORE8 => (2, 0) + | SLOAD => (1, 1) + | SSTORE => (2, 0) + | JUMP => (1, 0) + | JUMPI => (2, 0) + | PC => (0, 1) + | MSIZE => (0, 1) + | GAS => (0, 1) + | JUMPDEST => (0, 0) + + (* 0x60 *) + | PUSH n ok => (0, 1) + + (* 0x80 *) + | DUP n ok => let k := of_Z (Z.of_N n) in (k, k + 1) + + (* 0x90 *) + | SWAP n ok => let k := of_Z (Z.of_N n) in (k + 1, k + 1) + + (* 0xa0 *) + | LOG n ok => let k := of_Z (Z.of_N n) in (k + 2, 0) + + (* 0xf0 *) + | CREATE => (3, 1) + | CALL => (7, 1) + | CALLCODE => (7, 1) + | RETURN => (2, 0) + | DELEGATECALL => (6, 1) + | CREATE2 => (4, 1) + | STATICCALL => (6, 1) + | REVERT => (2, 0) + | SELFDESTRUCT => (1, 0) + end)%uint63. + +Definition consume_count (op: instruction) := fst (consume_and_produce_count op). +Definition produce_count (op: instruction) := snd (consume_and_produce_count op). \ No newline at end of file diff --git a/coq/CoqOfSolidity/CoqEvm/JumpDest.v b/coq/CoqOfSolidity/CoqEvm/JumpDest.v new file mode 100644 index 000000000000..e726a8f721db --- /dev/null +++ b/coq/CoqOfSolidity/CoqEvm/JumpDest.v @@ -0,0 +1,247 @@ +From Coq Require Import Arith NArith Lia. +Require Import Nibble Instructions List2 Logic2. + +(** This is N(i, w) defined in (141), quite close to the paper. *) +Definition paper_next_valid_instruction_position (i: N) (b: byte) +:= let push1 := N_of_byte (byte_of_instruction (PUSH 1 eq_refl)) in + let push32 := N_of_byte (byte_of_instruction (PUSH 32 eq_refl)) in + let w := N_of_byte b in + (if ((push1 <=? w) && (w <=? push32))%bool + then i + w - push1 + 2 + else i + 1)%N. + +(** This is a nicer equivalent of the previous function. *) +Definition next_valid_instruction_position (i: N) (b: byte) +:= (i + match instruction_of_byte b with + | Some (PUSH n _) => n + 1 + | _ => 1 + end)%N. + +Lemma next_valid_instruction_position_ok (i: N) (b: byte): + next_valid_instruction_position i b = paper_next_valid_instruction_position i b. +Proof. +unfold paper_next_valid_instruction_position. +match goal with +|- _ = if ?cond then (i + ?a - ?b + ?c)%N else (i + 1)%N => + replace (if cond then (i + a - b + c)%N else (i + 1)%N) + with (i + if cond then a - b + c else 1)%N +end. +2:{ + remember (andb _ _) as cond. destruct cond. + repeat (rewrite N.add_sub_assoc || rewrite N.add_assoc). 1-3: trivial. + symmetry in Heqcond. + apply Bool.andb_true_iff in Heqcond. + apply N.leb_le. tauto. +} +unfold next_valid_instruction_position. +f_equal. +(* this is stupid, we need an is_push test *) +destruct b as (b7, b6, b5, b4, b3, b2, b1, b0). +destruct b7; destruct b6; destruct b5; destruct b4; +destruct b3; destruct b2; destruct b1; destruct b0; trivial. +Qed. + +Lemma next_valid_instruction_position_bound (i: N) (b: byte): + (i + 1 <= next_valid_instruction_position i b)%N. +Proof. +unfold next_valid_instruction_position. +destruct (instruction_of_byte b) as [op|]; try destruct op; try apply N.le_refl. +lia. +Qed. + +(** + This is as close to D_J(c, i) defined in (140) as feasible, + however, fuel had to be introduced to satisfy Coq's termination check. + *) +Fixpoint paper_valid_jump_destinations_from (code: list byte) + (i: N) + (fuel: nat) +: list N +:= match fuel with + | O => nil + | S remaining_fuel => + match List.nth_error code (N.to_nat i) with + | None => nil + | Some b => + let tail := paper_valid_jump_destinations_from + code + (next_valid_instruction_position i b) + remaining_fuel + in if (N_of_byte b =? N_of_byte (byte_of_instruction JUMPDEST))%N + then i :: tail + else tail + end + end. + +Local Lemma valid_jump_destinations_from_2_helper + (code: list byte) + (i: N) + (b: byte) + (code_tail: list byte) + (ok: code_tail = List.skipn (N.to_nat i) code): + let next := next_valid_instruction_position i b in + List.skipn (N.to_nat (next - i)) code_tail = List.skipn (N.to_nat next) code. +Proof. +subst. intro. unfold next_valid_instruction_position in next. +rewrite skipn_skipn. +f_equal. subst next. +rewrite N.add_comm. +rewrite<- N.add_sub_assoc by apply N.le_refl. +rewrite N.sub_diag. +rewrite N.add_0_r. +symmetry. apply N2Nat.inj_add. +Qed. + +(* This version carries around the code tail so that it doesn't have to count from the start. *) +Local Fixpoint valid_jump_destinations_from_2 (code: list byte) + (i: N) + (fuel: nat) + (code_tail: list byte) + (ok: code_tail = List.skipn (N.to_nat i) code) +: list N +:= match fuel with + | O => nil + | S remaining_fuel => + match List.hd_error code_tail with + | None => nil + | Some b => + let next := next_valid_instruction_position i b in + let tail := valid_jump_destinations_from_2 + code + next + remaining_fuel + (List.skipn (N.to_nat (next - i)) code_tail) + (valid_jump_destinations_from_2_helper code i b code_tail ok) + in if (N_of_byte b =? N_of_byte (byte_of_instruction JUMPDEST))%N + then (i :: tail)%list + else tail + end + end. + +Local Lemma valid_jump_destinations_from_2_ok (code: list byte) + (i: N) + (fuel: nat) + (code_tail: list byte) + (ok: code_tail = List.skipn (N.to_nat i) code): + paper_valid_jump_destinations_from code i fuel + = + valid_jump_destinations_from_2 code i fuel code_tail ok. +Proof. +revert ok. revert code_tail. revert i code. +induction fuel. { easy. } +intros. cbn. +subst code_tail. rewrite<- List2.nth_hd_skipn. +destruct (List.nth_error code (N.to_nat i)). 2:{ trivial. } +destruct (N_of_byte b =? _)%N; now rewrite<- IHfuel. +Qed. + +(* This version replaces hd_error with a match and also drops [code] and [ok] parameters. *) +Local Fixpoint valid_jump_destinations_from_3 (code_tail: list byte) + (i: N) + (fuel: nat) +: list N +:= match fuel with + | O => nil + | S remaining_fuel => + match code_tail with + | nil => nil + | (b :: _)%list => + let next := next_valid_instruction_position i b in + let tail := valid_jump_destinations_from_3 + (List.skipn (N.to_nat (next - i)) code_tail) + next + remaining_fuel + in if (N_of_byte b =? N_of_byte (byte_of_instruction JUMPDEST))%N + then (i :: tail)%list + else tail + end + end. + +Local Lemma valid_jump_destinations_from_3_ok (code: list byte) + (i: N) + (fuel: nat) + (code_tail: list byte) + (ok: code_tail = List.skipn (N.to_nat i) code): + valid_jump_destinations_from_3 code_tail i fuel + = + valid_jump_destinations_from_2 code i fuel code_tail ok. +Proof. +revert code i code_tail ok. +induction fuel. { easy. } +intros. cbn. +destruct code_tail; cbn. { trivial. } +destruct (N_of_byte b =? _)%N; now rewrite<- IHfuel. +Qed. + +(* This version gets rid of the fuel and does skipping by itself. *) +Local Fixpoint valid_jump_destinations_from_4 (code: list byte) (current: N) (next_valid: N) +: list N +:= match code with + | nil => nil + | (h :: t)%list => + if (current ((a < b)%N <-> (c < d)%N). +Proof. +apply relation_quad; apply N.ltb_lt. +Qed. + +Lemma Z_ltb_lt_quad (a b c d: Z): + ((a ((a < b)%Z <-> (c < d)%Z). +Proof. +apply relation_quad; apply Z.ltb_lt. +Qed. + +Lemma N_leb_le_quad (a b c d: N): + ((a <=? b)%N = (c <=? d)%N) <-> ((a <= b)%N <-> (c <= d)%N). +Proof. +apply relation_quad; apply N.leb_le. +Qed. + +Lemma Z_leb_le_quad (a b c d: Z): + ((a <=? b)%Z = (c <=? d)%Z) <-> ((a <= b)%Z <-> (c <= d)%Z). +Proof. +apply relation_quad; apply Z.leb_le. +Qed. + +Lemma N2Z_ltb (n m: N): + (n (0 < n * m)%Z. +Proof. +split. { intro. apply Z.mul_pos_pos; assumption. } +apply (Z.mul_pos_cancel_r _ _ BM). +Qed. + +Lemma Z_mul_pos_iff_r (n m: Z) (BN: (0 < n)%Z): + (0 < m)%Z <-> (0 < n * m)%Z. +Proof. +split. { apply (Z.mul_pos_pos _ _ BN). } +apply (Z.mul_pos_cancel_l _ _ BN). +Qed. + +Lemma Z_shiftl_pos_iff (n m: Z) (BM: (0 <= m)%Z): + (0 < n)%Z <-> (0 < Z.shiftl n m)%Z. +Proof. +rewrite (Z.shiftl_mul_pow2 _ _ BM). +apply Z_mul_pos_iff_l. +apply Z.pow_pos_nonneg. +{ rewrite<- Z.ltb_lt. trivial. } +assumption. +Qed. + +Lemma Z_odd_land_1 (n: Z) (B: (0 <= n)%Z): + Z.odd n = (0 0%N <-> (0 < n)%N. +Proof. +split; intro H. +{ assert (CN := N.eq_0_gt_0_cases n). tauto. } +destruct n. { now apply N.lt_irrefl in H. } +discriminate. +Qed. + +Lemma N_div_0_r (n: N): + (n / 0 = 0)%N. +Proof. +now destruct n. +Qed. + +Lemma Z_div_0_r (n: Z): + (n / 0 = 0)%Z. +Proof. +now destruct n. +Qed. + +Lemma N_div_le (n: N) (d: N): + (n / d <= n)%N. +Proof. +assert (CN := N.eq_0_gt_0_cases n). +assert (CD := N.eq_0_gt_0_cases d). +case CN; intro. { subst. cbn. apply N.le_refl. } +case CD; intro. { subst. rewrite N_div_0_r. now apply N.lt_le_incl. } +assert (D: N.succ (N.pred d) = d). +{ apply N.succ_pred_pos. assumption. } +remember (N.pred d) as k. clear Heqk. subst. +assert (CK := N.eq_0_gt_0_cases k). +case CK; intro. { subst. cbn. now rewrite N.div_1_r. } +apply N.lt_le_incl. +apply N.div_lt. { assumption. } +now apply N.lt_pred_lt_succ. +Qed. + +Lemma Z_div_nonneg (a b: Z) + (A: (0 <= a)%Z) + (B: (0 <= b)%Z): + (0 <= a / b)%Z. +Proof. +destruct b. { rewrite Zdiv_0_r. apply Z.le_refl. } +{ apply Z.div_pos; easy. } +easy. +Qed. + +Lemma Z_abs_div_le (a b: Z): + (Z.abs a / Z.abs b <= Z.abs a)%Z. +Proof. +assert(A := Z.abs_nonneg a). +assert(B := Z.abs_nonneg b). +apply Z2N.inj_le. { now apply Z_div_nonneg. } +{ assumption. } +rewrite Z2N.inj_div; try assumption. +apply N_div_le. +Qed. + +Lemma Z_abs_sgn (a b: Z): + Z.abs (Z.sgn a * b)%Z = match a with + | 0%Z => 0%Z + | _ => Z.abs b + end. +Proof. +now destruct a, b. +Qed. + +Lemma Z_sgn_abs (a: Z): + (Z.sgn a * Z.abs a)%Z = a. +Proof. +now destruct a. +Qed. + +Lemma Z_add_nocarry_lor (a b: Z) (H: Z.land a b = 0%Z): + (a + b = Z.lor a b)%Z. +Proof. +rewrite Z.add_nocarry_lxor by assumption. +apply Z.lxor_lor. assumption. +Qed. + +Lemma Z_land_pow2_small (a b: Z) (A: (0 <= a < 2 ^ b)%Z) (B: (0 <= b)%Z): + Z.land a (2 ^ b) = 0%Z. +Proof. +rewrite Arith2.Z_land_pow2_shift by tauto. +replace (Z.shiftr a b) with 0%Z. { cbn. apply Z.shiftl_0_l. } +rewrite Z.shiftr_div_pow2 by tauto. +symmetry. apply Z.div_small. exact A. +Qed. + +Lemma Z_testbit_flag_mul_pow2 (f: bool) (k: Z) (K: (0 <= k)%Z): + Z.testbit ((if f then 1 else 0) * 2 ^ k) k = f. +Proof. +destruct f. +{ rewrite Z.mul_1_l. apply Z.pow2_bits_true. assumption. } +rewrite Z.mul_0_l. apply Z.bits_0. +Qed. + +(* A version of Z.bits_above_log2 with a different bound. *) +Lemma Z_testbit_small (a n: Z) (A: (0 <= a)%Z) + (B: (a < 2 ^ n)%Z): + Z.testbit a n = false. +Proof. +destruct a. { apply Z.testbit_0_l. } +{ apply Z.bits_above_log2. trivial. now apply Z.log2_lt_pow2. } +exfalso. rewrite<- Z.leb_le in A. cbn in A. discriminate. +Qed. + +(**************************************************************************) + +Lemma Z_pos_ne_0 (a: positive): + Z.pos a <> 0%Z. +Proof. +discriminate. +Qed. + +Lemma Z_0_lt_pos (a: positive): + (0 < Z.pos a)%Z. +Proof. +rewrite<- Z.ltb_lt. +trivial. +Qed. + +Lemma Z_ceiling_via_floor (a b: Z) (B: (0 <= b)%Z): + (- ((- a) / b) = (a + b - 1) / b)%Z. +Proof. +destruct b as [|b|b]. { now repeat rewrite Z_div_0_r. } +{ + assert (D := Z.div_mod (-a) (Z.pos b) (Z_pos_ne_0 b)). + assert (E := Z.div_mod (a + Z.pos b - 1) (Z.pos b) (Z_pos_ne_0 b)). + assert (P := Z.mod_pos_bound (-a) (Z.pos b) (Z_0_lt_pos b)). + assert (Q := Z.mod_pos_bound (a + Z.pos b - 1) (Z.pos b) (Z_0_lt_pos b)). + nia. +} +rewrite<- Z.leb_le in B. discriminate. +Qed. + +(**************************************************************************) + +Lemma Z_land_lxor_distr_l (a b c: Z): + Z.land (Z.lxor a b) c = Z.lxor (Z.land a c) (Z.land b c). +Proof. +apply Z.bits_inj. intro. +repeat (rewrite Z.land_spec || rewrite Z.lxor_spec). +destruct (Z.testbit a n); destruct (Z.testbit b n); destruct (Z.testbit c n); easy. +Qed. + +Lemma Z_land_lxor_distr_r (a b c: Z): + Z.land a (Z.lxor b c) = Z.lxor (Z.land a b) (Z.land a c). +Proof. +apply Z.bits_inj. intro. +repeat (rewrite Z.land_spec || rewrite Z.lxor_spec). +destruct (Z.testbit a n); destruct (Z.testbit b n); destruct (Z.testbit c n); easy. +Qed. + +(**************************************************************************) + +(* This is a version of Z.log2_lt_pow2 but a can be 0 and b cannot. *) +Lemma Z_log2_lt_pow2 (a b: Z) (BA: (0 <= a)%Z) (BB: (0 < b)%Z): + (a < 2 ^ b <-> Z.log2 a < b)%Z. +Proof. +destruct a. +{ + cbn. assert (P: (0 < 2 ^ b)%Z). apply Z_0_lt_pow2. { apply Z.lt_le_incl. assumption. } + tauto. +} +{ apply Z.log2_lt_pow2. rewrite<- Z.ltb_lt. trivial. } +rewrite<- Z.leb_le in BA. discriminate. +Qed. + +(**************************************************************************) + +Lemma Z_mod_add_l (a b c m: Z) + (H: (b mod m = c mod m)%Z): + ((a + b) mod m = (a + c) mod m)%Z. +Proof. +rewrite<- (Zplus_mod_idemp_r b a). +rewrite<- (Zplus_mod_idemp_r c a). +rewrite H. +trivial. +Qed. + +Lemma Z_mod_add_r (a b c m: Z) + (H: (a mod m = b mod m)%Z): + ((a + c) mod m = (b + c) mod m)%Z. +Proof. +rewrite<- (Zplus_mod_idemp_l a c). +rewrite<- (Zplus_mod_idemp_l b c). +rewrite H. +trivial. +Qed. + +(**************************************************************************) + +Lemma Nat2N_inj_div (a b: nat): + N.of_nat (a / b) = (N.of_nat a / N.of_nat b)%N. +Proof. +destruct b. { cbn. now rewrite N_div_0_r. } +assert (BNZ: S b <> 0) by discriminate. +assert (D := Nat.div_mod a (S b) BNZ). +remember (a / S b) as q. +remember (a mod S b) as r. +apply N.div_unique with (r := N.of_nat r). +{ + unfold N.lt. + rewrite<- Nat2N.inj_compare. + apply Nat.compare_lt_iff. + subst. apply (Nat.mod_upper_bound _ _ BNZ). +} +rewrite<- Nat2N.inj_mul. +rewrite<- Nat2N.inj_add. +now rewrite D. +Qed. + +Lemma Nat2N_inj_mod (a b: nat) (ok: b <> 0): + N.of_nat (a mod b) = (N.of_nat a mod N.of_nat b)%N. +Proof. +destruct b. { contradiction. } +rewrite Nat.Div0.mod_eq by discriminate. +rewrite Nat2N.inj_sub. +rewrite Nat2N.inj_mul. +rewrite Nat2N_inj_div. +symmetry. apply N.Div0.mod_eq. +Qed. + +(**************************************************************************) +(** This is a strenghtening of Pos.size_nat_monotone from [p < q] to [p <= q]. *) +Lemma Pos_size_nat_monotone (p q: positive) (LE: (p <= q)%positive): + (Pos.size_nat p <= Pos.size_nat q)%nat. +Proof. +remember (Pos.compare p q) as cmp. symmetry in Heqcmp. destruct cmp. +{ apply Pos.compare_eq in Heqcmp. subst. apply Nat.le_refl. } +{ apply Pos.size_nat_monotone. exact Heqcmp. } +contradiction. +Qed. \ No newline at end of file diff --git a/coq/CoqOfSolidity/CoqEvm/Lib2/List2.v b/coq/CoqOfSolidity/CoqEvm/Lib2/List2.v new file mode 100644 index 000000000000..b47d7b29ba4f --- /dev/null +++ b/coq/CoqOfSolidity/CoqEvm/Lib2/List2.v @@ -0,0 +1,37 @@ +From Coq Require Import List Arith. + +Local Open Scope list_scope. + +Lemma skipn_skipn {A} (l: list A) (n m: nat): + skipn n (skipn m l) = skipn (n + m) l. +Proof. +revert n l. +induction m, l; intros; try repeat rewrite skipn_nil; try easy. +{ cbn. now rewrite Nat.add_0_r. } +replace (n + S m) with (S (n + m)) by auto with arith. +repeat rewrite skipn_cons. +apply IHm. +Qed. + +Lemma nth_hd_skipn {A} (l: list A) (n: nat): + nth_error l n = hd_error (skipn n l). +Proof. +revert l. induction n, l; try easy. +cbn. apply IHn. +Qed. + +Fixpoint list_eqb {A} (eqb: A -> A -> bool) (l l': list A) +: bool +:= match l with + | nil => match l' with + | nil => true + | _ => false + end + | h :: t => match l' with + | nil => false + | h' :: t' => if eqb h h' + then list_eqb eqb t t' + else false + end + end. + diff --git a/coq/CoqOfSolidity/CoqEvm/Lib2/ListSet2.v b/coq/CoqOfSolidity/CoqEvm/Lib2/ListSet2.v new file mode 100644 index 000000000000..4e9cefe8b58c --- /dev/null +++ b/coq/CoqOfSolidity/CoqEvm/Lib2/ListSet2.v @@ -0,0 +1,332 @@ +(** + This file continues theories/Lists/ListSet.v from the standard library of Coq. + *) + +From Coq Require Import List ListSet. + +(** in_dec is a sumbool version of set_mem. *) +Lemma set_mem_in_dec {M: Type} (E: forall x y: M, {x = y} + {x <> y}) + (x: M) (l: list M): + set_mem E x l = if in_dec E x l then true else false. +Proof. +induction l. { trivial. } +simpl. destruct (E x a) as [EQ | NE]. +{ subst. now destruct (E a a). } +remember (match E a x with left _ => _ | right _ => _ end) as m. +destruct (E a x) as [EQ | NE2]. +{ clear Heqm. symmetry in EQ. contradiction. } +destruct in_dec; now subst. +Qed. + +Lemma set_mem_true {M: Type} (E: forall x y: M, {x = y} + {x <> y}) + (x: M) (l: list M): + set_mem E x l = true <-> In x l. +Proof. +rewrite set_mem_in_dec. +now destruct in_dec. +Qed. + +Lemma set_mem_false {M: Type} (E: forall x y: M, {x = y} + {x <> y}) + (x: M) (l: list M): + set_mem E x l = false <-> ~In x l. +Proof. +rewrite set_mem_in_dec. +now destruct in_dec. +Qed. + +(** nodup doesn't change set_mem. + This is a set_mem version of [nodup_In l x: In x (nodup l) <-> In x l]. + *) +Lemma set_mem_nodup {M: Type} (E: forall x y: M, {x = y} + {x <> y}) + (x: M) (l: list M): + set_mem E x (nodup E l) = set_mem E x l. +Proof. +repeat rewrite set_mem_in_dec. +destruct in_dec as [IN | IN]; + rewrite nodup_In in IN; + destruct in_dec; + trivial; + contradiction. +Qed. + +Definition nodup_list_in {M: Type} (E: forall x y: M, {x = y} + {x <> y}) + (x: M) (a: {l : list M | NoDup l}) +: bool +:= set_mem E x (proj1_sig a). + +Definition list_is_empty {M: Type} (l: list M) +: bool +:= match l with + | nil => true + | _ => false + end. + +Lemma list_is_empty_ok {M: Type} (l: list M): + list_is_empty l = true <-> l = nil. +Proof. +destruct l; cbn. { tauto. } +split; congruence. +Qed. + +Lemma list_add_ok {M: Type} (E: forall x y: M, {x = y} + {x <> y}) + (x: M) (l: list M) (y: M): + set_mem E y (set_add E x l) = if E x y then true else set_mem E y l. +Proof. +destruct (E x y) as [EQ|NE]. +{ + apply set_mem_correct2. + apply set_add_intro2. + symmetry. assumption. +} +remember (set_mem E y l) as m. +destruct m; symmetry in Heqm. +{ + apply set_mem_correct1 in Heqm. + apply set_mem_correct2. + apply set_add_intro1. assumption. +} +apply set_mem_complete1 in Heqm. +apply set_mem_complete2. +intro H. apply set_add_elim2 in H. { contradiction. } +intro EQ. symmetry in EQ. contradiction. +Qed. + +Definition nodup_list_add {M: Type} (E: forall x y: M, {x = y} + {x <> y}) + (x: M) (a: {l : list M | NoDup l}) +: {l : list M | NoDup l} +:= exist _ (set_add E x (proj1_sig a)) + (set_add_nodup E x (proj2_sig a)). + +Lemma nodup_list_add_ok {M: Type} (E: forall x y: M, {x = y} + {x <> y}) + (x: M) (a: {l : list M | NoDup l}) (y: M): + nodup_list_in E y (nodup_list_add E x a) = if E x y then true else nodup_list_in E y a. +Proof. +apply list_add_ok. +Qed. + +Lemma list_remove_ok {M: Type} (E: forall x y: M, {x = y} + {x <> y}) + (x: M) (l: list M) (N: NoDup l) (y: M): + set_mem E y (set_remove E x l) = if E x y then false else set_mem E y l. +Proof. +destruct (E x y) as [EQ|NE]. +{ + apply set_mem_complete2. intro H. + apply (set_remove_2 E N H). + symmetry. assumption. +} +remember (set_mem E y l) as m. +destruct m; symmetry in Heqm. +{ + apply set_mem_correct1 in Heqm. + apply set_mem_correct2. + apply set_remove_3. assumption. + intro H. symmetry in H. contradiction. +} +apply set_mem_complete1 in Heqm. +apply set_mem_complete2. +intro H. apply set_remove_1 in H. contradiction. +Qed. + +Definition nodup_list_remove {M: Type} (E: forall x y: M, {x = y} + {x <> y}) + (x: M) (a: {l : list M | NoDup l}) +: {l : list M | NoDup l} +:= exist _ (set_remove E x (proj1_sig a)) + (set_remove_nodup E x (proj2_sig a)). + +Lemma nodup_list_remove_ok {M: Type} (E: forall x y: M, {x = y} + {x <> y}) + (x: M) (a: {l : list M | NoDup l}) (y: M): + nodup_list_in E y (nodup_list_remove E x a) = if E x y then false else nodup_list_in E y a. +Proof. +apply list_remove_ok. apply (proj2_sig a). +Qed. + +(****************************************************************************) + +Ltac bool := repeat + ( rewrite Bool.andb_true_iff in * + || rewrite Bool.andb_false_iff in * + || rewrite Bool.orb_true_iff in * + || rewrite Bool.orb_false_iff in * + || rewrite Bool.negb_true_iff in * + || rewrite Bool.negb_false_iff in * + || rewrite set_mem_true in * + || rewrite set_mem_false in *). + +Lemma list_union_ok {M: Type} (E: forall x y: M, {x = y} + {x <> y}) + (a b: list M) (x: M): + set_mem E x (set_union E a b) + = + orb (set_mem E x a) (set_mem E x b). +Proof. +remember (set_mem E x (set_union E a b)) as in_a_or_b. +symmetry. symmetry in Heqin_a_or_b. +destruct in_a_or_b; bool; rewrite set_union_iff in Heqin_a_or_b; tauto. +Qed. + +Lemma list_inter_ok {M: Type} (E: forall x y: M, {x = y} + {x <> y}) + (a b: list M) (x: M): + set_mem E x (set_inter E a b) + = + andb (set_mem E x a) (set_mem E x b). +Proof. +remember (set_mem E x (set_inter E a b)) as in_a_and_b. +symmetry. symmetry in Heqin_a_and_b. +destruct in_a_and_b; + bool; rewrite set_inter_iff in Heqin_a_and_b. +{ assumption. } +destruct (in_dec E x a); destruct (in_dec E x b); tauto. +Qed. + +Lemma list_diff_ok {M: Type} (E: forall x y: M, {x = y} + {x <> y}) + (a b: list M) (x: M): + set_mem E x (set_diff E a b) + = + andb (set_mem E x a) (negb (set_mem E x b)). +Proof. +remember (set_mem E x (set_diff E a b)) as in_a_and_not_b. +symmetry. symmetry in Heqin_a_and_not_b. +destruct in_a_and_not_b; bool; + rewrite set_diff_iff in Heqin_a_and_not_b. +{ assumption. } +destruct (in_dec E x a); destruct (in_dec E x b); tauto. +Qed. + +Definition nodup_list_union {M: Type} (E: forall x y: M, {x = y} + {x <> y}) + (a b: {l : list M | NoDup l}) +: {l : list M | NoDup l} +:= exist _ (set_union E (proj1_sig a) (proj1_sig b)) + (set_union_nodup E (proj2_sig a) (proj2_sig b)). + +Definition nodup_list_inter {M: Type} (E: forall x y: M, {x = y} + {x <> y}) + (a b: {l : list M | NoDup l}) +: {l : list M | NoDup l} +:= exist _ (set_inter E (proj1_sig a) (proj1_sig b)) + (set_inter_nodup E (proj2_sig a) (proj2_sig b)). + +Definition nodup_list_diff {M: Type} (E: forall x y: M, {x = y} + {x <> y}) + (a b: {l : list M | NoDup l}) +: {l : list M | NoDup l} +:= exist _ (set_diff E (proj1_sig a) (proj1_sig b)) + (set_diff_nodup E (proj2_sig a) (proj2_sig b)). + +Lemma nodup_list_union_ok {M: Type} (E: forall x y: M, {x = y} + {x <> y}) + (a b: {l : list M | NoDup l}) (x: M): + nodup_list_in E x (nodup_list_union E a b) + = + orb (nodup_list_in E x a) (nodup_list_in E x b). +Proof. +apply list_union_ok. +Qed. + +Lemma nodup_list_inter_ok {M: Type} (E: forall x y: M, {x = y} + {x <> y}) + (a b: {l : list M | NoDup l}) (x: M): + nodup_list_in E x (nodup_list_inter E a b) + = + andb (nodup_list_in E x a) (nodup_list_in E x b). +Proof. +apply list_inter_ok. +Qed. + +Lemma nodup_list_diff_ok {M: Type} (E: forall x y: M, {x = y} + {x <> y}) + (a b: {l : list M | NoDup l}) (x: M): + nodup_list_in E x (nodup_list_diff E a b) + = + andb (nodup_list_in E x a) (negb (nodup_list_in E x b)). +Proof. +apply list_diff_ok. +Qed. + +Definition nodup_list_forall {M: Type} + (a: {l : list M | NoDup l}) + (p: M -> bool) +: bool +:= forallb p (proj1_sig a). + +Lemma nodup_list_forall_ok {M: Type} (E: forall x y: M, {x = y} + {x <> y}) + (a: {l : list M | NoDup l}) (p: M -> bool): + nodup_list_forall a p = true + <-> + forall x: M, + nodup_list_in E x a = true -> p x = true. +Proof. +unfold nodup_list_forall. unfold nodup_list_in. +destruct a as (l, N). cbn. clear N. +rewrite forallb_forall. +split; intros H x Z. +{ rewrite set_mem_true in Z. exact (H x Z). } +rewrite<- set_mem_true in Z. exact (H x Z). +Qed. + +Definition list_subset {M: Type} (E: forall x y: M, {x = y} + {x <> y}) + (a b: list M) +: bool +:= forallb (fun x => set_mem E x b) a. + +Definition nodup_list_subset {M: Type} (E: forall x y: M, {x = y} + {x <> y}) + (a b: {l : list M | NoDup l}) +: bool +:= list_subset E (proj1_sig a) (proj1_sig b). + +Lemma list_subset_ok {M: Type} (E: forall x y: M, {x = y} + {x <> y}) + (a b: list M): + list_subset E a b = true + <-> + forall x: M, + orb (negb (set_mem E x a)) (set_mem E x b) = true. +Proof. +unfold list_subset. +rewrite forallb_forall. +split; intros H x; assert (Hx := H x); bool; + destruct (in_dec E x a); destruct (in_dec E x b); tauto. +Qed. + +Lemma nodup_list_subset_ok {M: Type} (E: forall x y: M, {x = y} + {x <> y}) + (a b: {l : list M | NoDup l}): + nodup_list_subset E a b = true + <-> + forall x: M, + orb (negb (nodup_list_in E x a)) (nodup_list_in E x b) = true. +Proof. +apply list_subset_ok. +Qed. + +Definition list_set_eq {M: Type} (E: forall x y: M, {x = y} + {x <> y}) + (a b: list M) +: bool +:= andb (list_subset E a b) (list_subset E b a). + +Lemma list_set_eq_ok {M: Type} (E: forall x y: M, {x = y} + {x <> y}) + (a b: list M): + list_set_eq E a b = true + <-> + forall x: M, + set_mem E x a = set_mem E x b. +Proof. +unfold list_set_eq. bool. repeat rewrite list_subset_ok. +split. +{ + intros H x. + destruct H as (Ha, Hb). + assert (Hax := Ha x). clear Ha. + assert (Hbx := Hb x). clear Hb. + now destruct (set_mem E x a); destruct (set_mem E x b). +} +intros H. split; intro x; assert (Hx := H x); bool; repeat rewrite<- (set_mem_true E). + destruct (set_mem E x a); destruct (set_mem E x b); firstorder. +rewrite Hx. destruct (set_mem E x b); firstorder. +Qed. + +Definition nodup_list_set_eq {M: Type} (E: forall x y: M, {x = y} + {x <> y}) + (a b: {l : list M | NoDup l}) +: bool +:= list_set_eq E (proj1_sig a) (proj1_sig b). + +Lemma nodup_list_set_eq_ok {M: Type} (E: forall x y: M, {x = y} + {x <> y}) + (a b: {l : list M | NoDup l}): + nodup_list_set_eq E a b = true + <-> + forall x: M, + nodup_list_in E x a = nodup_list_in E x b. +Proof. +apply list_set_eq_ok. +Qed. \ No newline at end of file diff --git a/coq/CoqOfSolidity/CoqEvm/Lib2/Logic2.v b/coq/CoqOfSolidity/CoqEvm/Lib2/Logic2.v new file mode 100644 index 000000000000..797fabbc1f62 --- /dev/null +++ b/coq/CoqOfSolidity/CoqEvm/Lib2/Logic2.v @@ -0,0 +1,37 @@ +From Coq Require Setoid. + +Lemma b_false {b: bool} {P: Prop} (R: b = true <-> P): + b = false <-> ~P. +Proof. +split; intro H; destruct b; try intro T; try easy. +{ apply R in T. discriminate. } +exfalso. apply H. apply R. trivial. +Qed. + +Lemma relation_quad {TA TB TC TD: Type} + {R1: TA -> TB -> Prop} + {R2: TC -> TD -> Prop} + {r1: TA -> TB -> bool} + {r2: TC -> TD -> bool} + (H1: forall x y, r1 x y = true <-> R1 x y) + (H2: forall x y, r2 x y = true <-> R2 x y) + (a: TA) (b: TB) (c: TC) (d: TD): + (r1 a b = r2 c d) <-> (R1 a b <-> R2 c d). +Proof. +split; intro K; repeat rewrite<- H; + remember (r1 a b) as rab; symmetry in Heqrab; + remember (r2 c d) as rcd; symmetry in Heqrcd; + destruct rab; destruct rcd; + try rewrite H1 in Heqrab; try rewrite H2 in Heqrcd; try easy. + { + split; intro Q. + { rewrite<- H1 in Q. rewrite Heqrab in Q. discriminate. } + { rewrite<- H2 in Q. rewrite Heqrcd in Q. discriminate. } + } + { + rewrite K in Heqrab. rewrite<- H2 in Heqrab. + rewrite<- Heqrab. rewrite<- Heqrcd. reflexivity. + } + rewrite<- K in Heqrcd. rewrite<- H1 in Heqrcd. + rewrite<- Heqrab. rewrite<- Heqrcd. reflexivity. +Qed. diff --git a/coq/CoqOfSolidity/CoqEvm/Lib2/QArith2.v b/coq/CoqOfSolidity/CoqEvm/Lib2/QArith2.v new file mode 100644 index 000000000000..3cd636eb4b10 --- /dev/null +++ b/coq/CoqOfSolidity/CoqEvm/Lib2/QArith2.v @@ -0,0 +1,33 @@ +From Coq Require Import QArith Qround. + +Require Arith2. + +Lemma Q_floor_via_Z (a: Z) (b: positive): + Qfloor (a # b) = (a / Zpos b)%Z. +Proof. +rewrite Zdiv_Qdiv. +rewrite Qmake_Qdiv. +trivial. +Qed. + +Lemma Q_ceiling_via_Z (a: Z) (b: positive): + Qceiling (a # b) = (- ((- a) / Zpos b))%Z. +Proof. +unfold Qround.Qceiling. +rewrite Qmake_Qdiv. +rewrite Zdiv_Qdiv. +rewrite inject_Z_opp. +f_equal. f_equal. +unfold Qdiv. unfold Qmult. cbn. +repeat rewrite Z.mul_1_r. +trivial. +Qed. + +Lemma Q_ceiling_via_Z_floor (a: Z) (b: positive): + Qceiling (a # b) = ((a + Z.pos b - 1) / Zpos b)%Z. +Proof. +rewrite Q_ceiling_via_Z. +apply Arith2.Z_ceiling_via_floor. +rewrite<- Z.leb_le. +trivial. +Qed. \ No newline at end of file diff --git a/coq/CoqOfSolidity/CoqEvm/Lib2/Vector2.v b/coq/CoqOfSolidity/CoqEvm/Lib2/Vector2.v new file mode 100644 index 000000000000..effabd251e15 --- /dev/null +++ b/coq/CoqOfSolidity/CoqEvm/Lib2/Vector2.v @@ -0,0 +1,39 @@ +From Coq Require Vector. +From Coq Require List. + +Fixpoint append_one {A: Type} {n: nat} (v: Vector.t A n) (new: A) +: Vector.t A (S n) +:= match v with + | Vector.nil _ => Vector.cons _ new _ (Vector.nil _) + | Vector.cons _ h _ t => Vector.cons _ h _ (append_one t new) + end. + +Fixpoint rev {A: Type} {n: nat} (v: Vector.t A n) +: Vector.t A n +:= match v with + | Vector.nil _ => Vector.nil _ + | Vector.cons _ h _ t => append_one (rev t) h + end. + +(* Try doing that with Vector.rev! *) +Example rev_example: + rev + (Vector.cons nat 30 2 (Vector.cons nat 20 1 (Vector.cons nat 10 0 (Vector.nil nat)))) + = (Vector.cons nat 10 2 (Vector.cons nat 20 1 (Vector.cons nat 30 0 (Vector.nil nat)))). +Proof. trivial. Qed. + +Local Lemma vector_0_nil' {T: Type} {z} (v: Vector.t T z) (Zero: z = 0): + v = match (eq_sym Zero) in _ = y return Vector.t T y with + | eq_refl => Vector.nil _ + end. +Proof. +revert Zero v. destruct z, v; intros; try discriminate; + assert (X: Zero = eq_refl) by (apply Eqdep_dec.eq_proofs_unicity; decide equality); + now rewrite X. +Qed. + +Lemma vector_0_nil {T: Type} (v: Vector.t T 0): + v = Vector.nil _. +Proof. +apply vector_0_nil' with (Zero := eq_refl). +Qed. \ No newline at end of file diff --git a/coq/CoqOfSolidity/CoqEvm/README.md b/coq/CoqOfSolidity/CoqEvm/README.md new file mode 100644 index 000000000000..3301f80e2e65 --- /dev/null +++ b/coq/CoqOfSolidity/CoqEvm/README.md @@ -0,0 +1,25 @@ +# coq-evm + +This might or might not become a full Ethereum Virtual Machine in Coq someday. + +Right now you can have the hash functions: + + - Keccak-256 + - SHA256 + - RIPEMD160 + - BLAKE2b (F function only) + +All those functions use native Coq integers for speed. All of them are tested against their Go implementations. + +## Checking + + ./configure # just does coq_makefile + make + +## Testing + +This needs Go. + + cd test + ./configure # gives a warning but it's OK + make \ No newline at end of file diff --git a/coq/CoqOfSolidity/blacklist.txt b/coq/CoqOfSolidity/blacklist.txt index e9646723dbf1..8683c395fa28 100644 --- a/coq/CoqOfSolidity/blacklist.txt +++ b/coq/CoqOfSolidity/blacklist.txt @@ -1,4 +1,5 @@ contracts/erc20/proofs/contract.v contracts/erc20/shallow.v contracts/morpho/morpho_functional.v -contracts/scl/mulmuladdX_fullgen_b4/high_level.v \ No newline at end of file +contracts/scl/mulmuladdX_fullgen_b4/high_level.v +CoqEvm/Arith/SInt.v \ No newline at end of file diff --git a/coq/CoqOfSolidity/simulations/CoqOfSolidity.v b/coq/CoqOfSolidity/simulations/CoqOfSolidity.v index abba995c8f2b..4e5d683a7c1c 100644 --- a/coq/CoqOfSolidity/simulations/CoqOfSolidity.v +++ b/coq/CoqOfSolidity/simulations/CoqOfSolidity.v @@ -1,5 +1,5 @@ Require Import CoqOfSolidity.CoqOfSolidity. -Require EVM.Crypto.Keccak. +Require CoqOfSolidity.CoqEvm.Crypto.Keccak. (** We should probably use an existing library for the [Dict.t] definition. We have mainly two kinds of keys in our code: @@ -373,7 +373,7 @@ End State. (** Compute a selector from the signature of an entrypoint *) Definition get_selector (entrypoint_name : string) : U256.t := - let hash : list Nibble.byte := EVM.Crypto.Keccak.keccak_256_of_string entrypoint_name in + let hash : list Nibble.byte := CoqEvm.Crypto.Keccak.keccak_256_of_string entrypoint_name in let hash : list Z := (List.map (fun byte => Z.of_N (Nibble.N_of_byte byte))) hash in Memory.bytes_as_u256 (List.firstn 4 hash). @@ -389,7 +389,7 @@ Module StdlibAux. Definition keccak256 (bytes : list U256.t) : U256.t := let bytes := Memory.bytes_as_bytes bytes in - let hash : list Nibble.byte := EVM.Crypto.Keccak.keccak_256 bytes in + let hash : list Nibble.byte := CoqEvm.Crypto.Keccak.keccak_256 bytes in let hash : list Z := List.map (fun byte => Z.of_N (Nibble.N_of_byte byte)) hash in Memory.bytes_as_u256 hash. @@ -791,7 +791,7 @@ Module Stdlib. let bytes : list Z := Memory.u256_as_bytes address ++ Memory.u256_as_bytes nonce in let bytes : list Nibble.byte := Memory.bytes_as_bytes bytes in - let hash : list Nibble.byte := EVM.Crypto.Keccak.keccak_256 bytes in + let hash : list Nibble.byte := CoqEvm.Crypto.Keccak.keccak_256 bytes in let hash : list Z := (List.map (fun byte => Z.of_N (Nibble.N_of_byte byte))) hash in M.pure (Z.land ((2 ^ 160) - 1) (Memory.bytes_as_u256 hash)) in if n