`FAILWITH` should be allowed in `ITER`, `LOOP`, and `LOOP_LEFT`
If my understanding of script_ir_translator is correct, the Mi-Cho-Coq typer is a bit too restrictive; the following cases should be allowed but are currently rejected:
ITER { FAILWITH }
LOOP { FAILWITH }
LOOP_LEFT { FAILWITH }
However, DIP { FAILWITH }
seems always forbidden in Tezos and allowed in Mi-Cho-Coq where FAILWITH
is allowed.
There are mainly three files to edit to fix this:
-
syntax.v
: the propagation of thetff
flag for these instructions -
typer.v
: the type checker -
untyper.v
: the correctness proof of the type checker
Edited by Raphaël Cauderlier