Skip to main content

Asserts

Gitlab

This report list the assertions, (i.e. calls to assert) in the Tezos Protocol code. For each assertion we show :

  • What that assertion represents. We show comments that surround the assertion in the code and try to bring the context in which the assertion is surrounded.
  • If they could be avoided by writing the code in another way.
  • What are the conditions to show that the assertion does not occur.

For each file, we present the list of the assertions with a link to each assertion followed by the comments about it. Please note that the report is done over the commit b9b6f296c32a3364b64992fe41f4454d14936dfd, this is done so that the links in the report do not break.

Summary​

  • Number of files: 35
  • Number of assert false: 46
  • Total of assertions: 105
  • Main uses of assertions:
    • ⛔ Mark unreachable code
      • This has the form assert false and depends on some precondition that holds at that point in the code so that the assertion is never reached. To verify this kind of assertion we need to formulate the preconditions and show that from these preconditions the assertion is not evaluated.
    • 🕰 Ensure invariants
      • This has the form assert some_pre_condition, and also depends on some precondition, but this time is used to ensure that the precondition holds, the code is reachable but the condition should always hold (in that context). To verify it we need to state the preconditions and show that the predicate in the assertion holds.
    • 👮 Ensure valid arguments
      • This is the form assert some_argument_validation and it is used to ensure that arguments have sane values inside functions and functors. We can't verify this locally, we need to show that at some point of the code these functions or functors are not called with invalid arguments.

https://gitlab.com/tezos/tezos/-/blob/b9b6f296c32a3364b64992fe41f4454d14936dfd/src/proto_alpha/lib_protocol/

amendment.ml​

  • assert (Compare.Int.(Constants.max_proposals_per_delegate >= count)) 🔗
    • 🕰 Ensures invariants
    • This just ensures that the count (coming from Vote.recorded_proposal_count_for_delegate) is below the max_proposals_per_delegate.
    • One way to avoid this assertion is using minfunction to chop the value to a valid maximum.
    • To show that this does not happen we have two options.
      • By using the min function this becomes trivial.
      • Otherwise we need to show that no value greater than max_proposal_count is written to the storage.

apply_results.ml​

These are all inside encoding injections, for example: (line 340)

      ~proj:(function
| Reveal_result {consumed_gas} ->
(Gas.Arith.ceil consumed_gas, consumed_gas))
~inj:(fun (consumed_gas, consumed_milligas) ->
assert (Gas.Arith.(equal (ceil consumed_milligas) consumed_gas)) ;
Reveal_result {consumed_gas = consumed_milligas})
  • 🕰 Ensures invariants
  • To show that this does not happen we will need an axiom saying that the decoded value is the same that was encoded, then we can recover the ceil application in the decoding and show that the equality holds.
  • This can be replaced by using the conv_with_guard function from data_encoding, so that in case of failure the error is returned.
  • assert (Gas.Arith.(equal (ceil consumed_milligas) consumed_gas)) 🔗
  • assert (Gas.Arith.(equal (ceil consumed_milligas) consumed_gas)) 🔗
  • assert (Gas.Arith.(equal (ceil consumed_milligas) consumed_gas)) 🔗
  • assert (Gas.Arith.(equal (ceil consumed_milligas) consumed_gas)) 🔗
  • assert (Gas.Arith.(equal (ceil consumed_milligas) consumed_gas)) 🔗
  • assert (Gas.Arith.(equal (ceil consumed_milligas) consumed_gas)) 🔗
  • assert (Gas.Arith.(equal (ceil consumed_milligas) consumed_gas)) 🔗
  • assert (Gas.Arith.(equal (ceil consumed_milligas) consumed_gas)) 🔗
  • assert (Gas.Arith.(equal (ceil consumed_milligas) consumed_gas)) 🔗
  • assert (Gas.Arith.(equal (ceil consumed_milligas) consumed_gas)) 🔗
  • assert (Gas.Arith.(equal (ceil consumed_milligas) consumed_gas)) 🔗
  • assert (Gas.Arith.(equal (ceil consumed_milligas) consumed_gas)) 🔗
  • assert (Gas.Arith.(equal (ceil consumed_milligas) consumed_gas)) 🔗
  • assert (Gas.Arith.(equal (ceil consumed_milligas) consumed_gas)) 🔗
  • assert (Gas.Arith.(equal (ceil consumed_milligas) consumed_gas)) 🔗
  • assert (Gas.Arith.(equal (ceil consumed_milligas) consumed_gas)) 🔗
  • assert (Gas.Arith.(equal (ceil consumed_milligas) consumed_gas)) 🔗
  • assert (Gas.Arith.(equal (ceil consumed_milligas) consumed_gas)) 🔗
  • assert (Gas.Arith.(equal (ceil consumed_milligas) consumed_gas)) 🔗

cache_repr.ml​

This module introduces an opaque namespace type which is a string with no @ inside. Also, it defines a function val create_namespace : string -> namespace to construct namespaces from strings. This property of namespaces: not having a @ is used on the assertions.

  • ⛔ Marks unreachable code

  • To show that this does not happen we need to formulate the property of namespaces and then prove that the assertions are unreachable.

  • There is no simple way to rewrite this to get rid of the assertions.

  • | None -> assert false 🔗

    • Because of the property of namespaces, this assert false is unreachable.
  • assert false 🔗

    • From a comment in the code

      This execution path is impossible because all the keys of C's namespace (which is unique to C) is constructed with [K]. This [assert false] could have been pushed into the environment in exchange for extra complexity. The argument that justifies this [assert false] seems simple enough to keep the current design though.

  • assert false 🔗

    • This is assuming that the client invariants at 🔗 are holding. The invariants are checked at the beginning of the module construction at 🔗

contract_repr.ml​

  • assert (Operation_hash.equal first_hash last_hash) ; 🔗
    • 👮 Ensure valid arguments Comment in the code 🔗:

      The operation hash of nonce [since] and [until] must be the same or it will fail with an [assert]. [since] < [until] or the returned list is empty *)

    • To show that this does not happen we would need to show that originated_contracts are never called with wrong arguments which may not be possible.

contract_storage.ml​

  • | Remove -> assert false 🔗
    • 🕰 Ensure invariants
    • There is a fold where Remove items are not included by the way that rev_head is defined and used, this assertion relies on rev_head definition. Comment in the code

      ( Invariant: Updates are collected one by one, in reverse order, on the head diff item. So only and exactly the head diff item has its updates reversed. )

    • To show that this is unreachable we need to show that the invariant in the code holds, this would not be simple.
  • assert (Compare.Z.(total_size >= Z.zero)) ; 🔗

cycle_repr.ml​

  • 👮 Ensure valid arguments

  • Both assertions guard against negative values, they are in add and sub operations which have cycle -> int -> cycle and cycle -> int -> cycle option signatures, respectively.

  • No way to show that this holds, it depends on the caller.

  • assert (Compare.Int.(i >= 0)) ; 🔗

  • assert (Compare.Int.(i >= 0)) ; 🔗

delegate_storage.ml​

  • 🕰 Ensure invariants

  • assert (Compare.Bool.(slashed.for_double_endorsing = false)) ; 🔗

    • Same as below
  • assert (Compare.Bool.(slashed.for_double_baking = false)) ; 🔗

    • Storage.Slashed_deposits is used to avoid slashing the same event multiple times, this assertion guards this invariant.
    • To show that this (and the previous) assert holds we need to show that the invariants of the Storage.Slashed_deposits holds
  • assert (Compare.Int32.(level.cycle_position = 0l)) ; 🔗

    • Comment in the code in record_endorsing_participation operation, for when Signature.Public_key_hash.Map.find returns None

      ( This happens when the block is the first one in a cycle, and therefore the endorsements are for the last block of the previous cycle, and when the delegate does not have an active stake at the current cycle; in this case its participation is simply ignored. )

    • The assertion ensures the invariant in the comment
    • Again we need to show that the invariant in the comment holds, which should not be trivial.

entrypoint_repr.ml​

  • ⛔ Marks unreachable code

  • Pre_entrypoint.of_non_empty_string @@ Non_empty_string.of_string_exn "default" is guaranteed to not return None, "default" is statically known to not be empty.

  • We need to show that the assertion is unreachable from for literal string "default" argument, this may be trivial if we have all the definitions regarding this expression.

  • | None -> assert false 🔗

gas_input_size.ml​

  • ⛔ Marks unreachable code

  • To show that the assertion is unreachable we need Alpha_context.Script_int.to_int (Script_set.size set) succeedes for all set : 'a Script_typed_ir.set.

  • match res with None -> assert false | Some x -> x 🔗

    • The value is coming from Boxed_set.size which is an int so this
  • match res with None -> assert false | Some x -> x 🔗

level_repr.ml​

  • ⛔ Marks unreachable code

    • These assertions are unreachable assuming that the preconditions on the .mli file comment holds:

      (** Preconditions on the input list of cycle eras:

      • the list is not empty
      • the first levels and the first cycles are decreasing, meaning that the first era in the list is the current era, and the last era in the list is the oldest era Invariants:
      • the first era therefore contains the same constants as in Constants
      • the first level of an era is the first level of a cycle *)
  • We need to show that, assuming the above preconditions the assertions are unreachable.

  • 🕰 Ensures invariants

  • We need to show that level_position_in_era is always positive and then prove that this assertion holds.

    • assert (Compare.Int32.(level_position_in_era >= 0l)) ; 🔗
      • The level_position_in_era is used twice after this as first operand of div and rem, this assertion ensures that these operations will not return negative values.

level_storage.ml​

  • ⛔ Marks unreachable code

  • We need to assume that this function is never called for the genesis and then prove that the assertion is unreachable.

  • | None -> assert false (* We never validate the Genesis... *) 🔗

    • This is in previous operation, which is defined in terms of current, current will only return 0 level for the genesis and from the comment at the same line of the assert We never validate the Genesis.
  • | None -> assert false 🔗

    • For the same reason as the above

liquidity_baking_cpmm.ml​

  • ⛔ Marks unreachable code

  • To show that this assertion is unreachable we need to show that script_opt never returns None. This should be possible because it is being it depends on a string literal. With all the definitions in place, this should be trivially provable.

  • Option.value_f ~default:(fun () -> assert false) script_opt 🔗

    • script_bytes (in the same file) is guaranteed to be Some _ because it is constructed from the string literal script_hex, so that this assertion marks unreachable code.

liquidity_baking_lqt.ml​

  • ⛔ Marks unreachable code.

  • The same reasons as the previous file

  • Option.value_f ~default:(fun () -> assert false) script_opt 🔗

merkle_list.ml​

  • assert false 🔗
    • From the comment in the code

      (* Impossible by construction of the tree and of the key.

      • See [tree] invariants and [to_bin]. *)
  • assert false 🔗
    • The same as above

parameters_repr.ml​

  • 🕰 Ensure invariants (inside encoding)

  • This assertion would be removable if instead of checking that the hash is equal we encode only the public key and calculate the hash after decoding.

  • To show that this assertion holds we need to assume that the decoded value is the same that was encoded, then we should be able to recover the hash computation from the encoding and prove the equality of the hashes.

  • assert (Signature.Public_key_hash.equal (Signature.Public_key.hash public_key) public_key_hash) ; 🔗

    • This inside bootstrap_account_encoding, in a case. It ensures that the public_key_hash being encoded pertains to the public_key argument. we can encode only the public_key and compute the hash during encoding/decoding, but this has performance impact. Another way is to use an abstract type that can only be constructed from the public_key (computing the hash inside the smart constructor) then the instance of such type is a proof that the hash pertains to the public key, we'll need projections though.

raw_context.ml​

  • assert (Round_repr.equal round round') ; 🔗

    • From the comment in the code

      ( If the rounds are different, an error should have already been raised. )

    • 🕰 Enforces an invariant. This is not true locally though, it depends on the round argument and preconditions. Also, I didn't found from where this invariant is coming from.
    • It would be hard to prove this, depending on where the invariant is coming from, we can only show that it is valid in some contexts.
  • assert ( 🔗

    • 🕰 Enforce invariants
    • This function check_cycle_era ensures that blocks per cycle and blocks per commitment for the current era are equal to the values of the contants. The function is the assertion itself. Also, this function is not being called anywhere in the protocol here is the search
  • assert ( 🔗

    • Same as above.

raw_level_repr.ml​

  • 👮 Ensure valid arguments

  • We can't show that it holds in general, only for some callers.

  • It may be replaced by an opaque type that is known to be positive, but this does not solve the problem it just transports it to another module.

  • assert (Compare.Int.(i >= 0)) ; 🔗

  • assert (Compare.Int.(i >= 0)) ; 🔗

receipt_repr.ml​

  • ⛔ Marks unreachable code

    • This is unreachable because there is an if checking for the conditions first.
  • It should be provable to be true without a need for preconditions since the precondition is in the function body itself.

  • | None -> assert false (* [of_mutez z] is [None] iff [z < 0] *) 🔗

  • | None -> assert false (* same *) ) 🔗

sampler.ml​

  • 🕰 Ensure invariants

  • We need to find, state the preconditions and show that j is always positive.

  • assert (Compare.Int.(j >= 0)) ; 🔗

    • Comment in sampler.mli

      (* Efficient sampling from given finitely supported (nonzero, positive) measures using the alias method. Measures need not be normalized on input, but sampling proceeds from the normalized probability measure associated to the given measure. )

sapling_repr.ml​

  • 🕰 Ensure invariants (inside encoding)

  • As in parameters_repr.ml this ensure invariants inside encodings. We need to assume that the encoded value is the same as decoded, and then we can recover the encoded memo_size and prove the equality.

  • assert (Compare.Int.(Sapling.Ciphertext.get_memo_size ct = memo_size)) 🔗

    • This looks like a sanity check. The assertion is inside a encoding conversion, it ensures that the memo_size is the same as for all the list.

sapling_storage.ml​

  • 🕰 Ensure invariants, the invariants can be found at the beginning of the Commitments module 🔗

  • To verify this the best is to formulate the invariants of this module and prove that they hold in the operations. This will also prove that the assertions hold.

  • This is the assert_node definition:

    assert (let first_of_height = pow2 (max_height - height) in 
    let first_of_next_height = Int64.shift_left first_of_height 1 in
    Compare.Int64.(node >= first_of_height && node < first_of_next_height))

    🔗

  • assert (Compare.Int.(height >= 0 && height <= max_height)) 🔗

  • assert (Compare.Int64.(pos >= 0L && pos <= pow2 height)) 🔗

  • assert (Compare.Int.(l <= 1000)) ; 🔗

  • assert (Compare.Int64.(n' <= max_size)) ; 🔗

  • assert (Compare.Int.(List.compare_length_with nfs 1000 <= 0)) ; 🔗

  • assert ( 🔗

sapling_validator.ml​

  • 🕰 Ensure valid arguments

  • From a comment in the code :

    To avoid overflowing the balance, the number of inputs and outputs must be bounded.

  • To verify this we need to use the assertions as preconditions and prove that the function is correct.

  • assert (Compare.Int.(List.compare_length_with transaction.inputs 5208 <= 0)) ; 🔗

  • assert (Compare.Int.(List.compare_length_with transaction.outputs 2019 <= 0)) ; 🔗

saturation_repr.ml​

  • ⛔ Marks unreachable code

  • This is an internal function so that it's called only with known values, to show that the assertion is unreachable we need to show that this function is valid for the z and n values in the same module.

  • (* since the encoding is applied to values of type [t]. *) assert false 🔗

sc_rollup_arith.ml​

  • ⛔ Marks unreachable code

  • To verify this code to assume the invariants and then prove that the assertions are unreachable. There are invariants for the dequeue hash computation and int parsing.

  • | None -> (* By invariants of the Deque. *) assert false 🔗

  • | None -> (* By invariants of deque *) assert false 🔗

  • | _ -> (* Hash computation always succeeds. *) assert false 🔗

  • | None -> (* By validity of int parsing. *) assert false 🔗

sc_rollup_game.ml​

  • 🕰 Ensure invariants

  • This is in resolve_conflict and ensure that it is only called after conflic_game. These functions are internal, they are called by play_game and resolve_conflic is called after conflict_game so this assertion never fails w.r.t play_game function.

  • To show that this assertion holds we need to verify the correctness of the play_game function.

  • assert (conflict_found game) ; 🔗

sc_rollup_storage.ml​

  • 🕰 Ensure invariants

  • For each case we need to show that given the invariants the assertion holds. This involves I/O so it's not trivial to prove.

  • assert (Compare.Int.(size <= 0)) ; 🔗

    • Ensures that the amount of bytes written is the same as or less than the size of the previous value. size here is coming from Storage.Sc_rollup.Inbox_update, which is a Non_iterable_carbonated_indexed_data_storage which updates docs say:

      Updates the content of a bucket ; returns A {!Storage_Error Missing_key} if the value does not exists. Consumes serialization cost. Consumes [Gas_repr.write_bytes_cost size of the new value]. Returns the difference from the old to the new size. val update : context -> key -> value -> (Raw_context.t * int) tzresult Lwt.t

  • assert (Compare.Int.(size_diff = 0)) ; 🔗

    • As the above, but compares for equality instead of <=. Ensures that the amount of bytes written are the same as the previous write.
  • assert (Compare.Int.(size_diff = 0 || size_diff = expected_size_diff)) ; 🔗

    • Ensure that sane amount of bytes were written to the storage, from the comment in the code

      ( First submission adds [sc_rollup_commitment_storage_size_in_bytes] to storage. Later submission adds 0 due to content-addressing. )

  • assert (Compare.Int.(lcc_size_diff = 0)) ; 🔗

    • Same case, ensure that amount o bytes were written to the storage.
  • assert (Raw_level_repr.(info.inbox_level = inbox_level)) ; 🔗

    • Inbox level has some invariants that need to hold, ensure the invariants. In another place in the code is possible to see the invariants of the inbox.

      (* We want to check the following inequalities on [commitment.inbox_level], [commitment.predecessor.inbox_level] and the constant [sc_rollup_commitment_frequency].

      • Greater-than-or-equal (>=), to ensure inbox_levels are monotonically increasing. along each branch of commitments. Together with [assert_commitment_not_too_far_ahead] this is sufficient to limit the depth of the commitment tree, which is also the number commitments stored per staker. This constraint must be enforced at submission time.

      • Equality (=), so that that L2 blocks are produced at a regular rate. This ensures that there is only ever one branch of correct commitments, simplifying refutation logic. This could also be enforced at refutation time rather than submission time, but doing it here works too.

        Because [a >= b && a = b] is equivalent to [a = b], we can the latter as an optimization. *)

  • assert (Raw_level_repr.(commit1_info.inbox_level = commit2_info.inbox_level)) 🔗

    • The same as above, ensure the inbox level invariants

script_interpreter.ml​

  • ⛔ Marks unreachable code.

  • We need to show that given the invariants the assertions are not reached.

  • | _ -> assert false) 🔗

    ( Cannot overflow )

  • | _ -> assert false) 🔗

  • | None -> assert false (* Cannot overflow *) 🔗

  • | None -> assert false (* Cannot overflow *) 🔗

script_interpreter_defs.ml​

  • ⛔ Marks unreachable code

  • From a comment in the code

    ( TODO: https://gitlab.com/tezos/tezos/-/issues/2455 Refute this branch thanks to the type system. Thanks to the implementation of the [CONTRACT] instruction, this branch is unreachable. But this is not enforced by the type system, which means we are one refactoring away to reach it. )

  • We need to show code is unreachable given the interpreter invariants, it should not be trivial though.

  • As the comment and issue at the link says, the interpreter makes heavy use of GADTs so it may be possible to remove this by using GADTs.

  • assert false) 🔗

script_ir_translator.ml​

  • 👮 Validate input arguments

  • We need to show that parse_uint is valid given valid arguments where valid arguments are coming from the assertions at the beginning of the function.

  • assert (Compare.Int.(nb_bits >= 0 && nb_bits <= 30)) ; 🔗

  • ⛔ Marks unreachable code
  • From a comment in the code

    ( operations cannot appear in parameters or storage, the protocol should never parse the bytes of an operation )

  • It seems hard to verify this assumption, we can verify the function assuming these invariants and check that the assertion is never reached.

script_typed_ir_size.ml​

  • ⛔ Marks unreachable code

  • From a comment in the code

    ( Operations are neither storable nor pushable, so they can appear neither in the storage nor in the script. Hence they cannot appear in the cache and we never need to measure their size. )

  • Another case where unreachable code depends on the invariants on other modules in this case touching the cache and the storage system, it would be hard if possible to verify that these invariants hold.

  • | Operation_t -> assert false 🔗

seed_storage.ml​

  • ⛔ Marks unreachable code, as long as compute_for_cycle is not applied to the first cycle (in this case the assertion will fail)
  • This is an internal function called by cycle_end here is the relevant code snippet where it is used
    let inited_seed_cycle = Cycle_repr.add last_cycle (preserved + 1) in
    compute_for_cycle ctxt ~revealed inited_seed_cycle
  • We need to show that given inited_seed_cycle, compute_for_cycle is valid. The preserved value above is a constant so this should be easy to verify.
  • | None -> assert false (* should not happen *) 🔗

skip_list_repr.ml​

  • Here we have validation of input arguments and unreachable code, to verify this we need to show that given valid inputs the assertion is unreachable.

  • let () = assert (Compare.Int.(Parameters.basis >= 2)) 🔗

    • 👮 Ensure valid input arguments. A skip list with basis 1 is useless, and 0 or less is non-sense.
  • | None -> (* By [cell] invariants. *) assert false) 🔗

    • ⛔ Marks unreachable code
  • | None -> (* By precondition and invariants of cells. *) assert false [🔗](https://gitlab.com/tezos/tezos/-/blob/b9b6f296c32a3364b64992fe41f4454d1493 6dfd/src/proto_alpha/lib_protocol/skip_list_repr.ml#L168)

    • ⛔ Marks unreachable code

storage.ml​

  • 👮 Ensure valid input arguments

  • To verify we need to show that given valid input arguments the function path_lenght is valid.

  • assert (Compare.Int.(l1 = l2 && l2 = l3)) ; 🔗

storage_functors.ml​

  • ⛔ Marks unreachable code.

  • C.Tree.kind tree = `Value implies that I.of_path file is not None. The relation of file and tree here is that file is a key in the storage and tree is the value associated with that key. This is happening inside a fold of an indexed storage.

  • This is relying on the key and tree relation it would be hard to show that this relattionship exists in general, and once assuming it we are assuming the assertion condition, so not easy to prove it.

  • match I.of_path file with None -> assert false | Some p -> f p acc) 🔗

  • | None -> assert false 🔗 🔗

  • | None -> assert false 🔗

  • | _ -> assert false) 🔗

  • | None -> assert false 🔗

  • | None -> assert false 🔗

tx_rollup_state_repr.ml​

  • 👮 Ensure valid input arguments

  • As the other cases we need to use this predicate as validity of input arguments and show the correctness of the function.

  • assert (Tx_rollup_level_repr.(oldest <= newest)) ; 🔗

Conclusion​

The assertions are almost always related to some invariants.

  • By validating input arguments so that inner code can trust on invariants implicated by this validation.
  • Or by doubting some invariant and then using assert to ensure that it still holds. In this case, if the invariant stops holding the code will fail in the assertion instead of propagating the problem.
  • Or by trusting on some invariant and using assert false to mark unreachable code.
  • When something is validated and then does not need to be validated again so that assert false is used to mark unreachable code.

So it's all about invariants, some of them are easy to spot and locally provable, like the Cycle_repr.namespace, which is an opaque type holding a string with no @ inside. Others, cross subsystem boundaries like the Operation_t case in script_typed_ir_size.ml where operations are not storable nor pushable.

Particularly Storage subsystem is a big source of invariants that are hard to verify because they involve I/O and the complexity of the storage itself. We can assume, for example, that no cycle read from the storage system is negative, but it's hard to prove it, while showing that no Saturation_repr.t is negative is much easier.

Another source of invariants is the injection and projections in data encoding. It occurs in some places where the logic used in the injection is asserted in the projection. It's still much simpler than the proofs involving the storage subsystem, and for such cases there is the conv_with_guard function that propagates the error so that no assertion is needed.

It is hard to completely avoid these assertions. GADTs may help but they add undesirable complexity that sometimes does not pay off. Having local invariants guarded by some opaque type and the smart constructor is better than having global invariants so a solution would be to try to encapsulate these invariants behind an opaque type incrementally but this also is not always simple to do because some invariants span across multiple modules.