Uniqueness of variables in the environment

[zilinc]

@rossberg Is there any rule in the meta-semantics of SpecTec that requires all entries in the typing environment to be distinct? The VAR rule only checks existence:

rule Ok_exp/VAR:
  E |- VAR x : t
  -- if (x, t) <- E.EXP

which does not have the shadowing semantics.

Should such a check also be added to the IL validator? There are two cases that such non-fresh variable occur after some middle-end passes:

Example 1:

 ;; ../specification/wasm-3.0/1.1-syntax.values.spectec:133.6-133.13
relation tagsxx_is_wf: `%%`(var_0 : externidx*, ret_val : tagidx*)
  ;; ../specification/wasm-3.0/1.1-syntax.values.spectec:133.6-133.13
  rule tagsxx_is_wf_0{var_0 : externidx*, ret_val : tagidx*}:
    `%%`(var_0, ret_val)
    -- (wf_externidx: `%`(var_0))*{var_0 <- var_0}
    -- if (ret_val = $tagsxx(var_0))
    -- (wf_uN: `%%`(32, ret_val))*{ret_val <- ret_val}
}

After the undep pass, the problematic lowering {var_0 <- var_0} and {ret_val <- ret_val} are produced (this has been fixed by @DCupello1 in 52c7222), but this is not checked in the IL validator.

Example 2:

  ;; ../specification/wasm-3.0/4.0-execution.configurations.spectec:133.8-133.13
  rule instr_case_9{`labelidx*` : labelidx*, labelidx : labelidx}:
    `%`(BR_TABLE_instr(`labelidx*`, labelidx))
    -- (wf_uN: `%%`(32, labelidx))*{labelidx <- `labelidx*`}
    -- wf_uN: `%%`(32, labelidx)

This is also generated by the undep pass. The labelidx from the lowering conflicts with the top-level quantified one. IL validator doesn't reject this either. (@DCupello1 I think this should probably be fixed in the middle-end.)

The ultimate troublesome (but somewhat contrived) example is the following:

def $f(nat*) : bool
  ;; iter.spectec:2.1-3.19
  def $f{n : nat*}(n*{n <- n}) = true
    -- (if (n <- n*{n <- n}))*{n <- n}

[rossberg]

Ah, yes. Initially there basically were no local binders, so the question of shadowing variables didn't really arise. But now that has changed, so it needs to be resolved. Maybe disallowing shadowing would be the simplest choice, but I believe the EL elaborator does not enforce it at the moment.

[rossberg]

@zilinc, please see WebAssembly#2181.