Raphaël Cauderlier · ed4622b3 · ed4622b3 · ed4622b3 · ed4622b3
--- a/README.org
+++ b/README.org
+Definition parameter_ty := (pair (pair nat action_ty) (list_ (option_ signature))).
+
+Definition storage_ty := pair nat (pair nat (list_ key)).
+#+END_SRC
+
+We then axiomatize the protocol environment required for typing and evaluating Michelson contracts. We use a Coq [[https://coq.inria.fr/distrib/current/refman/language/gallina-extensions.html#section-mechanism][section]] and [[https://coq.inria.fr/distrib/current/refman/language/gallina-specification-language.html#coq:cmd.variable][section variables]] for this.
+
+#+BEGIN_SRC coq
+Section multisig.
+
+Variables (get_contract_type : contract_constant -> error.M type) (env : @proto_env get_contract_type parameter_ty).
+
+Definition instruction := @syntax.instruction get_contract_type parameter_ty.
+#+END_SRC
+
+Coq uses a di
--- a/README.org
+++ b/README.org
+    DROP ;; DROP ;;
+
+    DIP ( UNPAIR ;; PUSH nat (nat_constant 1%N) ;; ADD ;; PAIR ) ;;
+
+    NIL operation ;; SWAP ;;
+    IF_LEFT
+      ( UNPAIR ;; UNIT ;; TRANSFER_TOKENS ;; CONS )
+      ( IF_LEFT (SET_DELEGATE ;; CONS )
+                ( DIP ( SWAP ;; CAR ) ;; SWAP ;; PAIR ;; SWAP )) ;;
+    PAIR ).
+#+END_SRC
+
+
+** Functional Specification
+
+**
--- a/src/contracts_coq/multisig.v
+++ b/src/contracts_coq/multisig.v

+(** [pack_ty] is the type of the data that is packed before being signed. *)
+Definition pack_ty := pair address (pair nat action_ty).
+
+(** [multisig_spec] is the functional specification of the multisig
+contract. It is a relation between the inputs ([counter], [action],
+[sigs], [stored_counter], [threshold], and [keys]) and the outputs
+([new_stored_counter], [new_threshold], [new_keys], and
+[returned_operations]) of the contract.
+
+The main result is the theorem [multisig_correct] below. It states
+that, assuming enough fuel is provided to compute the contract,
+[multisig] evaluates successfully if and only if its input and outputs are related by the [multisig_spec] relation.
+
+*)

--- a/src/contracts_coq/multisig.v
+++ b/src/contracts_coq/multisig.v
-    | inr (inl kh) =>
+    | inr (inl kh_opt) =>
      new_threshold = threshold /\
      new_keys = keys /\
-      returned_operations = (set_delegate env kh :: nil)%list
+      returned_operations = (set_delegate env kh_opt :: nil)%list
    | inr (inr (nt, nks)) =>
      new_threshold = nt /\
      new_keys = nks /\
      returned_operations = nil
    end.

-Definition multisig_head (then_ : instruction (nat ::: list key ::: list (option signature) ::: bytes ::: action_ty ::: storage_ty ::: nil) (pair (list operation) storage_ty ::: nil)) :
+
+(** To ease verification, we split the multisig contracts in the 6 parts presented above. *)
+
--- a/src/contracts_coq/multisig.v
+++ b/src/contracts_coq/multisig.v
+(**
+[more_fuel] changes the proof state from
+... Hfuel : N <= fuel |- C(fuel) where N is a positive constant to
+... Hfuel : N-1 <= fuel |- C(S(fuel)).
+*)
+
+Ltac more_fuel :=
+  match goal with
+    | Hfuel : (_ <= ?fuel) |- _ =>
+      destruct fuel as [|fuel];
+      [inversion Hfuel; fail
+      | apply le_S_n in Hfuel]
+  end.
+
+(** We now prove each part of the multisig contract. *)
+
--- a/README.org
+++ b/README.org
+Definition parameter_ty := (pair (pair nat action_ty) (list_ (option_ signature))).
+
+Definition storage_ty := pair nat (pair nat (list_ key)).
+#+END_SRC
+
+We then axiomatize the protocol environment required for typing and evaluating Michelson contracts. We use a Coq [[https://coq.inria.fr/distrib/current/refman/language/gallina-extensions.html#section-mechanism][section]] and [[https://coq.inria.fr/distrib/current/refman/language/gallina-specification-language.html#coq:cmd.variable][section variables]] for this.
+
+#+BEGIN_SRC coq
+Section multisig.
+
+Variables (get_contract_type : contract_constant -> error.M type) (env : @proto_env get_contract_type parameter_ty).
+
+Definition instruction := @syntax.instruction get_contract_type parameter_ty.
+#+END_SRC
+
+Coq uses a di