Inconsistency in validating global

[ShinWonho]

Validation in the specification

When validating globals, it uses context C' which only contains imported globals igt in the global field.

Validation in the gc reference interpreter

let check_global (c : context) (glob : global) : context =
  ...
  {c with globals = c.globals @ [gtype]}

let check_list f xs (c : context) : context =
  List.fold_left f c xs

let check_module (m : module_) =
  ...
  let c =
    {empty_context with refs}
    ...
    |> check_list check_global m.it.globals
    ...

However, the gc reference interpreter continuously updates context and validates globals using the updated context.

Inconsistency

I check the following wasm module with wat2wasm in wabt and the gc reference interpreter

;; inconsistency.wat
(module (global i32 (i32.const 0)) (global i32 (global.get 0)))

Because this gc proposal contains function references and tail-call proposals, I enable all of them and run wat2wasm. wat2wasm raise type error, while reference interpreter doesn't.

$ wabt/bin/wat2wasm --enable-function-references --enable-tail-call --enable-gc inconsistency.wat
inconsistency.wat:1:60: error: initializer expression can only reference an imported global
(module (global i32 (i32.const 0)) (global i32 (global.get 0)))
                                                           ^
$ gc/interpreter/wasm inconsistency.wat
// terminates normally

[rossberg]

The typing rule for modules that you quote invokes a special rule for typing sequences of globals, which is defined here (or when you click on the turnstile). That updates the context incrementally, just like the interpreter does. This is different from iterating individual invocations as done for other entities.

So AFAICS there is no inconsistency between spec and interpreter, merely a bug in wat2wasm.

[ShinWonho]

Oh, the specification also updates the context in validating the sequence of globals. I missed that. Thank you for the comment!