🍬 Michelson_v1_gas.v
Proofs
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
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.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
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.
The function [manager_operation] is valid.
Lemma manager_operation_is_valid :
Saturation_repr.Valid.t Michelson_v1_gas.Cost_of.manager_operation.
Proof.
easy.
Qed.
Module Interpreter.
Import Proto_alpha.Michelson_v1_gas.Cost_of.Interpreter.
Lemma drop_is_not_zero : drop ≠ 0.
Proof. cbn; lia. Qed.
Lemma drop_is_valid : 0 < drop ≤ Saturation_repr.saturated.
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 cons_pair_is_valid : 0 < cons_pair ≤ Saturation_repr.saturated.
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_list.t 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_list.t a), list_iter l ≠ 0.
Proof. cbn; lia. Qed.
Lemma list_iter_is_valid :
∀ {a : Set} (l : Script_list.t a),
0 < list_iter l ≤ Saturation_repr.saturated.
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.
step; [|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
map_map
map_iter
: local_unfold1.
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 "*i", "/i".
unfold big_map_elt_size in ×.
Admitted.
(* 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 : Script_int.num)
(timestamp : Script_timestamp.t),
add_seconds_timestamp seconds timestamp ≠ 0.
Proof. (* @TODO *) Admitted.
Lemma add_timestamp_seconds_is_not_zero :
∀ (timestamp : Script_timestamp.t)
(seconds : Script_int.num),
add_timestamp_seconds timestamp seconds ≠ 0.
Proof. (* @TODO *) Admitted.
Lemma sub_timestamp_seconds_is_not_zero :
∀ (timestamp : Script_timestamp.t)
(seconds : Script_int.num),
sub_timestamp_seconds timestamp seconds ≠ 0.
Proof. (* @TODO *) Admitted.
Lemma diff_timestamps_is_not_zero :
∀ (t1 : Script_timestamp.t)
(t2 : Script_timestamp.t),
diff_timestamps t1 t2 ≠ 0.
Proof. (* @TODO *) Admitted.
Lemma concat_string_pair_is_not_zero :
∀ (s1 : Script_string.t)
(s2 : Script_string.t), concat_string_pair s1 s2 ≠ 0.
Proof. (* @TODO *) Admitted.
Lemma slice_string_is_not_zero :
∀ (s_value : 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 : 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 : Script_int.num), neg i_value ≠ 0.
Proof. (* @TODO *) Admitted.
Lemma add_int_is_not_zero :
∀ (i1 : Script_int.num)
(i2 : Script_int.num), add_int i1 i2 ≠ 0.
Proof. (* @TODO *) Admitted.
Lemma add_nat_is_not_zero :
∀ (i1 : Script_int.num)
(i2 : Script_int.num), add_nat i1 i2 ≠ 0.
Proof. (* @TODO *) Admitted.
Lemma sub_int_is_not_zero :
∀ (i1 : Script_int.num)
(i2 : Script_int.num), sub_int i1 i2 ≠ 0.
Proof. (* @TODO *) Admitted.
Lemma mul_int_is_not_zero :
∀ (i1 : Script_int.num)
(i2 : Script_int.num), mul_int i1 i2 ≠ 0.
Proof. (* @TODO *) Admitted.
Lemma mul_nat_is_not_zero :
∀ (i1 : Script_int.num)
(i2 : 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 : Script_int.num)
(i2 : Script_int.num), ediv_int i1 i2 ≠ 0.
Proof. (* @TODO *) Admitted.
Lemma ediv_nat_is_not_zero :
∀ (i1 : Script_int.num)
(i2 : 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 : Script_int.num), lsl_nat shifted ≠ 0.
Proof. (* @TODO *) Admitted.
Lemma lsr_nat_is_not_zero :
∀ (shifted : Script_int.num), lsr_nat shifted ≠ 0.
Proof. (* @TODO *) Admitted.
Lemma or_nat_is_not_zero :
∀ (n1 : Script_int.num)
(n2 : Script_int.num), or_nat n1 n2 ≠ 0.
Proof. (* @TODO *) Admitted.
Lemma and_nat_is_not_zero :
∀ (n1 : Script_int.num)
(n2 : Script_int.num), and_nat n1 n2 ≠ 0.
Proof. (* @TODO *) Admitted.
Lemma and_int_nat_is_not_zero :
∀ (n1 : Script_int.num)
(n2 : Script_int.num), and_int_nat n1 n2 ≠ 0.
Proof. (* @TODO *) Admitted.
Lemma xor_nat_is_not_zero :
∀ (n1 : Script_int.num)
(n2 : Script_int.num), xor_nat n1 n2 ≠ 0.
Proof. (* @TODO *) Admitted.
Lemma not_int_is_not_zero :
∀ (i_value : 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 : 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 : 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_list.t 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 {b} : apply b ≠ 0.
Proof. destruct_all bool; 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 :
∀ n1 n2, split_ticket 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 : Script_string.t)
(s2 : 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 : Script_int.num)
(i2 : Script_int.num), compare_int i1 i2 ≠ 0.
Proof. (* @TODO *) Admitted.
Lemma compare_nat_is_not_zero :
∀ (n1 : Script_int.num)
(n2 : 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 : Script_timestamp.t)
(t2 : 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.
Module Compare.
Saturation_repr.Valid.t Michelson_v1_gas.Cost_of.manager_operation.
Proof.
easy.
Qed.
Module Interpreter.
Import Proto_alpha.Michelson_v1_gas.Cost_of.Interpreter.
Lemma drop_is_not_zero : drop ≠ 0.
Proof. cbn; lia. Qed.
Lemma drop_is_valid : 0 < drop ≤ Saturation_repr.saturated.
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 cons_pair_is_valid : 0 < cons_pair ≤ Saturation_repr.saturated.
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_list.t 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_list.t a), list_iter l ≠ 0.
Proof. cbn; lia. Qed.
Lemma list_iter_is_valid :
∀ {a : Set} (l : Script_list.t a),
0 < list_iter l ≤ Saturation_repr.saturated.
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.
step; [|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
map_map
map_iter
: local_unfold1.
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 "*i", "/i".
unfold big_map_elt_size in ×.
Admitted.
(* 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 : Script_int.num)
(timestamp : Script_timestamp.t),
add_seconds_timestamp seconds timestamp ≠ 0.
Proof. (* @TODO *) Admitted.
Lemma add_timestamp_seconds_is_not_zero :
∀ (timestamp : Script_timestamp.t)
(seconds : Script_int.num),
add_timestamp_seconds timestamp seconds ≠ 0.
Proof. (* @TODO *) Admitted.
Lemma sub_timestamp_seconds_is_not_zero :
∀ (timestamp : Script_timestamp.t)
(seconds : Script_int.num),
sub_timestamp_seconds timestamp seconds ≠ 0.
Proof. (* @TODO *) Admitted.
Lemma diff_timestamps_is_not_zero :
∀ (t1 : Script_timestamp.t)
(t2 : Script_timestamp.t),
diff_timestamps t1 t2 ≠ 0.
Proof. (* @TODO *) Admitted.
Lemma concat_string_pair_is_not_zero :
∀ (s1 : Script_string.t)
(s2 : Script_string.t), concat_string_pair s1 s2 ≠ 0.
Proof. (* @TODO *) Admitted.
Lemma slice_string_is_not_zero :
∀ (s_value : 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 : 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 : Script_int.num), neg i_value ≠ 0.
Proof. (* @TODO *) Admitted.
Lemma add_int_is_not_zero :
∀ (i1 : Script_int.num)
(i2 : Script_int.num), add_int i1 i2 ≠ 0.
Proof. (* @TODO *) Admitted.
Lemma add_nat_is_not_zero :
∀ (i1 : Script_int.num)
(i2 : Script_int.num), add_nat i1 i2 ≠ 0.
Proof. (* @TODO *) Admitted.
Lemma sub_int_is_not_zero :
∀ (i1 : Script_int.num)
(i2 : Script_int.num), sub_int i1 i2 ≠ 0.
Proof. (* @TODO *) Admitted.
Lemma mul_int_is_not_zero :
∀ (i1 : Script_int.num)
(i2 : Script_int.num), mul_int i1 i2 ≠ 0.
Proof. (* @TODO *) Admitted.
Lemma mul_nat_is_not_zero :
∀ (i1 : Script_int.num)
(i2 : 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 : Script_int.num)
(i2 : Script_int.num), ediv_int i1 i2 ≠ 0.
Proof. (* @TODO *) Admitted.
Lemma ediv_nat_is_not_zero :
∀ (i1 : Script_int.num)
(i2 : 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 : Script_int.num), lsl_nat shifted ≠ 0.
Proof. (* @TODO *) Admitted.
Lemma lsr_nat_is_not_zero :
∀ (shifted : Script_int.num), lsr_nat shifted ≠ 0.
Proof. (* @TODO *) Admitted.
Lemma or_nat_is_not_zero :
∀ (n1 : Script_int.num)
(n2 : Script_int.num), or_nat n1 n2 ≠ 0.
Proof. (* @TODO *) Admitted.
Lemma and_nat_is_not_zero :
∀ (n1 : Script_int.num)
(n2 : Script_int.num), and_nat n1 n2 ≠ 0.
Proof. (* @TODO *) Admitted.
Lemma and_int_nat_is_not_zero :
∀ (n1 : Script_int.num)
(n2 : Script_int.num), and_int_nat n1 n2 ≠ 0.
Proof. (* @TODO *) Admitted.
Lemma xor_nat_is_not_zero :
∀ (n1 : Script_int.num)
(n2 : Script_int.num), xor_nat n1 n2 ≠ 0.
Proof. (* @TODO *) Admitted.
Lemma not_int_is_not_zero :
∀ (i_value : 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 : 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 : 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_list.t 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 {b} : apply b ≠ 0.
Proof. destruct_all bool; 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 :
∀ n1 n2, split_ticket 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 : Script_string.t)
(s2 : 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 : Script_int.num)
(i2 : Script_int.num), compare_int i1 i2 ≠ 0.
Proof. (* @TODO *) Admitted.
Lemma compare_nat_is_not_zero :
∀ (n1 : Script_int.num)
(n2 : 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 : Script_timestamp.t)
(t2 : 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.
Module Compare.
We can unroll the continuation of the function [Compare.compare].
Fixpoint compare_continuation_eq {a : Set}
(cty : Script_typed_ir.comparable_ty) (a1 a2 : a) acc k {struct cty} :
Compare.compare cty a1 a2 acc k =
Compare.apply (Compare.compare cty a1 a2 acc Return) k.
Proof.
Admitted.
End Compare.
(cty : Script_typed_ir.comparable_ty) (a1 a2 : a) acc k {struct cty} :
Compare.compare cty a1 a2 acc k =
Compare.apply (Compare.compare cty a1 a2 acc Return) k.
Proof.
Admitted.
End Compare.
The function [compare] is valid.
Fixpoint compare_is_valid {a : Set}
(cty : Script_typed_ir.comparable_ty) (a1 a2 : a) {struct cty} :
Saturation_repr.Valid.t (compare cty a1 a2).
Proof.
Admitted.
Lemma compare_is_not_zero {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 : 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 : 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 : 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_list.t 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.
(cty : Script_typed_ir.comparable_ty) (a1 a2 : a) {struct cty} :
Saturation_repr.Valid.t (compare cty a1 a2).
Proof.
Admitted.
Lemma compare_is_not_zero {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 : 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 : 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 : 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_list.t 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.