_CoqProject

Basic.v
Loop.v
Operation.v
Global.v
Crypto.v
Obj.v
SCaml.v
ExtrSCaml.v
Multisig.v

Basic.v

Parameter nat : Set.

Parameter int : Set.
Parameter int_plus : int -> int -> int.
Parameter int_sub : int -> int -> int.
Infix "+" := int_plus.
Infix "-" := int_sub.

Parameter nat_plus : nat -> nat -> nat.
Parameter nat_sub : nat -> nat -> nat.
Infix "+^" := nat_plus (at level 90).
Infix "-^" := nat_sub  (at level 90).

Parameter not_eq_bool : forall {A: Set}, A -> A -> bool.
Parameter lt_bool : forall {A: Set}, A -> A -> bool.
Infix "<>?" := not_eq_bool (at level 60).
Infix "<?" := lt_bool (at level 60).

Parameter tz : Set.

Inductive sum (A B: Set) := Left (a : A) | Right (b : B).
Arguments Left [A B].
Arguments Right [A B].

Parameter failwith : forall {A B:Set}, A -> B.

Parameter bytes : Set.

Parameter address : Set.

Parameter key_hash : Set.

Parameter timestamp : Set.

Parameter chain_id : Set.

Parameter env : Set.

Parameter contract_ : Set -> Set.

Parameter operation : Set.

Parameter key : Set.
Parameter signature : Set.

Crypto.v

Require Import Basic.

  Parameter check_signature : key -> signature -> bytes -> bool.
  Parameter blake2b : bytes -> bytes.
  Parameter sha256 : bytes -> bytes.
  Parameter sha512 : bytes -> bytes.
  Parameter hash_key  : key -> key_hash.

ExtrSCaml.v

Require Export ExtrOcamlBasic.
Require Import SCaml.

Extract Inlined Constant int => "SCaml.int".
Extract Inlined Constant nat => "SCaml.nat".
Extract Inlined Constant tz => "SCaml.tz".

Extract Inlined Constant int_plus => "SCaml.(+)".
Extract Inlined Constant int_sub => "SCaml.(-)".
Extract Inlined Constant nat_plus => "SCaml.(+^)".
Extract Inlined Constant nat_sub => "SCaml.(-^)".

Extract Inlined Constant not_eq_bool => "SCaml.(<>)".
Extract Inlined Constant lt_bool => "SCaml.(<)".


Extract Inlined Constant failwith => "SCaml.failwith".

Extract Inlined Constant Loop.left_fuel => "(fun _ f acc -> Some (SCaml.Loop.left f acc))".

Extract Inlined Constant bytes => "SCaml.bytes".

Extract Inlined Constant address => "SCaml.address".
Extract Inlined Constant key_hash => "SCaml.key_hash".

Extract Constant contract_ "'a" => "'a SCaml.contract".

Extract Inlined Constant operation => "SCaml.operation".
Extract Inlined Constant Operation.t => "SCaml.Operation.t".
Extract Inlined Constant Operation.transfer_tokens => "SCaml.Operation.transfer_tokens".
Extract Inlined Constant Operation.set_delegate => "SCaml.Operation.set_delegate".

Extract Inlined Constant chain_id => "SCaml.chain_id".

Extract Inlined Constant env => "unit".
Extract Inlined Constant Global.get_chain_id => "SCaml.Global.get_chain_id".
Extract Inlined Constant Global.get_sender => "SCaml.Global.get_sender".

Extract Inlined Constant key => "SCaml.key".
Extract Inlined Constant signature => "SCaml.signature".

Extract Inlined Constant Crypto.check_signature => "SCaml.Crypto.check_signature".
Extract Inlined Constant Obj.pack => "SCaml.Obj.pack".

Global.v

Require Import Basic.

  Parameter get_now      : env -> timestamp.
  Parameter get_amount   : env -> tz.
  Parameter get_balance  : env -> tz.
  Parameter get_source   : env -> address.
  Parameter get_sender   : env -> address.
  Parameter get_chain_id : env -> chain_id.
  Parameter get_steps_to_quota : env -> nat.

Loop.v

Require Import Basic.

Parameter left_fuel : forall {A B:Set},
    nat -> (A -> sum A B) -> A -> option B.

Multisig.v

Require Import SCaml ExtrSCaml.
Require Import List.
Import ListNotations.
Open Scope list_scope.

Parameter one zero: nat.
Parameter fuel : nat.

Inductive action :=
| Transfer (amount: tz) (dest: contract_ unit)
| Delegate (kh : option key_hash)
| ChangeKeys (threshold : nat) (keys : list key).

Definition check_signatures bytes sigs keys :=
  Loop.left_fuel fuel (fun '(acc, sigs, keys) =>
      match (sigs, keys) with
      | (_, nil) => Right (Some acc)
      | (nil, _ :: _) => Right None
      | (None :: sigs', _ :: keys') => Left (acc, sigs', keys')
      | (Some sig_ :: sigs', key :: keys') =>
     if Crypto.check_signature key sig_ bytes then
       Left (one +^ acc, sigs', keys')
     else
       Right None
      end
    )
  (zero, sigs, keys).

Inductive parameter :=
  Param (counter: nat) (action: action) (sigs : list (option signature)).

Inductive storage :=
  Storage (stored_counter: nat) (threshold: nat) (keys: list key).

Parameter env : env.

Definition main (param : parameter) (storage : storage) :=
  let '(Param counter action sigs) := param in
  let '(Storage stored_counter threshold keys) := storage in
  if counter <>? stored_counter then failwith counter else
    let chain_id := Global.get_chain_id env in
    let address := Global.get_sender env in
    let bytes := Obj.pack ((chain_id, address), (counter, action)) in
    match check_signatures bytes sigs keys with
    | None | Some None => failwith tt
    | Some (Some numb_of_valid_signatures) =>
       if numb_of_valid_signatures <? threshold then failwith tt else
         let new_counter := one +^ counter in
         match action with
         | Transfer amount dest =>
            let op := Operation.transfer_tokens tt amount dest in
            ([op], Storage new_counter threshold keys)
         | Delegate kh =>
            let op := Operation.set_delegate kh in
            ([op], Storage new_counter threshold keys)
         | ChangeKeys new_threshold new_keys =>
            let new_storage := Storage new_counter new_threshold new_keys in
            ([], new_storage)
         end
    end.
Extraction Language OCaml.

Extract Inlined Constant one => "(Nat 1)".
Extract Inlined Constant zero => "(Nat 0)".
Extract Inlined Constant fuel => "()".
Extract Inlined Constant env => "()".

Extraction "multisig.ml" main.

Obj.v

Require Import Basic.
  Parameter pack : forall {A: Set}, A -> bytes.
  Parameter unpack : forall {A: Set}, bytes -> option A.

Operation.v

Require Import Basic.

Definition t := operation.
Parameter transfer_tokens : forall {A : Set}, A -> tz -> contract_ A -> t.
Parameter set_delegate : option key_hash -> t.

SCaml.v

Require Export Basic.
Require Export Loop Operation Global Crypto Obj.