Skip to main content

🍬 CPS.v


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 :=

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.neverScript_typed_ir.Never_t
  | syntax_type.stringScript_typed_ir.String_t
  | syntax_type.natScript_typed_ir.Nat_t
  | syntax_type.intScript_typed_ir.Int_t
  | syntax_type.bytesScript_typed_ir.Bytes_t
  | syntax_type.boolScript_typed_ir.Bool_t
  | syntax_type.mutezScript_typed_ir.Mutez_t
  | syntax_type.addressScript_typed_ir.Address_t
  | syntax_type.key_hashScript_typed_ir.Key_hash_t
  | syntax_type.timestampScript_typed_ir.Timestamp_t
  | syntax_type.keyScript_typed_ir.Key_t
  | syntax_type.unitScript_typed_ir.Unit_t
  | syntax_type.signatureScript_typed_ir.Signature_t
  | syntax_type.chain_idScript_typed_ir.Chain_id_t

(* 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
        (ty_of_micho_comparable_ty a)
        (ty_of_micho_comparable_ty b)
        unused_metadata dand
  | syntax_type.Coption a
        (ty_of_micho_comparable_ty a)
        unused_metadata dbool
  | syntax_type.Cor a b
        (ty_of_micho_comparable_ty a)
        (ty_of_micho_comparable_ty b)
        unused_metadata dand

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
  | 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)
  | k v
      Script_typed_ir.Map_t (ty_of_micho_comparable_ty k) (ty_of_micho_ty v)
  | 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_frScript_typed_ir.Bls12_381_fr_t
  | syntax_type.bls12_381_g1Script_typed_ir.Bls12_381_g1_t
  | syntax_type.bls12_381_g2Script_typed_ir.Bls12_381_g2_t

(* 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.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} :
        (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_simple syntax_type.address) :: S) T
      instr_seq (syntax_type.option (syntax_type.comparable_type_to_type
         syntax_type.key_hash)) ::
         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))),
              (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_seqfun is'is'
  | failwithfun _failwith
  | neverfun _never
  | if_ if_fam is1 is2 is3fun is'
      if_ if_fam is1 is2 (sequence is3 is')
  | loop_ loop_fam is1 is2fun is'
      loop_ loop_fam is1 (sequence is2 is')
  | push d isfun is'push d (sequence is is')
  | lambda is1 is2fun is'lambda is1 (sequence is2 is')
  | iter i is1 is2fun is'iter i is1 (sequence is2 is')
  | map i is1 is2fun is'map i is1 (sequence is2 is')
  | create_contract is1 is2fun is'create_contract is1 (sequence is2 is')
  | self annot_opt pf isfun is'self annot_opt pf (sequence is is')
  | exec isfun is'exec (sequence is is')
  | dip pf is1 is2fun is'dip pf is1 (sequence is2 is')
  | opcode o isfun is'opcode o (sequence is is')

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.NEVERnever
  | 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 dpush d nil_seq
  | syntax.LAMBDA _ _ islambda (translate_instruction_seq is) nil_seq
  | syntax.ITER isiter _ (translate_instruction_seq is) nil_seq
  | syntax.MAP ismap _ (translate_instruction_seq is) nil_seq
  | syntax.CREATE_CONTRACT _ _ _ _ _ is
      create_contract (translate_instruction_seq is) nil_seq
  | syntax.SELF annot_opt pfself annot_opt pf nil_seq
  | syntax.EXECexec nil_seq
  | syntax.DIP n pf isdip pf (translate_instruction_seq is) nil_seq
  | syntax.Instruction_opcode oopcode o nil_seq

  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.NOOPnil_seq
    | syntax.Tail_fail itranslate_instruction i
    | syntax.SEQ i issequence
        (translate_instruction i)
        (translate_instruction_seq is)

An irrelevant [location] needed to produce terms of type [Script_typed_ir.kinstr]
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 :=
  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

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 :=
  match if_fam with
  | syntax.IF_boolfun i1 i2 i3
          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.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.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.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

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 :=
  match loop_fam with
  | syntax.LOOP_boolScript_typed_ir.ILoop unused_loc
  | syntax.LOOP_or _ _Script_typed_ir.ILoop_left unused_loc

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_seqScript_typed_ir.IHalt unused_loc
  | opcode o istranslate_opcode o (translate_instr_seq is)
  | @failwith a _ _Script_typed_ir.IFailwith unused_loc (ty_of_micho_ty a)
  | neverScript_typed_ir.INever unused_loc
  | if_ if_fam is1 is2 is3translate_if_family if_fam
      (translate_instr_seq is1)
      (translate_instr_seq is2)
      (translate_instr_seq is3)
  | loop_ loop_fam is1 is2translate_loop_family loop_fam
      (translate_instr_seq is1)
      (translate_instr_seq is2)
  | @push _ _ a d isScript_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