Skip to main content

🍬 Michelson_v1_gas.v

Proofs

See code, Gitlab , OCaml

Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.

Require Import TezosOfOCaml.Proto_alpha.Environment.
Require TezosOfOCaml.Proto_alpha.Michelson_v1_gas.
Require TezosOfOCaml.Proto_alpha.Saturation_repr.

Require Import TezosOfOCaml.Proto_alpha.Proofs.Saturation_repr.

Module S := Saturation_repr.

Module Cost_of.
  Module Interpreter.
    Import Proto_alpha.Michelson_v1_gas.Cost_of.Interpreter.

    Lemma drop_is_not_zero : drop 0.
    Proof. cbn; lia. Qed.

    Lemma dup_is_not_zero : dup 0.
    Proof. cbn; lia. Qed.

    Lemma swap_is_not_zero : swap 0.
    Proof. cbn; lia. Qed.

    Lemma cons_some_is_not_zero : cons_some 0.
    Proof. cbn; lia. Qed.

    Lemma cons_none_is_not_zero : cons_none 0.
    Proof. cbn; lia. Qed.

    Lemma if_none_is_not_zero : if_none 0.
    Proof. cbn; lia. Qed.

    Lemma opt_map_is_not_zero : opt_map 0.
    Proof. cbn; lia. Qed.

    Lemma cons_pair_is_not_zero : cons_pair 0.
    Proof. cbn; lia. Qed.

    Lemma unpair_is_not_zero : unpair 0.
    Proof. cbn; lia. Qed.

    Lemma car_is_not_zero : car 0.
    Proof. cbn; lia. Qed.

    Lemma cdr_is_not_zero : cdr 0.
    Proof. cbn; lia. Qed.

    Lemma cons_left_is_not_zero : cons_left 0.
    Proof. cbn; lia. Qed.

    Lemma cons_right_is_not_zero : cons_right 0.
    Proof. cbn; lia. Qed.

    Lemma if_left_is_not_zero : if_left 0.
    Proof. cbn; lia. Qed.

    Lemma cons_list_is_not_zero : cons_list 0.
    Proof. cbn; lia. Qed.

    Lemma nil_is_not_zero : nil 0.
    Proof. cbn; lia. Qed.

    Lemma if_cons_is_not_zero : if_cons 0.
    Proof. cbn; lia. Qed.

    Lemma list_map_is_not_zero :
       {a : Set} (l : Script_typed_ir.boxed_list a), list_map l 0.
    Proof. cbn; lia. Qed.

    Lemma list_size_is_not_zero : list_size 0.
    Proof. cbn; lia. Qed.

    Lemma list_iter_is_not_zero :
       {a : Set} (l : Script_typed_ir.boxed_list a), list_iter l 0.
    Proof. cbn; lia. Qed.

    Lemma empty_set_is_not_zero : empty_set 0.
    Proof. cbn; lia. Qed.

    (* @TODO WIP *)
    Lemma add_saturated_l_eq x :
      Saturation_repr.add x Michelson_v1_gas.S.saturated = Michelson_v1_gas.S.saturated.
    Admitted.

    (* @TODO WIP *)
    Lemma add_saturated_r_eq x :
      Strictly_valid.t x
      Saturation_repr.add Michelson_v1_gas.S.saturated x = Michelson_v1_gas.S.saturated.
    Proof.
      intros.
      unfold Saturation_repr.add. simpl.
      assert(Michelson_v1_gas.S.saturated +i x < 0).
      {
        unfold "+i", normalize_int.
        assert((Michelson_v1_gas.S.saturated + x + two_pow_62) mod two_pow_63 < two_pow_62).
        unfold Michelson_v1_gas.S.saturated, two_pow_62, two_pow_63, Pervasives.max_int.
        rewrite <- Z.add_assoc, Z.add_comm, <- Z.add_assoc, Z.add_comm.
        replace (4611686018427387904 + 4611686018427387903)%Z
          with 9223372036854775807 by reflexivity.
        rewrite Zmod_eq_full;[|lia].
        remember
          ((9223372036854775807 + x) / 9223372036854775808 ×
           9223372036854775808)%Z as y.
        (* @TODO *)
        (* Print Strictly_valid.t. *)
        (* Print Saturation_repr.saturated. *)
        (* Print Pervasives.max_int. *)
        (* 4611686018427387903 *)
        (* assert(0 < y < ((9223372036854775807 + 4611686018427387903) / 
                  9223372036854775808 * 9223372036854775808)%Z). *)

        admit.
        lia.
      }
      unfold ">=i"; simpl.
      destruct ( _ >=? _ ) eqn:E;[lia|trivial].
    Admitted.

    Lemma lt_0_add x y :
      Valid.t x
      Valid.t y
      x > 0 y > 0
      0 < Saturation_repr.add x y.
    Proof.
      intros; unfold Saturation_repr.add, "+i"; simpl.
      destruct (_ i _) eqn:?E; [|lia].
      destruct (normalize_int (x + y) >? 0) eqn:?E; lia.
    Qed.

    #[global] Hint Unfold
        set_iter Alpha_context.Gas.atomic_step_cost
        Alpha_context.Gas.S.may_saturate_value
        Michelson_v1_gas.Cost_of.Generated_costs.cost_N_ISet_iter
        Michelson_v1_gas.Cost_of.S_syntax.op_plus
        map_map
        map_iter
        Michelson_v1_gas.Cost_of.Generated_costs.cost_N_IMap_map
        Michelson_v1_gas.Cost_of.Generated_costs.cost_N_IMap_iter
        : local_unfold1.

    #[global] Hint Unfold
         Michelson_v1_gas.Cost_of.S_syntax.op_plus : local_unfold2.

    Ltac solve_simpl :=
      repeat
        match goal with
        | |- context [Saturation_repr.add _ Michelson_v1_gas.S.saturated] ⇒
          rewrite add_saturated_l_eq
        | |- context [Saturation_repr.add Michelson_v1_gas.S.saturated _] ⇒
          rewrite add_saturated_r_eq
        | |- context [Saturation_repr.add _ _] ⇒
          rewrite add_eq
        | |- context [saturate _] ⇒
          rewrite saturate_eq
        | |- context [normalize_int _ ] ⇒
          rewrite Pervasives.normalize_identity
        end; try lia.

    (* @TODO WIP *)
    Lemma set_iter_is_not_zero:
       {a : Set} (s : Script_typed_ir.set a),
        (* let 'Script_typed_ir.Set_tag s1 := s in *)
        (* let '(existS _ _ s2) := s1 in *)
        (*   s2.(Script_typed_ir.Boxed_set.size_value) <= Pervasives.max_int -> *)
        set_iter s 0.
    Proof.
      (*intros a [[t [s elt OPS boxed size_value]]]; simpl.
      (* @TODO: move assert to predicate *)
      assert(Valid : 0 <= size_value < Pervasives.max_int) by admit.
      autounfold with local_unfold1; simpl; unfold "*i", "/i".
      rewrite !safe_int_eq; [|lia..];
        rewrite !shift_right_eq; [|lia..];
          rewrite !Z.shiftr_div_pow2; [|lia..].
      destruct (Michelson_v1_gas.S.small_enough _) eqn:?Ese;
        [rewrite small_enough_eq in Ese;[|lia]|];
        [simpl in Ese;solve_simpl|].
      clear Ese;
        rewrite Pervasives.normalize_identity;[|lia].
      destruct ( _ >i _ ) eqn:E; [solve_simpl|].
      remember
        (Michelson_v1_gas.S.add 70 (normalize_int (7 * size_value)))
        as x.
      assert(Hx : 0 < x <= Michelson_v1_gas.S.saturated).
      rewrite Heqx; split;[|apply add_is_valid].
      apply lt_0_add; [|solve_simpl|left]; lia.
      assert(0 < Michelson_v1_gas.S.add (
                     Michelson_v1_gas.S.add x (size_value / 2 ^ 1))
                                        (size_value / 2 ^ 3)).
      {
        apply lt_0_add; [apply add_is_valid|lia|].
        assert(0 < Michelson_v1_gas.S.add x (size_value / 2 ^ 1))
          by (apply lt_0_add; [..|left]; lia).
        left; lia.
      }
      lia.*)

    Admitted.

    Lemma set_size_is_not_zero : set_size 0.
    Proof. cbn; lia. Qed.

    Lemma empty_map_is_not_zero : empty_map 0.
    Proof. cbn; lia. Qed.

    (* @TODO WIP *)
    Lemma map_map_is_not_zero :
       {k v : Set} (m : Script_typed_ir.map k v), map_map m 0.
    Proof.
      (*intros k v [[x [key value key_ty OPS boxed size_value]]].
      (* @TODO: move assert to predicate *)
      assert(Valid : 0 <= size_value < Pervasives.max_int) by admit.
      autounfold with local_unfold1. simpl.
      unfold "*i", "/i", Michelson_v1_gas.Cost_of.S_syntax.op_plus.
      rewrite !safe_int_eq; [|lia..];
        rewrite !shift_right_eq; [|lia..];
          rewrite !Z.shiftr_div_pow2; [|lia..].
      destruct (Michelson_v1_gas.S.small_enough _) eqn:?Ese;
        [rewrite small_enough_eq in Ese;[|lia]|];
        [simpl in Ese;solve_simpl|].
      clear Ese; rewrite Pervasives.normalize_identity;[|lia].
      destruct ( _ >i _ ) eqn:E; [solve_simpl|].
      remember (Michelson_v1_gas.S.add 265
                                       (Michelson_v1_gas.S.add (normalize_int (7 * size_value)) (size_value / 2 ^ 1))) as x'.
      assert (Hxx : 0 < x' <= Michelson_v1_gas.S.saturated).
      { rewrite Heqx'. split;[|apply add_is_valid].
        apply lt_0_add. lia.
        apply add_is_valid.
        left; lia. }
      lia.*)

    Admitted.

    (* WIP @TODO *)
    Lemma map_iter_is_not_zero :
       {k v : Set} (m : Script_typed_ir.map k v), map_iter m 0.
    Proof.
      (*intros k v [[x [key value key_ty OPS boxed size_value]]].
      (* @TODO move assert to predicate *)
      assert(Valid : 0 <= size_value < Pervasives.max_int) by admit.
      autounfold with local_unfold1. simpl.
      unfold "*i", "/i", Michelson_v1_gas.Cost_of.S_syntax.op_plus.
      rewrite !safe_int_eq; [|lia..];
        rewrite !shift_right_eq; [|lia..];
          rewrite !Z.shiftr_div_pow2; [|lia..].
      destruct (Michelson_v1_gas.S.small_enough _) eqn:?Ese;
        [rewrite small_enough_eq in Ese;[|lia]|];
        [simpl in Ese;solve_simpl|].
      clear Ese; rewrite Pervasives.normalize_identity;[|lia].
      destruct ( _ >i _ ) eqn:E; [solve_simpl|].
      remember
        (Michelson_v1_gas.S.add 70 (normalize_int (7 * size_value)))
        as x'.
      assert(Hx' : 0 < x' <= Michelson_v1_gas.S.saturated).
      rewrite Heqx'; split;[|apply add_is_valid].
      apply lt_0_add; [|solve_simpl|left]; lia.
      assert(0 < Michelson_v1_gas.S.add (
                     Michelson_v1_gas.S.add x' (size_value / 2 ^ 1))
                                        (size_value / 2 ^ 3)).
      {
        apply lt_0_add; [apply add_is_valid|lia|].
        assert(0 < Michelson_v1_gas.S.add x' (size_value / 2 ^ 1))
          by (apply lt_0_add; [..|left]; lia).
        left; lia.
      }
      lia.*)

    Admitted.

    Lemma map_size_is_not_zero : map_size 0.
    Proof. cbn; lia. Qed.

    Lemma big_map_elt_size_is_not_zero : big_map_elt_size 0.
    Proof. (* @TODO *) Admitted.

    (* WIP @TODO  *)
    Lemma big_map_mem_is_not_zero :
       {A B : Set} (m : Script_typed_ir.big_map_overlay A B),
        big_map_mem m 0.
    Proof.
      intros A B [map size].
      assert(Valid : Strictly_valid.t size) by admit.
      assert(Valid1 : Strictly_valid.t Script_expr_hash.size_value) by admit.
      unfold Strictly_valid.t in Valid.
      unfold Saturation_repr.saturated in Valid.
      unfold big_map_mem.
      unfold Alpha_context.Gas.atomic_step_cost.
      unfold Alpha_context.Gas.S.may_saturate_value.
      unfold Michelson_v1_gas.Cost_of.Generated_costs.cost_N_IMap_mem.
      unfold "*i", "/i", Michelson_v1_gas.Cost_of.S_syntax.op_plus.
      unfold Michelson_v1_gas.Cost_of.S_syntax.op_star.
      unfold big_map_elt_size in ×.
      rewrite !safe_int_eq; [|try lia..].
      assert (G: 0
                 Michelson_v1_gas.S.mul Script_expr_hash.size_value (Michelson_v1_gas.Cost_of.S_syntax.log2 size) Michelson_v1_gas.S.saturated).
      { admit. }
      rewrite !shift_right_eq; try apply G.
      rewrite !Z.shiftr_div_pow2;[|lia..].
      (* 1. remember whole expr. as x, assert that it's more than zero. 
                 prove final goal by lia. *)

      remember (Michelson_v1_gas.S.add
                  (Michelson_v1_gas.S.add 110
                                          (Michelson_v1_gas.S.mul Script_expr_hash.size_value
                                                                  (Michelson_v1_gas.Cost_of.S_syntax.log2 size) / 2 ^ 5))
                  (Michelson_v1_gas.S.mul Script_expr_hash.size_value
                                          (Michelson_v1_gas.Cost_of.S_syntax.log2 size) / 2 ^ 6)) as x.
      assert (Hxx : 0 < x Michelson_v1_gas.S.saturated).
      { rewrite Heqx. split;[|apply add_is_valid].
        assert (G': 0 < (Michelson_v1_gas.S.add 110
                                                (Michelson_v1_gas.S.mul Script_expr_hash.size_value
                                                                        (Michelson_v1_gas.Cost_of.S_syntax.log2 size) / 2 ^ 5)) Michelson_v1_gas.S.saturated ). {
          split;[|apply add_is_valid].
          apply lt_0_add; try lia. }
    Admitted.

    Lemma big_map_get_is_not_zero :
       {A B : Set} (m : Script_typed_ir.big_map_overlay A B),
        big_map_get m 0.
    Proof. (* @TODO *) Admitted.

    Lemma big_map_update_is_not_zero :
       {A B : Set} (m : Script_typed_ir.big_map_overlay A B),
        big_map_update m 0.
    Proof. (* @TODO *) Admitted.

    Lemma big_map_get_and_update_is_not_zero :
       {A B : Set} (m : Script_typed_ir.big_map_overlay A B),
        big_map_get_and_update m 0.
    Proof. (* @TODO *) Admitted.

    Lemma add_seconds_timestamp_is_not_zero :
       (seconds : Alpha_context.Script_int.num)
        (timestamp : Alpha_context.Script_timestamp.t),
        add_seconds_timestamp seconds timestamp 0.
    Proof. (* @TODO *) Admitted.

    Lemma add_timestamp_seconds_is_not_zero :
       (timestamp : Alpha_context.Script_timestamp.t)
        (seconds : Alpha_context.Script_int.num),
        add_timestamp_seconds timestamp seconds 0.
    Proof. (* @TODO *) Admitted.

    Lemma sub_timestamp_seconds_is_not_zero :
       (timestamp : Alpha_context.Script_timestamp.t)
        (seconds : Alpha_context.Script_int.num),
        sub_timestamp_seconds timestamp seconds 0.
    Proof. (* @TODO *) Admitted.

    Lemma diff_timestamps_is_not_zero :
       (t1 : Alpha_context.Script_timestamp.t)
        (t2 : Alpha_context.Script_timestamp.t),
        diff_timestamps t1 t2 0.
    Proof. (* @TODO *) Admitted.

    Lemma concat_string_pair_is_not_zero :
       (s1 : Alpha_context.Script_string.t)
        (s2 : Alpha_context.Script_string.t), concat_string_pair s1 s2 0.
    Proof. (* @TODO *) Admitted.

    Lemma slice_string_is_not_zero :
       (s_value : Alpha_context.Script_string.t), slice_string s_value 0.
    Proof. (* @TODO *) Admitted.

    Lemma string_size_is_not_zero : string_size 0.
    Proof. cbn; lia. Qed.

    Lemma concat_bytes_pair_is_not_zero :
       (b1 : bytes) (b2 : bytes), concat_bytes_pair b1 b2 0.
    Proof. (* @TODO *) Admitted.

    Lemma slice_bytes_is_not_zero :
       (b_value : bytes), slice_bytes b_value 0.
    Proof. (* @TODO *) Admitted.

    Lemma bytes_size_is_not_zero : bytes_size 0.
    Proof. cbn; lia. Qed.

    Lemma add_tez_is_not_zero : add_tez 0.
    Proof. cbn; lia. Qed.

    Lemma sub_tez_is_not_zero : sub_tez 0.
    Proof. cbn; lia. Qed.

    Lemma sub_tez_legacy_is_not_zero : sub_tez_legacy 0.
    Proof. cbn; lia. Qed.

    Lemma mul_teznat_is_not_zero : mul_teznat 0.
    Proof. cbn; lia. Qed.

    Lemma mul_nattez_is_not_zero : mul_nattez 0.
    Proof. cbn; lia. Qed.

    Lemma bool_or_is_not_zero : bool_or 0.
    Proof. cbn; lia. Qed.

    Lemma bool_and_is_not_zero : bool_and 0.
    Proof. cbn; lia. Qed.

    Lemma bool_xor_is_not_zero : bool_xor 0.
    Proof. cbn; lia. Qed.

    Lemma bool_not_is_not_zero : bool_not 0.
    Proof. cbn; lia. Qed.

    Lemma is_nat_is_not_zero : is_nat 0.
    Proof. cbn; lia. Qed.

    Lemma abs_int_is_not_zero :
       (i_value : Alpha_context.Script_int.num), abs_int i_value 0.
    Proof. (* @TODO *) Admitted.

    Lemma int_nat_is_not_zero : int_nat 0.
    Proof. cbn; lia. Qed.

    Lemma neg_is_not_zero :
       (i_value : Alpha_context.Script_int.num), neg i_value 0.
    Proof. (* @TODO *) Admitted.

    Lemma add_int_is_not_zero :
       (i1 : Alpha_context.Script_int.num)
        (i2 : Alpha_context.Script_int.num), add_int i1 i2 0.
    Proof. (* @TODO *) Admitted.

    Lemma add_nat_is_not_zero :
       (i1 : Alpha_context.Script_int.num)
        (i2 : Alpha_context.Script_int.num), add_nat i1 i2 0.
    Proof. (* @TODO *) Admitted.

    Lemma sub_int_is_not_zero :
       (i1 : Alpha_context.Script_int.num)
        (i2 : Alpha_context.Script_int.num), sub_int i1 i2 0.
    Proof. (* @TODO *) Admitted.

    Lemma mul_int_is_not_zero :
       (i1 : Alpha_context.Script_int.num)
        (i2 : Alpha_context.Script_int.num), mul_int i1 i2 0.
    Proof. (* @TODO *) Admitted.

    Lemma mul_nat_is_not_zero :
       (i1 : Alpha_context.Script_int.num)
        (i2 : Alpha_context.Script_int.num), mul_nat i1 i2 0.
    Proof. (* @TODO *) Admitted.

    Lemma ediv_teznat_is_not_zero : {A B : Set} (_tez : A) (_n : B),
        ediv_teznat _tez _n 0.
    Proof. (* @TODO *) Admitted.

    Lemma ediv_tez_is_not_zero : ediv_tez 0.
    Proof. cbn; lia. Qed.

    Lemma ediv_int_is_not_zero :
       (i1 : Alpha_context.Script_int.num)
        (i2 : Alpha_context.Script_int.num), ediv_int i1 i2 0.
    Proof. (* @TODO *) Admitted.

    Lemma ediv_nat_is_not_zero :
       (i1 : Alpha_context.Script_int.num)
        (i2 : Alpha_context.Script_int.num), ediv_nat i1 i2 0.
    Proof. (* @TODO *) Admitted.

    Lemma eq_value_is_not_zero : eq_value 0.
    Proof. cbn; lia. Qed.

    Lemma lsl_nat_is_not_zero :
       (shifted : Alpha_context.Script_int.num), lsl_nat shifted 0.
    Proof. (* @TODO *) Admitted.

    Lemma lsr_nat_is_not_zero :
       (shifted : Alpha_context.Script_int.num), lsr_nat shifted 0.
    Proof. (* @TODO *) Admitted.

    Lemma or_nat_is_not_zero :
       (n1 : Alpha_context.Script_int.num)
        (n2 : Alpha_context.Script_int.num), or_nat n1 n2 0.
    Proof. (* @TODO *) Admitted.

    Lemma and_nat_is_not_zero :
       (n1 : Alpha_context.Script_int.num)
        (n2 : Alpha_context.Script_int.num), and_nat n1 n2 0.
    Proof. (* @TODO *) Admitted.

    Lemma and_int_nat_is_not_zero :
       (n1 : Alpha_context.Script_int.num)
        (n2 : Alpha_context.Script_int.num), and_int_nat n1 n2 0.
    Proof. (* @TODO *) Admitted.

    Lemma xor_nat_is_not_zero :
       (n1 : Alpha_context.Script_int.num)
        (n2 : Alpha_context.Script_int.num), xor_nat n1 n2 0.
    Proof. (* @TODO *) Admitted.

    Lemma not_int_is_not_zero :
       (i_value : Alpha_context.Script_int.num), not_int i_value 0.
    Proof. (* @TODO *) Admitted.

    Lemma if__is_not_zero : if_ 0.
    Proof. cbn; lia. Qed.

    Lemma loop_is_not_zero : loop 0.
    Proof. cbn; lia. Qed.

    Lemma loop_left_is_not_zero : loop_left 0.
    Proof. cbn; lia. Qed.

    Lemma dip_is_not_zero : dip 0.
    Proof. cbn; lia. Qed.

    Lemma view_is_not_zero : view 0.
    Proof. cbn; lia. Qed.

    Lemma check_signature_is_not_zero :
       (pkey : Signature.public_key) (b_value : bytes),
        check_signature pkey b_value 0.
    Proof. (* @TODO *) Admitted.

    Lemma blake2b_is_not_zero : (b_value : bytes), blake2b b_value 0.
    Proof. (* @TODO *) Admitted.

    Lemma sha256_is_not_zero : (b_value : bytes), sha256 b_value 0.
    Proof. (* @TODO *) Admitted.

    Lemma sha512_is_not_zero : (b_value : bytes), sha512 b_value 0.
    Proof. (* @TODO *) Admitted.

    Lemma dign_is_not_zero : (n_value : int), dign n_value 0.
    Proof. (* @TODO *) Admitted.

    Lemma dugn_is_not_zero : (n_value : int), dugn n_value 0.
    Proof. (* @TODO *) Admitted.

    Lemma dipn_is_not_zero : (n_value : int), dipn n_value 0.
    Proof. (* @TODO *) Admitted.

    Lemma dropn_is_not_zero : (n_value : int), dropn n_value 0.
    Proof. (* @TODO *) Admitted.

    Lemma voting_power_is_not_zero : voting_power 0.
    Proof. cbn; lia. Qed.

    Lemma total_voting_power_is_not_zero : total_voting_power 0.
    Proof. cbn; lia. Qed.

    Lemma keccak_is_not_zero : (b_value : bytes), keccak b_value 0.
    Proof. (* @TODO *) Admitted.

    Lemma sha3_is_not_zero : (b_value : bytes) , sha3 b_value 0.
    Proof. (* @TODO *) Admitted.

    Lemma add_bls12_381_g1_is_not_zero : add_bls12_381_g1 0.
    Proof. cbn; lia. Qed.

    Lemma add_bls12_381_g2_is_not_zero : add_bls12_381_g2 0.
    Proof. cbn; lia. Qed.

    Lemma add_bls12_381_fr_is_not_zero : add_bls12_381_fr 0.
    Proof. cbn; lia. Qed.

    Lemma mul_bls12_381_g1_is_not_zero : mul_bls12_381_g1 0.
    Proof. cbn; lia. Qed.

    Lemma mul_bls12_381_g2_is_not_zero : mul_bls12_381_g2 0.
    Proof. cbn; lia. Qed.

    Lemma mul_bls12_381_fr_is_not_zero : mul_bls12_381_fr 0.
    Proof. cbn; lia. Qed.

    Lemma mul_bls12_381_fr_z_is_not_zero :
       (z_value : Alpha_context.Script_int.num),
        mul_bls12_381_fr_z z_value 0.
    Proof. (* @TODO *) Admitted.

    Lemma mul_bls12_381_z_fr_is_not_zero :
       (z_value : Alpha_context.Script_int.num),
        mul_bls12_381_z_fr z_value 0.
    Proof. (* @TODO *) Admitted.

    Lemma int_bls12_381_fr_is_not_zero : int_bls12_381_fr 0.
    Proof. cbn; lia. Qed.

    Lemma neg_bls12_381_g1_is_not_zero : neg_bls12_381_g1 0.
    Proof. cbn; lia. Qed.

    Lemma neg_bls12_381_g2_is_not_zero : neg_bls12_381_g2 0.
    Proof. cbn; lia. Qed.

    Lemma neg_bls12_381_fr_is_not_zero : neg_bls12_381_fr 0.
    Proof. cbn; lia. Qed.

    Lemma neq_is_not_zero : neq 0.
    Proof. cbn; lia. Qed.

    Lemma pairing_check_bls12_381_is_not_zero :
       {a : Set} (l_value : Script_typed_ir.boxed_list a),
        pairing_check_bls12_381 l_value 0.
    Proof. (* @TODO *) Admitted.

    Lemma comb_is_not_zero : (n_value : int), comb n_value 0.
    Proof. (* @TODO *) Admitted.

    Lemma uncomb_is_not_zero : (n_value : int), uncomb n_value 0.
    Proof. (* @TODO *) Admitted.

    Lemma comb_get_is_not_zero : (n_value : int), comb_get n_value 0.
    Proof. (* @TODO *) Admitted.

    Lemma comb_set_is_not_zero : (n_value : int), comb_set n_value 0.
    Proof. (* @TODO *) Admitted.

    Lemma dupn_is_not_zero : (n_value : int), dupn n_value 0.
    Proof. (* @TODO *) Admitted.

    Lemma sapling_verify_update_is_not_zero :
       (inputs outputs bound_data : int),
      sapling_verify_update inputs outputs bound_data 0.
    Proof. (* @TODO *) Admitted.

    Lemma sapling_empty_state_is_not_zero : sapling_empty_state 0.
    Proof. cbn; lia. Qed.

    Lemma halt_is_not_zero : halt 0.
    Proof. cbn; lia. Qed.

    Lemma const_is_not_zero : const 0.
    Proof. cbn; lia. Qed.

    Lemma empty_big_map_is_not_zero : empty_big_map 0.
    Proof. cbn; lia. Qed.

    Lemma lt_is_not_zero : lt 0.
    Proof. cbn; lia. Qed.

    Lemma le_is_not_zero : le 0.
    Proof. cbn; lia. Qed.

    Lemma gt_is_not_zero : gt 0.
    Proof. cbn; lia. Qed.

    Lemma ge_is_not_zero : ge 0.
    Proof. cbn; lia. Qed.

    Lemma exec_is_not_zero : exec 0.
    Proof. cbn; lia. Qed.

    Lemma apply_is_not_zero : apply 0.
    Proof. cbn; lia. Qed.

    Lemma lambda_is_not_zero : lambda 0.
    Proof. cbn; lia. Qed.

    Lemma address_is_not_zero : address 0.
    Proof. cbn; lia. Qed.

    Lemma contract_is_not_zero : contract 0.
    Proof. cbn; lia. Qed.

    Lemma transfer_tokens_is_not_zero : transfer_tokens 0.
    Proof. cbn; lia. Qed.

    Lemma implicit_account_is_not_zero : implicit_account 0.
    Proof. cbn; lia. Qed.

    Lemma create_contract_is_not_zero : create_contract 0.
    Proof. cbn; lia. Qed.

    Lemma set_delegate_is_not_zero : set_delegate 0.
    Proof. cbn; lia. Qed.

    Lemma level_is_not_zero : level 0.
    Proof. cbn; lia. Qed.

    Lemma now_is_not_zero : now 0.
    Proof. cbn; lia. Qed.

    Lemma source_is_not_zero : source 0.
    Proof. cbn; lia. Qed.

    Lemma sender_is_not_zero : sender 0.
    Proof. cbn; lia. Qed.

    Lemma self_is_not_zero : self 0.
    Proof. cbn; lia. Qed.

    Lemma self_address_is_not_zero : self_address 0.
    Proof. cbn; lia. Qed.

    Lemma amount_is_not_zero : amount 0.
    Proof. cbn; lia. Qed.

    Lemma chain_id_is_not_zero : chain_id 0.
    Proof. cbn; lia. Qed.

    Lemma ticket_is_not_zero : ticket 0.
    Proof. cbn; lia. Qed.

    Lemma read_ticket_is_not_zero : read_ticket 0.
    Proof. cbn; lia. Qed.

    Lemma hash_key_is_not_zero : {A : Set} (hk : A), hash_key hk 0.
    Proof. cbn; lia. Qed.

    Lemma split_ticket_is_not_zero :
       {A : Set} (t : A) n1 n2, split_ticket t n1 n2 0.
    Proof. (* @TODO *) Admitted.

    Lemma open_chest_is_not_zero :
       (chest : Script_typed_ir.Script_timelock.chest) (time : Z.t),
        open_chest chest time 0.
    Proof. (* @TODO *) Admitted.

    Lemma compare_unit_is_not_zero : compare_unit 0.
    Proof. cbn; lia. Qed.

    Lemma compare_pair_tag_is_not_zero : compare_pair_tag 0.
    Proof. cbn; lia. Qed.

    Lemma compare_union_tag_is_not_zero : compare_union_tag 0.
    Proof. cbn; lia. Qed.

    Lemma compare_option_tag_is_not_zero : compare_option_tag 0.
    Proof. cbn; lia. Qed.

    Lemma compare_bool_is_not_zero : compare_bool 0.
    Proof. cbn; lia. Qed.

    Lemma compare_signature_is_not_zero : compare_signature 0.
    Proof. cbn; lia. Qed.

    Lemma compare_string_is_not_zero :
       (s1 : Alpha_context.Script_string.t)
        (s2 : Alpha_context.Script_string.t), compare_string s1 s2 0.
    Proof. (* @TODO *) Admitted.

    Lemma compare_bytes_is_not_zero :
       (b1 : bytes) (b2 : bytes), compare_bytes b1 b2 0.
    Proof. (* @TODO *) Admitted.

    Lemma compare_mutez_is_not_zero : compare_mutez 0.
    Proof. cbn; lia. Qed.

    Lemma compare_int_is_not_zero :
       (i1 : Alpha_context.Script_int.num)
        (i2 : Alpha_context.Script_int.num), compare_int i1 i2 0.
    Proof. (* @TODO *) Admitted.

    Lemma compare_nat_is_not_zero :
       (n1 : Alpha_context.Script_int.num)
        (n2 : Alpha_context.Script_int.num), compare_nat n1 n2 0.
    Proof. (* @TODO *) Admitted.

    Lemma compare_key_hash_is_not_zero : compare_key_hash 0.
    Proof. (* @TODO *) Admitted.

    Lemma compare_key_is_not_zero : compare_key 0.
    Proof. cbn; lia. Qed.

    Lemma compare_timestamp_is_not_zero :
       (t1 : Alpha_context.Script_timestamp.t)
        (t2 : Alpha_context.Script_timestamp.t), compare_timestamp t1 t2 0.
    Proof. (* @TODO *) Admitted.

    Lemma entrypoint_size_is_not_zero : entrypoint_size 0.
    Proof. (* @TODO *) Admitted.

    Lemma compare_address_is_not_zero : compare_address 0.
    Proof. (* @TODO *) Admitted.

    Lemma compare_chain_id_is_not_zero : compare_chain_id 0.
    Proof. cbn; lia. Qed.

    Lemma compare : {a : Set} (cty : Script_typed_ir.comparable_ty)
                      (a1 a2 : a), compare cty a1 a2 0.
    Proof. (* @TODO *) Admitted.

    (*Lemma view_mem_is_not_zero :
      forall (elt_value : Alpha_context.Script_string.t)
        (m_value : Script_typed_ir.SMap.(Map.S.t) Script_typed_ir.view),
        view_mem elt_value m_value <> 0.
    Proof. @TODO Admitted.
    
    Lemma view_get_is_not_zeor :
      forall (s : Alpha_context.Script_string.t)
        (smap : Script_typed_ir.SMap.(Map.S.t) Script_typed_ir.view),
        view_mem s smap <> 0.
    Proof. (* @TODO *) Admitted.
    
    Lemma view_update_is_not_zero :
      forall (elt_value : Alpha_context.Script_string.t)
        (m_value : Script_typed_ir.SMap.(Map.S.t) Script_typed_ir.view),
        view_update elt_value m_value <> 0.
    Proof. (* @TODO *) Admitted.*)


    Lemma set_mem_is_not_zero :
       {a : Set} (elt_value : a) (set : Script_typed_ir.set a),
        set_mem elt_value set 0.
    Proof. (* @TODO *) Admitted.

    Lemma set_update_is_not_zero :
       {a : Set} (elt_value : a) (set : Script_typed_ir.set a),
        set_update elt_value set 0.
    Proof. (* @TODO *) Admitted.

    Lemma map_mem_is_not_zero :
       {k v : Set} (elt_value : k) (map : Script_typed_ir.map k v),
        map_mem elt_value map 0.
    Proof. (* @TODO *) Admitted.

    Lemma map_get_is_not_zero :
       {A B : Set} (k : A) (map : Script_typed_ir.map A B),
        map_get k map 0.
    Proof. (* @TODO *) Admitted.

    Lemma map_update_is_not_zero :
       {k v : Set} (elt_value : k) (map : Script_typed_ir.map k v),
        map_update elt_value map 0.
    Proof. (* @TODO *) Admitted.

    Lemma map_get_and_update_is_not_zero :
       {k v : Set} (elt_value : k) (map : Script_typed_ir.map k v),
        map_get_and_update elt_value map 0.
    Proof. (* @TODO *) Admitted.

    Lemma join_tickets_is_not_zero :
       {a : Set}
        (ty : Script_typed_ir.comparable_ty)
        (ticket_a : Script_typed_ir.ticket a)
        (ticket_b : Script_typed_ir.ticket a), join_tickets ty ticket_a ticket_b 0.
    Proof. (* @TODO *) Admitted.

    Module Control.
      Import Proto_alpha.Michelson_v1_gas.Cost_of.Interpreter.Control.

      Lemma nil_is_not_zero : nil 0.
      Proof. cbn; lia. Qed.

      Lemma cons_value_is_not_zero : cons_value 0.
      Proof. cbn; lia. Qed.

      Lemma _return_is_not_zero : _return 0.
      Proof. cbn; lia. Qed.

      Lemma view_exit_is_not_zero : view_exit 0.
      Proof. cbn; lia. Qed.

      Lemma map_head_is_not_zero : map_head 0.
      Proof. cbn; lia. Qed.

      Lemma undip_is_not_zero : undip 0.
      Proof. cbn; lia. Qed.

      Lemma loop_in_is_not_zero : loop_in 0.
      Proof. cbn; lia. Qed.

      Lemma loop_in_left_is_not_zero : loop_in_left 0.
      Proof. cbn; lia. Qed.

      Lemma iter_is_not_zero : iter 0.
      Proof. cbn; lia. Qed.

      Lemma list_enter_body_is_not_zero :
         {A : Set} (xs : list A) (ys_len : int),
          list_enter_body xs ys_len 0.
      Proof. (* @TODO *) Admitted.

      Lemma list_exit_body_is_not_zero : list_exit_body 0.
      Proof. cbn; lia. Qed.

      Lemma map_enter_body_is_not_zero : map_enter_body 0.
      Proof. cbn; lia. Qed.

      Lemma map_exit_body_is_not_zero :
         {k v : Set} (key_value : k) (map : Script_typed_ir.map k v),
          map_exit_body key_value map 0.
      Proof. (* @TODO *) Admitted.
    End Control.

    Lemma concat_string_precheck_is_not_zero :
       {a : Set} (l_value : Script_typed_ir.boxed_list a),
        concat_string_precheck l_value 0.
    Proof. (* @TODO *) Admitted.

    (* @TODO *)
    (* Lemma concat_string_is_not_zero : *)
    (*   forall (total_bytes : S.t), concat_string total_bytes <> 0. *)
    (* Proof. (* @TODO *) Admitted. *)

    (* @TODO *)
    (* Lemma concat_bytes_is_not_zero : *)
    (*   forall (total_bytes : S.t), concat_bytes total_bytes <> 0. *)
    (* Proof. (* @TODO *) Admitted. *)

    Lemma balance_is_not_zero : balance 0.
    Proof. (* @TODO *) Admitted.

    Lemma unpack_is_not_zero :
       (bytes_value : bytes), unpack bytes_value 0.
    Proof. (* @TODO *) Admitted.

    Lemma unpack_failed_is_not_zero :
       (bytes_value : string), unpack_failed bytes_value 0.
    Proof. (* @TODO *) Admitted.
  End Interpreter.
End Cost_of.