🍬 Script_ir_annot.v

Proofs

Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.

Require Import TezosOfOCaml.Environment.V8.
Require Import TezosOfOCaml.Proto_alpha.Proofs.Error.
Require Import TezosOfOCaml.Proto_alpha.Script_ir_annot.

[error_unexpected_annot] is valid.

Lemma error_unexpected_annot_is_valid {A : Set} loc_value annot :
  letP ? res :=
    @error_unexpected_annot A loc_value annot in
    True.
Proof.
  unfold error_unexpected_annot. step; reflexivity.
Qed.

The function [string_iter] does not have internal errors.

Lemma string_iter_is_valid
  (p_value : ascii → M ? unit)
  (s_value : string)
  (i_value : int)
  : letP ? _ := string_iter p_value s_value i_value in True.
Proof.
Admitted.

[check_char] is valid.

Lemma check_char_is_valid {A : Set} loc_value c_value :
  letP ? res :=
    check_char loc_value c_value in
    True.
Proof.
  unfold check_char. step; reflexivity.
Qed.

The function [parse_annot] is valid.

Lemma parse_annot_is_valid
  (loc_value : Alpha_context.Script.location)
  (s_value : string)
  : letP ? _ := parse_annot loc_value s_value in True.
Proof.
Admitted.

The function [parse_annots] is valid.

Lemma parse_annots_is_valid
  (loc_value : Alpha_context.Script.location)
  (op_staroptstar : option bool)
  (ob : option bool)
  (ls : list string)
  : letP ? _ := parse_annots loc_value op_staroptstar ob ls in True.
Proof.
Admitted.

The function [classify_annot] is valid.

Lemma classify_annot_is_valid
  (loc_value : Alpha_context.Script.location)
  (l_value : list annot_opt)
  : letP ? _ := classify_annot loc_value l_value in True.
Proof.
Admitted.

The function [get_one_annot] is valid.

Lemma get_one_annot_is_valid {A : Set}
  (loc_value : Alpha_context.Script.location)
  (function_parameter : list (option A))
  : letP ? _ := get_one_annot loc_value function_parameter in True.
Proof.
Admitted.

The function [get_two_annot] is valid.

Lemma get_two_annot_is_valid {A : Set}
  (loc_value : Alpha_context.Script.location)
  (function_parameter : list (option A))
  : letP ? _ := get_two_annot loc_value function_parameter in True.
Proof.
Admitted.

The function [check_type_annot] is valid.

Lemma check_type_annot_is_valid
  (loc_value : Alpha_context.Script.location)
  (annot : list string)
  : letP ? _ := check_type_annot loc_value annot in True.
Proof.
Admitted.

The function [check_composed_type_annot] is valid.

Lemma check_composed_type_annot_is_valid
  (loc_value : Alpha_context.Script.location)
  (annot : list string)
  : letP ? _ := check_composed_type_annot loc_value annot in True.
Proof.
Admitted.

The function [parse_field_annot] is valid.

Lemma parse_field_annot_is_valid
  (loc_value : Alpha_context.Script.location)
  (annot : string)
  : letP ? _ := parse_field_annot loc_value annot in True.
Proof.
Admitted.

The function [is_field_annot] is valid.

Lemma is_field_annot_is_valid
  (loc_value : Alpha_context.Script.location)
  (annot : string)
  : letP ? _ := is_field_annot loc_value annot in True.
Proof.
Admitted.

The function [extract_field_annot] is valid.

Lemma extract_field_annot_is_valid
(node : Alpha_context.Script.node)
: letP ? _ := extract_field_annot node in True.
Proof.
Admitted.

The function [has_field_annot] is valid.

Lemma has_field_annot_is_valid
(node : Alpha_context.Script.node)
: letP ? _ := has_field_annot node in True.
Proof.
Admitted.

The function [remove_field_annot] is valid.

Lemma remove_field_annot_is_valid
(node : Alpha_context.Script.node)
: letP ? _ := remove_field_annot node in True.
Proof.
Admitted.

The function [extract_entrypoint_annot] is valid.

Lemma extract_entrypoint_annot_is_valid
(node : Alpha_context.Script.node)
: letP ? _ := extract_entrypoint_annot node in True.
Proof.
Admitted.

The function [check_var_annot] is valid.

Lemma check_var_annot_is_valid
  (loc_value : Alpha_context.Script.location)
  (annot : list string)
  : letP ? _ := check_var_annot loc_value annot in True.
Proof.
Admitted.

The function [check_constr_annot] is valid.

Lemma check_constr_annot_is_valid
  (loc_value : Alpha_context.Script.location)
  (annot : list string)
  : letP ? _ := check_constr_annot loc_value annot in True.
Proof.
Admitted.

The function [check_two_var_annot] is valid.

Lemma check_two_var_annot_is_valid
  (loc_value : Alpha_context.Script.location)
  (annot : list string)
  : letP ? _ := check_two_var_annot loc_value annot in True.
Proof.
Admitted.

The function [check_destr_annot] is valid.

Lemma check_destr_annot_is_valid
  (loc_value : Alpha_context.Script.location)
  (annot : list string)
  : letP ? _ := check_destr_annot loc_value annot in True.
Proof.
Admitted.

The function [check_unpair_annot] is valid.

Lemma check_unpair_annot_is_valid
  (loc_value : Alpha_context.Script.location)
  (annot : list string)
  : letP ? _ := check_unpair_annot loc_value annot in True.
Proof.
Admitted.

The function [parse_entrypoint_annot] is valid.

Lemma parse_entrypoint_annot_is_valid
  (loc_value : Alpha_context.Script.location)
  (annot : list string)
  : letP ? _ := parse_entrypoint_annot loc_value annot in True.
Proof.
Admitted.

The function [parse_entrypoint_annot_strict] is valid.

Lemma parse_entrypoint_annot_strict_is_valid
  (loc_value : Alpha_context.Script.location)
  (annot : list string)
  : letP ? _ := parse_entrypoint_annot_strict loc_value annot in True.
Proof.
Admitted.

The function [parse_entrypoint_annot_lax] is valid.

Lemma parse_entrypoint_annot_lax_is_valid
  (loc_value : Alpha_context.Script.location)
  (annot : list string)
  : letP ? _ := parse_entrypoint_annot_lax loc_value annot in True.
Proof.
Admitted.

The function [check_var_type_annot] is valid.

Lemma check_var_type_annot_is_valid
  (loc_value : Alpha_context.Script.location)
  (annot : list string)
  : letP ? _ := check_var_type_annot loc_value annot in True.
Proof.
Admitted.