fix: circuit simplify and extens must not prove false judgements

src/ecCircuits.ml

@@ -1009,12 +1009,16 @@ let circ_simplify_form_bitstring_equality
   let env = toenv hyps in
   let st = Option.default (create_state (EcEnv.gstate env)) st in
 
+  (* An equality that the circuits prove valid (under [pres]) is replaced
+     by [true]. Any other one is kept: it may still hold in some states,
+     and replacing it by [false] would be unsound under a negation (or on
+     the left of an implication). *)
   let rec check (f : form) =
     match EcFol.sform_of_form f with
     | SFeq (f1, f2)
       when (Option.is_some @@ EcEnv.Circuit.lookup_bitstring env f1.f_ty)
            || (Option.is_some @@ EcEnv.Circuit.lookup_array env f1.f_ty) ->
-      f_bool (circuit_simplify_equality ~st ~hyps ~pres f1 f2)
+      if circuit_simplify_equality ~st ~hyps ~pres f1 f2 then f_true else f
     | _ -> f_map (fun ty -> ty) check f
   in
   check f

src/phl/ecPhlBDep.ml

@@ -357,6 +357,14 @@ let t_extens (v : string option) (tt : backward) (tc : tcenv1) =
         | `Bitstring {ofint} :: _ -> ofint
         | _ -> tc_error (tc1_penv tc) "Only finite size bitstring supported"
       in
+      (* Each instance replaces [v] by a constant in the program, the
+         precondition and the postcondition. The postcondition reads [v]
+         in the final memory: this is only sound if the program does not
+         write [v]. *)
+      if EcPV.PV.mem_pv (tc1_env tc) (pv_loc v.v_name)
+           (EcPV.s_write (tc1_env tc) hs.hs_s) then
+        tc_error (tc1_penv tc)
+          "extens: the program writes the variable %s" v.v_name;
       let ngoals = 1 lsl size in
       List.init ngoals (fun i ->
           let subst =

tests/circuits/circuit_soundness.ec

@@ -0,0 +1,40 @@
+require import AllCore List QFABV.
+type W8.
+op to_bits : W8 -> bool list.
+op from_bits : bool list -> W8.
+op of_int : int -> W8.
+op to_uint : W8 -> int.
+op to_sint : W8 -> int.
+bind bitstring to_bits from_bits to_uint to_sint of_int W8 8.
+realize gt0_size by admit.
+realize tolistP by admit.
+realize oflistP by admit.
+realize touintP by admit.
+realize tosintP by admit.
+realize ofintP by admit.
+realize size_tolist by admit.
+
+(* [circuit simplify] replaces an equality by [true] when the circuits prove
+   it valid, and keeps it otherwise: replacing it by [false] would be
+   unsound under a negation. *)
+module M = {
+  proc f(x : W8) = { return x; }
+
+  proc g(x : W8) = { x <- of_int 0; return x; }
+
+  proc h(x : W8, y : W8) = { y <- x; return y; }
+}.
+
+lemma simplify_neg : hoare[M.f : true ==> !(res = of_int 0)].
+proof. proc. circuit simplify. fail by trivial. abort.
+
+lemma simplify_valid (x_ : W8) : hoare[M.f : x = x_ ==> res = x_].
+proof. proc. circuit simplify. trivial. qed.
+
+(* [extens [x]] substitutes [x] in the postcondition, read in the final
+   memory: it requires the program not to write [x]. *)
+lemma extens_written : hoare[M.g : x = of_int 1 ==> res = of_int 1].
+proof. proc. fail extens [x] : (wp; skip; smt()). abort.
+
+lemma extens_ok (x_ : W8) : hoare[M.h : x = x_ ==> res = x_].
+proof. proc. extens [x] : (wp; skip; smt()). qed.