After each new release of the protocol there comes a need to validate it. One of the options would be to start from scratch, but fortunately there is no need for that since many parts of the protocol are only slightly changed or stay the same. That allows us to reuse old proofs in consequent versions and speed up the validation.

Of course there is a small number of proofs which stop working due to the changes and that has to be repaired. This process can sometimes be tricky since it requires an understanding of how different functions and proofs depend on each other, but that makes it very interesting. In this post, we will show examples of broken proofs, discuss reasons for their failure, and show techniques we used to fix issues.

## Missing codeâ€‹

The easiest case is when a source file no longer contains the function or module that the proof validates. Then it suffices to remove the proofs or, if the corresponding code is now in another file, move them accordingly.

## Compare and equalityâ€‹

Often a proof fails because validated data structure has been modified. Most often it breaks validation of equality or compare function because they depend directly on the structure of a particular type. In that case failure is caused by incomplete definition of projection to the type where the equality or compare function can be expressed from already proven-correct combinators (see Verifying the compare functions of OCaml for more information). To fix the proof we have to add projections for new constructors and accordingly modify comparison used after projection.

For example `Destination_repr`

initially contained the following type:

`Inductive t : Set :=`

| Contract : Contract_repr.t -> t

| Tx_rollup : Tx_rollup_repr.t -> t.

and the proof of the validity of its compare function in the corresponding proofs file:

`Lemma compare_is_valid :`

Compare.Valid.t (fun _ => True) id Destination_repr.compare.

Proof.

apply (Compare.equality (

let proj_tx_rollup x :=

match x with

| Destination_repr.Tx_rollup x => Some x

| _ => None

end in

let proj_contract x :=

match x with

| Destination_repr.Contract x => Some x

| _ => None

end in

let proj x :=

(proj_tx_rollup x, proj_contract x) in

Compare.projection proj (

Compare.lexicographic

(Compare.Option.compare Tx_rollup_repr.compare)

(Compare.Option.compare Contract_repr.compare)

)

)); [intros [] []; cbn; hauto lq: on |].

Compare.valid_auto.

unfold id; sauto lq: on.

Qed.

but now we receive a message from the prover informing that `hauto`

failed. If we temporarily remove `hauto`

tactic we will see that some of the goals are now false, like this one:

`True -> True -> -1 = 1`

That indicates the projection and comparison used in tactic `apply`

are invalid.

Indeed, in newer version new constructor of type `t`

have been added:

`Inductive t : Set :=`

| Contract : Contract_repr.t -> t

| Tx_rollup : Tx_rollup_repr.t -> t

| Sc_rollup : Sc_rollup_repr.t -> t.

so we modify the projection getting:

`Lemma compare_is_valid :`

Compare.Valid.t (fun _ => True) id Destination_repr.compare.

Proof.

apply (Compare.equality (

let proj_sc_rollup x :=

match x with

| Destination_repr.Sc_rollup x => Some x

| _ => None

end in

let proj_tx_rollup x :=

match x with

| Destination_repr.Tx_rollup x => Some x

| _ => None

end in

let proj_contract x :=

match x with

| Destination_repr.Contract x => Some x

| _ => None

end in

let proj x :=

(proj_sc_rollup x, (proj_tx_rollup x, proj_contract x)) in

Compare.projection proj (

Compare.lexicographic

(Compare.Option.compare Sc_rollup_repr.Address.compare)

(

Compare.lexicographic

(Compare.Option.compare Tx_rollup_repr.compare)

(Compare.Option.compare Contract_repr.compare)

))

)); [intros [] []; cbn; hauto lq: on |].

Compare.valid_auto.

unfold id; sauto lq: on.

Qed.

so now the proof is fixed.

## Encodingâ€‹

Sometimes extending a data type affects more functions. One of these functions that is also often validated is encoding. Adding new constructors to a type returned by encoding causes tactic `Data_encoding.Valid.data_encoding_auto`

we use in proofs of its validity to fail to solve some intermediate goals causing the proof to break.

The reason why `Data_encoding.Valid.data_encoding_auto`

does not work properly is that it requires proofs of validity of other encoding functions our encoding depends on. These should be included in the hint database `Data_encoding_db`

. To fix the proof of encoding validity, we define and add relevant lemmas to the database.

Let us consider the following example:

`Sc_rollup_inbox`

contains a type `t : Set`

that initially was:

` Record record : Set := Build {`

rollup : Sc_rollup_repr.t;

level : Raw_level_repr.t;

nb_available_messages : int64;

message_counter : Z.t;

current_messages_hash : unit -> Context.Proof.hash;

old_levels_messages : history_proof;

}.

but it have been extended with two new constructors:

` nb_messages_in_commitment_period : int64;`

starting_level_of_current_commitment_period : Raw_level_repr.t;

so the proof of encoding validity:

`Lemma encoding_is_valid :`

Data_encoding.Valid.t Valid.t Sc_rollup_inbox_repr.encoding.

Proof.

Data_encoding.Valid.data_encoding_auto.

repeat (split; try dtauto).

destruct_all Sc_rollup_inbox_repr.t; f_equal.

now apply functional_extentionality_unit.

Qed.

no longer works because it is missing a lemma in `Data_encoding_db`

database stating that `Sc_rollup_inbox_repr.Hash.encoding`

is valid:

` Lemma encoding_is_valid :`

Data_encoding.Valid.t (fun _ => True)

Sc_rollup_inbox_repr.Hash.encoding.

In order to fix the proof we add that lemma and also add:

` starting_level_of_current_commitment_period : Raw_level_repr.Valid.t x.(starting_level_of_current_commitment_period);`

nb_available_messages : Int64.Valid.t x.(nb_available_messages);

to the record `Valid.t`

:

` Record t (x : Sc_rollup_inbox_repr.t) : Prop := {`

level : Raw_level_repr.Valid.t x.(level);

nb_available_messages : Int64.Valid.t x.(nb_available_messages);

message_counter : 0 <= x.(message_counter);

}.

because that particular proof also depends on it.

## More complicated functionsâ€‹

Sometimes it happens that in a new release simple function gets very complicated with many local functions defined using `let`

, which cannot be eliminated by applying lemmas (because you cannot create a lemma describing a local function). In that situation we create a new equivalent definition of the same function, but with its local functions defined externally. It lets us to create lemmas about these local functions, what allows us to make only little changes to the structure of the reused proof.