Skip to main content

🍬 Script_interpreter_defs.v

Proofs

See code, See simulations, Gitlab , OCaml

Our definition behaves as the original OCaml code.
Lemma dep_cost_of_instr_eq {s f}
  (i : With_family.kinstr s f)
  (accu : With_family.stack_ty_to_dep_Set_head s)
  (stack : With_family.stack_ty_to_dep_Set_tail s) :
  Script_interpreter_defs.dep_cost_of_instr i (accu, stack) =
  Script_interpreter_defs.cost_of_instr
    (With_family.to_kinstr i)
    (With_family.to_stack_value_head accu)
    (With_family.to_stack_value_tail stack).
Proof.
  dep_destruct i;
    unfold Script_interpreter_defs.cost_of_instr; simpl;
    try rewrite cast_eval;
    cbn in *;
    unfold Script_typed_ir.comparable_ty;
    destruct_all Script_typed_ir.never;
    Tactics.destruct_pairs;
    try rewrite_cast_exists;
    try match goal with
    | s : _ |- context[cast_exists ?T _] ⇒
      rewrite (cast_exists_eval_1 (T := T) (E1 := Stack_ty.to_Set s))
    end;
    (* I do not know why but this [cbn] optimizes heavily
       the [reflexivity] tactic. *)

    cbn;
    reflexivity.
Qed.

The cost of an instruction is valid in saturated arithmetic.
Lemma dep_cost_of_instr_is_valid {s f}
  (i : With_family.kinstr s f)
  (dep_accu_stack : With_family.stack_ty_to_dep_Set s) :
  Saturation_repr.Valid.t
    (Script_interpreter_defs.dep_cost_of_instr i dep_accu_stack).
Proof.
  destruct i; simpl;
    apply axiom. (*TODO: fix this*)
    (* now apply Saturation_repr.Valid.decide.*)
Qed.

The cost of an instruction is not zero, except for a few instructions.
Lemma dep_cost_of_instr_is_not_zero {s f}
  (i : With_family.kinstr s f)
  (dep_accu_stack : With_family.stack_ty_to_dep_Set s) :
  Script_interpreter_defs.dep_cost_of_instr i dep_accu_stack 0.
Admitted.
  (* TODO: fix, currently getting universe issues *)
  (* match i with *)
  (* | With_family.IFailwith _ _ _ => True *)
  (* | _ => (dep_cost_of_instr i accu_stack) <> 0 *)
  (* end *)
  (* ******* *)
  (* String below eats about 14GB of memory and I kill it *)
  (* I'm not 100% sure but I think it started after changes I made in dep_cost_of_instr *)
  (* ******* *)
  (* destruct i, accu_stack; simpl; cbv; trivial; try congruence; *)
  (* apply axiom. (*TODO*) *)
(* Qed. *)

The simulation [dep_consume_instr] is valid.
The simulation [dep_kundip] is valid.
Fixpoint dep_kundip_eq {s z u w t}
  (w_value : With_family.stack_prefix_preservation_witness s z u w)
  (accu : With_family.stack_ty_to_dep_Set_head u)
  (stack : With_family.stack_ty_to_dep_Set_tail u)
  (k_value : With_family.kinstr w t) :
  (let '(stack, instr) :=
    Script_interpreter_defs.dep_kundip w_value (accu, stack) k_value in
  (With_family.to_stack_value stack, With_family.to_kinstr instr)) =
  Script_interpreter_defs.kundip
    (With_family.to_stack_prefix_preservation_witness w_value)
    (With_family.to_stack_value_head accu)
    (With_family.to_stack_value_tail stack)
    (With_family.to_kinstr k_value).
Proof.
  destruct w_value; simpl.
  { rewrite cast_eval; reflexivity. }
  { match goal with
    | _ : ?t1, _ : ?t2 |- context[cast_exists ?T ?e] ⇒
      rewrite (cast_exists_eval_2 (T := T)
        (E1 := Stack_ty.to_Set_head u)
        (E2 := Stack_ty.to_Set_tail u)
      )
    end.
    simpl in *; Tactics.destruct_pairs; simpl.
    hauto lq: on.
  }
Qed.

(* TODO *)
The simulation [dep_apply] is valid.