gistfile1.txt

docs/PROOF.md:Lemma run_unwrap_or_default {T : Set}
CoqOfRust/proofs/M.v:  Lemma eqb_refl (kind : IntegerKind.t) : IntegerKind.eqb kind kind = true.
CoqOfRust/experiments/MonadExperiments.v:  Lemma State_is_valid : State.Valid.t State_Trait.
CoqOfRust/experiments/MonadExperiments.v:  Lemma run_main :
CoqOfRust/lib/proofs/lib.v:  Lemma normalize_wrap_is_valid (kind : IntegerKind.t) (z : Z) :
CoqOfRust/lib/proofs/lib.v:  Lemma normalize_with_error_eq (kind : IntegerKind.t) (z z' : Z) :
CoqOfRust/lib/proofs/lib.v:    Lemma add_is_valid (kind : IntegerKind.t) (z1 z2 z : Z)
CoqOfRust/core/num/flt2dec/strategy/grisu.v:            // scale fps. this gives the maximal error of 1 ulp (proved from Theorem 5.1).
CoqOfRust/core/num/flt2dec/strategy/grisu.v:            // Theorem 6.2: if `k` is the greatest integer s.t. `0 <= y mod 10^k <= y - x`,
CoqOfRust/core/num/flt2dec/strategy/grisu.v:            // find the digit length `kappa` between `(minus1, plus1)` as per Theorem 6.2.
CoqOfRust/core/num/flt2dec/strategy/grisu.v:            // Theorem 6.2 can be adopted to exclude `x` by requiring `y mod 10^k < y - x` instead.
CoqOfRust/core/num/flt2dec/strategy/grisu.v:            // both old `v` and new `v` (scaled by `10^-k`) has an error of < 1 ulp (Theorem 5.1).
CoqOfRust/revm/links/interpreter/interpreter/gas.v:    Lemma get_limit_is_valid :
CoqOfRust/revm/links/interpreter/interpreter/gas.v:    Lemma get_remaining_is_valid :
CoqOfRust/revm/links/interpreter/interpreter/gas.v:    Lemma get_refunded_is_valid :
CoqOfRust/move_sui/simulations/move_abstract_stack/unit_tests/mod.v:Lemma test_empty_stack_correct :
CoqOfRust/move_sui/simulations/move_abstract_stack/unit_tests/mod.v:Lemma test_simple_push_pop_correct :
CoqOfRust/move_sui/simulations/move_abstract_stack/unit_tests/mod.v:Lemma test_not_eq_correct :
CoqOfRust/move_sui/simulations/move_abstract_stack/unit_tests/mod.v:Lemma test_not_enough_values_correct :
CoqOfRust/examples/default/examples/ink_contracts/proofs/erc721.v:  Lemma is_valid : State.Valid.t I.
CoqOfRust/examples/default/examples/ink_contracts/proofs/erc721.v:  Lemma run_Default : default.Default.TraitHasRun erc721.Balance.t.
CoqOfRust/examples/default/examples/ink_contracts/proofs/erc721.v:  Lemma run_caller (env : erc721.Env.t) (state : State.t) :
CoqOfRust/examples/default/examples/ink_contracts/proofs/erc721.v:  Lemma run_emit_event
CoqOfRust/examples/default/examples/ink_contracts/proofs/erc721.v:Lemma run_init_env (env : erc721.Env.t) (storage : erc721.Erc721.t) :
CoqOfRust/examples/default/examples/ink_contracts/proofs/erc721.v:Lemma run_env (env : erc721.Env.t) (storage : erc721.Erc721.t) :
CoqOfRust/examples/default/examples/ink_contracts/proofs/erc721.v:Lemma run_balance_of_or_zero
CoqOfRust/examples/default/examples/ink_contracts/proofs/erc721.v:Lemma run_approved_for_all
CoqOfRust/examples/default/examples/ink_contracts/proofs/erc721.v:Lemma run_owner_of
CoqOfRust/examples/default/examples/ink_contracts/proofs/erc721.v:Lemma run_exists
CoqOfRust/examples/default/examples/ink_contracts/proofs/erc721.v:Lemma run_balance_of
CoqOfRust/examples/default/examples/ink_contracts/proofs/erc721.v:Lemma run_get_approved
CoqOfRust/examples/default/examples/ink_contracts/proofs/erc721.v:Lemma run_is_approved_for_all
CoqOfRust/examples/default/examples/ink_contracts/proofs/erc721.v:Lemma run_clear_approval
CoqOfRust/examples/default/examples/ink_contracts/proofs/erc721.v:Lemma run_set_approval_for_all
CoqOfRust/examples/default/examples/ink_contracts/proofs/erc721.v:Lemma run_approve_for
CoqOfRust/examples/default/examples/ink_contracts/proofs/erc721.v:Lemma run_approve
CoqOfRust/examples/default/examples/ink_contracts/proofs/erc721.v:Lemma run_remove_token_from
CoqOfRust/examples/default/examples/ink_contracts/proofs/erc721.v:Lemma run_add_token_to
CoqOfRust/examples/default/examples/ink_contracts/proofs/erc721.v:Lemma run_transfer_token_from
CoqOfRust/examples/default/examples/ink_contracts/proofs/erc721.v:Lemma run_transfer
CoqOfRust/examples/default/examples/ink_contracts/proofs/erc721.v:Lemma run_transfer_from
CoqOfRust/examples/default/examples/ink_contracts/proofs/erc721.v:Lemma run_mint
CoqOfRust/examples/default/examples/ink_contracts/proofs/erc721.v:Lemma run_burn
CoqOfRust/examples/default/examples/ink_contracts/proofs/erc20.v:  Lemma run_Default : default.Default.TraitHasRun erc20.Balance.t (Ty.path "u128").
CoqOfRust/examples/default/examples/ink_contracts/proofs/erc20.v:    Lemma get_total_supply_is_valid :
CoqOfRust/examples/default/examples/ink_contracts/proofs/erc20.v:    Lemma get_balances_is_valid :
CoqOfRust/examples/default/examples/ink_contracts/proofs/erc20.v:    Lemma get_allowances_is_valid :
CoqOfRust/examples/default/examples/ink_contracts/proofs/erc20.v:  Lemma eq_or_neq (x y : erc20.AccountId.t) :
CoqOfRust/examples/default/examples/ink_contracts/proofs/erc20.v:  Lemma eq_or_neq_couple (x y : erc20.AccountId.t * erc20.AccountId.t) :
CoqOfRust/examples/default/examples/ink_contracts/proofs/erc20.v:  Lemma insert_balances_is_valid from diff storage
CoqOfRust/examples/default/examples/ink_contracts/proofs/erc20.v:  Lemma insert_allowances_is_valid couple diff storage
CoqOfRust/examples/default/examples/ink_contracts/proofs/erc20.v:  Lemma of_mstate_storage_eq (x : erc20.MState.t) (y : erc20.Erc20.t) :
CoqOfRust/examples/default/examples/ink_contracts/proofs/erc20.v:  Lemma is_valid : M.State.Valid.t I.
CoqOfRust/examples/default/examples/ink_contracts/proofs/erc20.v:  Lemma run_caller (env : erc20.Env.t) (state : State.t) :
CoqOfRust/examples/default/examples/ink_contracts/proofs/erc20.v:  Lemma run_emit_event
CoqOfRust/examples/default/examples/ink_contracts/proofs/erc20.v:Lemma run_init_env (env : erc20.Env.t) (state : erc20.State.t) :
CoqOfRust/examples/default/examples/ink_contracts/proofs/erc20.v:Lemma run_env (env : erc20.Env.t) (state : erc20.State.t) :
CoqOfRust/examples/default/examples/ink_contracts/proofs/erc20.v:Lemma run_total_supply
CoqOfRust/examples/default/examples/ink_contracts/proofs/erc20.v:Lemma run_balance_of_impl
CoqOfRust/examples/default/examples/ink_contracts/proofs/erc20.v:Lemma balance_of_impl_is_valid
CoqOfRust/examples/default/examples/ink_contracts/proofs/erc20.v:Lemma run_balance_of
CoqOfRust/examples/default/examples/ink_contracts/proofs/erc20.v:Lemma run_allowance_impl
CoqOfRust/examples/default/examples/ink_contracts/proofs/erc20.v:Lemma allowance_impl_is_valid
CoqOfRust/examples/default/examples/ink_contracts/proofs/erc20.v:Lemma run_allowance
CoqOfRust/examples/default/examples/ink_contracts/proofs/erc20.v:Lemma sub_eq_optimistic (v1 v2 : Z) :
CoqOfRust/examples/default/examples/ink_contracts/proofs/erc20.v:Lemma run_transfer_from_to
CoqOfRust/examples/default/examples/ink_contracts/proofs/erc20.v:Lemma run_transfer
CoqOfRust/examples/default/examples/ink_contracts/proofs/erc20.v:Lemma run_approve
CoqOfRust/examples/default/examples/ink_contracts/proofs/erc20.v:Lemma run_transfer_from
CoqOfRust/examples/default/examples/ink_contracts/proofs/erc20.v:  Lemma run_dispatch
CoqOfRust/examples/default/examples/ink_contracts/proofs/erc20.v:  Lemma run_dispatch
CoqOfRust/examples/default/examples/ink_contracts/proofs/erc20.v:Lemma read_message_no_panic
CoqOfRust/examples/default/examples/ink_contracts/proofs/erc20.v:Lemma transfer_from_to_is_valid
CoqOfRust/examples/default/examples/ink_contracts/proofs/erc20.v:Lemma transfer_is_valid
CoqOfRust/examples/default/examples/ink_contracts/proofs/erc20.v:Lemma approve_is_valid
CoqOfRust/examples/default/examples/ink_contracts/proofs/erc20.v:Lemma transfer_from_is_valid
CoqOfRust/examples/default/examples/ink_contracts/proofs/erc20.v:Lemma write_dispatch_is_valid
CoqOfRust/examples/default/examples/ink_contracts/proofs/erc20.v:  Lemma transfer_from_to_constant
CoqOfRust/examples/default/examples/ink_contracts/proofs/erc20.v:  Lemma transfer_is_constant
CoqOfRust/examples/default/examples/ink_contracts/proofs/erc20.v:  Lemma approve_is_constant
CoqOfRust/examples/default/examples/ink_contracts/proofs/erc20.v:  Lemma transfer_from_is_constant
CoqOfRust/examples/default/examples/ink_contracts/proofs/erc20.v:  Lemma write_dispatch_is_constant
CoqOfRust/examples/default/examples/ink_contracts/proofs/erc20.v:  Lemma transfer_from_to_on_storage
CoqOfRust/examples/default/examples/ink_contracts/proofs/erc20.v:  Lemma event_from_transfer_from_to
CoqOfRust/examples/default/examples/ink_contracts/proofs/erc20.v:  Lemma retrieve_action_from_logs
CoqOfRust/examples/default/examples/ink_contracts/proofs/erc20.v:Lemma approve_only_changes_owner_allowance
CoqOfRust/examples/default/examples/ink_contracts/proofs/lib.v:  Lemma insert_insert (k : K) (v1 v2 : V) m :
CoqOfRust/examples/default/examples/ink_contracts/proofs/lib.v:  Lemma insert_id (k : K) (v : V) m :
CoqOfRust/examples/default/examples/ink_contracts/proofs/lib.v:  Lemma insert_switch (k1 k2 : K) (v1 v2 : V) m :
CoqOfRust/examples/default/examples/ink_contracts/proofs/lib.v:  Lemma Forall_insert : forall P k v m,