Merge remote-tracking branch 'origin/main' into bdep_ecCircuitsRefactor

Author: Gustavo2622

scripts/docker/Dockerfile.base

@@ -2,11 +2,11 @@
 
 FROM debian:stable
 
-MAINTAINER Pierre-Yves Strub <[email protected]>
+LABEL org.opencontainers.image.maintainer="Pierre-Yves Strub <[email protected]>"
 
 ARG user=charlie
 
-ENV DEBIAN_FRONTEND noninteractive
+ENV DEBIAN_FRONTEND=noninteractive
 
 RUN \
 	apt-get -q -y update && \

scripts/docker/Dockerfile.formosa

@@ -0,0 +1,7 @@
+# syntax = devthefuture/dockerfile-x
+
+FROM ./Dockerfile.build as build-formosa
+
+RUN \
+	opam install --deps-only --confirm-level=unsafe-yes jasmin && \
+	opam clean

scripts/docker/Dockerfile.test

@@ -5,7 +5,6 @@ FROM ./Dockerfile.build
 ARG EC_VERSION=main
 
 RUN \
-	opam pin --dev-repo \
-	add -n easycrypt https://github.com/EasyCrypt/easycrypt.git#${EC_VERSION} && \
+	opam pin add -n easycrypt https://github.com/EasyCrypt/easycrypt.git#${EC_VERSION} && \
 	opam install -v easycrypt && \
 	rm -rf .opam/packages.dev/*

src/dune

@@ -1,7 +1,7 @@
 (env
  (dev     (flags :standard -rectypes -w @[email protected]@31..39@[email protected]@[email protected] -warn-error -a+31))
  (ci      (flags :standard -rectypes -w @[email protected]@31..39@[email protected]@[email protected] -warn-error +a))
- (release (flags :standard -rectypes)
+ (release (flags :standard -rectypes -w @[email protected]@31..39@[email protected]@[email protected] -warn-error -a)
           (ocamlopt_flags -O3 -unbox-closures)))
 
 

src/ecCoreModules.ml

@@ -494,6 +494,9 @@ type top_module_expr = {
   tme_loca : locality;
 }
 
+let is_me_body_alias (body : module_body) =
+  match body with ME_Alias _ -> true | _ -> false
+
 (* -------------------------------------------------------------------- *)
 let ur_hash = EcAst.ur_hash
 

src/ecCoreModules.mli

@@ -247,6 +247,8 @@ type top_module_expr = {
   tme_loca : locality;
 }
 
+val is_me_body_alias : module_body -> bool
+
 (* -------------------------------------------------------------------- *)
 val mty_equal :
   module_type ->

src/ecHiGoal.ml

@@ -1515,8 +1515,12 @@ let rec process_mintros_1 ?(cf = true) ttenv pis gs =
   and intro1_rw (_ : ST.state) (o, s) tc =
     let h = EcIdent.create "_" in
     let rwt tc =
-      let pt = PT.pt_of_hyp !!tc (FApi.tc1_hyps tc) h in
-      process_rewrite1_core ~close:false (s, None, o) pt tc
+      match LDecl.by_id h (FApi.tc1_hyps tc) with
+      | LD_hyp _ ->
+        let pt = PT.pt_of_hyp !!tc (FApi.tc1_hyps tc) h in
+        process_rewrite1_core ~close:false (s, None, o) pt tc
+      | _ ->
+        tc_error !!tc "top assumption is not an hypothesis";
     in t_seqs [t_intros_i [h]; rwt; t_clear h] tc
 
   and intro1_unfold (_ : ST.state) (s, o) p tc =

src/ecMatching.ml

@@ -837,19 +837,20 @@ let f_match_core opts hyps (ue, ev) f1 f2 =
     cb (odfl reduced (EcReduction.h_red_opt EcReduction.beta_red hyps reduced))
 
   and doit_mem _env mxs m1 m2 =
-    match EV.get m1 !ev.evm_mem with
-    | None ->
-        if not (EcMemory.mem_equal m1 m2) then
+    if not (EcMemory.mem_equal m1 m2) then begin
+      match EV.get m1 !ev.evm_mem with
+      | None ->
           raise MatchFailure
 
-    | Some `Unset ->
-        if Mid.mem m2 mxs then
-          raise MatchFailure;
-        ev := { !ev with evm_mem = EV.set m1 m2 !ev.evm_mem }
-
-    | Some (`Set m1) ->
-        if not (EcMemory.mem_equal m1 m2) then
-          raise MatchFailure
+      | Some `Unset ->
+          if Mid.mem m2 mxs then
+            raise MatchFailure;
+          ev := { !ev with evm_mem = EV.set m1 m2 !ev.evm_mem }
+
+      | Some (`Set m1) ->
+          if not (EcMemory.mem_equal m1 m2) then
+            raise MatchFailure
+  end
 
   and doit_bindings env (subst, mxs) q1 q2 =
     let doit_binding (env, subst, mxs) (x1, gty1) (x2, gty2) =