Introduction

This tutorial will show how to write a very simple auction smart contract in Coqueligot, then write a formal specification for some of the behaviour of that contract.

Finally, this tutorial will explain the proof techniques used to ensure that the contract meets the specification for any possible sequence of on-chain calls to that contract.

The contract

As a first step, we will write a very simple auction smart contract. The principe of this contract is that :

1. At first, there is an available item for sale.
2. People can place a bid on the item, each one bidding higher than the previous one.
3. At the end, the highest bidder can claim their item.

This means that the smart contract can be in 3 possible states (the state will be in the smart contract storage)

Available

The item is available but there have been no bids so far;

CurrentBid price

The current bid value is price;

Sold price

The object has been sold for price, no more bids can be placed.

Therefore the type of the state will be :

(* Declare enum for the storage (three states) *)
Inductive storage :=
| Available  : storage
| CurrentBid : nat -> storage
| Sold       : nat -> storage.

Users of the contract can either place a bid or claim the object, which leads to the transaction type being :

(* Declare enum for the parameter (two possible actions) *)
Inductive param :=
| Bid   : nat -> param
| Claim : param.

• Someone bids, and it's the first bid
In this case, the contracts saves the bid, whatever the price provided.
• Someone bids, and it's NOT the first bid
In that case, the contracts checks that the bid is higher than the current price. if not, then the transaction is invalid.
• Someone claims their item
The contract checks that the claimer is the highest bidder and hasn't claimed already. Otherwise, the transaction is invalid.
• In all other cases, the transaction is invalid

(* Simple auction contract *)

(* Require Coq built-ins, declare LIGO built-ins and shorthands *)
Require Import Notations.
Require Import List.
Require Import Nat.
Import ListNotations.
Notation "()" := tt.                (* tt means "null" or "Unit" in Coq *)
Parameter tez : Type.
Parameter operation : Type.             (* declare external LIGO type "operation" *)
(*
Definition operation : Type.        (* type operation = … *)
(* could substitute with an actual implementation of operation as e.g. a string of bytes. *)
exact (list nat).
Qed. (* make it opaque. *)
*)
Parameter contract : Type -> Type.
Parameter destination_account : contract unit.
Parameter transaction : forall {param : Type} (action : param) (amount : tez), contract param -> operation.
Parameter mutez : nat -> tez.

(* Declare external LIGO function "fail_in_main". Note that it should only be
   used once at the top-level of the "main" wrapper function. This is due to the
   fact that Coq does not support exceptions or partial functions, so it must be
   absolutely clear that the behaviour of failure is identical to a no-op contract.
   See the explanation below in the section about extraction. *)
Definition fail_in_main {A} (a : A) := a.

(* ********************************************* *)
(*                    Contract                   *)
(* ********************************************* *)

(* Behaviour of the contract. *)
Definition main_option (ps : param * storage) : option ((list operation) * storage) :=
  match ps with
  (* Start a bid *)
  | (Bid newAmount, Available)                 => Some ([], CurrentBid newAmount)
  (* New bid (must be higher than the existing *)
  | (Bid newAmount, CurrentBid existingAmount) =>
    if existingAmount <? newAmount then
      Some ([], CurrentBid newAmount)
    else
      None
  (* Finish the auction *)
  | (Claim,         CurrentBid existingAmount) => Some ([transaction tt (mutez 0) destination_account], Sold existingAmount)
  (* All other cases are errors. *)
  | (_,             _storage)                  => None
  end.

Definition main (ps : param * storage) : (list operation * storage) :=
  match main_option ps with
  (* On success, return the result *)
  | Some result => result
  (* On failure, return an empty list of operations and the unmodified storage *)
  | None => fail_in_main ([], let (p,s) := ps in s)
  end.

Note : Several checks are not done here, like checking if the user claiming the sale has the right permissions to do that, for example.
This contract is indeed just an example, not production-ready.
We wanted the contract to remain simple in order to focus on illustrating the potential of formally proving properties with Coqueligot.

Finally, we declare what should be the initial storage of the contract when deployed.

Definition initial_storage := Available.

(* ********************************************* *)
(*                End of Contract                *)
(* ********************************************* *)

Ltac subproof name :=
  refine ?[name]; shelve.

Ltac check_is_ctor ctor c :=
match c with
| ctor => idtac
| ?f _ => check_is_ctor ctor f
end.

Tactic Notation "when" constr(ctor) ident_list(pat) "as" ident(H) :=
intros pat;
match goal with
| |- _ = ?c -> _ => check_is_ctor ctor c
| _ => fail "wrong constructor, expected" ctor
end;
intro H.

Specification

Require Import List.
Import ListNotations.

Fixpoint filter_args {state : Type} {arg : Type} (valid : state -> arg -> bool) f (s : state) (l : list arg) :=
  match l with
  | [] => []
  | hd :: tl =>
    if valid s hd
    then
      hd :: (filter_args valid f (f s hd) tl)
    else
            (filter_args valid f (f s hd) tl)
  end.

Require Import Notations.
Require Import List.
Import ListNotations.
Require Import Nat.

Random tests vs. formal proofs

When writing a program, it is good practice to write tests. Instead of jotting down a few test cases for specific inputs, we will write a formal specification describing some aspects of the expected behaviour. That specification will indicate if a behaviour is correct, for any possible input. This is a common practice when using a test framework which randomizes the inputs: the test specification compares the input and output of the main function, and asserts that the output is correct for the given input. Instead of checking that this property holds for a random subset of possible inputs, Coqueligot allows us to check that the specification holds for all possible inputs.

The properties to prove (i.e. our specification)

The property we will try to prove is that the object is sold for an amount equal to the maximum bid, or phrased differently, that all bids are less than or equal to the sold-for amount. These two phrasings are not strictly equivalent, and we chose to include both statements in the specification. Having redundancy in the specification, with statements which look intuitively correct, is an easy way to have a more convincingly correct specification.

All bids are less than or equal to the sold-for amount.

(* The object is sold for an amount greater than or equal to any (valid) bid seen so far. *)

Definition main_get_storage (s : storage) (p : param) :=
  snd (main (p, s)).

Definition run_multiple_calls_ (s : storage) (l : list param) :=
  fold_left main_get_storage l s.

Definition run_multiple_calls (l : list param) :=
  run_multiple_calls_ initial_storage l.

Fixpoint contains_bid_ (has_bid : bool) (l : list param) (amount : nat) :=
  match l with
  | [] => False
  | Bid a :: tl => if a =? amount then True else contains_bid_ true tl amount
  | Claim :: tl => if has_bid then False else contains_bid_ has_bid tl amount
  end.

Definition contains_bid (l : list param) (amount : nat) :=
   contains_bid_ false l amount.

(* If after some operations, the object is sold for an amount,
   it will be sold for an amount >= any bid.

   In other words, the object is never sold for less than
   the amount of a (valid) bid. *)
Definition spec_bids_are_less_than_sold_for_amount :=
  forall (l : list param) (amount : nat),
    forall (Hcontains : contains_bid l amount),
      match run_multiple_calls l with
      | Sold sold_for_amount => 
          amount <= sold_for_amount
      | _ => True
      end.

The storage is equal to the max of the bids seen so far

(* The (current or final) price of the object is the max of all the (valid) bids seen so far *)

Definition valid_op (s : storage) (p : param) :=
  match (p, s) with
  | (Bid newAmount, Available)                 => true
  | (Bid newAmount, CurrentBid existingAmount) => existingAmount <? newAmount
  | (Claim,         CurrentBid existingAmount) => true
  | (_,             _storage)                  => false
  end.
Definition valid_ops := filter_args valid_op main_get_storage.
Definition valid_ops' lop := valid_ops initial_storage lop.
Fixpoint map_filter {A B} (f : A -> option B) l :=
  match l with
  | [] => []
  | hd :: tl => match f hd with
                | Some x => x :: map_filter f tl
                | None => map_filter f tl
                end
  end.
Definition get_bid (p : param) :=
  match p with
  | Bid n => Some n
  | Claim => None
  end.
Definition get_bids (l : list param) := map_filter get_bid l.
Definition aux_max := nat.
Definition Pmax (s : storage) (a : aux_max) : Prop :=
  (* Pmax: the storage is equal to the max of the bids seen so far *)
  match s with
  | Available => a = 0
  | CurrentBid n => n = a
  | Sold n => n = a
  end.

Definition spec_max :=
  forall (l : list param),
    Pmax (run_multiple_calls l) (list_max (get_bids (valid_ops' l))).

Redundancy in specification

Care should be taken, however, to ensure that the specification is strict enough, and does not allow for incorrect behaviour.
For example, "all bids are less than or equal to the sold-for amount" actually allows the object to be sold for an amount greater than any of the bids.
The follwoing sequence of states :

Available
CurrentBid 1
CurrentBid 3
CurrentBid 8

The "sold for an amount equal to the maximum bid" part of the specification, on the other hand, sets precise bounds on the sold-for price:
it should be exactly equal to the maximum of all bids, no more, no less.
In that sense, that property gives us a stronger guarantee on the correctness of the contract.

Induction on blockchain transactions

The induction principle

So far, we wrote the contract, and wrote the specification (the two properties to prove). Now we would like to prove them.

Notice that those properties reason on the contract state over a list of transactions, whereas our smart contract is a function (main) operating on one transaction.
It decides what should be state n + 1 given a state n and a transaction.

More generally, writing the contract implies a per-transaction reasoning, while writing the specification often requires an over-all-transactions reasoning.

So, the specification contains properties over transaction lists, but we would prefer to prove properties over a single transaction with the code of main, so we need a way to "reduce" proofs over a transaction list to proofs over a single transaction; we need an induction principle over blockchain transactions, and this is essentially what Coqueligot's fold_invariant_aux theorem provides.

Provide a proof that the main function of the smart contract preserves an invariant P over the state, and that it holds for the initial state, and this induction principle will provide you a proof that P holds for the state after any sequence of transactions.

Parallel with a list fold

In its core idea, this is just a fold over a list. The list_fold function takes

• l : a list of elements
• f: a function operating over the elements
• accu_init : an initial value for the accumulator

• l is our list of transactions
• f is the main function of the smart contract
• the accumulator is the state (+ some auxiliaty data)
• accu_init is the initial value of the contract storage
• the final acccumulator value is the state of the contract storage after executing the list of transaction.

1. Filters invalid transactions (provided a predicate telling when a transaction is valid or not)
2. Allows for carrying auxliary cross-transaction data to reason about in our proofs.
   It is used when we need some information to be saved over transaction calls (so we can reason about them in our proofs) but that are not part of the contract so we don't want them in the actual on-chain storage.

Signature of the lemma

Require Import List.
Import ListNotations.

Lemma fold_left_cons :
  forall (A B : Type) (f : A -> B -> A) (x : B) (l : list B) (i : A),
    fold_left f (x :: l) i = fold_left f l (f i x).
intros A B f x l i.
fold ([x] ++ l).
rewrite fold_left_app.
reflexivity.
Qed.

Definition Psnd {A B BB : Type} (P : A -> B -> Prop) a (b : BB * B) : Prop := P a (snd b).

Program Definition Psnd_rw :
  forall A B BB (P : A -> B -> Prop) a (b : BB * B),
    P a (snd b) = (Psnd P) a b := _.

Definition run_if_valid {state arg aux : Type}
                        (valid : state -> arg -> bool) f g (acc : state * aux) x :=
  if valid (fst acc) x then (f (fst acc) x, g (snd acc) x) else acc.

Lemma run_if_valid_rw :
  forall {state arg aux : Type}
         (valid : state -> arg -> bool)
         f
         g
         l
         (acc : state * aux)
         initial_value
         (initial_acc : aux)
         (Invalid_is_noop :
            forall state arg,
              valid state arg = false ->
              f state arg = state),
    fold_left g (filter_args valid f initial_value l) initial_acc
    = snd (fold_left (run_if_valid valid f g) l (initial_value, initial_acc)).
intros state arg aux valid f g l.
induction l; [ compute; auto | ].
intros acc initial_value initial_acc Invalid_is_noop.
case_eq (valid initial_value a).
- intros Hvalid.
  unfold filter_args; rewrite Hvalid; fold (filter_args valid).
  rewrite fold_left_cons.
  rewrite fold_left_cons.
  unfold run_if_valid at 2.
  unfold fst.
  unfold snd at 2.
  rewrite Hvalid.
  apply IHl; assumption.
- intros Hinvalid.
  unfold filter_args; rewrite Hinvalid; fold (filter_args valid).
  rewrite fold_left_cons.
  rewrite Invalid_is_noop; try assumption.
  unfold run_if_valid at 2.
  unfold fst.
  rewrite Hinvalid.
  apply IHl; assumption.
Qed.

Lemma fold_invariant_aux :
  forall {state         : Type}                           (* The type of the contract storage, for us its 'storage_state' *)
    {aux           : Type}                           (* The type of the auxiliaty cross-transaction data *)
    (initial_value : state)                          (* Value of the storage before the first transaction *)
    (initial_aux   : aux)                            (* Same as above for auxiliary data *)
    {arg           : Type}                           (* Type of a transaction, for us its 'param' *)
    (f             : state -> arg -> state)            (* The code of the contract's main function, 'main_option' *)
    (g             : aux -> arg -> aux)                (* Function describing what to do with aux data during a transaction *)
    (l             : list arg)                       (* The list of blockchain transactions *)
    (valid         : state -> arg -> bool)             (* The predicate saying when a transaction is valid or not *)
    (filter_valid
        := filter_args valid f initial_value)
    (P             : state -> aux -> Prop)                (* The over-all-transaction property we want to prove *)

    (Invalid_is_noop :                               (* A proof that invalid transactions lead to no change of state *)
      forall state arg,
        valid state arg = false ->
        f state arg = state)

    (Hind : forall xarg xstate xaux,                      (* A proof that P is preserved over one call to the contract *)
              P xstate xaux ->
              (*In xarg l ->*)
              valid xstate xarg = true ->
              P (f xstate xarg) (g xaux xarg))

    (H0 : P initial_value initial_aux),              (* A proof that P is true in the first place, at the start *)

    P (fold_left f               l  initial_value)   (* The return type, aka the proof that P hold all the time *)
      (fold_left g (filter_valid l) initial_aux).

intros.
unfold filter_valid.
rewrite run_if_valid_rw; try constructor; try assumption.
rewrite Psnd_rw.
set (PP := Psnd P).
generalize dependent initial_value.
generalize dependent initial_aux.
induction l as [ | hd tl Hind' ]; [compute; auto | ].
intros.
repeat rewrite fold_left_cons.
unfold run_if_valid at 2.
unfold fst.
case_eq (valid initial_value hd).
- intros Hvalid.
  unfold snd.
  apply Hind'.
  apply Hind; try constructor; try assumption; auto.
- intros Hinvalid.
  rewrite Invalid_is_noop; try assumption.
  apply Hind'; assumption.
Qed.

1. Invaid_is_noop (the main function is a no-op when a parameter is invalid)
2. Induction property : Hind : P(x, extra_context) -> P(f(x), g(extra_context)
3. Property on the initial state : H0: P(initial_x, initial_extra_context)

This lemma allows us to strengthen an invariant of the main function iterated over lists of valid parameters, to an invariant on the main function iterated over lists of any parameters.

This lemma also allows us to reason about the history of past parameters (e.g. the running maximum of the bids seen so far), by using an auxiliary value starting at initial_aux, and stepped using the function g over only the valid parameters.

These aspects of the lemma allow us to leverage local reasoning about invariants of the main function, in the "happy path" case of valid parameters, in order to obtain global properties on the iterated application of main to a list of parameters, i.e. it allows us to guarantee a property on any sequence of contract calls, using an invariant that reasons only about a single call to the main function using valid parameters only.

A proof for the specification, using our lemma

Require Import Notations.
Require Import List.
Import ListNotations.
Require Import Nat.
Require Import Coq.Arith.PeanoNat.
Require Import Lia.

Definition sold_for (s : storage) (l : list param) :=
  match run_multiple_calls_ s l with
  | Available    => 0
  | CurrentBid n => n
  | Sold       n => n
  end.



Theorem filter_valid_ops :
  forall (l : list param) (s : storage),
    run_multiple_calls_ s l =
    run_multiple_calls_ s (valid_ops s l).

intros l.
induction l as [| hd tl IHl].
- intro s.
  auto.
- intro s.
  case_eq hd.
  * intros n Hhd.
    case_eq s.
    + intro Hs.
      unfold valid_ops.
      fold valid_ops.
      unfold valid_op.
      simpl.
      apply IHl.
    + intro Hs.
      case_eq (Hs <? n).
      -- intros HH XX.
         unfold valid_ops.
         unfold filter_args; fold (filter_args valid_op).
         unfold valid_op.
         unfold main.
         unfold main_option.
         rewrite HH.
         simpl snd.
         unfold run_multiple_calls_.
         unfold fold_left.
         unfold main_get_storage.
         unfold main.
         unfold main_option.
         rewrite HH.
         simpl snd.
         apply IHl.
      -- intros HH XX.
         unfold valid_ops.
         unfold filter_args; fold (filter_args valid_op).
         unfold main.
         unfold main_option.
         unfold valid_op.
         rewrite HH.
         simpl snd.
         unfold run_multiple_calls_.
         unfold fold_left.
         unfold main_get_storage.
         unfold main.
         unfold main_option.
         rewrite HH.
         simpl snd.
         apply IHl.
    + intros n0 Hs.
      unfold valid_ops.
      fold valid_ops.
      unfold valid_op.
      simpl.
      apply IHl.
  * intros Hhd.
    unfold valid_ops.
    fold valid_ops.
    unfold valid_op.
    case_eq s.
    + intros Hs.
      apply IHl.
    + intros n Hs.
      apply IHl.
    + intros n Hs.
      apply IHl.
Qed.

Lemma filter_valid_ops_short_proof :
  forall (l : list param) (s : storage),
    run_multiple_calls_ s l =
    run_multiple_calls_ s (valid_ops s l).

intros l.
induction l as [| hd tl IHl].
- auto.
- intro s.
  case_eq hd.
  * intros n Hhd.
    case_eq s;
      intros n0;
      intros;
      try apply IHl.
      case_eq (n0 <? n);
         intros HH;
         unfold valid_ops;
         unfold filter_args;
         unfold valid_op;
         unfold run_multiple_calls_;
         unfold fold_left;
         unfold main_get_storage;
         unfold main;
         unfold main_option;
         rewrite HH;
         try rewrite HH;
         apply IHl.
  * intros.
    case_eq s;
      intros;
      apply IHl.
Qed.

Theorem filter_valid_ops' :
  forall (l : list param),
    run_multiple_calls l =
    run_multiple_calls (valid_ops' l).
intros.
unfold run_multiple_calls.
unfold valid_ops.
apply filter_valid_ops.
Qed.

Lemma first_op_is_bid'' :
  forall (l : list param),
    match (valid_ops initial_storage l) with
    | Bid n :: _ => True
    | [] => True
    | _ => False
    end.
intros l.
induction l as [| p l IHl].
- now compute.
- case_eq p.
  * intros n Hp.
    unfold initial_storage.
    unfold valid_ops.
    unfold filter_args; fold (filter_args valid_op).
    unfold valid_op.
    fold valid_op.
    auto.
  * compute.
    auto.
Qed.

Lemma first_op_is_bid_eqv :
  forall (l : list param),
    (valid_ops initial_storage l) <> [] ->
    (match (valid_ops initial_storage l) with
     | Bid n :: _ => True
     | _ => False
     end)
    = (match (valid_ops initial_storage l) with
       | Bid n :: _ => True
       | [] => True
       | _ => False
       end).
intros l nonempty.
set (filtered := valid_ops initial_storage l) in *.
case_eq filtered.
- contradiction.
- auto.
Qed.

Theorem first_op_is_bid :
  forall (l : list param),
    (valid_ops initial_storage l) <> [] ->
    match (valid_ops initial_storage l) with
     | Bid n :: _ => True
     | _ => False
     end.
intros l nonempty.
set (H := first_op_is_bid_eqv l nonempty).
rewrite H.
apply first_op_is_bid''.
Qed.

Fixpoint max_bid (s : storage) (l : list param) :=
  match l with
  | [] => s
  | Bid n :: tl =>
    match s with
    | Available => max_bid (CurrentBid n) tl
    | CurrentBid max =>
      if n <? max
      then max_bid (CurrentBid max) tl
      else max_bid (CurrentBid n) tl
    | Sold n => Sold n (* TODO: impossible with assumption valid_ops *)
    end
  | hd :: tl => max_bid s tl
  end.

Definition u_max (a : nat) (p : param) :=
  match p with
  | Bid n => max n a
  | Claim => a
  end.

(*
Compute fold_left u_max                      [ Bid 1; Bid 2; Bid 3; Claim ] 0.
Compute fold_left u_max                      [ Bid 1; Bid 2; Bid 3; Claim; Bid 4 ] 0.
Compute fold_left u_max (valid_ops Available [ Bid 1; Bid 2; Bid 3; Claim; Bid 4 ]) 0.
*)

Lemma fold_get_bids :
  forall l z,
    (fold_left max (get_bids (valid_ops' l)) z)
  = (fold_left u_max (valid_ops' l) z).
intros l.
induction (valid_ops' l) as [| a ll IHll]; [ compute; auto | ].
intros z0.
unfold get_bids.
unfold map_filter; fold (map_filter get_bid).
case_eq a.
- intros n Ha.
  unfold get_bid at 1.
  fold ([n] ++ (map_filter get_bid ll)).
  rewrite fold_left_app.
  fold (get_bids ll).
  fold ([Bid n] ++ ll).
  rewrite fold_left_app.
  replace (fold_left u_max [Bid n] z0) with (fold_left max [n] z0).
  + apply IHll.
  + apply Nat.max_comm.
- intros Ha.
  unfold get_bid at 1.
  fold ([Claim] ++ ll).
  rewrite fold_left_app.
  fold (get_bids ll).
  replace (fold_left u_max [Claim] z0) with z0.
  + apply IHll.
  + reflexivity.
Qed.

Module Type SigSubProofs.
  Axiom invalid_is_noop_on_main :
    forall storage x,
      valid_op storage x = false -> main_get_storage storage x = storage.
  
  Axiom main_preserves_invariant_max :
    forall (xarg : param)
         (xstate : storage)
         (xaux : nat)
         (Pprev : Pmax xstate xaux)
         (Hvalid : valid_op xstate xarg = true),
    Pmax (main_get_storage xstate xarg) (u_max xaux xarg).
End SigSubProofs.

Module UnitTestMax (SubProofs : SigSubProofs).

Definition invalid_is_noop_on_main := SubProofs.invalid_is_noop_on_main.
Definition main_preserves_invariant_max := SubProofs.main_preserves_invariant_max.

Print spec_max.
(* spec_max =
    forall l : list param,
      Pmax (run_multiple_calls l) (list_max (get_bids (valid_ops' l)))
    : Prop *)

Step 1 : Decomposing with the proof goal using the fold_invariant_aux lemma

Theorem unit_test_max : spec_max.
intros l.

unfold list_max.
rewrite <- fold_symmetric; cycle 1. 
- intros x y z.
  rewrite Nat.max_assoc.
  reflexivity.
- intros y.
  rewrite Nat.max_0_l.
  rewrite Nat.max_0_r.
  reflexivity.
- rewrite fold_get_bids.
  unfold valid_ops'.
  unfold valid_ops.
  unfold run_multiple_calls.
  unfold run_multiple_calls_.
  apply fold_invariant_aux.
  + intros state arg Hinvalid.
    rewrite invalid_is_noop_on_main; auto.
  + apply main_preserves_invariant_max.
  + compute; auto.
Qed.

End UnitTestMax.

Module SubProofs <: SigSubProofs.

Step 2 : Subproof that invalid transactions don't change the state

Theorem invalid_is_noop_on_main :
  forall storage x,
    valid_op storage x = false -> main_get_storage storage x = storage.

On valid cases, the precondition valid_op storage x = false evaluates to true = false and the inversion tactic is used to prove these cases by contradiction.

On invalid cases, the postcondition main_get_storage storage x = storage becomes trivial enough so it can be solved using the reflexivity tactic, after expanding some parts of the code.

intros s x Hinvalid.
unfold main_get_storage.
unfold main.
case_eq x.
- case_eq s.
  + intros Hs n Hx.
    rewrite Hs in Hinvalid.
    rewrite Hx in Hinvalid.
    unfold valid_op in Hinvalid.
    inversion Hinvalid.
  + intros n Hs n0 Hx.
    rewrite Hs in Hinvalid.
    rewrite Hx in Hinvalid.
    unfold valid_op in Hinvalid.
    case_eq (n <? n0).
    * intros Hless.
      rewrite Hless in Hinvalid.
      inversion Hinvalid.
    * intros Hmore.
      unfold main_option.
      rewrite Hmore.
      reflexivity.
  + intros n Hs n0 Hx.
    reflexivity.
- case_eq s.
  + intros Hs Hx.
    reflexivity.
  + intros n Hs Hx.
    rewrite Hs in Hinvalid.
    rewrite Hx in Hinvalid.
    unfold valid_op in Hinvalid.
    inversion Hinvalid.
  + intros n Hs Hx.
    reflexivity.
Qed.

Step 3 : Subproof that a call to the contract preserves the invariant

Lemma main_preserves_invariant_max :
  forall (xarg : param)
         (xstate : storage)
         (xaux : nat)
         (Pprev : Pmax xstate xaux)
         (Hvalid : valid_op xstate xarg = true),
    Pmax (main_get_storage xstate xarg) (u_max xaux xarg).
intros xarg xstate xaux Pprev Hvalid.
case_eq xarg.
- case_eq xstate.
  * intros Hstate n Harg.
    cut (xaux = 0).
    + intros Haux.
      unfold u_max.
      rewrite Haux.
      rewrite Nat.max_0_r.
      compute.
      auto.
    + unfold Pmax in Pprev.
      rewrite Hstate in Pprev.
      assumption.
  * intros n Hstate n0 Harg.
    rewrite Hstate in Hvalid.
    rewrite Harg in Hvalid.
    unfold valid_op in Hvalid.
    unfold Pmax in Pprev.
    rewrite Hstate in Pprev.
    unfold main_get_storage.
    unfold u_max.
    unfold main.
    unfold main_option.
    rewrite Hvalid.
    rewrite <- Pprev.
    unfold snd.
    unfold Pmax.
    rewrite Nat.max_comm.
    rewrite Nat.max_r.
    + reflexivity.
    + apply Nat.leb_le in Hvalid.
      lia.
  * intros n Hstate n0 Harg.
    rewrite Hstate in Hvalid.
    rewrite Harg in Hvalid.
    unfold valid_op in Hvalid.
    inversion Hvalid.
- case_eq xstate.
  * intros Hstate Harg.
    rewrite Hstate, Harg in Hvalid.
    unfold valid_op in Hvalid.
    inversion Hvalid.
  * intros n Hstate Harg.
    unfold main_get_storage.
    unfold u_max.
    unfold main.
    unfold main_option.
    unfold snd.
    unfold Pmax.
    rewrite Hstate in Pprev.
    unfold Pmax in Pprev.
    rewrite Pprev in *.
    reflexivity.
  * intros n Hstate Harg.
    unfold main_get_storage.
    unfold u_max.
    unfold main.
    unfold main_option.
    unfold fail_in_main.
    unfold snd.
    unfold Pmax.
    rewrite Hstate in Pprev.
    unfold Pmax in Pprev.
    rewrite Pprev in *.
    reflexivity.
Qed.

End SubProofs.
Module CompletedUnitTestMax := UnitTestMax SubProofs.
Definition unit_test_max := CompletedUnitTestMax.unit_test_max.

• Simplifying the problem down with the fold_invariant_aux lemma
• Decomposing the proofs by case analysis over the parameter and state values
• Then, for each case :
• Stepping into the goal to prove with some rewrite and unfold
• The rest depends on the actual goal, but as we saw, it can be trivial enough to be solved with reflexivity

Extraction

Require Import List.
Import ListNotations.
Require Import Nat.

(* Extract to OCaml language *)
Require Extraction.
Extraction Language OCaml.

(* LIGO built-ins *)
Extract Inlined Constant tez => "tez".
Extract Inlined Constant operation => "operation".
Extract Constant contract "'t" => "'t contract".
Extract Inlined Constant destination_account => "(Tezos.get_contract_with_error (Tezos.get_sender ()) ""oops"" : unit contract)".
Extract Inlined Constant transaction => "Tezos.transaction".
Extract Inlined Constant mutez => "(fun n -> mutez_of_nat (abs n))".

(* OCaml built-ins *)
Extract Inductive unit => unit ["()"].
(* Implement external LIGO function "fail" *)
(*Extraction Implicit fail [A a].*)
(* It is okay for some proofs to implement our identity function named "fail" with
   "failwith", even in the case where the code isn't
   "let main = function … | … -> fail | …" but e.g. is
   "let main = function … | … -> f (fail) | …".

   In the coq world, the extra f(identity(some_value)) in the chain of calls
   still needs to satisfy the proofs. This is okay for some proofs, but not e.g.
   for proofs saying that a user is always able to claim an auction after some
   time (the action of claiming an auction could go through a "fail" path, which
   would make it seem possible in Coq but wouldn't actually be possible on-chain).

   We therefore use fail_in_main only once, at the top-level, where it is obvious
   that its return value is never used by the rest of the contract.

   If the following line is removed, the resulting contract will behave exactly
   the same way, but will consume gas and perform a no-op instead of warning the
   user before performing invalid operations.
 *)
Definition ok_main (ps : param * storage) : (list operation * storage) :=
  match ps with
  (* Start a bid *)
  | (Bid newAmount, Available) => ([], CurrentBid newAmount)
  (* e.g. rest is not implemented yet *)
  | (_p,s)                     => fail_in_main ([], s)
  end.
Definition bad_f (x : list operation * storage) := (fst x, CurrentBid 42).
Definition bad_main (ps : param * storage) : (list operation * storage) :=
  match ps with
  (* Start a bid *)
  | (Bid newAmount, Available) => ([], CurrentBid newAmount)
  | (_p,s)                     => bad_f (fail_in_main ([], s))
  end.
Extract Inlined Constant fail_in_main => "(fun (_ : (operation list * storage)) : (operation list * storage) -> failwith ""Err"")".
(*Unset Extraction SafeImplicits.*)
Extract Inductive list => "list" [ "[]" "(::)" ].
Extract Inductive prod => "(*)"  [ "(,)" ].
Extract Inductive option => "option"  [ "Some" "None" ].
Extract Inductive nat => nat [ "0" "succ" ] "(fun fO fS n -> if n=0 then fO () else fS (n-1))".
Extract Inductive bool => "bool" [ "true" "false" ].
Extract Inlined Constant ltb => "(fun (a : nat) (b : nat) : bool -> a < b)".

(* Prevent access to opaque definitions. *)
Unset Extraction AccessOpaque.

Definition checkAssumptions := (main, unit_test_max).
Print Assumptions checkAssumptions.
(*
Axioms:
transaction : ∀ param : Type, param → tez → contract param → operation
operation  : Type
mutez  : nat → tez
destination_account  : contract unit
*)

(* Compile Coq code to OCaml *)
Extraction "contract.1.ocaml.ml" main.

Tooling

The build.sh script performs the following tasks:

• Extract the coq source code into OCaml code, using coqc
• Convert the OCaml code to CameLIGO code (a few minor compatibility details)
• Runs ligo compile contract to produce Michelson code

Further reading

• Software Foundations
• Certified Programming with Dependent Types>