# Asserts

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.

- This has the form
- đ° 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.

- This has the form
- đŽ 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.

- This is the form

- â Mark unreachable code

## 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
`min`

function 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.

- Because of the property of namespaces, this
`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.

- From a comment in the code
`assert false`

đ

## 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.

- đŽ Ensure valid arguments
Comment in the code đ:

## 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.

- Comment in the code in

## 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

- The value is coming from
`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 *)

- These assertions are unreachable assuming that the preconditions on the
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.

- The

## 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*.

- This is in
`| 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]. *)

- From the comment in the code
`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.

- This inside

## 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.

- From the comment in the code
`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.*)

- Comment in

## 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.

- This looks like a sanity check. The assertion is inside a encoding conversion,
it ensures that the

## 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

- Ensures that the amount of bytes written is the same as or less
than the size of the previous value.
`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.

- As the above, but compares for equality instead of
`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.*)

- Ensure that sane amount of bytes were written to the storage,
from the comment in the code
`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. *)

- 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.
`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.

`assert false`

đ

## 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`

đ`| _ -> 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.