Specify Script_typed_ir.kinstr and values
Define a mutually recursive predicate Valid.kinstr
on Script_typed_ir.kinstr
and the values (and maybe a few other types that are dependent on the above), taking inspiration from what we already have on the simulations.
A template:
Module Valid.
Inductive kinstr : Stack_ty.t -> Stack_ty.t -> Prop :=
| IConst {t s f} loc typ (value : Ty.to_Set t) k :
Valid.ty t typ ->
Valid.value t value ->
Valid.kinstr (t :: s) f k ->
Valid.kinstr s f (Script_typed_it.IConst loc typ value k)
| ...
with value : forall (t : Ty.t), Ty.to_Set t -> Prop :=
| Bool_value b : Valid.value Ty.Bool b
| ...
The goal is to capture all the typing constraints given by the GADTs in OCaml, together with the additional invariants such as validity of tez amounts, etc. We should already have these properties in the current predicate on the simulations.