Both backends are asked whether they store where the render said they do

The x86 block asks the break loop's questions of an --x86 host so that the two
sets of answers can be read against each other rather than merely found
plausible. A store is where they could most easily differ: the place forms the
walk ends at are lowered by each backend's own `place', and the two disagree
about an Option — which is why what may be written is settled in session.ml
above both of them and not in either. So the same slot is written, read back,
and refused for a type that does not fit, on this backend too.

And `Check.expressions' carries the comment that was written for the function
it replaced; the one-expression entry beside it has its own line.

lib/check.ml

@@ -7068,30 +7068,30 @@ let instances_since env mark =
   List.rev
     (List.filteri (fun i _ -> i < fresh) env.instances)
 
-(* One expression, checked against a program that is already running. The
-   frame is empty — a REPL expression has no parameters and no enclosing
-   function — so the slots it needs are whatever its own [let]s allocate.
+(* Expressions checked against a program that is already running, all of them
+   into *one* frame. It is empty to start with — a REPL expression has no
+   parameters and no enclosing function — so the slots it ends up with are
+   whatever their own [let]s allocate.
 
-   [want] is the inspector's write verb and nothing else: [C-x C-e] has no
-   expectation to offer, but a store into a slot of type [f32] does, and the
-   whole value of passing it is that [3] arrives as an [f32] rather than as an
-   [i32] the store would then have to be refused for. The expectation flows
-   through [check] the way it flows anywhere — that is what bidirectional
-   means — and [expect] at the end is what catches the cases that ignore it,
-   so the refusal is the checker's own "expected f32, found string" and not a
-   second sentence written here that would drift from it. *)
-(* Several of them against one frame, which is what the inspector's write verb
-   needs and what it must not build by hand. Two expressions checked
-   separately each number their slots from zero, so splicing them into one
-   thunk would have the second one's [let] reading and writing the first
-   one's storage — a frame that is two frames wearing one frame's clothes.
-   Sharing the [ctx] is the whole of the fix, and it is a fix because there is
-   exactly one allocator of slot indices in this compiler and it is this
-   record's counter.
+   One frame and not one each, which is what the inspector's write verb needs
+   and what it must not assemble by hand. Two expressions checked separately
+   both number their slots from zero, so splicing them into one thunk would
+   have the second one's [let] reading and writing the first one's storage — a
+   frame that is two frames wearing one frame's clothes. Sharing the [ctx] is
+   the whole of the fix, and it is a fix because there is exactly one allocator
+   of slot indices in this compiler and it is this record's counter.
 
-   The expressions are otherwise independent: nothing binds a name for the
-   next one, because the list is a list of values being stored and not a
-   sequence. *)
+   They are otherwise independent: none of them binds a name for the next,
+   because the list is a list of values being stored and not a sequence.
+
+   [want] is the write verb too, and [C-x C-e] passes none: a store into a
+   slot of type [f32] has an expectation to offer and a typed expression does
+   not. The whole value of passing it is that [3] arrives as an [f32] rather
+   than as an [i32] the store would then have to be refused for. It flows
+   through [check] the way an expectation flows anywhere — that is what
+   bidirectional means — and [expect] at the end catches the arms that ignore
+   it, so the refusal is the checker's own "expected f32, found string" rather
+   than a second sentence written here that would drift from it. *)
 let expressions env (es : (Types.t option * Ast.expr) list) :
   Tast.expr list * Types.t array * string option array =
   let ctx =
@@ -7113,6 +7113,7 @@ let expressions env (es : (Types.t option * Ast.expr) list) :
   (ts, Array.of_list (List.rev ctx.slot_tys),
    Array.of_list (List.rev ctx.slot_names))
 
+(* The one-expression case, which is every caller but the write verb. *)
 let expression env ?want (e : Ast.expr) :
   Tast.expr * Types.t array * string option array =
   match expressions env [ (want, e) ] with

test/test_dev.ml

@@ -4487,6 +4487,33 @@ let () =
         else if Wire.string_field r "value" <> Some "(Point {.x 1.5 .y 2.5})" then
           fail "x86 inspect of slot 2 answered %S"
             (Option.value ~default:"" (Wire.string_field r "value"));
+        (* And the write half of the same root, for the reason this whole block
+           exists: the two backends must answer the same. A store is where they
+           could most easily not — the place forms the walk ends at are lowered
+           by each backend's own [place], and the two disagree about an Option,
+           which is why what may be written is settled in [session.ml] above
+           both of them rather than in either. *)
+        let r =
+          request c
+            "(:op \"set\" :frame 0 :slot 2 :path (\"y\") :edits ((:code \"6.5\")))"
+        in
+        if status r <> "ok" then fail "x86 set: %s" (said r)
+        else if Wire.string_field r "value" <> Some "6.5" then
+          fail "x86 set of p.y answered %S"
+            (Option.value ~default:"" (Wire.string_field r "value"));
+        let r = request c "(:op \"inspect\" :frame 0 :slot 2)" in
+        if Wire.string_field r "value" <> Some "(Point {.x 1.5 .y 6.5})" then
+          fail "x86: the store did not land where the render says it did: %S"
+            (Option.value ~default:"" (Wire.string_field r "value"));
+        (* A refusal that comes from above both backends reads the same here
+           as it does there, which is the claim rather than the refusal. *)
+        let r =
+          request c
+            "(:op \"set\" :frame 0 :slot 2 :path (\"y\") :edits ((:code \"\\\"no\\\"\")))"
+        in
+        if status r <> "error" || not (contains_sub (said r) "expected f32") then
+          fail "x86: a value of the wrong type was not refused by the checker: %s"
+            (said r);
         (* And the globals, which are not in the frame at all -- they are found
            through the same descriptor's fingerprint, and a frame whose
            [refsig] disagreed with what the daemon recomputes would refuse