Purge all mentions of the word that must not be named

Previously we documented that when binding to theorem prover definitions, one
has to destinguish between 'a -> b' and 'a -> M b', for a Sail function 'a -> b'
Notably, this is because Sail does not infact use monads in any significant way,
so the information has to be given only when the rubber meets the theorem prover road.

For users of Sail who are not binding to custom theorem prover definitions, this is
mostly irrelevant, but this saves the pain of users pressing Ctrl+f "monad' in the
manual and leaving with misconceptions.

As part of this we change 'monadic' to 'impure' everywhere user-facing (which is barely
anywhere in the first place)

doc/asciidoc/language.adoc

@@ -1070,11 +1070,9 @@ Perhaps surprisingly for a specification language, Sail has exception
 support. This is because exceptions as a language feature do sometimes
 appear in vendor ISA pseudocode (they are a feature in Arm's ASL
 language), and such code would be very difficult to translate into
-Sail if Sail did not itself support exceptions. We already translate
-Sail to monadic theorem prover code, so working with a monad that
-supports exceptions is fairly natural. In practice Sail language-level
-exceptions end up being quite a nice tool for implementing processor
-exceptions in ISA specifications.
+Sail if Sail did not itself support exceptions. In practice Sail
+language-level exceptions end up being quite a nice tool for
+implementing processor exceptions in ISA specifications.
 
 For exceptions we have two language features: `throw` statements
 and `try`--`catch` blocks. The throw keyword takes a value of

doc/asciidoc/parser.sed

@@ -11,6 +11,7 @@
 /Mutual/d
 /Impl/d
 /LcurlyBar/d
+/Monadic/d
 
 s/Pragma/$LINE_DIRECTIVE/g
 s/Fixity/FIXITY_DEF/g
@@ -22,6 +23,7 @@ s/End/end/g
 s/Default/default/g
 s/Scattered/scattered/g
 s/Monadic/monadic/g
+s/Impure/impure/g
 s/Typedef/type/g
 s/Enum/enum/g
 s/With/with/g

doc/examples/riscv_duopod.sail

@@ -116,7 +116,7 @@ overload X = {rX, wX}
 $span end
 
 /* Accessors for memory */
-val MEMr = monadic { lem: "MEMr", coq: "MEMr", _ : "read_ram" } : forall 'n 'm, 'n >= 0.
+val MEMr = impure { lem: "MEMr", coq: "MEMr", _ : "read_ram" } : forall 'n 'm, 'n >= 0.
    (int('m), int('n), bits('m), bits('m)) -> bits(8 * 'n)
 
 val read_mem : forall 'n, 'n >= 0. (xlenbits, int('n)) -> bits(8 * 'n)

lib/concurrency_interface/common.sail

@@ -87,7 +87,7 @@ $include <concurrency_interface/emulator_memory.sail>
 
 $ifdef SYMBOLIC
 val sail_instr_announce
-  = monadic "instr_announce"
+  = impure "instr_announce"
   : forall 'n, 'n > 0.
   bits('n) -> unit
 $else
@@ -101,7 +101,7 @@ $endif
 
 $ifdef SYMBOLIC
 val sail_branch_announce
-  = monadic "branch_announce"
+  = impure "branch_announce"
   : forall 'addrsize, 'addrsize in {32, 64}.
   (int('addrsize), bits('addrsize)) -> unit
 $else
@@ -117,10 +117,10 @@ $endif
   call [sail_end_cycle], to increment the cycle count and indicate the
   end of the current instruction. Cycle 0 is reserved for
   initialisation before executing the first instruction. */
-val sail_end_cycle = monadic "cycle_count" : unit -> unit
+val sail_end_cycle = impure "cycle_count" : unit -> unit
 
 /*! Returns the current cycle count */
-val sail_get_cycle_count = monadic "get_cycle_count" : unit -> int
+val sail_get_cycle_count = impure "get_cycle_count" : unit -> int
 
 $ifdef SYMBOLIC
 val sail_reset_registers = pure "reset_registers" : unit -> unit

lib/concurrency_interface/emulator_memory.sail

@@ -93,14 +93,14 @@ $endif
 
 //! Read memory
 $iftarget isla
-val read_mem# = monadic "read_mem" : forall ('a: Type) 'n 'addrsize, 'n >= 0 & 'addrsize in {32, 64}.
+val read_mem# = impure "read_mem" : forall ('a: Type) 'n 'addrsize, 'n >= 0 & 'addrsize in {32, 64}.
     ('a, int('addrsize), bits('addrsize), int('n)) -> bits(8 * 'n)
 $else
 val read_mem# : forall ('a: Type) 'n 'addrsize, 'n >= 0 & 'addrsize in {32, 64}.
     ('a, int('addrsize), bits('addrsize), int('n)) -> bits(8 * 'n)
 
 $ifdef _EMULATOR_MEMORY_PRIMOPS
-val __read_mem# = monadic "emulator_read_mem" : forall 'n 'addrsize, 'n >= 0 & 'addrsize in {32, 64}.
+val __read_mem# = impure "emulator_read_mem" : forall 'n 'addrsize, 'n >= 0 & 'addrsize in {32, 64}.
     (int('addrsize), bits('addrsize), int('n)) -> bits(8 * 'n)
 
 function read_mem#(_, addrsize, addr, n) = __read_mem#(addrsize, addr, n)
@@ -109,14 +109,14 @@ $endif
 
 //! Read memory, but signal to the emulator that this is an ifetch read
 $iftarget isla
-val read_mem_ifetch# = monadic "read_mem_ifetch" : forall ('a: Type) 'n 'addrsize, 'n >= 0 & 'addrsize in {32, 64}.
+val read_mem_ifetch# = impure "read_mem_ifetch" : forall ('a: Type) 'n 'addrsize, 'n >= 0 & 'addrsize in {32, 64}.
     ('a, int('addrsize), bits('addrsize), int('n)) -> bits(8 * 'n)
 $else
 val read_mem_ifetch# : forall ('a: Type) 'n 'addrsize, 'n >= 0 & 'addrsize in {32, 64}.
     ('a, int('addrsize), bits('addrsize), int('n)) -> bits(8 * 'n)
 
 $ifdef _EMULATOR_MEMORY_PRIMOPS
-val __read_mem_ifetch# = monadic "emulator_read_mem_ifetch" : forall 'n 'addrsize, 'n >= 0 & 'addrsize in {32, 64}.
+val __read_mem_ifetch# = impure "emulator_read_mem_ifetch" : forall 'n 'addrsize, 'n >= 0 & 'addrsize in {32, 64}.
     (int('addrsize), bits('addrsize), int('n)) -> bits(8 * 'n)
 
 function read_mem_ifetch#(_, addrsize, addr, n) = __read_mem_ifetch#(addrsize, addr, n)
@@ -125,14 +125,14 @@ $endif
 
 //! Read memory, and signal to the emulator that this read should be treated as an exclusive access
 $iftarget isla
-val read_mem_exclusive# = monadic "read_mem_exclusive" : forall ('a: Type) 'n 'addrsize, 'n >= 0 & 'addrsize in {32, 64}.
+val read_mem_exclusive# = impure "read_mem_exclusive" : forall ('a: Type) 'n 'addrsize, 'n >= 0 & 'addrsize in {32, 64}.
     ('a, int('addrsize), bits('addrsize), int('n)) -> bits(8 * 'n)
 $else
 val read_mem_exclusive# : forall ('a: Type) 'n 'addrsize, 'n >= 0 & 'addrsize in {32, 64}.
     ('a, int('addrsize), bits('addrsize), int('n)) -> bits(8 * 'n)
 
 $ifdef _EMULATOR_MEMORY_PRIMOPS
-val __read_mem_exclusive# = monadic "emulator_read_mem_exclusive" : forall 'n 'addrsize, 'n >= 0 & 'addrsize in {32, 64}.
+val __read_mem_exclusive# = impure "emulator_read_mem_exclusive" : forall 'n 'addrsize, 'n >= 0 & 'addrsize in {32, 64}.
     (int('addrsize), bits('addrsize), int('n)) -> bits(8 * 'n)
 
 function read_mem_exclusive#(_, addrsize, addr, n) = __read_mem_exclusive#(addrsize, addr, n)
@@ -141,14 +141,14 @@ $endif
 
 //! Write memory
 $iftarget isla
-val write_mem# = monadic "write_mem" : forall ('a: Type) 'n 'addrsize, 'n > 0 & 'addrsize in {32, 64}.
+val write_mem# = impure "write_mem" : forall ('a: Type) 'n 'addrsize, 'n > 0 & 'addrsize in {32, 64}.
     ('a, int('addrsize), bits('addrsize), int('n), bits(8 * 'n)) -> bool
 $else
 val write_mem# : forall ('a: Type) 'n 'addrsize, 'n > 0 & 'addrsize in {32, 64}.
     ('a, int('addrsize), bits('addrsize), int('n), bits(8 * 'n)) -> bool
 
 $ifdef _EMULATOR_MEMORY_PRIMOPS
-val __write_mem# = monadic "emulator_write_mem" : forall 'n 'addrsize, 'n > 0 & 'addrsize in {32, 64}.
+val __write_mem# = impure "emulator_write_mem" : forall 'n 'addrsize, 'n > 0 & 'addrsize in {32, 64}.
     (int('addrsize), bits('addrsize), int('n), bits(8 * 'n)) -> bool
 
 function write_mem#(_, addrsize, addr, n, value) = __write_mem#(addrsize, addr, n, value)
@@ -157,22 +157,22 @@ $endif
 
 //! Write memory, and signal to the emulator that this read should be treated as an exclusive access
 $iftarget isla
-val write_mem_exclusive# = monadic "write_mem_exclusive" : forall ('a: Type) 'n 'addrsize, 'n > 0 & 'addrsize in {32, 64}.
+val write_mem_exclusive# = impure "write_mem_exclusive" : forall ('a: Type) 'n 'addrsize, 'n > 0 & 'addrsize in {32, 64}.
     ('a, int('addrsize), bits('addrsize), int('n), bits(8 * 'n)) -> bool
 $else
 val write_mem_exclusive# : forall ('a: Type) 'n 'addrsize, 'n > 0 & 'addrsize in {32, 64}.
     ('a, int('addrsize), bits('addrsize), int('n), bits(8 * 'n)) -> bool
 
 $ifdef _EMULATOR_MEMORY_PRIMOPS
-val __write_mem_exclusive# = monadic "emulator_write_mem_exclusive" : forall 'n 'addrsize, 'n > 0 & 'addrsize in {32, 64}.
+val __write_mem_exclusive# = impure "emulator_write_mem_exclusive" : forall 'n 'addrsize, 'n > 0 & 'addrsize in {32, 64}.
     (int('addrsize), bits('addrsize), int('n), bits(8 * 'n)) -> bool
 
 function write_mem_exclusive#(_, addrsize, addr, n, value) = __write_mem_exclusive#(addrsize, addr, n, value)
 $endif
 $endif
 
-val read_tag# = monadic "emulator_read_tag"  : forall 'addrsize, 'addrsize in {32, 64}. (int('addrsize), bits('addrsize)) -> bool
+val read_tag# = impure "emulator_read_tag"  : forall 'addrsize, 'addrsize in {32, 64}. (int('addrsize), bits('addrsize)) -> bool
 
-val write_tag# = monadic "emulator_write_tag" : forall 'addrsize, 'addrsize in {32, 64}. (int('addrsize), bits('addrsize), bool) -> unit
+val write_tag# = impure "emulator_write_tag" : forall 'addrsize, 'addrsize in {32, 64}. (int('addrsize), bits('addrsize), bool) -> unit
 
 $endif

lib/concurrency_interface/read_write.sail

@@ -271,7 +271,7 @@ with
 
 // Used when we want a non memory read/write to appear in Isla's addr relation
 $iftarget isla
-val sail_address_announce = monadic "address_announce" : forall 'addrsize, 'addrsize in {32, 64}. (int('addrsize), bits('addrsize)) -> unit
+val sail_address_announce = impure "address_announce" : forall 'addrsize, 'addrsize in {32, 64}. (int('addrsize), bits('addrsize)) -> unit
 $else
 val sail_address_announce : forall 'addrsize, 'addrsize in {32, 64}. (int('addrsize), bits('addrsize)) -> unit
 

lib/float.sail

@@ -79,10 +79,10 @@ val round_toward_positive = pure "round_toward_positive" : unit -> rounding_mode
 val round_toward_negative = pure "round_toward_negative" : unit -> rounding_mode
 val round_toward_zero = pure "round_toward_zero" : unit -> rounding_mode
 
-val undefined_float16 = monadic "fp16_undefined" : unit -> float16
-val undefined_float32 = monadic "fp32_undefined" : unit -> float32
-val undefined_float64 = monadic "fp64_undefined" : unit -> float64
-val undefined_float128 = monadic "fp128_undefined" : unit -> float128
+val undefined_float16 = impure "fp16_undefined" : unit -> float16
+val undefined_float32 = impure "fp32_undefined" : unit -> float32
+val undefined_float64 = impure "fp64_undefined" : unit -> float64
+val undefined_float128 = impure "fp128_undefined" : unit -> float128
 
 val fp16_nan = pure "fp16_nan" : unit -> float16
 val fp32_nan = pure "fp32_nan" : unit -> float32

lib/flow.sail

@@ -128,6 +128,6 @@ function __id forall 'n. (x: int('n)) -> int('n) = x
 
 overload __size = {__id}
 
-val __deref = monadic "reg_deref" : forall ('a : Type). register('a) -> 'a
+val __deref = impure "reg_deref" : forall ('a : Type). register('a) -> 'a
 
 $endif

lib/regfp.sail

@@ -222,55 +222,55 @@ union instruction_kind = {
 }
 
 val __read_mem
-  = monadic { ocaml: "Platform.read_mem", c: "platform_read_mem", _: "read_mem" }
+  = impure { ocaml: "Platform.read_mem", c: "platform_read_mem", _: "read_mem" }
   : forall 'n 'addrsize, 'n > 0 & 'addrsize in {32, 64}.
   (read_kind, int('addrsize), bits('addrsize), int('n)) -> bits(8 * 'n)
 
 val __read_memt
-  = monadic { ocaml: "Platform.read_memt", c: "platform_read_memt", _: "read_memt" }
+  = impure { ocaml: "Platform.read_memt", c: "platform_read_memt", _: "read_memt" }
   : forall 'n 'addrsize, 'n > 0 & 'addrsize in {32, 64}.
   (read_kind, bits('addrsize), int('n)) -> (bits(8 * 'n), bit)
 
 val __write_mem_ea
-  = monadic { ocaml: "Platform.write_mem_ea", c: "platform_write_mem_ea", _: "write_mem_ea" }
+  = impure { ocaml: "Platform.write_mem_ea", c: "platform_write_mem_ea", _: "write_mem_ea" }
   : forall 'n 'addrsize, 'n > 0 & 'addrsize in {32, 64}.
   (write_kind, int('addrsize), bits('addrsize), int('n)) -> unit
 
 val __write_mem
-  = monadic { ocaml: "Platform.write_mem", c: "platform_write_mem", _: "write_mem" }
+  = impure { ocaml: "Platform.write_mem", c: "platform_write_mem", _: "write_mem" }
   : forall 'n 'addrsize, 'n > 0 & 'addrsize in {32, 64}.
   (write_kind, int('addrsize), bits('addrsize), int('n), bits(8 * 'n)) -> bool
 
 val __write_memt
-  = monadic { ocaml: "Platform.write_memt", c: "platform_write_memt", _: "write_memt" }
+  = impure { ocaml: "Platform.write_memt", c: "platform_write_memt", _: "write_memt" }
   : forall 'n 'addrsize, 'n > 0 & 'addrsize in {32, 64}.
   (write_kind, bits('addrsize), int('n), bits(8 * 'n), bit) -> bool
 
 val __write_tag
-  = monadic { ocaml: "Platform.write_tag", c: "platform_write_tag", _: "write_tag" }
+  = impure { ocaml: "Platform.write_tag", c: "platform_write_tag", _: "write_tag" }
   : forall 'addrsize, 'addrsize in {32, 64}.
   (write_kind, bits('addrsize), bit) -> bool
 
 val __excl_res
-  = monadic { ocaml: "Platform.excl_res", c: "platform_excl_res", _: "excl_result" }
+  = impure { ocaml: "Platform.excl_res", c: "platform_excl_res", _: "excl_result" }
   : unit -> bool
 
 val __barrier
-  = monadic { ocaml: "Platform.barrier", c: "platform_barrier", _: "barrier" }
+  = impure { ocaml: "Platform.barrier", c: "platform_barrier", _: "barrier" }
   : barrier_kind -> unit
 
 val __branch_announce
-  = monadic { ocaml: "Platform.branch_announce", c: "platform_branch_announce", _ : "branch_announce" }
+  = impure { ocaml: "Platform.branch_announce", c: "platform_branch_announce", _ : "branch_announce" }
   : forall 'addrsize, 'addrsize in {32, 64}.
   (int('addrsize), bits('addrsize)) -> unit
 
 val __cache_maintenance
-  = monadic { ocaml: "Platform.cache_maintenance", c: "platform_cache_maintenance", _ : "cache_maintenance" }
+  = impure { ocaml: "Platform.cache_maintenance", c: "platform_cache_maintenance", _ : "cache_maintenance" }
   : forall 'addrsize, 'addrsize in {32, 64}.
   (cache_op_kind, int('addrsize), bits('addrsize)) -> unit
 
 val __instr_announce
-  = monadic { ocaml: "Platform.instr_announce", c: "platform_instr_announce", _: "instr_announce" }
+  = impure { ocaml: "Platform.instr_announce", c: "platform_instr_announce", _: "instr_announce" }
   : forall 'n, 'n > 0.
   bits('n) -> unit
 

src/lib/format_sail.ml

@@ -559,7 +559,7 @@ module Make (Config : CONFIG) = struct
              ( match vs.extern_opt with
              | Some extern ->
                  space ^^ char '=' ^^ space
-                 ^^ string (if extern.pure then "pure" else "monadic")
+                 ^^ string (if extern.pure then "pure" else "impure")
                  ^^ space
                  ^^ surround indent 1 (char '{')
                       (separate_map (char ',' ^^ break 1) doc_binding extern.bindings)

src/lib/lexer.mll

@@ -112,6 +112,7 @@ let kw_table =
      ("Order",                   (fun _ -> Order));
      ("Bool",                    (fun _ -> Bool));
      ("pure",                    (fun _ -> Pure));
+     ("impure",                  (fun _ -> Impure));
      ("monadic",                 (fun _ -> Monadic));
      ("register",		 (fun _ -> Register));
      ("return",                  (fun _ -> Return));

src/lib/parser.mly

@@ -222,7 +222,7 @@ let old_bitfield_deprecated ?(bitfield = "<bitfield>") l field =
     ("Old bitfield syntax, use '" ^ replace ^ "' instead")
 
 let warn_extern_effect l =
-  Reporting.warn ~once_from:__POS__ "Deprecated" l "All external bindings should be marked as either monadic or pure"
+  Reporting.warn ~once_from:__POS__ "Deprecated" l "All external bindings should be marked as either pure or impure"
 
 let forwards_mapcl_deprecated l =
   Reporting.warn ~once_from:__POS__ "Deprecated" l "Single direction mapping clause should be prefixed by a direction, either forwards or backwards"
@@ -236,7 +236,7 @@ let set_syntax_deprecated l =
 
 %token And As Assert Bitzero Bitone By Match Clause Dec Default Effect End Op
 %token Enum Else False Forall Foreach Overload Function_ Mapping If_ In Inc Let_ Int Order Bool Cast
-%token Pure Monadic Register Return Scattered Sizeof Struct Then True TwoCaret TYPE Typedef
+%token Pure Impure Monadic Register Return Scattered Sizeof Struct Then True TwoCaret TYPE Typedef
 %token Undefined Union Newtype With Val Outcome Constraint Throw Try Catch Exit Bitfield Constant
 %token Repeat Until While Do Mutual Var Ref Configuration TerminationMeasure Instantiation Impl Private
 %token InternalPLet InternalReturn InternalAssume
@@ -1178,6 +1178,8 @@ outcome_spec_def:
 pure_opt:
   | Monadic
     { false }
+  | Impure
+    { false }
   | Pure
     { true }
 

test/c/cheri_capreg.sail

@@ -9,7 +9,7 @@ $include <vector_dec.sail>
 
 val "reg_deref" : forall ('a : Type). register('a) -> 'a
 /* sneaky deref with no effect necessary for bitfield writes */
-val _reg_deref = monadic "reg_deref" : forall ('a : Type). register('a) -> 'a
+val _reg_deref = impure "reg_deref" : forall ('a : Type). register('a) -> 'a
 
 val zeros_0 = pure "zeros" : forall 'n. int('n) -> bits('n)
 

test/format/default/val.expect

@@ -1,8 +1,8 @@
 default Order dec
 $include <prelude.sail>
 
-val foo = monadic { _: "foo" } : unit -> unit // foo
-val bar = monadic { c: "foo_c", _: "foo" } : (
+val foo = impure { _: "foo" } : unit -> unit // foo
+val bar = impure { c: "foo_c", _: "foo" } : (
         unit,
         unit,
         unit,

test/format/val.sail

@@ -1,9 +1,9 @@
 default Order dec
 $include <prelude.sail>
 
-val foo = monadic { _: "foo" } : unit -> unit // foo
+val foo = impure { _: "foo" } : unit -> unit // foo
 
-val bar = monadic { c: "foo_c", _: "foo" } : (unit, unit, unit, vector(16, dec, vector(32, dec, int)), unit, unit, unit, vector(32, dec, int)) -> unit
+val bar = impure { c: "foo_c", _: "foo" } : (unit, unit, unit, vector(16, dec, vector(32, dec, int)), unit, unit, unit, vector(32, dec, int)) -> unit
 
 val baz : unit -> unit // baz
 val quuz : unit -> unit

test/ocaml/reg_passing/reg_passing.sail

@@ -3,7 +3,7 @@ register R1 : int
 register R2 : int
 register R3 : int
 
-val __deref = monadic "reg_deref" : forall ('a : Type). register('a) -> 'a effect {rreg}
+val __deref = impure "reg_deref" : forall ('a : Type). register('a) -> 'a effect {rreg}
 
 val output = {
     ocaml: "(fun (str, n) -> print_endline (str ^ Big_int.to_string n))",

test/typecheck/fail/add_vec_lit_old.sail

@@ -1,9 +1,9 @@
 default Order inc
 
-val add_vec = monadic {ocaml: "add_vec", lem: "add_vec"}: forall ('n : Int).
+val add_vec = impure {ocaml: "add_vec", lem: "add_vec"}: forall ('n : Int).
   (bitvector('n, inc), bitvector('n, inc)) -> bitvector('n, inc)
 
-val add_range = monadic {ocaml: "add_range", lem: "add_range"}: forall ('n : Int) ('m : Int) ('o : Int) ('p : Int).
+val add_range = impure {ocaml: "add_range", lem: "add_range"}: forall ('n : Int) ('m : Int) ('o : Int) ('p : Int).
   (range('n, 'm), range('o, 'p)) -> range('n + 'o, 'm + 'p)
 
 val cast unsigned : forall ('n : Int).

test/typecheck/pass/bool_constraint/v1.expect

@@ -2,7 +2,7 @@
 27 |val my_not = {coq: "negb", _: "not"} : forall ('p : Bool). bool('p) -> {('q : Bool), 'p <--> not('q). bool('q)}
    |           ^-----------------------^
    | 
-All external bindings should be marked as either monadic or pure
+All external bindings should be marked as either pure or impure
 
 Type error:
 pass/bool_constraint/v1.sail:12.19-20:

test/typecheck/pass/bool_constraint/v2.expect

@@ -2,7 +2,7 @@
 27 |val my_not = {coq: "negb", _: "not"} : forall ('p : Bool). bool('p) -> {('q : Bool), 'p <--> not('q). bool('q)}
    |           ^-----------------------^
    | 
-All external bindings should be marked as either monadic or pure
+All external bindings should be marked as either pure or impure
 
 Type error:
 pass/bool_constraint/v2.sail:38.4-32:

test/typecheck/pass/bool_constraint/v3.expect

@@ -2,7 +2,7 @@
 27 |val my_not = {coq: "negb", _: "not"} : forall ('p : Bool). bool('p) -> {('q : Bool), 'p <--> 'q. bool('q)}
    |           ^-----------------------^
    | 
-All external bindings should be marked as either monadic or pure
+All external bindings should be marked as either pure or impure
 
 Type error:
 pass/bool_constraint/v3.sail:46.4-32:

test/typecheck/pass/bool_constraint/v4.expect

@@ -2,7 +2,7 @@
 27 |val my_not = {coq: "negb", _: "not"} : forall ('p : Bool). bool('p) -> {('q : Bool), 'p <--> not('q). bool('q)}
    |           ^-----------------------^
    | 
-All external bindings should be marked as either monadic or pure
+All external bindings should be marked as either pure or impure
 
 Type error:
 pass/bool_constraint/v4.sail:46.4-32: