Loose typing of instructions in block contexts.

[Keyholder]

Greetings! I'm currently working on a pretty esoteric derivative of your project, that requires additional statements about its internals (particularly, proving run_one_step_ctx to be not just some reduce implementation, but the only possible one). So, on my way there I need to tighten eval_ctx class with additional property to look like this:

    Class eval_ctx (ctx_t: Type): Type :=
      {
        ctx_fill: list administrative_instruction -> ctx_t -> list administrative_instruction;
        ctx_frame_mask: ctx_t -> frame -> frame;
        ctx_frame_cond: ctx_t -> frame -> frame -> Prop;
        ctx_reduce: forall (ctx: ctx_t) hs s f es hs' s' f' es',
          ctx_frame_cond ctx f f' ->
          reduce hs s (ctx_frame_mask ctx f) es hs' s' (ctx_frame_mask ctx f') es' ->
          reduce hs s f (ctx_fill es ctx) hs' s' f' (ctx_fill es' ctx);
        ctx_expand: forall (ctx: ctx_t) hs s f es hs' s' f' es',
          ctx_frame_cond ctx f f' ->
          reduction_possible s f es -> (* checking shape of es for validity *)
          reduce hs s f (ctx_fill es ctx) hs' s' f' (ctx_fill es' ctx) ->
          reduce hs s (ctx_frame_mask ctx f) es hs' s' (ctx_frame_mask ctx f') es';
      }.

The problem is, that while trying to prove ctx_expand for various contexts I'm starting to feel that in many places typing of instruction sequences is somewhat too loose, but I'm not sure if this is deliberate or not. The most glaring example is, probably, definition of lholed. In datatypes.v it is defined as:

Inductive lholed : nat -> Type :=
| LH_base : list value -> list administrative_instruction -> lholed 0
| LH_rec {k: nat}: list value -> nat -> list administrative_instruction -> lholed k -> list administrative_instruction -> lholed (S k)
.

I'm really struggling to understand, why I see list administrative_instruction here and not simply expr? It seems that at no point of deductions right parts of a hole can contain anything but AI_basic wrappers. Any administrative instruction created in the hole either stays in the hole until destruction, or falls through into values part as reference. So, why not simply

Inductive lholed : nat -> Type :=
| LH_base : list value -> expr -> lholed 0
| LH_rec {k: nat}: list value -> nat -> expr -> lholed k -> expr -> lholed (S k)
.

Am I missing some hidden reason? Tighter instruction type here would really help with required proofs.

[raoxiaojia]

This is where the specification is slightly ambiguous, as in both places 'instr' are stated, which is later 'extended to include administrative insturctions' later in the specification.

Considering the actual execution semantics, you are right that in the current version of semantics, the continuation of the label can be restricted from administrative_instruction to expr, since it can only be generated from expanding block-like constructs.

The other part:

It seems that at no point of deductions right parts of a hole can contain anything but AI_basic wrappers.

is not completely true -- consider e.g. table.fill which pushes two copies of the ref values to later part of the stack (and one of them is to the right of some active instructions to be resolved), whose runtime representation are not part of the basic instructions (since they refer to store addresses directly). I think the above category is the only family of violations in the current version of semantics though, so e.g. Label/Frames cannot be in the right parts of a hole indeed.

The issue is that, in principle, there's no inherent mechanism that prevents the specification from introducing some new instructions that violate either of the above properties in the future, so we tend to keep as close as possible to what the spec actually states instead of making inferences. In fact, the boundary between instructions and admin instructions becomes even less vague in Wasm 3.0, so this change might be in the opposite direction of where the specification seems to be going.

What is the concrete statement you're trying to prove when you said

proving run_one_step_ctx to be not just some reduce implementation, but the only possible one

? Note that Wasm's semantics is not deterministic, so there certainly can be other non-equivalent implementations of the interpreter on the non-det parts.

[Keyholder]

Damn, right you are - I have missed table.fill somehow. Well, that answers my question fully - conformance to spec comes before type snugness, considering scope of your project. Really unfortunate for me, though - my ctx_expand becomes much, MUCH weirder if we can't discard impossible right parts of the hole by simple type restriction. In my case, it may be easier to just drop table.fill from the list of supported instructions and try tightening types anyways.

You see, stuff I'm working on is really experimental, so full conformance to spec is sort of low on the list of priorities. Also, yes, I understand that WASM semantics is non-deterministic. Moreover, I'm extending it with new non-deterministic instructions. If you are curious, you can find theoretical background of my project here - what I'm trying to do, is to showcase usage of controllable non-determinism as a vehicle to express formal specifications (HOL-equivalent in terms of descriptive power) of algorithms in the same languages they are written in, albeit slightly extended. Naturally, your WASM mechanization is a perfect playground for such endeavor.

So, when I'm talking about run_one_step_ctx here, it is not exactly yours definition - mine has one additional parameter of finite type clue, responsible for selection of particular reduction out of whole non-deterministic spectrum. For my theory to work, two statements need to be proven: a) wrong clue can make run_one_step_ctx fail, but can not make it choose illegal reduction, and b) for every legal reduction there should be a clue, that makes run_one_step_ctx produce it. Your mechanization essentially has a) with minor cleanup, but b) is a very different beast.

[raoxiaojia]

It should be possible to assume a simpler context (i.e. the one you suggested, with expr replacing admin instructions) if you remove the bulk table/memory instructions -- those are the only instructions I can think of in the current version of Wasm.

The idea of the interpreter taking an additional clue for choosing its evaluation path is quite interesting! This will probably work nicely for Wasm since its non-determinism is currently quite limited. The only sources are basically table/memory.grow (2 possible outcomes only), and payload of NaN in some arithmetic operations. I can imagine a design where the interpreter simply passes down the clue to the individual auxiliary operations (e.g. arithmetic ops), which can then provably return all possible results depending on what the clue is. This might be a natural way to encode a 'definitional' interpreter even for a non-deterministic language! Pinging @conrad-watt regarding our previous discussion on this.

[Keyholder]

It should be possible to assume a simpler context (i.e. the one you suggested, with expr replacing admin instructions) if you remove the bulk table/memory instructions -- those are the only instructions I can think of in the current version of Wasm.

Yeah, currently that's what I hope for.

The idea of the interpreter taking an additional clue for choosing its evaluation path is quite interesting! This will probably work nicely for Wasm since its non-determinism is currently quite limited. The only sources are basically table/memory.grow (2 possible outcomes only), and payload of NaN in some arithmetic operations. I can imagine a design where the interpreter simply passes down the clue to the individual auxiliary operations (e.g. arithmetic ops), which can then provably return all possible results depending on what the clue is. This might be a natural way to encode a 'definitional' interpreter even for a non-deterministic language!

Exactly! In my vision (fuel: nat) parameter of run_multi_step_ctx can be replaced with (path: list clue), simultaneously serving both as structural recursion guard and as breadcrumbs for non-deterministic choices along the way. Then such interpreter can be indeed proven to be the only possible implementation of reduction rules, and my theory will have the ability to reason about whole spaces of possible computations.