Anomaly as a result of extraction in CertiCoq (assertion fails in ml code) #1072

mkarup · 2024-04-01T19:40:49Z

I apologize if this is not the right place to report this, I admit I haven't investigated it thoroughly.
Using the CertiCoq project to try to extract the parsing of the binary representation of a WebAssembly module (using WasmCert-Coq), I encountered an "anomaly", and at a quick glance, it looked like it originated in one of the phases that MetaCoq is responsible for.
Again, I haven't investigated exactly what part of WasmCert that triggers this, so for now I leave this "minimal" example, and I will report back if I pinpoint it more accurately.

From Coq Require Import List.
From Coq.Strings Require Import Byte.
From CertiCoq.Plugin Require Import CertiCoq.
From Wasm Require Import binary_format_parser datatypes instantiation_func.

Definition test_bytes : list Byte.byte := x00 :: x61 :: x73 :: x6d :: x01 :: x00 :: x00 :: x00 :: nil.

Definition test_module : option module := run_parse_module test_bytes.

CertiCoq Compile test_module.

Error message:

Error:
Anomaly
"File "extraction/pCUICSafeRetyping.ml", line 48, characters 25-31: Assertion failed."
Please report at http://coq.inria.fr/bugs/.

Don't know if it even makes sense to include this, but the assertion failing code snippet in question is this:

(** val infer_as_sort :
    checker_flags -> abstract_env_impl -> __ -> PCUICEnvironment.context ->
    term -> principal_type -> principal_sort **)

let infer_as_sort cf x_type x _UU0393_ t0 tx =
  let filtered_var =
    reduce_to_sort cf x_type x _UU0393_
      (principal_type_type cf x_type x _UU0393_ t0 tx)
  in
  (match filtered_var with
   | Checked_comp a -> let Coq_existT (u, _) = a in Coq_existT (u, __)
   | TypeError_comp _ -> assert false (* absurd case *))

The text was updated successfully, but these errors were encountered:

mkarup · 2024-04-15T14:18:15Z

I have to go back on my statement:
I currently don't have the time to investigate this, so take the above code as the full bug report.

mattam82 · 2024-06-06T20:04:33Z

That's an interesting report, will look into it!

spitters · 2024-09-16T09:25:07Z

@mattam82 Did you have the chance to look into this? It's also blocking some other programs we'd like to extract.
Thanks!

mattam82 · 2024-10-08T13:58:14Z

I've not had a chance yet. The usual suspect is lack of template-polymorphism, but it's unlikely to raise that error a priori. Maybe run_parse_module is using some fancy feature? It would be great if you could trace what t0 and tx are here. I think the error happens during the erasure phase here, where we retype terms to know if they should be erased or not.

JasonGross · 2024-10-12T21:38:05Z

Does it make sense to do
@coqbot minimize coq.8.17

opam install -y coq-wasm
cat > test_bug.v <<EOF
From Coq Require Import List.
From Coq.Strings Require Import Byte.
From CertiCoq.Plugin Require Import CertiCoq.
From Wasm Require Import binary_format_parser datatypes instantiation_func.

Definition test_bytes : list Byte.byte := x00 :: x61 :: x73 :: x6d :: x01 :: x00 :: x00 :: x00 :: nil.

Definition test_module : option module := run_parse_module test_bytes.

CertiCoq Compile test_module.
EOF
coqc -q test_bug.v

JasonGross · 2024-10-16T18:53:09Z

I guess coqbot doesn't listen to comments on this repo, so running minimization at coq-community/run-coq-bug-minimizer#2 (comment)

JasonGross · 2024-10-16T19:09:20Z

@mkarup what version of Coq are you using? There are no versions of coq-certicoq and coq-wasm on opam that are compatible with the same Coq versions.

mkarup · 2024-10-17T11:49:26Z

@JasonGross I reported this a while back, so I can't quite remember what the versions were at the time.
I also haven't tested whether the issue is still present.

For a version of coq-wasm that should be compatible with certicoq, you could try pinning coq-wasm to this commit (it is from a fork that we use for certicoq-wasm, specifically that commit).
There are some minor modifications from upstream and it is a little bit behind, but I don't think the differences relate to this issue.

raoxiaojia · 2024-10-17T19:54:39Z

@JasonGross I reported this a while back, so I can't quite remember what the versions were at the time. I also haven't tested whether the issue is still present.

For a version of coq-wasm that should be compatible with certicoq, you could try pinning coq-wasm to this commit (it is from a fork that we use for certicoq-wasm, specifically that commit). There are some minor modifications from upstream and it is a little bit behind, but I don't think the differences relate to this issue.

I've created a PR on opam for WasmCert-Coq that works with Coq 8.19 (which is a few commits ahead of the commit @mkarup has linked but nothing too different) -- hopefully this makes the debugging here slightly easier.

JasonGross · 2024-10-18T21:53:14Z

Here is a somewhat reduced test-case, that depends only on the Declare ML Module "coq-certicoq.plugin". and on compcert.lib.Integers (still working on working around AbsInt/CompCert#526)

(* -*- mode: coq; coq-prog-args: ("-emacs" "-q" "-w" "-deprecated-native-compiler-option,-native-compiler-disabled" "-native-compiler" "ondemand" "-Q" "/github/workspace/cwd" "Top" "-Q" "/home/coq/.opam/4.13.1+flambda/lib/coq/user-contrib/Bignums" "Bignums" "-Q" "/home/coq/.opam/4.13.1+flambda/lib/coq/user-contrib/CertiCoq" "CertiCoq" "-Q" "/home/coq/.opam/4.13.1+flambda/lib/coq/user-contrib/Coqprime" "Coqprime" "-Q" "/home/coq/.opam/4.13.1+flambda/lib/coq/user-contrib/Equations" "Equations" "-Q" "/home/coq/.opam/4.13.1+flambda/lib/coq/user-contrib/ExtLib" "ExtLib" "-Q" "/home/coq/.opam/4.13.1+flambda/lib/coq/user-contrib/Flocq" "Flocq" "-Q" "/home/coq/.opam/4.13.1+flambda/lib/coq/user-contrib/Ltac2" "Ltac2" "-Q" "/home/coq/.opam/4.13.1+flambda/lib/coq/user-contrib/MenhirLib" "MenhirLib" "-Q" "/home/coq/.opam/4.13.1+flambda/lib/coq/user-contrib/MetaCoq" "MetaCoq" "-Q" "/home/coq/.opam/4.13.1+flambda/lib/coq/user-contrib/Wasm" "Wasm" "-Q" "/home/coq/.opam/4.13.1+flambda/lib/coq/user-contrib/compcert" "compcert" "-Q" "/home/coq/.opam/4.13.1+flambda/lib/coq/user-contrib/mathcomp" "mathcomp" "-Q" "/home/coq/.opam/4.13.1+flambda/lib/coq/user-contrib/parseque" "parseque" "-top" "test_bug") -*- *)
(* File reduced by coq-bug-minimizer from original input, then from 27 lines to 14 lines, then from 27 lines to 1263 lines, then from 1266 lines to 132 lines, then from 145 lines to 747 lines, then from 749 lines to 133 lines, then from 146 lines to 1309 lines, then from 1288 lines to 561 lines, then from 574 lines to 954 lines, then from 957 lines to 560 lines, then from 573 lines to 2533 lines, then from 2530 lines to 580 lines, then from 593 lines to 1687 lines, then from 1687 lines to 582 lines, then from 595 lines to 1631 lines, then from 1636 lines to 596 lines, then from 609 lines to 831 lines, then from 836 lines to 596 lines, then from 609 lines to 637 lines, then from 642 lines to 598 lines, then from 611 lines to 881 lines, then from 884 lines to 703 lines, then from 716 lines to 787 lines, then from 792 lines to 744 lines, then from 757 lines to 830 lines, then from 835 lines to 752 lines, then from 765 lines to 832 lines, then from 837 lines to 759 lines, then from 772 lines to 814 lines, then from 819 lines to 770 lines, then from 783 lines to 805 lines, then from 809 lines to 769 lines, then from 782 lines to 898 lines, then from 901 lines to 809 lines, then from 814 lines to 811 lines *)
(* coqc version 8.19.2 compiled with OCaml 4.13.1
   coqtop version 8.19.2
   Expected coqc runtime on this file: 0.647 sec *)

Require compcert.lib.Integers.
Require Coq.ssr.ssrbool.

Axiom proof_admitted : False.
Tactic Notation "admit" := abstract case proof_admitted.
Module Export Category.
Class RawFunctor (F : Type -> Type) :=
  MkRawFunctor { _fmap : forall A B, (A -> B) -> (F A -> F B)
               }.

Class RawApplicative (F : Type -> Type) `{RawFunctor F} :=
  MkRawApplicative { _pure       : forall A, A -> F A
                   ; _app        : forall A B, F (A -> B) -> (F A -> F B)
                   }.
Definition pure {F : Type -> Type} `{RawApplicative F} {A : Type} : A -> F A.
Admitted.

Class RawAlternative (F : Type -> Type) `{RawApplicative F} :=
  MkRawAlternative { _fail : forall A, F A
                   ; _alt  : forall A, F A -> F A -> F A
                   }.
Definition alt {F : Type -> Type} `{RawAlternative F} {A : Type} : F A -> F A -> F A.
Admitted.

Class RawMonad (F : Type -> Type) `{RawApplicative F} :=
  MkRawMonad { _bind : forall A B, F A -> (A -> F B) -> F B }.
Definition bind {F : Type -> Type} `{RawMonad F} {A B : Type} :
  F A -> (A -> F B) -> F B.
Admitted.

Class RawMonadRun (F : Type -> Type) `{RawMonad F} :=
  MkRawMonadRun { _runMonad : forall A, F A -> list A }.
#[global]
Instance listRawFunctor : RawFunctor list.
Admitted.
#[global]
Instance listRawApplicative : RawApplicative list.
Admitted.
#[global]
Instance listRawAlternative : RawAlternative list.
Admitted.
#[global]
Instance listRawMonad : RawMonad list.
Admitted.
#[global]
Instance listRawMonadRun : RawMonadRun list.
Admitted.
Class EqDec (A : Type) := MkEqDec { eq_dec : forall (a b : A), { a = b } + { a <> b } }.
Section Indexed.

Context {I : Type} (T : Type) (A B : I -> Type).
Definition IArrow : I -> Type.
exact (fun i => A i -> B i).
Defined.
Definition IForall : Type.
exact (forall i, A i).
Defined.

End Indexed.
Notation "A :-> B" := (IArrow A B)   (at level 20, right associativity).
Notation "[ A ]"   := (IForall A)    (at level 70).
Import Coq.Arith.PeanoNat.

Record Box (A : nat -> Type) (n : nat) : Type :=
  MkBox { call : forall m, m < n -> A m }.

Arguments call {_} {_} _ {_}.

Definition Fix A (alg : [ Box A :-> A ]) : [ A ].
Admitted.

Definition View (As : nat -> Type) (A : Type) (n : nat) : Type :=
match n with
  | O    => False
  | S n' => A * As n'
end.

Class Sized As A : Type := MkSized { uncons {n} : As n -> option (View As A n) }.

Record SizedType {A : Type} (size : A -> nat) (n : nat) : Type :=
  MkSizedType { value : A
              ; sized : size value = n
              }.

Definition SizedList (A : Type) n := SizedType (@length A) n.

#[global]
Instance sizedList : forall (A : Type), Sized (SizedList A) A.
Admitted.
Module Export Success.

Record Success (Toks : nat -> Type) (Tok : Type) (A : Type) (n : nat) :=
  MkSuccess { value     : A
            ; size      : nat
            ; small     : size < n
            ; leftovers : Toks size
            }.

Arguments MkSuccess {_} {_} {_} {_} _ {_}.
Arguments value     {_} {_} {_} {_}.
Arguments small     {_} {_} {_} {_}.
Arguments leftovers {_} {_} {_} {_}.

Section Success.

Context {Toks : nat -> Type} {Tok : Type} {A B C : Type} {n : nat}.
Definition map (f : A -> B) : Success Toks Tok A n -> Success Toks Tok B n.
admit.
Defined.

Definition le_lift {m n : nat} (p : m <= n) (s : Success Toks Tok A m) :
  Success Toks Tok A n :=
  let small := Nat.le_trans _ _ _  (small s) p
  in MkSuccess (value s) small (leftovers s).

Definition lt_lift {m n : nat} (p : m < n) (s : Success Toks Tok A m) :
  Success Toks Tok A n := le_lift (Nat.lt_le_incl _ _ p) s.

End Success.
Module Export parseque.

Record Parser (Toks : nat -> Type) (Tok : Type)
              (M : Type -> Type) (A : Type) (n : nat) : Type :=
  MkParser { runParser {m} : m <= n -> Toks m -> M (Success Toks Tok A m) }.

Arguments MkParser {_} {_} {_} {_} {_}.
Arguments runParser {_} {_} {_} {_} {_} _ {_}.

Section Lower.

Context
  {Toks : nat -> Type} {Tok : Type}
  {M : Type -> Type}
  {A : Type} {m n : nat}.
Definition lt_lower (mltn : m < n) (p : Parser Toks Tok M A n) : Parser Toks Tok M A m.
Admitted.

End Lower.
Definition box {Toks Tok M A n} : Parser Toks Tok M A n -> Box (Parser Toks Tok M A) n.
Admitted.

Coercion box : Parser >-> Box.

Section Combinators1.

Context
  {Toks : nat -> Type} {Tok : Type} `{Sized Toks Tok}
  {M : Type -> Type} `{RawFunctor M} `{RawApplicative M} `{RawMonad M} `{RawAlternative M}
  {A B : Type} {n : nat}.
Definition map (f : A -> B) (p : Parser Toks Tok M A n) :
  Parser Toks Tok M B n.
Admitted.
Definition cmap (b : B) (p : Parser Toks Tok M A n) : Parser Toks Tok M B n.
Admitted.
Definition alt (p q : Parser Toks Tok M A n) : Parser Toks Tok M A n.
exact (MkParser (fun _ mlen toks =>
  alt (runParser p mlen toks) (runParser q mlen toks))).
Defined.

End Combinators1.

Section Combinators2.

Context
  {Toks : nat -> Type} {Tok : Type} `{Sized Toks Tok}
  {M : Type -> Type} `{RawFunctor M} `{RawApplicative M} `{RawMonad M} `{RawAlternative M}
  {A B : Type} {n : nat}.
Definition bind (p : Parser Toks Tok M A n)
  (q : A -> Box (Parser Toks Tok M B) n) : Parser Toks Tok M B n.
Admitted.
Definition rand (p : Parser Toks Tok M A n) (q : Box (Parser Toks Tok M B) n) :
  Parser Toks Tok M B n.
Admitted.

End Combinators2.

Section Combinators3.

Context
  {Toks : nat -> Type} {Tok : Type} `{Sized Toks Tok} `{EqDec Tok}
  {M : Type -> Type} `{RawFunctor M} `{RawApplicative M} `{RawMonad M} `{RawAlternative M}
  {A B C : Type} {n : nat}.
Definition app (p : Parser Toks Tok M (A -> B) n)
  (q : Box (Parser Toks Tok M A) n) : Parser Toks Tok M B n.
admit.
Defined.

End Combinators3.

Section HChainl.

Context
  {Toks : nat -> Type} {Tok : Type}
  {M : Type -> Type} `{RawFunctor M} `{RawApplicative M} `{RawMonad M} `{RawAlternative M}
  {A B : Type} {n : nat}.

Definition RChain (n : nat) : Type :=
  Parser Toks Tok M (A -> A) n -> Parser Toks Tok M A n -> Parser Toks Tok M A n.

Definition iterater_aux (n : nat) (rec : Box RChain n) :
  RChain n := fun op val => MkParser (fun _ mlen ts =>
  Category.bind (runParser op mlen ts) (fun sop =>
  let sopltn := Nat.le_trans _ _ _ (small sop) mlen in
  let op'    := lt_lower sopltn op in
  let val'   := lt_lower sopltn val in
  Category.bind (runParser (call rec sopltn op' val') (Nat.le_refl _) (leftovers sop)) (fun res =>
  pure (lt_lift (small sop) (Success.map (value sop) res))))).

Definition iterater {n : nat} (op : Parser Toks Tok M (A -> A) n)
  (val : Parser Toks Tok M A n) : Parser Toks Tok M A n :=
  Fix _ (fun n rec op val => alt (iterater_aux n rec op val) val) n op val.

End HChainl.

Notation "p <|> q"   := (alt p q)  (at level 60, right associativity).
Notation "f <$> p"   := (map f p)  (at level 59, right associativity).
Notation "p >>= q"   := (bind p q)     (at level 60, right associativity).
Notation "p  &> q"   := (rand p q)     (at level 50, left associativity).
Notation "p <*> q"   := (app p q)      (at level 50, left associativity).
Export Coq.ssr.ssrbool.

Set Implicit Arguments.

Definition axiom T (e : rel T) := forall x y, reflect (x = y) (e x y).

Structure mixin_of T := Mixin {op : rel T; _ : axiom op}.
Notation class_of := mixin_of (only parsing).

Section ClassDef.

Structure type := Pack {sort; _ : class_of sort}.

End ClassDef.
Coercion sort : type >-> Sortclass.
Notation eqType := type.

Module Export Wasm_int.

Module Make (WS: Integers.WORDSIZE).

Import compcert.lib.Integers.

Include Make (WS).

End Make.

Module Export Int32.
Include Make(Integers.Wordsize_32).
Definition i32 : eqType.
Admitted.
Definition i64 : eqType.
Admitted.
Definition f32 : eqType.
Admitted.
Definition f64 : eqType.
Admitted.
Import compcert.lib.Integers.
Import Coq.NArith.BinNat.
Definition u32 : Set.
Admitted.
Definition u8: Set.
Admitted.
Definition typeidx : Set.
Admitted.
Definition funcidx : Set.
Admitted.
Definition tableidx : Set.
Admitted.
Definition memidx : Set.
Admitted.
Definition globalidx : Set.
Admitted.
Definition elemidx : Set.
Admitted.
Definition dataidx : Set.
Admitted.
Definition localidx : Set.
Admitted.
Definition labelidx : Set.
Admitted.

Inductive value_num : Type :=
  | VAL_int32 : i32 -> value_num
  | VAL_int64 : i64 -> value_num
  | VAL_float32 : f32 -> value_num
  | VAL_float64 : f64 -> value_num
.

Inductive value_vec : Set :=
  | VAL_vec128: unit -> value_vec
.

Definition name := list Byte.byte.

Section Types.

Inductive number_type : Set :=
  | T_i32
  | T_i64
  | T_f32
  | T_f64
  .

Inductive vector_type : Set :=
| T_v128
.

Inductive reference_type : Set :=
| T_funcref
| T_externref
.

Inductive value_type: Set :=
| T_num: number_type -> value_type
| T_vec: vector_type -> value_type
| T_ref: reference_type -> value_type
| T_bot: value_type
.
Definition result_type : Set.
Admitted.

Inductive function_type :=
| Tf : result_type -> result_type -> function_type
.

Record limits : Set := {
  lim_min : u32;
  lim_max : option u32;
}.

Definition memory_type := limits.

Record table_type : Set := {
  tt_limits : limits;
  tt_elem_type : reference_type;
}.

Inductive mutability : Set :=
  | MUT_const
  | MUT_var
  .

Record global_type : Set :=  {
  tg_mut : mutability;
  tg_t : value_type
}.

Inductive block_type : Set :=
| BT_id: typeidx -> block_type
| BT_valtype: option value_type -> block_type
.

End Types.

Section Instructions.

Inductive sx : Set :=
  | SX_S
  | SX_U
  .

Inductive unop_i : Set :=
  | UOI_clz
  | UOI_ctz
  | UOI_popcnt
  .

Inductive unop_f : Set :=
  | UOF_abs
  | UOF_neg
  | UOF_sqrt
  | UOF_ceil
  | UOF_floor
  | UOF_trunc
  | UOF_nearest
  .

Inductive unop : Set :=
  | Unop_i : unop_i -> unop
  | Unop_f : unop_f -> unop
  | Unop_extend : N -> unop
  .

Inductive binop_i : Set :=
  | BOI_add
  | BOI_sub
  | BOI_mul
  | BOI_div : sx -> binop_i
  | BOI_rem : sx -> binop_i
  | BOI_and
  | BOI_or
  | BOI_xor
  | BOI_shl
  | BOI_shr : sx -> binop_i
  | BOI_rotl
  | BOI_rotr
  .

Inductive binop_f : Set :=
  | BOF_add
  | BOF_sub
  | BOF_mul
  | BOF_div
  | BOF_min
  | BOF_max
  | BOF_copysign
  .

Inductive binop : Set :=
  | Binop_i : binop_i -> binop
  | Binop_f : binop_f -> binop
  .

Inductive testop : Set :=
  | TO_eqz
  .

Inductive relop_i : Set :=
  | ROI_eq
  | ROI_ne
  | ROI_lt : sx -> relop_i
  | ROI_gt : sx -> relop_i
  | ROI_le : sx -> relop_i
  | ROI_ge : sx -> relop_i
  .

Inductive relop_f : Set :=
  | ROF_eq
  | ROF_ne
  | ROF_lt
  | ROF_gt
  | ROF_le
  | ROF_ge
  .

Inductive relop : Set :=
  | Relop_i : relop_i -> relop
  | Relop_f : relop_f -> relop
  .

Inductive cvtop : Set :=
  | CVO_wrap
  | CVO_extend
  | CVO_trunc
  | CVO_trunc_sat
  | CVO_convert
  | CVO_demote
  | CVO_promote
  | CVO_reinterpret
  .

Inductive packed_type : Set :=
  | Tp_i8
  | Tp_i16
  | Tp_i32
  .

Inductive shape_vec_i: Set :=
  | SVI_8_16
  | SVI_16_8
  | SVI_32_4
  | SVI_64_2
  .

Inductive shape_vec_f: Set :=
  | SVF_32_4
  | SVF_64_2
  .

Inductive shape_vec : Set :=
  | SV_ishape: shape_vec_i -> shape_vec
  | SV_fshape: shape_vec_f -> shape_vec
  .

Inductive unop_vec : Set :=
  | VUO_not
  .

Inductive binop_vec : Set :=
  | VBO_and
  .

Inductive ternop_vec : Set :=
  | VTO_bitselect
  .

Inductive test_vec : Set :=
  | VT_any_true
  .

Inductive shift_vec : Set :=
  | VSH_any_true
  .

Definition laneidx := u8.

Inductive packed_type_vec :=
  | Tptv_8_8
  | Tptv_16_4
  | Tptv_32_2
.

Inductive zero_type_vec :=
  | Tztv_32
  | Tztv_64
.

Inductive width_vec :=
  | Twv_8
  | Twv_16
  | Twv_32
  | Twv_64
  .

Inductive load_vec_arg :=
  | LVA_packed: packed_type_vec -> sx -> load_vec_arg
  | LVA_zero: zero_type_vec -> load_vec_arg
  | LVA_splat: width_vec -> load_vec_arg
  .

Record memarg : Set :=
  { memarg_offset : u32;
    memarg_align: u32
  }.

Inductive basic_instruction : Type :=

  | BI_const_num : value_num -> basic_instruction
  | BI_unop : number_type -> unop -> basic_instruction
  | BI_binop : number_type -> binop -> basic_instruction
  | BI_testop : number_type -> testop -> basic_instruction
  | BI_relop : number_type -> relop -> basic_instruction
  | BI_cvtop : number_type -> cvtop -> number_type -> option sx -> basic_instruction

  | BI_const_vec : value_vec -> basic_instruction
  | BI_unop_vec: unop_vec -> basic_instruction
  | BI_binop_vec: binop_vec -> basic_instruction
  | BI_ternop_vec: ternop_vec -> basic_instruction
  | BI_test_vec: test_vec -> basic_instruction
  | BI_shift_vec: shift_vec -> basic_instruction
  | BI_splat_vec: shape_vec -> basic_instruction
  | BI_extract_vec: shape_vec -> option sx -> laneidx -> basic_instruction
  | BI_replace_vec: shape_vec -> laneidx -> basic_instruction

  | BI_ref_null : reference_type -> basic_instruction
  | BI_ref_is_null
  | BI_ref_func : funcidx -> basic_instruction

  | BI_drop
  | BI_select : option (list value_type) -> basic_instruction

  | BI_local_get : localidx -> basic_instruction
  | BI_local_set : localidx -> basic_instruction
  | BI_local_tee : localidx -> basic_instruction
  | BI_global_get : globalidx -> basic_instruction
  | BI_global_set : globalidx -> basic_instruction

  | BI_table_get : tableidx -> basic_instruction
  | BI_table_set : tableidx -> basic_instruction
  | BI_table_size : tableidx -> basic_instruction
  | BI_table_grow : tableidx -> basic_instruction
  | BI_table_fill : tableidx -> basic_instruction
  | BI_table_copy : tableidx -> tableidx -> basic_instruction
  | BI_table_init : tableidx -> elemidx -> basic_instruction
  | BI_elem_drop : elemidx -> basic_instruction

  | BI_load : number_type -> option (packed_type * sx) -> memarg -> basic_instruction
  | BI_load_vec : load_vec_arg -> memarg -> basic_instruction

  | BI_load_vec_lane : width_vec -> memarg -> laneidx -> basic_instruction
  | BI_store : number_type -> option packed_type -> memarg-> basic_instruction
  | BI_store_vec_lane : width_vec -> memarg -> laneidx -> basic_instruction
  | BI_memory_size
  | BI_memory_grow
  | BI_memory_fill
  | BI_memory_copy
  | BI_memory_init: dataidx -> basic_instruction
  | BI_data_drop: dataidx -> basic_instruction

  | BI_nop
  | BI_unreachable
  | BI_block : block_type -> list basic_instruction -> basic_instruction
  | BI_loop : block_type -> list basic_instruction -> basic_instruction
  | BI_if : block_type -> list basic_instruction -> list basic_instruction -> basic_instruction
  | BI_br : labelidx -> basic_instruction
  | BI_br_if : labelidx -> basic_instruction
  | BI_br_table : list labelidx -> labelidx -> basic_instruction
  | BI_return
  | BI_call : funcidx -> basic_instruction
  | BI_call_indirect : tableidx -> typeidx -> basic_instruction
  | BI_return_call : funcidx -> basic_instruction
  | BI_return_call_indirect : tableidx -> typeidx -> basic_instruction
  .

Definition expr := list basic_instruction.

End Instructions.

Section Modules.

Inductive module_import_desc : Set :=
| MID_func : typeidx -> module_import_desc
| MID_table : table_type -> module_import_desc
| MID_mem : memory_type -> module_import_desc
| MID_global : global_type -> module_import_desc.

Record module_import : Set := {
  imp_module : name;
  imp_name : name;
  imp_desc : module_import_desc;
}.

Record module_func : Type := {
  modfunc_type : typeidx;
  modfunc_locals : list value_type;
  modfunc_body : expr;
}.

Record module_table : Set := {
  modtab_type : table_type;
}.

Record module_mem : Set := {
  modmem_type : memory_type;
}.

Record module_global : Type := {
  modglob_type : global_type;
  modglob_init : expr;
}.

Inductive module_elemmode : Type :=
| ME_passive
| ME_active : tableidx -> expr -> module_elemmode
| ME_declarative
.

Record module_element : Type := {
  modelem_type : reference_type;
  modelem_init : list expr;
  modelem_mode : module_elemmode;
}.

Inductive module_datamode : Type :=
| MD_passive
| MD_active : memidx -> expr -> module_datamode
.

Record module_data : Type := {
  moddata_init : list byte;
  moddata_mode : module_datamode;
}.

Record module_start : Set := {
  modstart_func : funcidx;
}.

Inductive module_export_desc : Set :=
| MED_func : funcidx -> module_export_desc
| MED_table : tableidx -> module_export_desc
| MED_mem : memidx -> module_export_desc
| MED_global : globalidx -> module_export_desc.

Record module_export : Set := {
  modexp_name : name;
  modexp_desc : module_export_desc;
}.

Record module : Type := {
  mod_types : list function_type;
  mod_funcs : list module_func;
  mod_tables : list module_table;
  mod_mems : list module_mem;
  mod_globals : list module_global;
  mod_elems : list module_element;
  mod_datas : list module_data;
  mod_start : option module_start;
  mod_imports : list module_import;
  mod_exports : list module_export;
}.

End Modules.
Import Coq.Strings.Byte.

Notation "p $> b" := (cmap b p) (at level 59, right associativity).

Section Language.

Context
  {Toks : nat -> Type} `{Sized Toks byte}
  {M : Type -> Type} `{RawMonad M} `{RawAlternative M}.

Definition byte_parser A n := Parser Toks byte M A n.
Definition exact_byte (b : byte) {n} : byte_parser byte n.
Admitted.
Definition parse_u32_as_int32 {n} : byte_parser Wasm_int.Int32.int n.
Admitted.
Definition parse_u32_zero_as_int32 {n} : byte_parser Wasm_int.Int32.int n.
Admitted.
Definition parse_vec_length {n} : byte_parser nat n.
Admitted.

Fixpoint parse_vec_aux {B} {n} (f : byte_parser B n) (k : nat)
  : byte_parser (list B) n :=
  match k with
  | 0 => (fun x => cons x nil) <$> f
  | S 0 => (fun x => cons x nil) <$> f
  | S k' => (cons <$> f) <*> parse_vec_aux f k'
  end.
Definition parse_vec {B} {n} (f : byte_parser B n) : byte_parser (list B) n.
exact ((parse_u32_zero_as_int32 $> nil) <|>
  (parse_vec_length >>= (fun k => parse_vec_aux f k))).
Defined.
Definition parse_function_type {n} : byte_parser function_type n.
Admitted.

Definition module_func_without_type : Type := (list value_type) * expr.
Definition parse_typesec {n} : byte_parser (list function_type) n.
exact (exact_byte x01 &> parse_u32_as_int32 &> parse_vec parse_function_type).
Defined.
Definition parse_magic {n} : byte_parser unit n.
Admitted.
Definition parse_version {n} : byte_parser unit n.
Admitted.
Definition parse_customsec_forget {A n} : byte_parser (A -> A) n.
Admitted.

Definition parse_with_customsec_star_before {A : Type} {n} f :=
  @iterater _ _ _ _ _ _ _ _ _ A n parse_customsec_forget f.

Record parsing_module : Type := {
  pmod_types : list function_type;
  pmod_funcs : list typeidx;
  pmod_tables : list module_table;
  pmod_mems : list module_mem;
  pmod_globals : list module_global;
  pmod_elems : list module_element;
  pmod_datas : list module_data;
  pmod_start : option module_start;
  pmod_imports : list module_import;
  pmod_exports : list module_export;
  pmod_code : list module_func_without_type;
}.
Definition merge_parsing_modules (m1 m2 : parsing_module) : parsing_module.
Admitted.
Definition parse_typesec_wrapper {n} : byte_parser parsing_module n.
exact ((fun types => {|
    pmod_types := types;
    pmod_funcs := nil;
    pmod_tables := nil;
    pmod_mems := nil;
    pmod_globals := nil;
    pmod_elems := nil;
    pmod_datas := nil;
    pmod_start := None;
    pmod_imports := nil;
    pmod_exports := nil;
    pmod_code := nil;
  |}) <$>
  (parse_with_customsec_star_before parse_typesec)).
Defined.
Definition end_marker : byte.
Admitted.
Definition parse_importsec_onwards {n} : byte_parser parsing_module n.
Admitted.
Definition parse_typesec_onwards {n} : byte_parser parsing_module n.
exact (((merge_parsing_modules <$> parse_typesec_wrapper) <*> parse_importsec_onwards) <|>
  parse_importsec_onwards).
Defined.
Definition module_of_parsing_module (m : parsing_module) : module.
Admitted.
Definition parse_module {n} : byte_parser module n.
exact (module_of_parsing_module <$>
  (parse_magic &>
  parse_version &>
  parse_typesec_onwards)).
Defined.

End Language.

Class Tokenizer (A : Type) : Type :=
  MkTokenizer { _tokenize : list byte -> list A }.
#[export]
Instance tokBytes : Tokenizer byte.
Admitted.

Section Run.

Context
  {M : Type -> Type} `{RawMonad M} `{RawAlternative M} `{RawMonadRun M}
  {Tok : Type} `{Tokenizer Tok}
  {A : Type}.
Definition run : list byte -> [ Parser (SizedList Tok) Tok M A ] -> option A.
Admitted.

End Run.
Definition run_parse_module (bs : list byte) : option module.
exact (run (bs ++ cons end_marker nil) (fun n => parse_module)).
Defined.

Declare ML Module "coq-certicoq.plugin".
Definition test_bytes : list Byte.byte.
Admitted.
Definition test_module : option module.
exact (run_parse_module test_bytes).
Defined.

CertiCoq Compile test_module.

JasonGross · 2024-10-18T21:56:06Z

I don't suppose there's a way to bypass CertiCoq Compile and replicate the same anomaly with just MetaCoq commands?

JasonGross · 2024-10-19T21:31:24Z

And here's a version that depends only on Declare ML Module "coq-certicoq.plugin".

(* -*- mode: coq; coq-prog-args: ("-emacs" "-q" "-w" "-deprecated-native-compiler-option,-native-compiler-disabled" "-native-compiler" "ondemand" "-Q" "/github/workspace/cwd" "Top" "-Q" "/home/coq/.opam/4.13.1+flambda/lib/coq/user-contrib/Bignums" "Bignums" "-Q" "/home/coq/.opam/4.13.1+flambda/lib/coq/user-contrib/CertiCoq" "CertiCoq" "-Q" "/home/coq/.opam/4.13.1+flambda/lib/coq/user-contrib/Coqprime" "Coqprime" "-Q" "/home/coq/.opam/4.13.1+flambda/lib/coq/user-contrib/Equations" "Equations" "-Q" "/home/coq/.opam/4.13.1+flambda/lib/coq/user-contrib/ExtLib" "ExtLib" "-Q" "/home/coq/.opam/4.13.1+flambda/lib/coq/user-contrib/Flocq" "Flocq" "-Q" "/home/coq/.opam/4.13.1+flambda/lib/coq/user-contrib/Ltac2" "Ltac2" "-Q" "/home/coq/.opam/4.13.1+flambda/lib/coq/user-contrib/MenhirLib" "MenhirLib" "-Q" "/home/coq/.opam/4.13.1+flambda/lib/coq/user-contrib/MetaCoq" "MetaCoq" "-Q" "/home/coq/.opam/4.13.1+flambda/lib/coq/user-contrib/Wasm" "Wasm" "-Q" "/home/coq/.opam/4.13.1+flambda/lib/coq/user-contrib/compcert" "compcert" "-Q" "/home/coq/.opam/4.13.1+flambda/lib/coq/user-contrib/mathcomp" "mathcomp" "-Q" "/home/coq/.opam/4.13.1+flambda/lib/coq/user-contrib/parseque" "parseque" "-top" "test_bug") -*- *)
(* File reduced by coq-bug-minimizer from original input, then from 27 lines to 14 lines, then from 27 lines to 1263 lines, then from 1266 lines to 132 lines, then from 145 lines to 747 lines, then from 749 lines to 133 lines, then from 146 lines to 1309 lines, then from 1288 lines to 561 lines, then from 574 lines to 954 lines, then from 957 lines to 560 lines, then from 573 lines to 2533 lines, then from 2530 lines to 580 lines, then from 593 lines to 1687 lines, then from 1687 lines to 582 lines, then from 595 lines to 1631 lines, then from 1636 lines to 596 lines, then from 609 lines to 831 lines, then from 836 lines to 596 lines, then from 609 lines to 637 lines, then from 642 lines to 598 lines, then from 611 lines to 881 lines, then from 884 lines to 703 lines, then from 716 lines to 787 lines, then from 792 lines to 744 lines, then from 757 lines to 830 lines, then from 835 lines to 752 lines, then from 765 lines to 832 lines, then from 837 lines to 759 lines, then from 772 lines to 814 lines, then from 819 lines to 770 lines, then from 783 lines to 805 lines, then from 809 lines to 769 lines, then from 782 lines to 898 lines, then from 901 lines to 809 lines, then from 814 lines to 811 lines, then from 824 lines to 809 lines, then from 822 lines to 5831 lines, then from 5835 lines to 853 lines, then from 866 lines to 2280 lines, then from 2285 lines to 891 lines, then from 896 lines to 893 lines *)
(* coqc version 8.19.2 compiled with OCaml 4.13.1
   coqtop version 8.19.2
   Expected coqc runtime on this file: 0.617 sec *)

Require Coq.ZArith.ZArith.
Require Coq.ssr.ssrbool.

Axiom proof_admitted : False.
Tactic Notation "admit" := abstract case proof_admitted.

Module compcert_DOT_lib_DOT_Coqlib_WRAPPED.
Module Export Coqlib.
Export Coq.ZArith.ZArith.
Export Coq.ZArith.Znumtheory.

Section POSITIVE_ITERATION.

End POSITIVE_ITERATION.

Section LIST_FOLD.

End LIST_FOLD.

Section FORALL2.

End FORALL2.

Section DECIDABLE_EQUALITY.

End DECIDABLE_EQUALITY.

Section DECIDABLE_PREDICATE.

End DECIDABLE_PREDICATE.

Section LEX_ORDER.

End LEX_ORDER.

End Coqlib.

End compcert_DOT_lib_DOT_Coqlib_WRAPPED.
Module Export compcert.
Module Export lib.
Module Coqlib.
Include compcert_DOT_lib_DOT_Coqlib_WRAPPED.Coqlib.
End Coqlib.
Module Export Integers.
Import compcert.lib.Coqlib.

Module Type WORDSIZE.
End WORDSIZE.

Module Make(WS: WORDSIZE).
Definition modulus : Z.
Admitted.

Record int: Type := mkint { intval: Z; intrange: -1 < intval < modulus }.

End Make.

Module Export Wordsize_32.
End Wordsize_32.

Module Export Wordsize_8.
End Wordsize_8.

Module Byte := Make(Wordsize_8).

Notation byte := Byte.int.

Module Export Wordsize_64.
End Wordsize_64.

Module Export Int64.

End Int64.

Module Export Wordsize_Ptrofs.
End Wordsize_Ptrofs.

Module Export Ptrofs.

Section AGREE32.

End AGREE32.

Section AGREE64.

End AGREE64.

End Ptrofs.

End Integers.
Module Export Category.
Class RawFunctor (F : Type -> Type) :=
  MkRawFunctor { _fmap : forall A B, (A -> B) -> (F A -> F B)
               }.

Class RawApplicative (F : Type -> Type) `{RawFunctor F} :=
  MkRawApplicative { _pure       : forall A, A -> F A
                   ; _app        : forall A B, F (A -> B) -> (F A -> F B)
                   }.
Definition pure {F : Type -> Type} `{RawApplicative F} {A : Type} : A -> F A.
Admitted.

Class RawAlternative (F : Type -> Type) `{RawApplicative F} :=
  MkRawAlternative { _fail : forall A, F A
                   ; _alt  : forall A, F A -> F A -> F A
                   }.
Definition alt {F : Type -> Type} `{RawAlternative F} {A : Type} : F A -> F A -> F A.
Admitted.

Class RawMonad (F : Type -> Type) `{RawApplicative F} :=
  MkRawMonad { _bind : forall A B, F A -> (A -> F B) -> F B }.
Definition bind {F : Type -> Type} `{RawMonad F} {A B : Type} :
  F A -> (A -> F B) -> F B.
Admitted.

Class RawMonadRun (F : Type -> Type) `{RawMonad F} :=
  MkRawMonadRun { _runMonad : forall A, F A -> list A }.
#[global]
Instance listRawFunctor : RawFunctor list.
Admitted.
#[global]
Instance listRawApplicative : RawApplicative list.
Admitted.
#[global]
Instance listRawAlternative : RawAlternative list.
Admitted.
#[global]
Instance listRawMonad : RawMonad list.
Admitted.
#[global]
Instance listRawMonadRun : RawMonadRun list.
Admitted.
Class EqDec (A : Type) := MkEqDec { eq_dec : forall (a b : A), { a = b } + { a <> b } }.
Section Indexed.

Context {I : Type} (T : Type) (A B : I -> Type).
Definition IArrow : I -> Type.
exact (fun i => A i -> B i).
Defined.
Definition IForall : Type.
exact (forall i, A i).
Defined.

End Indexed.
Notation "A :-> B" := (IArrow A B)   (at level 20, right associativity).
Notation "[ A ]"   := (IForall A)    (at level 70).
Import Coq.Arith.PeanoNat.

Record Box (A : nat -> Type) (n : nat) : Type :=
  MkBox { call : forall m, m < n -> A m }.

Arguments call {_} {_} _ {_}.

Definition Fix A (alg : [ Box A :-> A ]) : [ A ].
Admitted.

Definition View (As : nat -> Type) (A : Type) (n : nat) : Type :=
match n with
  | O    => False
  | S n' => A * As n'
end.

Class Sized As A : Type := MkSized { uncons {n} : As n -> option (View As A n) }.

Record SizedType {A : Type} (size : A -> nat) (n : nat) : Type :=
  MkSizedType { value : A
              ; sized : size value = n
              }.

Definition SizedList (A : Type) n := SizedType (@length A) n.

#[global]
Instance sizedList : forall (A : Type), Sized (SizedList A) A.
Admitted.
Module Export Success.

Record Success (Toks : nat -> Type) (Tok : Type) (A : Type) (n : nat) :=
  MkSuccess { value     : A
            ; size      : nat
            ; small     : size < n
            ; leftovers : Toks size
            }.

Arguments MkSuccess {_} {_} {_} {_} _ {_}.
Arguments value     {_} {_} {_} {_}.
Arguments small     {_} {_} {_} {_}.
Arguments leftovers {_} {_} {_} {_}.

Section Success.

Context {Toks : nat -> Type} {Tok : Type} {A B C : Type} {n : nat}.
Definition map (f : A -> B) : Success Toks Tok A n -> Success Toks Tok B n.
admit.
Defined.

Definition le_lift {m n : nat} (p : m <= n) (s : Success Toks Tok A m) :
  Success Toks Tok A n :=
  let small := Nat.le_trans _ _ _  (small s) p
  in MkSuccess (value s) small (leftovers s).

Definition lt_lift {m n : nat} (p : m < n) (s : Success Toks Tok A m) :
  Success Toks Tok A n := le_lift (Nat.lt_le_incl _ _ p) s.

End Success.
Module Export parseque.

Record Parser (Toks : nat -> Type) (Tok : Type)
              (M : Type -> Type) (A : Type) (n : nat) : Type :=
  MkParser { runParser {m} : m <= n -> Toks m -> M (Success Toks Tok A m) }.

Arguments MkParser {_} {_} {_} {_} {_}.
Arguments runParser {_} {_} {_} {_} {_} _ {_}.

Section Lower.

Context
  {Toks : nat -> Type} {Tok : Type}
  {M : Type -> Type}
  {A : Type} {m n : nat}.
Definition lt_lower (mltn : m < n) (p : Parser Toks Tok M A n) : Parser Toks Tok M A m.
Admitted.

End Lower.
Definition box {Toks Tok M A n} : Parser Toks Tok M A n -> Box (Parser Toks Tok M A) n.
Admitted.

Coercion box : Parser >-> Box.

Section Combinators1.

Context
  {Toks : nat -> Type} {Tok : Type} `{Sized Toks Tok}
  {M : Type -> Type} `{RawFunctor M} `{RawApplicative M} `{RawMonad M} `{RawAlternative M}
  {A B : Type} {n : nat}.
Definition map (f : A -> B) (p : Parser Toks Tok M A n) :
  Parser Toks Tok M B n.
Admitted.
Definition cmap (b : B) (p : Parser Toks Tok M A n) : Parser Toks Tok M B n.
Admitted.
Definition alt (p q : Parser Toks Tok M A n) : Parser Toks Tok M A n.
exact (MkParser (fun _ mlen toks =>
  alt (runParser p mlen toks) (runParser q mlen toks))).
Defined.

End Combinators1.

Section Combinators2.

Context
  {Toks : nat -> Type} {Tok : Type} `{Sized Toks Tok}
  {M : Type -> Type} `{RawFunctor M} `{RawApplicative M} `{RawMonad M} `{RawAlternative M}
  {A B : Type} {n : nat}.
Definition bind (p : Parser Toks Tok M A n)
  (q : A -> Box (Parser Toks Tok M B) n) : Parser Toks Tok M B n.
Admitted.
Definition rand (p : Parser Toks Tok M A n) (q : Box (Parser Toks Tok M B) n) :
  Parser Toks Tok M B n.
Admitted.

End Combinators2.

Section Combinators3.

Context
  {Toks : nat -> Type} {Tok : Type} `{Sized Toks Tok} `{EqDec Tok}
  {M : Type -> Type} `{RawFunctor M} `{RawApplicative M} `{RawMonad M} `{RawAlternative M}
  {A B C : Type} {n : nat}.
Definition app (p : Parser Toks Tok M (A -> B) n)
  (q : Box (Parser Toks Tok M A) n) : Parser Toks Tok M B n.
admit.
Defined.

End Combinators3.

Section HChainl.

Context
  {Toks : nat -> Type} {Tok : Type}
  {M : Type -> Type} `{RawFunctor M} `{RawApplicative M} `{RawMonad M} `{RawAlternative M}
  {A B : Type} {n : nat}.

Definition RChain (n : nat) : Type :=
  Parser Toks Tok M (A -> A) n -> Parser Toks Tok M A n -> Parser Toks Tok M A n.

Definition iterater_aux (n : nat) (rec : Box RChain n) :
  RChain n := fun op val => MkParser (fun _ mlen ts =>
  Category.bind (runParser op mlen ts) (fun sop =>
  let sopltn := Nat.le_trans _ _ _ (small sop) mlen in
  let op'    := lt_lower sopltn op in
  let val'   := lt_lower sopltn val in
  Category.bind (runParser (call rec sopltn op' val') (Nat.le_refl _) (leftovers sop)) (fun res =>
  pure (lt_lift (small sop) (Success.map (value sop) res))))).

Definition iterater {n : nat} (op : Parser Toks Tok M (A -> A) n)
  (val : Parser Toks Tok M A n) : Parser Toks Tok M A n :=
  Fix _ (fun n rec op val => alt (iterater_aux n rec op val) val) n op val.

End HChainl.

Notation "p <|> q"   := (alt p q)  (at level 60, right associativity).
Notation "f <$> p"   := (map f p)  (at level 59, right associativity).
Notation "p >>= q"   := (bind p q)     (at level 60, right associativity).
Notation "p  &> q"   := (rand p q)     (at level 50, left associativity).
Notation "p <*> q"   := (app p q)      (at level 50, left associativity).
Export Coq.ssr.ssrbool.

Set Implicit Arguments.

Definition axiom T (e : rel T) := forall x y, reflect (x = y) (e x y).

Structure mixin_of T := Mixin {op : rel T; _ : axiom op}.
Notation class_of := mixin_of (only parsing).

Section ClassDef.

Structure type := Pack {sort; _ : class_of sort}.

End ClassDef.
Coercion sort : type >-> Sortclass.
Notation eqType := type.

Module Export Wasm_int.

Module Make (WS: Integers.WORDSIZE).

Include Make (WS).

End Make.

Module Export Int32.
Include Make(Integers.Wordsize_32).
Definition i32 : eqType.
Admitted.
Definition i64 : eqType.
Admitted.
Definition f32 : eqType.
Admitted.
Definition f64 : eqType.
Admitted.
Import Coq.NArith.BinNat.
Definition u32 : Set.
Admitted.
Definition u8: Set.
Admitted.
Definition typeidx : Set.
Admitted.
Definition funcidx : Set.
Admitted.
Definition tableidx : Set.
Admitted.
Definition memidx : Set.
Admitted.
Definition globalidx : Set.
Admitted.
Definition elemidx : Set.
Admitted.
Definition dataidx : Set.
Admitted.
Definition localidx : Set.
Admitted.
Definition labelidx : Set.
Admitted.

Inductive value_num : Type :=
  | VAL_int32 : i32 -> value_num
  | VAL_int64 : i64 -> value_num
  | VAL_float32 : f32 -> value_num
  | VAL_float64 : f64 -> value_num
.

Inductive value_vec : Set :=
  | VAL_vec128: unit -> value_vec
.

Definition name := list Byte.byte.

Section Types.

Inductive number_type : Set :=
  | T_i32
  | T_i64
  | T_f32
  | T_f64
  .

Inductive vector_type : Set :=
| T_v128
.

Inductive reference_type : Set :=
| T_funcref
| T_externref
.

Inductive value_type: Set :=
| T_num: number_type -> value_type
| T_vec: vector_type -> value_type
| T_ref: reference_type -> value_type
| T_bot: value_type
.
Definition result_type : Set.
Admitted.

Inductive function_type :=
| Tf : result_type -> result_type -> function_type
.

Record limits : Set := {
  lim_min : u32;
  lim_max : option u32;
}.

Definition memory_type := limits.

Record table_type : Set := {
  tt_limits : limits;
  tt_elem_type : reference_type;
}.

Inductive mutability : Set :=
  | MUT_const
  | MUT_var
  .

Record global_type : Set :=  {
  tg_mut : mutability;
  tg_t : value_type
}.

Inductive block_type : Set :=
| BT_id: typeidx -> block_type
| BT_valtype: option value_type -> block_type
.

End Types.

Section Instructions.

Inductive sx : Set :=
  | SX_S
  | SX_U
  .

Inductive unop_i : Set :=
  | UOI_clz
  | UOI_ctz
  | UOI_popcnt
  .

Inductive unop_f : Set :=
  | UOF_abs
  | UOF_neg
  | UOF_sqrt
  | UOF_ceil
  | UOF_floor
  | UOF_trunc
  | UOF_nearest
  .

Inductive unop : Set :=
  | Unop_i : unop_i -> unop
  | Unop_f : unop_f -> unop
  | Unop_extend : N -> unop
  .

Inductive binop_i : Set :=
  | BOI_add
  | BOI_sub
  | BOI_mul
  | BOI_div : sx -> binop_i
  | BOI_rem : sx -> binop_i
  | BOI_and
  | BOI_or
  | BOI_xor
  | BOI_shl
  | BOI_shr : sx -> binop_i
  | BOI_rotl
  | BOI_rotr
  .

Inductive binop_f : Set :=
  | BOF_add
  | BOF_sub
  | BOF_mul
  | BOF_div
  | BOF_min
  | BOF_max
  | BOF_copysign
  .

Inductive binop : Set :=
  | Binop_i : binop_i -> binop
  | Binop_f : binop_f -> binop
  .

Inductive testop : Set :=
  | TO_eqz
  .

Inductive relop_i : Set :=
  | ROI_eq
  | ROI_ne
  | ROI_lt : sx -> relop_i
  | ROI_gt : sx -> relop_i
  | ROI_le : sx -> relop_i
  | ROI_ge : sx -> relop_i
  .

Inductive relop_f : Set :=
  | ROF_eq
  | ROF_ne
  | ROF_lt
  | ROF_gt
  | ROF_le
  | ROF_ge
  .

Inductive relop : Set :=
  | Relop_i : relop_i -> relop
  | Relop_f : relop_f -> relop
  .

Inductive cvtop : Set :=
  | CVO_wrap
  | CVO_extend
  | CVO_trunc
  | CVO_trunc_sat
  | CVO_convert
  | CVO_demote
  | CVO_promote
  | CVO_reinterpret
  .

Inductive packed_type : Set :=
  | Tp_i8
  | Tp_i16
  | Tp_i32
  .

Inductive shape_vec_i: Set :=
  | SVI_8_16
  | SVI_16_8
  | SVI_32_4
  | SVI_64_2
  .

Inductive shape_vec_f: Set :=
  | SVF_32_4
  | SVF_64_2
  .

Inductive shape_vec : Set :=
  | SV_ishape: shape_vec_i -> shape_vec
  | SV_fshape: shape_vec_f -> shape_vec
  .

Inductive unop_vec : Set :=
  | VUO_not
  .

Inductive binop_vec : Set :=
  | VBO_and
  .

Inductive ternop_vec : Set :=
  | VTO_bitselect
  .

Inductive test_vec : Set :=
  | VT_any_true
  .

Inductive shift_vec : Set :=
  | VSH_any_true
  .

Definition laneidx := u8.

Inductive packed_type_vec :=
  | Tptv_8_8
  | Tptv_16_4
  | Tptv_32_2
.

Inductive zero_type_vec :=
  | Tztv_32
  | Tztv_64
.

Inductive width_vec :=
  | Twv_8
  | Twv_16
  | Twv_32
  | Twv_64
  .

Inductive load_vec_arg :=
  | LVA_packed: packed_type_vec -> sx -> load_vec_arg
  | LVA_zero: zero_type_vec -> load_vec_arg
  | LVA_splat: width_vec -> load_vec_arg
  .

Record memarg : Set :=
  { memarg_offset : u32;
    memarg_align: u32
  }.

Inductive basic_instruction : Type :=

  | BI_const_num : value_num -> basic_instruction
  | BI_unop : number_type -> unop -> basic_instruction
  | BI_binop : number_type -> binop -> basic_instruction
  | BI_testop : number_type -> testop -> basic_instruction
  | BI_relop : number_type -> relop -> basic_instruction
  | BI_cvtop : number_type -> cvtop -> number_type -> option sx -> basic_instruction

  | BI_const_vec : value_vec -> basic_instruction
  | BI_unop_vec: unop_vec -> basic_instruction
  | BI_binop_vec: binop_vec -> basic_instruction
  | BI_ternop_vec: ternop_vec -> basic_instruction
  | BI_test_vec: test_vec -> basic_instruction
  | BI_shift_vec: shift_vec -> basic_instruction
  | BI_splat_vec: shape_vec -> basic_instruction
  | BI_extract_vec: shape_vec -> option sx -> laneidx -> basic_instruction
  | BI_replace_vec: shape_vec -> laneidx -> basic_instruction

  | BI_ref_null : reference_type -> basic_instruction
  | BI_ref_is_null
  | BI_ref_func : funcidx -> basic_instruction

  | BI_drop
  | BI_select : option (list value_type) -> basic_instruction

  | BI_local_get : localidx -> basic_instruction
  | BI_local_set : localidx -> basic_instruction
  | BI_local_tee : localidx -> basic_instruction
  | BI_global_get : globalidx -> basic_instruction
  | BI_global_set : globalidx -> basic_instruction

  | BI_table_get : tableidx -> basic_instruction
  | BI_table_set : tableidx -> basic_instruction
  | BI_table_size : tableidx -> basic_instruction
  | BI_table_grow : tableidx -> basic_instruction
  | BI_table_fill : tableidx -> basic_instruction
  | BI_table_copy : tableidx -> tableidx -> basic_instruction
  | BI_table_init : tableidx -> elemidx -> basic_instruction
  | BI_elem_drop : elemidx -> basic_instruction

  | BI_load : number_type -> option (packed_type * sx) -> memarg -> basic_instruction
  | BI_load_vec : load_vec_arg -> memarg -> basic_instruction

  | BI_load_vec_lane : width_vec -> memarg -> laneidx -> basic_instruction
  | BI_store : number_type -> option packed_type -> memarg-> basic_instruction
  | BI_store_vec_lane : width_vec -> memarg -> laneidx -> basic_instruction
  | BI_memory_size
  | BI_memory_grow
  | BI_memory_fill
  | BI_memory_copy
  | BI_memory_init: dataidx -> basic_instruction
  | BI_data_drop: dataidx -> basic_instruction

  | BI_nop
  | BI_unreachable
  | BI_block : block_type -> list basic_instruction -> basic_instruction
  | BI_loop : block_type -> list basic_instruction -> basic_instruction
  | BI_if : block_type -> list basic_instruction -> list basic_instruction -> basic_instruction
  | BI_br : labelidx -> basic_instruction
  | BI_br_if : labelidx -> basic_instruction
  | BI_br_table : list labelidx -> labelidx -> basic_instruction
  | BI_return
  | BI_call : funcidx -> basic_instruction
  | BI_call_indirect : tableidx -> typeidx -> basic_instruction
  | BI_return_call : funcidx -> basic_instruction
  | BI_return_call_indirect : tableidx -> typeidx -> basic_instruction
  .

Definition expr := list basic_instruction.

End Instructions.

Section Modules.

Inductive module_import_desc : Set :=
| MID_func : typeidx -> module_import_desc
| MID_table : table_type -> module_import_desc
| MID_mem : memory_type -> module_import_desc
| MID_global : global_type -> module_import_desc.

Record module_import : Set := {
  imp_module : name;
  imp_name : name;
  imp_desc : module_import_desc;
}.

Record module_func : Type := {
  modfunc_type : typeidx;
  modfunc_locals : list value_type;
  modfunc_body : expr;
}.

Record module_table : Set := {
  modtab_type : table_type;
}.

Record module_mem : Set := {
  modmem_type : memory_type;
}.

Record module_global : Type := {
  modglob_type : global_type;
  modglob_init : expr;
}.

Inductive module_elemmode : Type :=
| ME_passive
| ME_active : tableidx -> expr -> module_elemmode
| ME_declarative
.

Record module_element : Type := {
  modelem_type : reference_type;
  modelem_init : list expr;
  modelem_mode : module_elemmode;
}.

Inductive module_datamode : Type :=
| MD_passive
| MD_active : memidx -> expr -> module_datamode
.

Record module_data : Type := {
  moddata_init : list byte;
  moddata_mode : module_datamode;
}.

Record module_start : Set := {
  modstart_func : funcidx;
}.

Inductive module_export_desc : Set :=
| MED_func : funcidx -> module_export_desc
| MED_table : tableidx -> module_export_desc
| MED_mem : memidx -> module_export_desc
| MED_global : globalidx -> module_export_desc.

Record module_export : Set := {
  modexp_name : name;
  modexp_desc : module_export_desc;
}.

Record module : Type := {
  mod_types : list function_type;
  mod_funcs : list module_func;
  mod_tables : list module_table;
  mod_mems : list module_mem;
  mod_globals : list module_global;
  mod_elems : list module_element;
  mod_datas : list module_data;
  mod_start : option module_start;
  mod_imports : list module_import;
  mod_exports : list module_export;
}.

End Modules.
Import Coq.Strings.Byte.

Notation "p $> b" := (cmap b p) (at level 59, right associativity).

Section Language.

Context
  {Toks : nat -> Type} `{Sized Toks byte}
  {M : Type -> Type} `{RawMonad M} `{RawAlternative M}.

Definition byte_parser A n := Parser Toks byte M A n.
Definition exact_byte (b : byte) {n} : byte_parser byte n.
Admitted.
Definition parse_u32_as_int32 {n} : byte_parser Wasm_int.Int32.int n.
Admitted.
Definition parse_u32_zero_as_int32 {n} : byte_parser Wasm_int.Int32.int n.
Admitted.
Definition parse_vec_length {n} : byte_parser nat n.
Admitted.

Fixpoint parse_vec_aux {B} {n} (f : byte_parser B n) (k : nat)
  : byte_parser (list B) n :=
  match k with
  | 0 => (fun x => cons x nil) <$> f
  | S 0 => (fun x => cons x nil) <$> f
  | S k' => (cons <$> f) <*> parse_vec_aux f k'
  end.
Definition parse_vec {B} {n} (f : byte_parser B n) : byte_parser (list B) n.
exact ((parse_u32_zero_as_int32 $> nil) <|>
  (parse_vec_length >>= (fun k => parse_vec_aux f k))).
Defined.
Definition parse_function_type {n} : byte_parser function_type n.
Admitted.

Definition module_func_without_type : Type := (list value_type) * expr.
Definition parse_typesec {n} : byte_parser (list function_type) n.
exact (exact_byte x01 &> parse_u32_as_int32 &> parse_vec parse_function_type).
Defined.
Definition parse_magic {n} : byte_parser unit n.
Admitted.
Definition parse_version {n} : byte_parser unit n.
Admitted.
Definition parse_customsec_forget {A n} : byte_parser (A -> A) n.
Admitted.

Definition parse_with_customsec_star_before {A : Type} {n} f :=
  @iterater _ _ _ _ _ _ _ _ _ A n parse_customsec_forget f.

Record parsing_module : Type := {
  pmod_types : list function_type;
  pmod_funcs : list typeidx;
  pmod_tables : list module_table;
  pmod_mems : list module_mem;
  pmod_globals : list module_global;
  pmod_elems : list module_element;
  pmod_datas : list module_data;
  pmod_start : option module_start;
  pmod_imports : list module_import;
  pmod_exports : list module_export;
  pmod_code : list module_func_without_type;
}.
Definition merge_parsing_modules (m1 m2 : parsing_module) : parsing_module.
Admitted.
Definition parse_typesec_wrapper {n} : byte_parser parsing_module n.
exact ((fun types => {|
    pmod_types := types;
    pmod_funcs := nil;
    pmod_tables := nil;
    pmod_mems := nil;
    pmod_globals := nil;
    pmod_elems := nil;
    pmod_datas := nil;
    pmod_start := None;
    pmod_imports := nil;
    pmod_exports := nil;
    pmod_code := nil;
  |}) <$>
  (parse_with_customsec_star_before parse_typesec)).
Defined.
Definition end_marker : byte.
Admitted.
Definition parse_importsec_onwards {n} : byte_parser parsing_module n.
Admitted.
Definition parse_typesec_onwards {n} : byte_parser parsing_module n.
exact (((merge_parsing_modules <$> parse_typesec_wrapper) <*> parse_importsec_onwards) <|>
  parse_importsec_onwards).
Defined.
Definition module_of_parsing_module (m : parsing_module) : module.
Admitted.
Definition parse_module {n} : byte_parser module n.
exact (module_of_parsing_module <$>
  (parse_magic &>
  parse_version &>
  parse_typesec_onwards)).
Defined.

End Language.

Class Tokenizer (A : Type) : Type :=
  MkTokenizer { _tokenize : list byte -> list A }.
#[export]
Instance tokBytes : Tokenizer byte.
Admitted.

Section Run.

Context
  {M : Type -> Type} `{RawMonad M} `{RawAlternative M} `{RawMonadRun M}
  {Tok : Type} `{Tokenizer Tok}
  {A : Type}.
Definition run : list byte -> [ Parser (SizedList Tok) Tok M A ] -> option A.
Admitted.

End Run.
Definition run_parse_module (bs : list byte) : option module.
exact (run (bs ++ cons end_marker nil) (fun n => parse_module)).
Defined.

Declare ML Module "coq-certicoq.plugin".
Definition test_bytes : list Byte.byte.
Admitted.
Definition test_module : option module.
exact (run_parse_module test_bytes).
Defined.

CertiCoq Compile test_module.

4ever2 · 2024-11-05T13:24:13Z

Here's a further reduced version that only depends on MetaCoq.

Declare ML Module "coq-metacoq-erasure.plugin".

Inductive l (A : Type) : Type :=
| c : nat -> A -> l A.

Definition test := @c nat.

MetaCoq Erase test.

4ever2 · 2024-11-06T12:43:44Z

The bug seems to be in eta expansion, @c nat gets expanded to fun n : nat => fun H : n => c nat n H but the correct expansion should be fun n : nat => fun H : nat => c nat n H

4ever2 · 2024-11-06T14:22:29Z

Swapping the eta_single function in

metacoq/template-coq/theories/EtaExpand.v

Line 55 in c451d74

    
           Definition eta_single (t : Ast.term) (args : list Ast.term) (ty : Ast.term) (count : nat): term :=

with the one in

metacoq/erasure/theories/Typed/CertifyingEta.v

Line 50 in c451d74

Definition eta_single (Γ : list term)

fixes the issue in the minimized code. However, the original code still fails, the failure again looks to be due to eta expansion.

mattam82 · 2024-11-12T06:42:42Z

@4ever2 is #1117 fixing the original code as well?

4ever2 · 2024-11-12T09:08:37Z

@4ever2 is #1117 fixing the original code as well?

Yes, it also fixes the original code

This was referenced Oct 12, 2024

Test issue creation coq-community/run-coq-bug-minimizer#2

Closed

Test coqbot responses JasonGross/coq-tools#217

Closed

This comment was marked as duplicate.

Sign in to view

This was referenced Oct 16, 2024

opam version compatible with Coq 8.19 WasmCert/WasmCert-Coq#55

Closed

opam version compatible with Coq 8.17? CertiCoq/certicoq#102

Open

4ever2 mentioned this issue Nov 8, 2024

Fix substitution during eta expansion of partial application #1117

Merged

mattam82 closed this as completed in #1117 Nov 12, 2024

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Anomaly as a result of extraction in CertiCoq (assertion fails in ml code) #1072

Anomaly as a result of extraction in CertiCoq (assertion fails in ml code) #1072

mkarup commented Apr 1, 2024

mkarup commented Apr 15, 2024

mattam82 commented Jun 6, 2024

spitters commented Sep 16, 2024

mattam82 commented Oct 8, 2024 •

edited

Loading

JasonGross commented Oct 12, 2024

This comment was marked as duplicate.

JasonGross commented Oct 16, 2024

JasonGross commented Oct 16, 2024

mkarup commented Oct 17, 2024 •

edited

Loading

raoxiaojia commented Oct 17, 2024

JasonGross commented Oct 18, 2024

JasonGross commented Oct 18, 2024

JasonGross commented Oct 19, 2024 •

edited

Loading

4ever2 commented Nov 5, 2024 •

edited

Loading

4ever2 commented Nov 6, 2024

4ever2 commented Nov 6, 2024

mattam82 commented Nov 12, 2024

4ever2 commented Nov 12, 2024

Anomaly as a result of extraction in CertiCoq (assertion fails in ml code) #1072

Anomaly as a result of extraction in CertiCoq (assertion fails in ml code) #1072

Comments

mkarup commented Apr 1, 2024

mkarup commented Apr 15, 2024

mattam82 commented Jun 6, 2024

spitters commented Sep 16, 2024

mattam82 commented Oct 8, 2024 • edited Loading

JasonGross commented Oct 12, 2024

This comment was marked as duplicate.

JasonGross commented Oct 16, 2024

JasonGross commented Oct 16, 2024

mkarup commented Oct 17, 2024 • edited Loading

raoxiaojia commented Oct 17, 2024

JasonGross commented Oct 18, 2024

JasonGross commented Oct 18, 2024

JasonGross commented Oct 19, 2024 • edited Loading

4ever2 commented Nov 5, 2024 • edited Loading

4ever2 commented Nov 6, 2024

4ever2 commented Nov 6, 2024

mattam82 commented Nov 12, 2024

4ever2 commented Nov 12, 2024

mattam82 commented Oct 8, 2024 •

edited

Loading

mkarup commented Oct 17, 2024 •

edited

Loading

JasonGross commented Oct 19, 2024 •

edited

Loading

4ever2 commented Nov 5, 2024 •

edited

Loading