🍬 CPS.v

Gitlab

Require Michocoq.syntax_type.
Require Michocoq.syntax.

Require TezosOfOCaml.Proto_alpha.Script_typed_ir.

Convert from a [memo_size] to a [Memo_size.t].

Definition convert_memo_size : syntax_type.memo_size →
  Alpha_context.Sapling.Memo_size.t :=
  BinInt.Z.of_nat.

Convert from a [simple_comparable_type] to a [ty].

Definition ty_of_micho_simple_comparable_ty
  (t : syntax_type.simple_comparable_type) : Script_typed_ir.ty :=
  match t with
  | syntax_type.never ⇒ Script_typed_ir.Never_t
  | syntax_type.string ⇒ Script_typed_ir.String_t
  | syntax_type.nat ⇒ Script_typed_ir.Nat_t
  | syntax_type.int ⇒ Script_typed_ir.Int_t
  | syntax_type.bytes ⇒ Script_typed_ir.Bytes_t
  | syntax_type.bool ⇒ Script_typed_ir.Bool_t
  | syntax_type.mutez ⇒ Script_typed_ir.Mutez_t
  | syntax_type.address ⇒ Script_typed_ir.Address_t
  | syntax_type.key_hash ⇒ Script_typed_ir.Key_hash_t
  | syntax_type.timestamp ⇒ Script_typed_ir.Timestamp_t
  | syntax_type.key ⇒ Script_typed_ir.Key_t
  | syntax_type.unit ⇒ Script_typed_ir.Unit_t
  | syntax_type.signature ⇒ Script_typed_ir.Signature_t
  | syntax_type.chain_id ⇒ Script_typed_ir.Chain_id_t
  end.

(* TODO: figure these out *)
Axiom unused_metadata : Script_typed_ir.ty_metadata.
Axiom dand : Dependent_bool.dand.
Axiom dbool : Dependent_bool.dbool.

Convert from a [comparable_type] to a [ty].

Fixpoint ty_of_micho_comparable_ty (t : syntax_type.comparable_type)
  : Script_typed_ir.ty :=
  match t with
  | syntax_type.Comparable_type_simple a ⇒
      ty_of_micho_simple_comparable_ty a
  | syntax_type.Cpair a b ⇒
      Script_typed_ir.Pair_t
        (ty_of_micho_comparable_ty a)
        (ty_of_micho_comparable_ty b)
        unused_metadata dand
  | syntax_type.Coption a ⇒
      Script_typed_ir.Option_t
        (ty_of_micho_comparable_ty a)
        unused_metadata dbool
  | syntax_type.Cor a b ⇒
      Script_typed_ir.Union_t
        (ty_of_micho_comparable_ty a)
        (ty_of_micho_comparable_ty b)
        unused_metadata dand
  end.

Convert from a [type] to a [ty].

Fixpoint ty_of_micho_ty (t : syntax_type.type) : Script_typed_ir.ty :=
  match t with
  | syntax_type.Comparable_type s ⇒
      ty_of_micho_simple_comparable_ty s
  | syntax_type.option a ⇒
      Script_typed_ir.Option_t (ty_of_micho_ty a) unused_metadata dbool
  | syntax_type.list a ⇒
      Script_typed_ir.List_t (ty_of_micho_ty a) unused_metadata
  | syntax_type.set a ⇒
      Script_typed_ir.Set_t (ty_of_micho_comparable_ty a) unused_metadata
  | syntax_type.contract a ⇒
      Script_typed_ir.Contract_t (ty_of_micho_ty a) unused_metadata
  | syntax_type.operation ⇒
      Script_typed_ir.Operation_t
  | syntax_type.pair a b ⇒
      Script_typed_ir.Pair_t (ty_of_micho_ty a) (ty_of_micho_ty b)
        unused_metadata dand
  | syntax_type.or a b ⇒
      Script_typed_ir.Union_t (ty_of_micho_ty a) (ty_of_micho_ty b)
        unused_metadata dand
  | syntax_type.lambda a b ⇒
      Script_typed_ir.Lambda_t (ty_of_micho_ty a) (ty_of_micho_ty b)
        unused_metadata
  | syntax_type.map k v ⇒
      Script_typed_ir.Map_t (ty_of_micho_comparable_ty k) (ty_of_micho_ty v)
        unused_metadata
  | syntax_type.big_map k v ⇒
      Script_typed_ir.Big_map_t (ty_of_micho_comparable_ty k)
        (ty_of_micho_ty v) unused_metadata
  | syntax_type.ticket a ⇒
      Script_typed_ir.Ticket_t (ty_of_micho_comparable_ty a) unused_metadata
  | syntax_type.sapling_state ms ⇒
      Script_typed_ir.Sapling_state_t (convert_memo_size ms)
  | syntax_type.sapling_transaction ms ⇒
      Script_typed_ir.Sapling_transaction_t (convert_memo_size ms)
  | syntax_type.bls12_381_fr ⇒ Script_typed_ir.Bls12_381_fr_t
  | syntax_type.bls12_381_g1 ⇒ Script_typed_ir.Bls12_381_g1_t
  | syntax_type.bls12_381_g2 ⇒ Script_typed_ir.Bls12_381_g2_t
  end.

(* TODO: remove upon completion of all definitions. *)
Axiom todo : ∀ {X}, X.

[instr_seq S T] is the type of sequences of Michelson instructions which take a stack of shape [S] and return a stack of shape [T].

Inductive instr_seq : ∀ (S T : list syntax_type.type), Set :=
  | nil_seq {S} :
      instr_seq S S
  | failwith {a} {S T} :
      instr_seq (a :: S) T
  | never {S T} :
      instr_seq (syntax_type.comparable_type_to_type
        (syntax_type.Comparable_type_simple
         syntax_type.never) :: S) T
  | if_ {S1 S2 S T U} {a} :
      syntax.if_family S1 S2 a →
      instr_seq (S1 ++ S) T →
      instr_seq (S2 ++ S) T →
      instr_seq T U →
      instr_seq (a :: S) U
  | loop_ {S1 S2 S T} {a} :
      syntax.loop_family S1 S2 a →
      instr_seq (S1 ++ S) (a :: S) →
      instr_seq (S2 ++ S) T →
      instr_seq (a :: S) T
  | push {S T} {a} :
      syntax.concrete_data a →
      instr_seq (a :: S) T →
      instr_seq S T
  | lambda {S T} {a b} :
      instr_seq (a :: nil) (b :: nil) →
      instr_seq (syntax_type.lambda a b :: S) T →
      instr_seq S T
  | iter {S T} {collection} :
      ∀ (i : syntax.iter_struct collection),
      instr_seq (@syntax.iter_elt_type _ i :: S) S →
      instr_seq S T →
      instr_seq (collection :: S) T
  | map {S T} {collection b} :
      ∀ (i : syntax.map_struct collection b),
      instr_seq (@syntax.map_in_type _ _ i :: S) (b :: S) →
      instr_seq (@syntax.map_out_collection_type _ _ i :: S) T →
      instr_seq (collection :: S) T
  | create_contract {S T} {g operation} {p} :
      instr_seq
        (syntax_type.pair (entrypoints.entrypoint_tree_to_type p) g :: nil)
        (syntax_type.pair (syntax_type.list operation) g :: nil) →
      instr_seq (syntax_type.operation ::
        syntax_type.comparable_type_to_type
          (syntax_type.Comparable_type_simple syntax_type.address) :: S) T →
      instr_seq (syntax_type.option (syntax_type.comparable_type_to_type
        (syntax_type.Comparable_type_simple
         syntax_type.key_hash)) ::
      (syntax_type.comparable_type_to_type
        (syntax_type.Comparable_type_simple
         syntax_type.mutez)) :: g :: S) T
  | self {S T} {self_type self_annot} :
      ∀ (annot_opt : syntax_type.annot_o)
             (H : base.Is_true (base.isSome
               (entrypoints.get_entrypoint_opt annot_opt
                self_type self_annot))),
      instr_seq
          (syntax_type.contract
            (syntax.get_opt
              (entrypoints.get_entrypoint_opt annot_opt self_type self_annot) H)
          :: S) T →
      instr_seq S T
  | exec {S T} {a b} :
      instr_seq (b :: S) T →
      instr_seq (a :: syntax_type.lambda a b :: S) T
  | dip {R S T U} {n} :
      length R = n →
      instr_seq S T →
      instr_seq (R ++ T) U →
      instr_seq (R ++ S) U
  | opcode {self_type} {S T U} :
      @syntax.opcode self_type S T →
      instr_seq T U →
      instr_seq S U.

Concatenation of two [instr_seq]'s.

Fixpoint sequence {S T U} (is : instr_seq S T) :
  instr_seq T U → instr_seq S U :=
  match is with
  | nil_seq ⇒ fun is' ⇒ is'
  | failwith ⇒ fun _ ⇒ failwith
  | never ⇒ fun _ ⇒ never
  | if_ if_fam is1 is2 is3 ⇒ fun is' ⇒
      if_ if_fam is1 is2 (sequence is3 is')
  | loop_ loop_fam is1 is2 ⇒ fun is' ⇒
      loop_ loop_fam is1 (sequence is2 is')
  | push d is ⇒ fun is' ⇒ push d (sequence is is')
  | lambda is1 is2 ⇒ fun is' ⇒ lambda is1 (sequence is2 is')
  | iter i is1 is2 ⇒ fun is' ⇒ iter i is1 (sequence is2 is')
  | map i is1 is2 ⇒ fun is' ⇒ map i is1 (sequence is2 is')
  | create_contract is1 is2 ⇒ fun is' ⇒ create_contract is1 (sequence is2 is')
  | self annot_opt pf is ⇒ fun is' ⇒ self annot_opt pf (sequence is is')
  | exec is ⇒ fun is' ⇒ exec (sequence is is')
  | dip pf is1 is2 ⇒ fun is' ⇒ dip pf is1 (sequence is2 is')
  | opcode o is ⇒ fun is' ⇒ opcode o (sequence is is')
  end.

Translates a Mi-Cho-Coq [instruction] into an equivalently shaped [instr_seq].

Fixpoint translate_instruction {self_type} {b} {S T}
  (i : syntax.instruction self_type b S T) {struct i} :
  instr_seq S T :=
  match i with
  | syntax.Instruction_seq is ⇒
      translate_instruction_seq is
  | syntax.FAILWITH _ ⇒ failwith
  | syntax.NEVER ⇒ never
  | syntax.IF_ if_fam is1 is2 ⇒
      if_ if_fam (translate_instruction_seq is1) (translate_instruction_seq is2) nil_seq
  | syntax.LOOP_ loop_fam is ⇒
      loop_ loop_fam (translate_instruction_seq is) nil_seq
  | syntax.PUSH a d ⇒ push d nil_seq
  | syntax.LAMBDA _ _ is ⇒ lambda (translate_instruction_seq is) nil_seq
  | syntax.ITER is ⇒ iter _ (translate_instruction_seq is) nil_seq
  | syntax.MAP is ⇒ map _ (translate_instruction_seq is) nil_seq
  | syntax.CREATE_CONTRACT _ _ _ _ _ is ⇒
      create_contract (translate_instruction_seq is) nil_seq
  | syntax.SELF annot_opt pf ⇒ self annot_opt pf nil_seq
  | syntax.EXEC ⇒ exec nil_seq
  | syntax.DIP n pf is ⇒ dip pf (translate_instruction_seq is) nil_seq
  | syntax.Instruction_opcode o ⇒ opcode o nil_seq
  end

  with translate_instruction_seq {self_type} {b} {S T}
    (is : syntax.instruction_seq self_type b S T) {struct is} :
    instr_seq S T :=
    match is with
    | syntax.NOOP ⇒ nil_seq
    | syntax.Tail_fail i ⇒ translate_instruction i
    | syntax.SEQ i is ⇒ sequence
        (translate_instruction i)
        (translate_instruction_seq is)
    end.

An irrelevant [location] needed to produce terms of type [Script_typed_ir.kinstr]

Axiom unused_loc : Alpha_context.Script.location.

Translates an [opcode] into a unary [kinstr] function.

Definition translate_opcode {self_type} {S T}
  (o : @syntax.opcode self_type S T) :
  Script_typed_ir.kinstr →
  Script_typed_ir.kinstr :=
  match o with
  | @syntax.APPLY _ a _ _ _ _ ⇒
      Script_typed_ir.IApply unused_loc (ty_of_micho_ty a)
  | syntax.DUP _ ⇒
      Script_typed_ir.IDup unused_loc
  | syntax.SWAP ⇒
      Script_typed_ir.ISwap unused_loc
  (* etc. *)
  | _ ⇒ todo
  end.

Translates an [if_family] into a ternary [kinstr] function.

Definition translate_if_family {S T} {a}
  (if_fam : syntax.if_family S T a) :
  Script_typed_ir.kinstr →
  Script_typed_ir.kinstr →
  Script_typed_ir.kinstr →
  Script_typed_ir.kinstr :=
  match if_fam with
  | syntax.IF_bool ⇒ fun i1 i2 i3 ⇒
      Script_typed_ir.IIf
        {|
          Script_typed_ir.kinstr.IIf.loc := unused_loc;
          Script_typed_ir.kinstr.IIf.branch_if_true := i1;
          Script_typed_ir.kinstr.IIf.branch_if_false := i2;
          Script_typed_ir.kinstr.IIf.k := i3
        |}
  | syntax.IF_or _ _ ⇒ fun i1 i2 i3 ⇒
      Script_typed_ir.IIf_left
        {|
          Script_typed_ir.kinstr.IIf_left.loc := unused_loc;
          Script_typed_ir.kinstr.IIf_left.branch_if_left := i1;
          Script_typed_ir.kinstr.IIf_left.branch_if_right := i2;
          Script_typed_ir.kinstr.IIf_left.k := i3
        |}
  | syntax.IF_option _ ⇒ fun i1 i2 i3 ⇒
      Script_typed_ir.IIf_none
        {|
          Script_typed_ir.kinstr.IIf_none.loc := unused_loc;
          Script_typed_ir.kinstr.IIf_none.branch_if_none := i1;
          Script_typed_ir.kinstr.IIf_none.branch_if_some := i2;
          Script_typed_ir.kinstr.IIf_none.k := i3
        |}
  | syntax.IF_list _ ⇒ fun i1 i2 i3 ⇒
      Script_typed_ir.IIf_cons
        {|
          Script_typed_ir.kinstr.IIf_cons.loc := unused_loc;
          Script_typed_ir.kinstr.IIf_cons.branch_if_cons := i1;
          Script_typed_ir.kinstr.IIf_cons.branch_if_nil := i2;
          Script_typed_ir.kinstr.IIf_cons.k := i3
        |}
  end.

Translates an [if_family] into a ternary [kinstr] function.

Definition translate_loop_family {S T} {a}
  (loop_fam : syntax.loop_family S T a) :
  Script_typed_ir.kinstr →
  Script_typed_ir.kinstr →
  Script_typed_ir.kinstr :=
  match loop_fam with
  | syntax.LOOP_bool ⇒ Script_typed_ir.ILoop unused_loc
  | syntax.LOOP_or _ _ ⇒ Script_typed_ir.ILoop_left unused_loc
  end.

Translates an [instr_seq] to a [kinstr]

Fixpoint translate_instr_seq {S T}
  (is : instr_seq S T) : Script_typed_ir.kinstr :=
  match is with
  | nil_seq ⇒ Script_typed_ir.IHalt unused_loc
  | opcode o is ⇒ translate_opcode o (translate_instr_seq is)
  | @failwith a _ _ ⇒ Script_typed_ir.IFailwith unused_loc (ty_of_micho_ty a)
  | never ⇒ Script_typed_ir.INever unused_loc
  | if_ if_fam is1 is2 is3 ⇒ translate_if_family if_fam
      (translate_instr_seq is1)
      (translate_instr_seq is2)
      (translate_instr_seq is3)
  | loop_ loop_fam is1 is2 ⇒ translate_loop_family loop_fam
      (translate_instr_seq is1)
      (translate_instr_seq is2)
  | @push _ _ a d is ⇒ Script_typed_ir.IConst unused_loc (ty_of_micho_ty a) d (* TODO: figure out how to convert the data [d] *)
      (translate_instr_seq is)
  | _ ⇒ todo
  end.