From ab5cc67105668fb681b91b5d9fe9c42c489861ca Mon Sep 17 00:00:00 2001
From: Vincent Laporte <Vincent.Laporte@inria.fr>
Date: Fri, 30 Jan 2026 14:52:48 +0100
Subject: [PATCH 1/5] Docs: fix syntax of memory accesses
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Co-authored-by: Jean-Christophe Léchenet <jean-christophe.lechenet@inria.fr>
---
 docs/source/language/syntax/expressions.md | 19 +++++++++++--------
 1 file changed, 11 insertions(+), 8 deletions(-)

diff --git a/docs/source/language/syntax/expressions.md b/docs/source/language/syntax/expressions.md
index 93efad600e..1625abe10f 100644
--- a/docs/source/language/syntax/expressions.md
+++ b/docs/source/language/syntax/expressions.md
@@ -4,13 +4,16 @@
   | <int>  // Integer constant.
   | <bool>  // Boolean constant.
   | <var>  // Variable.
-  | (<wsize>)[<var> + <expr>] // Memory access.
-  | (<wsize>)[<var> - <expr>] // Memory access.
+  | [<expr>] // Memory access.
+  | [:<wsize> <expr>] // Memory access.
   | <var>[<expr>]  // Array access.
-  | <var>[<wsize> <expr>]  // Array access.
-  | <var>.[<wsize> <expr>]  // Unscaled array access.
-  | <var>[<wsize> <expr> : <expr>]  // Subarray.
-  | <var>.[<wsize> <expr> : <expr>]  // Unscaled subarray.
+  | <var>[:<wsize> <expr>]  // Array access.
+  | <var>.[<expr>]  // Unscaled array access.
+  | <var>.[:<wsize> <expr>]  // Unscaled array access.
+  | <var>[<expr> : <expr>]  // Subarray.
+  | <var>[:<wsize> <expr> : <expr>]  // Subarray.
+  | <var>.[<expr> : <expr>]  // Unscaled subarray.
+  | <var>.[:<wsize> <expr> : <expr>]  // Unscaled subarray.
   | <op1> <expr>  // Unary operation.
   | <expr> <op2> <expr>  // Binary operation.
   | <expr> ? <expr> : <expr>  // Conditional.
@@ -26,8 +29,8 @@ Expressions are made of:
   - packs (`(4u2)[0, 3, 2, 1]`);
   - variables (`x`);
   - parenthesized subexpressions (`(e)`);
-  - memory loads (`(u16)[p + 2 * i]`);
-  - array accesses (`x[i]`);
+  - memory loads (`[:u16 p + 2 * i]`);
+  - array accesses (`x[i]`, `x.[i]`, `x[:u16 i]`);
   - unary operators (`- e`);
   - binary operators (`e - f`);
   - conditional expressions (`c ? th : el`);

From 52b7ee493ecc699076db4c758e8bbe7c5e60871d Mon Sep 17 00:00:00 2001
From: Vincent Laporte <Vincent.Laporte@inria.fr>
Date: Fri, 30 Jan 2026 13:30:15 +0100
Subject: [PATCH 2/5] WArray.uincl is decidable

---
 proofs/lang/warray_.v | 24 ++++++++++++++++++++++++
 1 file changed, 24 insertions(+)

diff --git a/proofs/lang/warray_.v b/proofs/lang/warray_.v
index c46c6cb425..558bfa7a58 100644
--- a/proofs/lang/warray_.v
+++ b/proofs/lang/warray_.v
@@ -227,6 +227,30 @@ Module WArray.
 
   End WITH_POINTER_DATA.
 
+  Definition is_uincl x y (a: array x) (b: array y) : bool :=
+    (x == y) &&
+    (all (fun i => match read a Aligned i U8, read b Aligned i U8 with Ok p, Ok q => p == q | Ok _, Error _ => false | Error _, _ => true end) (ziota 0 x)).
+
+  Lemma is_uinclP x y (a: array x) (b: array y) :
+    reflect (uincl a b) (is_uincl a b).
+  Proof.
+    rewrite /uincl /is_uincl.
+    case: (x =P y); last by right; tauto.
+    move => ?; subst; case: allP => h; [ left | right ].
+    - split; first by [].
+      move => i w; rewrite /read /= is_align8 add_0 /=; t_xrbindP => _ p ok_p <- <-.
+      move: h => /(_ i); rewrite in_ziota => /(_ (get_valid8 ok_p)).
+      rewrite /read /= is_align8 add_0 ok_p /=.
+      by case: get8 => //= => ? /eqP <-.
+    case => _ k; apply: h => i; rewrite in_ziota => i_bounds.
+    move: k => /(_ i).
+    rewrite /read /= is_align8 add_0 /=.
+    case: get8; last by [].
+    move => x /(_ _ erefl).
+    case: get8; last by [].
+    by move => /= ? /ok_inj <-.
+  Qed.
+
   Lemma castK len (a:array len) : WArray.cast len a = ok a.
   Proof. by rewrite /cast eqxx; case: a. Qed.
 

From ac26ab6b3bb458b3fb554de84703c83d6251777a Mon Sep 17 00:00:00 2001
From: Vincent Laporte <Vincent.Laporte@inria.fr>
Date: Tue, 27 Jan 2026 06:45:51 +0100
Subject: [PATCH 3/5] Add literal byte arrays

---
 compiler/src/alias.ml                    |  1 +
 compiler/src/printer.ml                  |  2 ++
 compiler/src/toEC.ml                     |  5 +++++
 proofs/compiler/constant_prop.v          | 11 ++++-------
 proofs/compiler/constant_prop_proof.v    |  7 ++-----
 proofs/compiler/propagate_inline.v       |  2 +-
 proofs/compiler/propagate_inline_proof.v |  5 ++++-
 proofs/compiler/slh_lowering_proof.v     | 16 ++++++++--------
 proofs/lang/expr.v                       |  2 ++
 proofs/lang/psem_core.v                  |  2 +-
 proofs/lang/sem_op_typed.v               |  3 +++
 11 files changed, 33 insertions(+), 23 deletions(-)

diff --git a/compiler/src/alias.ml b/compiler/src/alias.ml
index 9f4e778e46..acb06d4567 100644
--- a/compiler/src/alias.ml
+++ b/compiler/src/alias.ml
@@ -207,6 +207,7 @@ let slice_of_pexpr a =
   | Parr_init _ -> None
   | Pvar x -> Some (normalize_gvar a x)
   | Psub (aa, ws, len, x, i) -> Some (normalize_asub a aa ws len x i)
+  | PappN (Oarray _, _) -> hierror_no_loc "stack literal arrays are not supported"
   | (Pconst _ | Pbool _ | Pget _ | Pload _ | Papp1 _ | Papp2 _ | PappN _ ) -> assert false
   | Pif _ -> hierror_no_loc "conditional move of (ptr) arrays is not supported yet"
 
diff --git a/compiler/src/printer.ml b/compiler/src/printer.ml
index eee3930b09..59044f19f8 100644
--- a/compiler/src/printer.ml
+++ b/compiler/src/printer.ml
@@ -54,6 +54,8 @@ let pp_ge ~debug (pp_len: 'len pp) (pp_var: 'len gvar pp) : 'len gexpr pp =
     F.fprintf fmt "@[(%du%n)[%a]@]" (List.length es) (int_of_pe pe) (pp_list ",@ " (pp_expr NoAssoc priority_min)) es
   | PappN (Ocombine_flags c, es) ->
     F.fprintf fmt "@[%s(%a)@]" (string_of_combine_flags c) (pp_list ",@ " (pp_expr NoAssoc priority_min)) es
+  | PappN (E.Oarray len, es) ->
+     F.fprintf fmt "/* %du8 */ @[{ %a }@]" (Conv.int_of_pos len) (pp_list ",@ " (pp_expr NoAssoc priority_min)) es
   | Pif(_, e,e1,e2) ->
      let p = priority_ternary in
      optparent fmt prio side p "%a ? %a : %a" (pp_expr Left p) e (pp_expr NoAssoc p) e1 (pp_expr Right p) e2
diff --git a/compiler/src/toEC.ml b/compiler/src/toEC.ml
index 67c58af59c..d81690a535 100644
--- a/compiler/src/toEC.ml
+++ b/compiler/src/toEC.ml
@@ -1451,6 +1451,11 @@ module EcExpression(EA: EcArray): EcExpression = struct
                   ec_ident (Printer.string_of_combine_flags c),
                   List.map (toec_expr env) es
               )
+          | Oarray len ->
+              Eapp (
+                  EA.of_list env U8 (Conv.int_of_pos len),
+                  [Elist (List.map (toec_expr env) es)]
+              )
           end
       | Pif(_,e1,et,ef) ->
           let ty = ty_expr e in
diff --git a/proofs/compiler/constant_prop.v b/proofs/compiler/constant_prop.v
index 4bf0285929..b51725fb79 100644
--- a/proofs/compiler/constant_prop.v
+++ b/proofs/compiler/constant_prop.v
@@ -288,13 +288,10 @@ Definition app_sopn := app_sopn of_expr.
 Arguments app_sopn {A} ts _ _.
 
 Definition s_opN (op:opN) (es:pexprs) : pexpr :=
-  match app_sopn _ (sem_opN_typed op) es with
-  | Ok r =>
-    match op return sem_t (eval_atype (type_of_opN op).2) -> _ with
-    | Opack ws _ => fun w => Papp1 (Oword_of_int ws) (Pconst (wunsigned w))
-    | Ocombine_flags _ => fun b => Pbool b
-    end r
-  | _ => PappN op es
+  match op, app_sopn _ (sem_opN_typed op) es with
+  | Opack ws _, Ok w => Papp1 (Oword_of_int ws) (Pconst (wunsigned w))
+  | Ocombine_flags _, Ok b => Pbool b
+  | _, _ => PappN op es
   end.
 
 Definition s_if t e e1 e2 :=
diff --git a/proofs/compiler/constant_prop_proof.v b/proofs/compiler/constant_prop_proof.v
index fd1ab52696..0c05fb3183 100644
--- a/proofs/compiler/constant_prop_proof.v
+++ b/proofs/compiler/constant_prop_proof.v
@@ -488,14 +488,11 @@ Proof.
 
 Opaque app_sopn values.app_sopn.
   rewrite /s_opN.
+  case: op => [ sz' pe | // | c ];
   case h: app_sopn => [r | //].
-  case: op r h => [sz' pe | c] /=.
-
-  + move=> w h.
-    rewrite /sem_sop1 /= wrepr_unsigned /sem_opN /=.
+  + rewrite /= /sem_sop1 /= wrepr_unsigned /sem_opN /=.
     by rewrite -Let_Let (app_sopnP _ h).
 
-  move=> b h.
   rewrite /sem_opN /=.
   by rewrite -Let_Let (app_sopnP s h).
 Transparent app_sopn values.app_sopn.
diff --git a/proofs/compiler/propagate_inline.v b/proofs/compiler/propagate_inline.v
index 613cb3b996..5091579861 100644
--- a/proofs/compiler/propagate_inline.v
+++ b/proofs/compiler/propagate_inline.v
@@ -91,7 +91,7 @@ Fixpoint pi_e (pi:pimap) (e:pexpr) :=
   | PappN o es         => 
     let es := (map (pi_e pi) es) in
     match o with
-    | Opack _ _ => PappN o es
+    | Opack _ _ | Oarray _ => PappN o es
     | Ocombine_flags c => scfc c es
     end
   | Pif t e e1 e2      => Pif t (pi_e pi e) (pi_e pi e1) (pi_e pi e2)
diff --git a/proofs/compiler/propagate_inline_proof.v b/proofs/compiler/propagate_inline_proof.v
index 1b2d503739..87c4c42206 100644
--- a/proofs/compiler/propagate_inline_proof.v
+++ b/proofs/compiler/propagate_inline_proof.v
@@ -247,10 +247,13 @@ Proof.
   + move=> op e1 hrec1 e2 hrec2 v; t_xrbindP => ve1 /hrec1 [ve1' -> hu1] ve2 /hrec2 [ve2' -> hu2] /= hs.
     by rewrite (vuincl_sem_sop2 hu1 hu2 hs); eauto.
   + move=> o es hrec ?; t_xrbindP => ? /hrec [vs' hs' hu].
-    case: o => [wz pe | c] /=.
+    case: o => [wz pe | len | c] /=.
     + move=> ho; rewrite -/(sem_pexprs wdb gd _ (pi_es pi es)) hs' /=.
       rewrite (vuincl_sem_opN hu ho).
       by eexists; first by reflexivity.
+    + move => /(vuincl_sem_opN hu).
+      rewrite -/(sem_pexprs wdb gd s) hs' /= => ->.
+      by eexists; first reflexivity.
     move=> ho; have ho' := vuincl_sem_opN hu ho.
     by rewrite -/(pi_es pi es) (scfcP hs' ho'); eauto.
   move=> ?? hrec ? hrec1 ? hrec2 v; t_xrbindP.
diff --git a/proofs/compiler/slh_lowering_proof.v b/proofs/compiler/slh_lowering_proof.v
index 82cd755549..ad468786b8 100644
--- a/proofs/compiler/slh_lowering_proof.v
+++ b/proofs/compiler/slh_lowering_proof.v
@@ -144,14 +144,14 @@ Section CONST_PROP.
       by rewrite (use_mem_s_op2 _ h0 h1).
 
     - rewrite /s_opN.
-      case: app_sopn; first by case: opn.
-      move=> _.
-      elim: es h hindes => //= e es hind /norP [he hes] hindes.
-      rewrite negb_or.
-      rewrite (hindes _ _ he) /=; last by left.
-      apply: (hind hes) => e' he'.
-      apply: hindes.
-      by right.
+      have ih : ~~ has use_mem [seq const_prop_e None cpm i | i <- es].
+      + elim: es h hindes => //= e es hind /norP [he hes] hindes.
+        rewrite negb_or.
+        rewrite (hindes _ _ he) /=; last by left.
+        apply: (hind hes) => e' he'.
+        apply: hindes.
+        by right.
+      case: opn => [ sz' pe | len | c ] => //; by case: app_sopn.
 
     rewrite /s_if /=.
     move: h => /norP [] /norP [] /hinde h /hinde0 h0 /hinde1 h1.
diff --git a/proofs/lang/expr.v b/proofs/lang/expr.v
index 49cb0da695..272735bd1b 100644
--- a/proofs/lang/expr.v
+++ b/proofs/lang/expr.v
@@ -128,6 +128,7 @@ Variant combine_flags :=
 #[only(eqbOK)] derive
 Variant opN :=
 | Opack of wsize & pelem (* Pack words of size pelem into one word of wsize *)
+| Oarray of positive (* Literal array of bytes *)
 | Ocombine_flags of combine_flags
 .
 
@@ -332,6 +333,7 @@ Definition type_of_opN (op: opN) : seq atype * atype :=
   | Opack ws p =>
     let n := nat_of_wsize ws %/ nat_of_pelem p in
     (nseq n aint, aword ws)
+  | Oarray len => (nseq (Pos.to_nat len) (aword U8), aarr U8 len)
   | Ocombine_flags c => (tin_combine_flags, abool)
   end.
 
diff --git a/proofs/lang/psem_core.v b/proofs/lang/psem_core.v
index 27a219d0a9..647ae80bcb 100644
--- a/proofs/lang/psem_core.v
+++ b/proofs/lang/psem_core.v
@@ -920,7 +920,7 @@ Proof.
   have -> /= := vuincl_sopn _ hvs ok_q.
   + by eauto.
   case: {q ok_q} op => //.
-  by move => sz n; rewrite /= all_map all_nseq orbT.
+  all: by move => *; rewrite /= all_map all_nseq orbT.
 Qed.
 
 Lemma sem_opN_truncate_val o vs v :
diff --git a/proofs/lang/sem_op_typed.v b/proofs/lang/sem_op_typed.v
index e5c4e7f858..d96c823bf9 100644
--- a/proofs/lang/sem_op_typed.v
+++ b/proofs/lang/sem_op_typed.v
@@ -188,6 +188,9 @@ Definition sem_opN_typed (o: opN) :
   | Opack sz pe =>
       let ty := curry (A := cint) (sz %/ pe) (λ vs, ok (wpack sz pe vs)) in
       ecast l (sem_prod l _) (esym (map_nseq _ _ _)) ty
+  | Oarray len =>
+      let ty := curry (A := cword U8) (Pos.to_nat len) (λ bs, WArray.fill len (rev bs)) in
+      ecast l (sem_prod l _) (esym (map_nseq _ _ _)) ty
   | Ocombine_flags cf =>
       fun b0 b1 b2 b3 => ok (sem_combine_flags cf b0 b1 b2 b3)
   end.

From eb09e959d0e10279af52db0745087e43ec73ba41 Mon Sep 17 00:00:00 2001
From: Vincent Laporte <Vincent.Laporte@inria.fr>
Date: Thu, 29 Jan 2026 15:41:00 +0100
Subject: [PATCH 4/5] Remove-global handle literal arrays

---
 proofs/compiler/compiler_proof.v       |   3 +-
 proofs/compiler/it_compiler_proof.v    |   2 +-
 proofs/compiler/remove_globals.v       |  69 +++-
 proofs/compiler/remove_globals_proof.v | 455 ++++++++++++++++++-------
 4 files changed, 388 insertions(+), 141 deletions(-)

diff --git a/proofs/compiler/compiler_proof.v b/proofs/compiler/compiler_proof.v
index 4f60f08432..6603089987 100644
--- a/proofs/compiler/compiler_proof.v
+++ b/proofs/compiler/compiler_proof.v
@@ -345,7 +345,8 @@ Proof.
          ok_fvars).
   apply: compose_pass.
   + by move=> vr'; apply: load_constants_progP; apply ok_plc.
-  apply: compose_pass; first by move => vr'; apply: (RGP.remove_globP ok_pi).
+  apply: compose_pass_uincl'.
+  - move => vr'; apply: (RGP.remove_globP ok_pi).
   apply: compose_pass_uincl'.
   - move => vr'; apply: (live_range_splittingP ok_ph).
   apply: compose_pass.
diff --git a/proofs/compiler/it_compiler_proof.v b/proofs/compiler/it_compiler_proof.v
index e4692b67a8..e28cdc5be0 100644
--- a/proofs/compiler/it_compiler_proof.v
+++ b/proofs/compiler/it_compiler_proof.v
@@ -207,7 +207,7 @@ apply: wiequiv_f_trans_EE_EU.
 apply: wiequiv_f_trans_UU_EU; first exact: it_indirect_to_direct.
 apply: wiequiv_f_trans_EE_EU; first exact: (it_expand_callP ok_pg ok_fn).
 apply: wiequiv_f_trans_EU_EU; first exact: it_live_range_splittingP ok_ph.
-apply: wiequiv_f_trans_EE_EU; first exact: RGP.it_remove_globP ok_pi.
+apply: wiequiv_f_trans_EU_EU; first exact: RGP.it_remove_globP ok_pi.
 apply: wiequiv_f_trans_EE_EU; first exact: (it_load_constants_progP ok_plc).
 apply: wiequiv_f_trans_EE_EU; first exact:
   (hlop_it_lower_callP
diff --git a/proofs/compiler/remove_globals.v b/proofs/compiler/remove_globals.v
index be3ad89f19..17336409f0 100644
--- a/proofs/compiler/remove_globals.v
+++ b/proofs/compiler/remove_globals.v
@@ -3,16 +3,23 @@ From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssralg.
 From mathcomp Require Import word_ssrZ.
 From Coq Require Import ZArith.
 Require Import xseq.
+Require Import psem_defs.
 Require Import expr compiler_util.
 
+Definition type_of_glob_value (gv: glob_value) : atype :=
+  match gv with
+  | Gword ws _ => aword ws
+  | Garr p _ => aarr U8 p
+  end.
+
 Local Open Scope seq_scope.
 
 Module Import E.
 
   Definition pass : string := "remove globals".
 
-  Definition rm_glob_error (ii:instr_info) (x:var) := {|
-    pel_msg := pp_box [:: pp_s "Cannot remove global variable"; pp_var x];
+  Definition rm_glob_error_gen (ii: instr_info) (x: var) (extra: seq pp_error) := {|
+    pel_msg := pp_box (pp_s "Cannot remove global variable" :: pp_var x :: extra);
     pel_fn := None;
     pel_fi := None;
     pel_ii := Some ii;
@@ -21,6 +28,8 @@ Module Import E.
     pel_internal := false
   |}.
 
+  Definition rm_glob_error ii x := rm_glob_error_gen ii x [::].
+
   Definition rm_glob_error_dup (ii:instr_info) (x:var) := {|
     pel_msg := pp_box [:: pp_s "Duplicate definition of global variable"; pp_var x];
     pel_fn := None;
@@ -41,32 +50,47 @@ Section REMOVE.
 
   Context `{asmop:asmOp}.
   Context (fresh_id : glob_decls -> var -> Ident.ident).
+  Context {fcp : FlagCombinationParams}.
 
   Notation venv := (Mvar.t var).
 
-  Definition check_data (d:glob_value) (ws:wsize) (w:word ws) := 
-    match d with
-    | @Gword ws' w' => (ws == ws') && (w == zero_extend ws w')
-    | _             => false
+  Definition check_data (d' d: glob_value) : bool :=
+    match d', d with
+    | @Gword ws' w', @Gword ws w => (ws == ws') && (w == zero_extend ws w')
+    | @Garr len' arr', @Garr len arr => WArray.is_uincl arr arr'
+    | _, _ => false
     end.
 
-  Definition find_glob ii (xi:var_i) (gd:glob_decls) (ws:wsize) (w:word ws) :=
-    let test (gv:glob_decl) := 
-      if convertible (aword ws) (vtype gv.1) && (check_data gv.2 w) then Some gv.1
-      else None in 
+  Definition check (gv: glob_value) (gd: glob_decl) : bool :=
+    (convertible (type_of_glob_value gv) (vtype gd.1)) && (check_data gd.2 gv).
+
+  Definition find_glob ii (xi: var_i) (gd: glob_decls) (gv: glob_value) :=
+    let test gd := if check gv gd then Some gd.1 else None in
     match find_map test gd with
     | None => Error (rm_glob_error ii xi)
     | Some g => ok g
-    end. 
+    end.
 
-  Definition add_glob ii (x:var) (gd:glob_decls) (ws:wsize) (w:word ws) :=
-    let test (gv:glob_decl) := 
-       convertible (aword ws) (vtype gv.1) && (check_data gv.2 w) in
-    if has test gd then ok gd 
+  Definition add_glob ii (x: var) (gd: glob_decls) (gv: glob_value) :=
+    if has (check gv) gd then ok gd
     else
       let gx := {| vtype := vtype x; vname := fresh_id gd x |} in
       if has (fun g' => g'.1 == gx) gd then Error (rm_glob_error_dup ii gx)
-      else ok ((gx, Gword w) :: gd).
+      else ok ((gx, gv) :: gd).
+
+  Definition evaluate_bytes ii x : pexprs -> result pp_error_loc values :=
+    mapM (fun pe =>
+      if pe is Papp1 (Oword_of_int sz) (Pconst z)
+      then ok (Vword (wrepr sz z))
+      else Error (rm_glob_error_gen ii x [:: pp_s "a cell has a non-constant value"; pp_e pe ])
+    ).
+
+  Definition array_from_cells ii x (len: positive) (cells: pexprs) : result pp_error_loc (WArray.array len) :=
+    Let bytes := evaluate_bytes ii x cells in
+    match sem_opN (Oarray len) bytes >>= to_arr len with
+    | Ok array => Ok _ array
+    | Error _ => Error (rm_glob_error_gen ii x [:: pp_s "cannot fill the array"])
+    end.
 
   Fixpoint extend_glob_i  (i:instr) (gd:glob_decls) :=
     let (ii,i) := i in
@@ -77,7 +101,10 @@ Section REMOVE.
         let x := xi.(v_var) in
         if is_glob_var x then
           match e with
-          | Papp1 (Oword_of_int ws) (Pconst z) => add_glob ii x gd (wrepr ws z)
+          | Papp1 (Oword_of_int ws) (Pconst z) => add_glob ii x gd (Gword (wrepr ws z))
+          | PappN (Oarray len) cells =>
+              Let array := array_from_cells ii x len cells in
+              add_glob ii x gd (Garr array)
           | _                   => Error (rm_glob_error ii xi)
           end
         else ok gd
@@ -248,9 +275,15 @@ Section REMOVE.
               match e with
               | Papp1 (Oword_of_int ws) (Pconst z) =>
                 if convertible ty (aword ws) && convertible (vtype x) (aword ws) then
-                  Let g := find_glob ii xi gd (wrepr ws z) in
+                  Let g := find_glob ii xi gd (Gword (wrepr ws z)) in
                   ok (Mvar.set env x g, [::])
                 else Error (rm_glob_error ii xi)
+              | PappN (Oarray len) cells =>
+                  if convertible (vtype x) (aarr U8 len) then
+                    Let array := array_from_cells ii x len cells in
+                    Let g := find_glob ii xi gd (Garr array) in
+                    ok (Mvar.set env x g, [::])
+                  else Error (rm_glob_error ii xi)
               | _ => Error (rm_glob_error ii xi)
               end
             else
diff --git a/proofs/compiler/remove_globals_proof.v b/proofs/compiler/remove_globals_proof.v
index 37e43f3fca..dffb9a2cb9 100644
--- a/proofs/compiler/remove_globals_proof.v
+++ b/proofs/compiler/remove_globals_proof.v
@@ -275,6 +275,7 @@ End INCL. End INCL. Import INCL.
 Module EXTEND. Section ASM_OP.
 
 Context `{asmop:asmOp}.
+Context {spp: SemPexprParams}.
 
 Section PROOFS.
 
@@ -318,11 +319,11 @@ Section PROOFS.
     by elim: s => //= -[x' u] l ih; case: eqP => [-> [<-] | ? /ih];auto.
   Qed.
 
-  Local Lemma Hasgn: forall x tg ty e, Pr (Cassgn x tg ty e).
+  Lemma add_glob_gd_incl ii x gd1 gv gd2 :
+      add_glob fresh_id ii x gd1 gv = ok gd2 →
+      gd_incl gd1 gd2.
   Proof.
-    move=> [ii ty|x|al ws x e|al aa ws x e|aa ws len x e] ?? e1 ??? //=. 1,3-5: by move=> [<-].
-    case: ifP => ?; last by move=> [<-].
-    case: e1 => // - [] // w [] // z; rewrite /add_glob.
+    rewrite /add_glob.
     case:ifPn => hhas1; first by move=> [<-].
     case:ifPn => // /hasPP hhas2 [<-] g v.
     rewrite /get_global /get_global_value /=.
@@ -331,6 +332,14 @@ Section PROOFS.
     by have hin := assoc_memP ha; elim hhas2;eauto.
   Qed.
 
+  Local Lemma Hasgn: forall x tg ty e, Pr (Cassgn x tg ty e).
+  Proof.
+    move=> [ii ty|x|al ws x e|al aa ws x e|aa ws len x e] ?? e1 ??? //=. 1,3-5: by move=> [<-].
+    case: ifP => ?; last by move=> [<-].
+    case: e1 => // [ [] // w [] // z | [] // len es ]; last t_xrbindP => array _.
+    all: exact: add_glob_gd_incl.
+  Qed.
+
   Local Lemma Hopn : forall xs t o es, Pr (Copn xs t o es).
   Proof. by move=> xs t o es ii gd1 gd2 /= [<-]. Qed.
 
@@ -403,11 +412,31 @@ Module RGP. Section PROOFS.
 
   Definition valid (m:venv) (s1 s2:estate) :=
     [/\ s1.(escs) = s2.(escs), s1.(emem) = s2.(emem),
-        (forall x, ~~is_glob_var x -> (evm s1).[x] = (evm s2).[x]),
+        (forall x, ~~is_glob_var x -> value_uincl (evm s1).[x] (evm s2).[x]),
         (forall x g, Mvar.get m x = Some g -> is_glob_var x) &
         (forall x g,
            Mvar.get m x = Some g ->
-           get_global gd g = ok (evm s1).[x]) ].
+           exists2 gv,
+           get_global gd g = ok gv & value_uincl (evm s1).[x] gv) ].
+
+  Lemma vm_uincl_valid m s vm s' :
+    valid m (with_vm s vm) s' →
+    evm s <=1 vm →
+    valid m s s'.
+  Proof.
+    case => ?? hlocal ? hglobal le_vm; split => //.
+    + move => ? /hlocal; exact: (value_uincl_trans (le_vm _)).
+    by move => ?? /hglobal[] gv -> ?; exists gv; last apply: (value_uincl_trans (le_vm _)).
+  Qed.
+
+  Lemma valid_vm_uincl m s s' vm :
+    valid m s s' →
+    evm s' <=1 vm →
+    valid m s (with_vm s' vm).
+  Proof.
+    case => ?? hlocal ?? le_vm; split => // ? /hlocal ?.
+    exact: value_uincl_trans (le_vm _).
+  Qed.
 
   Section REMOVE_GLOB_E.
     Context (wdb : bool) (m: venv) (ii: instr_info) (s1 s2: estate) (hvalid: valid m s1 s2).
@@ -416,57 +445,103 @@ Module RGP. Section PROOFS.
       ∀ e' v,
         remove_glob_e ii m e = ok e' →
         sem_pexpr wdb gd s1 e = ok v →
-        sem_pexpr wdb gd s2 e' = ok v.
+        exists2 v', sem_pexpr wdb gd s2 e' = ok v' & value_uincl v v'.
 
     Let Pes es : Prop :=
       ∀ es' vs,
         mapM (remove_glob_e ii m) es = ok es' →
         sem_pexprs wdb gd s1 es = ok vs →
-        sem_pexprs wdb gd s2 es' = ok vs.
+        exists2 vs', sem_pexprs wdb gd s2 es' = ok vs' & List.Forall2 value_uincl vs vs'.
 
     Lemma remove_glob_e_esP : (∀ e, Pe e) ∧ (∀ es, Pes es).
     Proof.
       case: hvalid => hscs hmem hm1 hm2 hm3.
       apply: pexprs_ind_pair; subst Pe Pes; split => //=.
-      - by move => _ _ [<-] [<-].
-      - move => e he es hes q qs; t_xrbindP => e' ok_e' es' ok_es' <- {q} v ok_v vs ok_vs <- {qs} /=.
-        by rewrite (he _ _ ok_e' ok_v) (hes _ _ ok_es' ok_vs).
-      - by move => z _ _ [<-] [<-].
-      - by move => b _ _ [<-] [<-].
-      - by move => ws n _ _ [<-] [<-].
+      - by move => _ _ [<-] [<-]; exists [::].
+      - move => e he es hes q qs.
+        t_xrbindP => e' /he{}he es' /hes{}hes <- {q} v /he[] v' ok_e' ok_v' vs /hes[] vs' ok_es' ok_vs' <- {qs}.
+        exists (v' :: vs').
+        + by rewrite /= ok_e' ok_es'.
+        by constructor.
+      - by move => z _ _ [<-] [<-]; eexists; first reflexivity.
+      - by move => b _ _ [<-] [<-]; eexists; first reflexivity.
+      - by move => ws n _ _ [<-] [<-]; eexists; first reflexivity.
       - move => [x []] e' v /=; rewrite /get_gvar /get_var_ /=.
         + case : ifP => hx.
           + case heq: (Mvar.get _ _) => [ g | // ] [<-] /=.
             by rewrite /get_gvar /get_var /=; t_xrbindP => hdef <-; apply hm3.
-          by move=> [<-] h; rewrite /= /get_gvar /get_var -hm1 // hx.
-        by case => [<-] h;rewrite /= /get_gvar /=.
+          move/ok_inj => <-.
+          move: hm1 => /(_ x); rewrite hx => /(_ erefl) {}hx.
+          rewrite /= /get_gvar /get_var /=; t_xrbindP => hdef <- {v}.
+          eexists; last exact: hx.
+          case: wdb hdef (@value_uincl_defined (~~wdb) _ _ hx); last by [].
+          by move => hdef /(_ hdef) ->.
+        by move/ok_inj => <-; rewrite /= /get_gvar /= => ->; eexists; first reflexivity.
       - move => al aa ws [x []] e he q v; rewrite /get_var_ /=; t_xrbindP => e' ok_e'; last first.
         + move=> <- /=; apply: on_arr_gvarP; rewrite /on_arr_var /get_gvar /= => n t heq ->.
-          by t_xrbindP => ?? /(he _ _ ok_e') -> /= -> ? /= -> <-.
+          t_xrbindP => z ? /(he _ _ ok_e')[] v' -> ok_v' /to_intI ?; subst.
+          case: v' ok_v' => // _ /= <- w -> <-.
+          by eexists; first reflexivity.
         move=> gx; case: ifPn => // hx; last first.
         + move=> [<-] <-;apply: on_arr_gvarP; rewrite /= /on_arr_var /get_gvar /= => n t heq.
-          by rewrite /get_var -hm1 // => -> /=; t_xrbindP => ?? /(he _ _ ok_e') -> /= -> ? /= -> <-.
+          rewrite /get_var; t_xrbindP => ok_x ok_t i ? /(he _ _ ok_e')[] v' -> ok_v' /to_intI ?; subst.
+          case: v' ok_v' => // _ /= <- w ok_w <-.
+          move: hm1 => /(_ x); rewrite hx ok_t => /(_ erefl) /value_uinclE[] t' -> ok_t'.
+          rewrite orbT /= (WArray.uincl_get ok_t' ok_w).
+          eexists; first reflexivity.
+          exact: word_uincl_refl.
         case heq: (Mvar.get _ _) => [ g | // ] [<-] <-.
         apply: on_arr_gvarP; rewrite /= /on_arr_var /get_gvar /get_var /= => n t ?.
-        by t_xrbindP => hdef; have:= hm3 _ _ heq => -> -> /= ?? /(he _ _ ok_e') -> /= -> ? /= -> <-.
+        t_xrbindP => hdef ok_x z ? /(he _ _ ok_e')[] v' -> ok_v' /to_intI ?; subst.
+        case: v' ok_v' => // _ /= <- w ok_w <-.
+        case: (hm3 _ _ heq) => ? -> /value_uinclE.
+        rewrite ok_x => - [] t' -> ok_t' /=.
+        rewrite (WArray.uincl_get ok_t' ok_w).
+        eexists; first reflexivity.
+        exact: word_uincl_refl.
       - move => aa ws len [x []] e he q v; rewrite /get_var_ /=; t_xrbindP => e' ok_e'; last first.
         + move=> <- /=; apply: on_arr_gvarP; rewrite /on_arr_var /get_gvar /= => n t heq ->.
-          by t_xrbindP => ?? /(he _ _ ok_e') -> /= -> ? /= -> <-.
+          t_xrbindP => ? ? /(he _ _ ok_e')[] z -> ok_z /to_intI ?; subst.
+          case: z ok_z => // _ /= <- t' -> <- /=.
+          by eexists; first reflexivity.
         move=> gx; case: ifPn => // hx; last first.
         + move=> [<-] <-;apply: on_arr_gvarP; rewrite /= /on_arr_var /get_gvar /get_var /= => n t heq.
-          by rewrite -hm1 // => -> /=; t_xrbindP => ?? /(he _ _ ok_e') -> /= -> ? /= -> <-.
+          t_xrbindP => hdef ht i ? /(he _ _ ok_e')[] v' -> ok_v' /to_intI ?; subst.
+          case: v' ok_v' => // _ /= <- arr ok_arr <-.
+          move: (hm1 _ hx); rewrite ht => /value_uinclE[] t' -> ok_t'.
+          rewrite orbT /=.
+          case: (WArray.uincl_get_sub ok_t' ok_arr) => arr' -> ok_arr'.
+          by eexists; first reflexivity.
         case heq: (Mvar.get _ _) => [ g | // ] [<-] <-.
         apply: on_arr_gvarP; rewrite /= /on_arr_var /get_gvar /get_var /= => n t ?.
-        by t_xrbindP; have := hm3 _ _ heq => -> ? -> /= ?? /(he _ _ ok_e') -> /= -> ? /= -> <-.
+        t_xrbindP => _ ht i ? /(he _ _ ok_e')[] v' -> ok_v' /to_intI ?; subst.
+        case: v' ok_v' => // _ /= <- arr ok_arr <-.
+        case: (hm3 _ _ heq) => ? -> /value_uinclE.
+        rewrite ht => - [] t' -> ok_t' /=.
+        case: (WArray.uincl_get_sub ok_t' ok_arr) => arr' -> ok_arr'.
+        by eexists; first reflexivity.
       - move => ??? ih ??.
-        t_xrbindP => ? /ih h <- /= ?? /h -> /= -> ? /=.
-        by rewrite hmem => -> <-.
-      - by move=> ?? hrec ??; t_xrbindP => ? /hrec h <- /= ? /h -> /=.
-      - by move=> ?? hrec1 ? hrec2 ??; t_xrbindP=> ? /hrec1 h1 ? /hrec2 h2 <- ? /= /h1 -> ? /h2 ->.
-      - move => ?? ih ??; t_xrbindP => ? /ih{}ih <- ? /ih /=.
-        by rewrite -/(sem_pexprs _ _ _) => ->.
+        t_xrbindP => ? /ih h <- adr ? /h[] ? /= -> /= A /to_wordI[] ? [] ? [] ? ok_adr; subst.
+        move/value_uinclE: A => [] ? [] ? [] ? ok_adr'; subst => /=.
+        rewrite (word_uincl_truncate ok_adr' ok_adr) /= hmem => ? -> <-.
+        by eexists; first reflexivity.
+      - move => ?? hrec ??; t_xrbindP => ? /hrec h <- /= ? /h[] ? -> {} h ok_v /=.
+        rewrite (vuincl_sem_sop1 h ok_v).
+        by eexists; first reflexivity.
+      - move=> ?? hrec1 ? hrec2 ??; t_xrbindP=> ? /hrec1 h1 ? /hrec2 h2 <- ? /= /h1 [] ? -> {} h1 ? /h2[] ? -> {} h2 ok_v.
+        rewrite /= (vuincl_sem_sop2 h1 h2 ok_v).
+        by eexists; first reflexivity.
+      - move => ?? ih ??; t_xrbindP => ? /ih{}ih <- ? /ih /=[] ?.
+        rewrite -/(sem_pexprs _ _ _) => -> h ok_v.
+        rewrite /= (vuincl_sem_opN h ok_v).
+        by eexists; first reflexivity.
       move=> ? ? hrec1 ? hrec2 ? hrec3 ??.
-      by t_xrbindP => ? /hrec1 h1 ? /hrec2 h2 ? /hrec3 h3 <- ?? /= /h1 -> /= -> ?? /h2 -> /= -> ?? /h3 -> /= -> <-.
+      t_xrbindP => ? /hrec1 h1 ? /hrec2 h2 ? /hrec3 h3 <- b ? /= /h1[] ? -> /= /value_uinclE {} h1 /to_boolI ?; subst; subst.
+      move => ?? /h2[] ? -> {} h2 ok_v2 ?? /h3[] ? -> {} h3 ok_v3 /=.
+      case: (value_uincl_truncate h2 ok_v2) => ? -> {} h2.
+      case: (value_uincl_truncate h3 ok_v3) => ? -> {} h3 /= <-.
+      eexists (if b then _ else _); first reflexivity.
+      by case: b.
     Qed.
 
   End REMOVE_GLOB_E.
@@ -477,20 +552,29 @@ Module RGP. Section PROOFS.
   Definition remove_glob_esP wdb m ii s1 s2 es es' vs h :=
     (@remove_glob_e_esP wdb m ii s1 s2 h).2 es es' vs.
 
-  Lemma write_var_remove wdb (x:var_i) m s1 s2 v s1' :
+  Lemma write_var_remove_uincl wdb (x:var_i) m s1 s2 v v' s1' :
     ~~ is_glob_var x ->
     valid m s1 s2 ->
     write_var wdb x v s1 = ok s1' ->
-    exists s2', valid m s1' s2' /\ write_var wdb x v s2 = ok s2'.
+    value_uincl v v' ->
+    exists s2', valid m s1' s2' /\ write_var wdb x v' s2 = ok s2'.
   Proof.
-    move=> hglob hval /write_varP [-> hdb htr].
-    rewrite (write_var_truncate hdb htr); eexists; split; eauto.
+    move=> hglob hval /write_varP [-> hdb htr] hv'.
+    case: (compat_truncate_uincl (compat_ctype_refl _ _) htr hv' hdb) => htr' hvv' hdb'.
+    rewrite (write_var_truncate hdb' htr'); eexists; split; eauto.
     case: hval => hsc hmem h1 h2 h3; split => //= z hz.
-    + by rewrite !Vm.setP h1.
+    + by rewrite !Vm.setP; case: eqP; last by auto.
     move=> hv1; rewrite Vm.setP_neq; first by apply h3.
     by apply/eqP => ?; subst z; rewrite (h2 _ _ hv1) in hglob.
   Qed.
 
+  Lemma write_var_remove wdb (x:var_i) m s1 s2 v s1' :
+    ~~ is_glob_var x ->
+    valid m s1 s2 ->
+    write_var wdb x v s1 = ok s1' ->
+    exists s2', valid m s1' s2' /\ write_var wdb x v s2 = ok s2'.
+  Proof. by move => hglob hval hw; apply: (write_var_remove_uincl hglob hval hw). Qed.
+
   Lemma remove_glob_lvP wdb m ii s1 s1' s2 lv lv' v :
     valid m s1 s2 ->
     remove_glob_lv ii m lv = ok lv' ->
@@ -502,49 +586,80 @@ Module RGP. Section PROOFS.
     + by move=> [<-] /write_noneP; rewrite /= /write_none => -[-> -> ->]; eauto.
     + by case: ifPn => // hg [<-] /=; apply write_var_remove.
     + t_xrbindP => ? /(remove_glob_eP hval) h <- ??.
-      rewrite hmem /= => /h -> /= -> ? -> ? /= -> <- /=.
-      by eexists;split;last reflexivity; split.
+      rewrite hmem /= => /h[] ? -> /value_uinclE {}h /to_wordI[] ? [] ? [] ? h1; subst.
+      case: h => ? [] ? [] ? h2; subst.
+      rewrite /= (word_uincl_truncate h2 h1) /=.
+      move => ? /to_wordI[] ? [] ? [] ?; subst => /= -> /= ? -> <- /=.
+      by eexists; split; last reflexivity.
     + case: ifPn => hg //.
       t_xrbindP => ? /(remove_glob_eP hval) h <-.
       apply: on_arr_varP => ?? hty.
-      rewrite /= /get_var /on_arr_var /= (hm1 _ hg) => -> /=.
-      t_xrbindP => ??/h /= -> /= -> ? -> ? /= ->.
-      by apply write_var_remove.
+      rewrite /= /get_var /on_arr_var /=; t_xrbindP => _ ht.
+      have := hm1 _ hg; rewrite ht => /value_uinclE[] ? -> {} ht.
+      rewrite orbT /= => ? ? /h[] ? -> /value_uinclE {} h /to_intI ?; subst => /=; subst => /=.
+      move => ? -> t ok_t ok_s' /=.
+      have := WArray.uincl_set ht ok_t.
+      case => t' [] -> ok_t' /=.
+      by apply: write_var_remove_uincl; eauto.
     case: ifPn => hg //.
     t_xrbindP => ? /(remove_glob_eP hval) h <-.
-    apply: on_arr_varP => ?? hty; rewrite /= /get_var /on_arr_var (hm1 _ hg) => -> /=.
-    t_xrbindP => ??/h /= -> /= -> ? -> ? /= ->.
-    by apply write_var_remove.
+    apply: on_arr_varP => ?? hty; rewrite /= /get_var /on_arr_var.
+    t_xrbindP => hdef ht.
+    have := hm1 _ hg.
+    rewrite ht => /value_uinclE[] t' -> ht' ?? /h[] ? -> /value_uinclE {} h /to_intI ?; subst; subst.
+    move => arr ok_arr sub ok_sub ok_w.
+    rewrite orbT /= ok_arr /=.
+    have := WArray.uincl_set_sub ht' (WArray.uincl_refl _) ok_sub.
+    case => sub' -> ok_sub' /=.
+    by apply: write_var_remove_uincl; eauto.
   Qed.
 
   Lemma remove_glob_lvsP wdb m ii s1 s1' s2 lv lv' v :
     valid m s1 s2 ->
     mapM (remove_glob_lv ii m) lv = ok lv' ->
     write_lvals wdb gd s1 lv v = ok s1' ->
-    exists s2',
-      valid m s1' s2' /\ write_lvals wdb gd s2 lv' v = ok s2'.
+    exists2 s2',
+      write_lvals wdb gd s2 lv' v = ok s2'
+      & valid m s1' s2'.
   Proof.
     elim: lv lv' v s1 s1' s2 => //=.
     + by move=> ? []// s1 s1' s2 ? [<-] [<-]; exists s2.
     move=> x xs hrec lv' vs s1 s1' s2 hval.
     t_xrbindP=> x' /(remove_glob_lvP hval) h1 xs' /hrec h2 <-.
     case: vs => // v vs.
-    t_xrbindP => s3 /h1 [s4 [hs4 w4]] /(h2 _ _ _ _ hs4) [s5 [hs5 w5]].
-    exists s5;split => //.
+    t_xrbindP => s3 /h1 [s4 [hs4 w4]] /(h2 _ _ _ _ hs4) [s5 w5 hs5].
+    exists s5 => //.
     by rewrite /write_lvals /= w4.
   Qed.
 
-  Lemma find_globP ii xi sz (w:word sz) g :
-    find_glob ii xi gd w = ok g ->
-    get_global gd g =  ok (Vword w).
+  Lemma check_dataP gv gv' ty :
+    convertible (type_of_glob_value gv) ty →
+    check_data gv' gv →
+    type_of_val (gv2val gv') = eval_atype ty ∧ value_uincl (gv2val gv) (gv2val gv').
+  Proof.
+    case: gv gv' => [ ws w | len arr ] [ ws' w' | len' arr' ] //=.
+    - move/eqP => <- /andP[] /eqP ? /eqP ->; subst.
+      by rewrite zero_extend_u.
+    case: ty => // ws n /eqP; rewrite arr_sizeE Z.mul_1_l => eq_len /WArray.is_uinclP => h.
+    split; last by [].
+    by case: h => ? _; subst; congr carr; rewrite -eq_len.
+  Qed.
+
+  Lemma find_globP ii xi gv g :
+    find_glob ii xi gd gv = ok g ->
+    exists2 gv', get_global gd g = ok (gv2val gv') & value_uincl (gv2val gv) (gv2val gv').
   Proof.
     rewrite /find_glob /get_global /get_global_value.
-    elim: gd uniq_gd => //= -[g' z'] gd hrec /andP /= [hg' huniq]; case: ifPn => /= /andP.
-    + move=> [];case : z' => //= ws s /eqP heq /andP[] /eqP ? /eqP ? [?];subst.
-      by rewrite eq_refl /= -heq eq_refl zero_extend_u.
+    elim: gd uniq_gd => //= -[g' gv'] gd hrec /andP /= [hg' huniq]; case: ifPn => /= /andP.
+    + case => /= ok_type ok_data /ok_inj ?; subst g'.
+      rewrite eq_refl /=.
+      have [ -> h ] := check_dataP ok_type ok_data.
+      rewrite eq_refl.
+      by eexists; first reflexivity.
     move=> hn /(hrec huniq) hget {hrec}.
     case: eqP => heq //; subst g'.
-    case heq : assoc hget hg' => [z1 | //].
+    case: hget hg' => gv₀.
+    case heq : assoc => [z1 | // ].
     by rewrite (assoc_mem_dom' heq).
   Qed.
 
@@ -630,6 +745,46 @@ Module RGP. Section PROOFS.
     by exists f'.
   Qed.
 
+  Lemma evaluate_bytesP ii xi es vs s:
+    evaluate_bytes ii xi es = ok vs ->
+    sem_pexprs true gd s es = ok vs.
+  Proof.
+    rewrite /evaluate_bytes /sem_pexprs.
+    elim: es vs; first by case.
+    move => e es ih vs' /=.
+    case: e => // - [] // sz [] // z /=.
+    by t_xrbindP => vs /ih -> <-.
+  Qed.
+
+  Lemma array_from_cellsP ii xi len cells arr s bytes :
+    array_from_cells ii xi len cells = ok arr →
+    sem_pexprs true gd s cells = ok bytes →
+    sem_opN (Oarray len) bytes = ok (Varr arr).
+  Proof.
+    rewrite /array_from_cells; t_xrbindP => ? /evaluate_bytesP - /(_ s) -> h /ok_inj ?; subst.
+    case: sem_opN h => // v /=.
+    case h: to_arr => // /ok_inj ?; subst.
+    by rewrite (to_arrI h).
+  Qed.
+
+  Lemma valid_set ii (x: var_i) m s s' g gv v :
+    is_glob_var x →
+    find_glob ii x gd gv = ok g →
+    value_uincl (vm_truncate_val (eval_atype (vtype x)) v) (gv2val gv) →
+    valid m s s' →
+    valid (Mvar.set m x g) (with_vm s (evm s).[x <- v]) s'.
+  Proof.
+    move => hglob hfind htr [] hscs hm hm1 hm2 hm3; split => //=.
+    * move=> y hy; rewrite Vm.setP_neq; first by apply hm1.
+      by apply/eqP => ?;subst y;move: hy;rewrite hglob.
+    * by move=> y gy;rewrite Mvar.setP; case:eqP => [<- // | ?]; apply hm2.
+    move=> y gy;rewrite Mvar.setP Vm.setP //; case:eqP => [|/eqP hneq]; last by apply hm3.
+    move=> ?[?]; subst.
+    case: (find_globP hfind) => gv' -> hgv.
+    eexists; first reflexivity.
+    exact: value_uincl_trans htr hgv.
+  Qed.
+
   Lemma Hassgn_aux m m' ii x tag ty e c' :
     remove_glob_i gd m (MkI ii (Cassgn x tag ty e)) = ok (m', c') ->
     forall s1 s2 s1', valid m s1 s1' ->
@@ -637,27 +792,49 @@ Module RGP. Section PROOFS.
       exists2 s2', esem P' ev c' s1' = ok s2' & valid m' s2 s2'.
   Proof.
     rewrite /= /sem_assgn; t_xrbindP => e' he hx s1 s2 s1' hval v hv v' htr hw.
-    have he' := remove_glob_eP hval he hv. clear he.
+    have [ w ok_w v_w ] := remove_glob_eP hval he hv. clear he.
     have h :
       (Let lv := remove_glob_lv ii m x in
       ok (m, [:: MkI ii (Cassgn lv tag ty e')])) = ok (m', c') ->
       exists2 s2', esem P' ev c' s1' = ok s2' & valid m' s2 s2' .
-    + t_xrbindP => x' /(remove_glob_lvP hval) -/(_ _ _ _ hw) [s2' [hs2' hw' ]] <- <-.
-      by exists s2' => //=; rewrite /sem_assgn he' /= htr /= hw'.
+    + t_xrbindP => x' /(remove_glob_lvP hval) h <- <-.
+      rewrite /= /sem_assgn ok_w /=.
+      have [ w' -> v_w' /= ] := value_uincl_truncate v_w htr.
+      have [ vm ] := write_uincl (vm_uincl_refl _) v_w' hw.
+      rewrite with_vm_same => {} hw' le_vm.
+      move: h => /(_ true _ w' hw')[] s2' [] hval' ->.
+      eexists; first reflexivity.
+      exact: vm_uincl_valid le_vm.
     case: x hw h hx => //=.
     move=> xi hxi hdef; case: ifPn => // hglob {hdef}.
-    case: e' he' => // - [] // sz [] //= z [?]; subst v.
+    case: e' ok_w => // [ [] // sz [] // z /= /ok_inj ? | [] // len cells /= ]; last first.
+    + t_xrbindP => bytes ok_bytes ok_w.
+      case: ifP => // htxi.
+      t_xrbindP => arr ok_arr g hfind <-{m'} <-{c'}.
+      eexists; first reflexivity.
+      move/write_varP: hxi => [-> hdb htr'].
+      apply: (valid_set hglob hfind) hval.
+      move: htr'.
+      rewrite (convertible_eval_atype htxi) /=.
+      case: v' htr hdb => //; move => len' arr' /truncate_valI; case => hty ? _; subst.
+      move=>/eqP ?; subst.
+      rewrite /= eqxx.
+      move: ok_w.
+      by rewrite (array_from_cellsP ok_arr ok_bytes) => /ok_inj ->.
+    subst.
     case: andP => //= -[hty htxi].
-    move: htr; rewrite (convertible_eval_atype hty) /truncate_val /= truncate_word_u /= => -[?]; subst v'.
-    t_xrbindP => h hfind <- <-; exists s1' => //.
+    move: htr; rewrite (convertible_eval_atype hty) /truncate_val /=.
+    t_xrbindP => w ok_w ?; subst => g hfind <- <-; exists s1' => //.
     move/write_varP: hxi => [-> hdb htr].
-    case: hval => hscs hm hm1 hm2 hm3; split => //=.
-    + move=> y hy; rewrite Vm.setP_neq; first by apply hm1.
-      by apply/eqP => ?;subst y;move: hy;rewrite hglob.
-    + by move=> y gy;rewrite Mvar.setP; case:eqP => [<- // | ?]; apply hm2.
-    move=> y gy;rewrite Mvar.setP Vm.setP //; case:eqP => [|/eqP hneq]; last by apply hm3.
-    move=> ?[?]; subst; rewrite (find_globP hfind).
-    by have /vm_truncate_valE [ws] := htr; rewrite (convertible_eval_atype htxi) => -[[->] ?->]; rewrite cmp_le_refl.
+    apply: (valid_set hglob hfind) hval.
+    have /vm_truncate_valE [ws] := htr.
+    rewrite (convertible_eval_atype htxi) => -[] [<-] _ ->.
+    rewrite cmp_le_refl.
+    case/to_wordI: ok_w => ? [] ? [] ?; subst.
+    case/truncate_wordP => sz_le ?; subst.
+    case/andP: v_w => le_sz /eqP ?; subst.
+    have ? := cmp_le_antisym sz_le le_sz; subst.
+    by rewrite ! zero_extend_u.
   Qed.
 
   Section SEM.
@@ -681,8 +858,10 @@ Module RGP. Section PROOFS.
     forall s1', valid m s1 s1' ->
     exists s2', valid m s2 s2' /\ sem_for P' ev xi vs s1' c' s2'.
 
-  Let Pfun scs m fn vs scs' m' vs' :=
-    sem_call P' ev scs m fn vs scs' m' vs'.
+  Let Pfun scs m fn vargs scs' m' vres :=
+    exists2 vres',
+    List.Forall2 value_uincl vres vres' &
+    sem_call P' ev scs m fn vargs scs' m' vres'.
 
   Local Lemma Hnil : sem_Ind_nil Pc.
   Proof.
@@ -713,28 +892,34 @@ Module RGP. Section PROOFS.
    move=> s1 s2 t o xs es ho ii m m' c /= hrm s1' hval.
    move: hrm; t_xrbindP.
    move=> xs' /(remove_glob_lvsP hval) hxs' es' /(remove_glob_esP hval) hes' <- <-.
-   move: ho;rewrite /sem_sopn; t_xrbindP => vs vres /hes' h1 h2 /hxs' [s2' [hval' h]].
-   exists s2';split => //.
-   by apply sem_seq1; constructor; constructor; rewrite /sem_sopn h1 /= h2.
+   move: ho;rewrite /sem_sopn; t_xrbindP => vs vres /hes'[] vs' h1 vs_vs' h2 /hxs' [s2' h hval'].
+   have [ vs'' {} h2 vs_vs'' ] := vuincl_exec_opn vs_vs' h2.
+   have [ vm ] := writes_uincl (vm_uincl_refl _) vs_vs'' h.
+   rewrite with_vm_same => {} h le_vm.
+   eexists; split; first exact: valid_vm_uincl le_vm.
+   by apply sem_seq1; constructor; constructor; rewrite /sem_sopn h1 /= h2 /= h.
   Qed.
 
   Local Lemma Hsyscall : sem_Ind_syscall P Pi_r.
   Proof.
    move=> s1 scs mem s2 o xs es ves vs hes ho hw ii m m' c /= hrm s1' hval.
    move: hrm; t_xrbindP => xs' hrlv es' hres <- <-.
-   have hes' := remove_glob_esP hval hres hes.
-   have hval' : valid m (with_scs (with_mem s1 mem) scs) (with_scs (with_mem s1' mem) scs).
-   + case: hval => hscs hm hm1 hm2 hm3; split => //=.
-   have [s2' [hval1 h]]:= remove_glob_lvsP hval' hrlv hw.
-   exists s2';split => //.
+   have [ vres' hes' hvres' ] := remove_glob_esP hval hres hes.
+   have [ vs' ho' hvs' ] := exec_syscallP ho hvres'.
+   have [ vm /= hw' le_vm ] := writes_uincl (vm_uincl_refl _) hvs' hw.
+   have hval' : valid m (with_vm (with_scs (with_mem s1 mem) scs) (evm s1)) (with_scs (with_mem s1' mem) scs).
+   + by case: hval.
+   have [ s2' hw'' hval'' ] := remove_glob_lvsP hval' hrlv hw'.
+   exists s2'; split.
+   + exact: vm_uincl_valid le_vm.
    apply sem_seq1; constructor; econstructor; eauto.
-   by case: hval => <- <-.
+   by case: hval => <- <- *; exact: ho'.
   Qed.
 
   Local Lemma Hif_true : sem_Ind_if_true P ev Pc Pi_r.
   Proof.
     move=> s1 s2 e c1 c2 he _ hc ii m m' c' /= hrm s1' hval.
-    move: hrm; t_xrbindP => e' /(remove_glob_eP hval) -/(_ _ _ he) he'.
+    move: hrm; t_xrbindP => e' /(remove_glob_eP hval) -/(_ _ _ he) [] [] // [] // he' _.
     move=> [m1 c1'] /hc -/(_ _ hval) [s2' [hval' hc1']].
     move=> [m2 c2'] h /= <- <-.
     exists s2'; split.
@@ -745,7 +930,7 @@ Module RGP. Section PROOFS.
   Local Lemma Hif_false : sem_Ind_if_false P ev Pc Pi_r.
   Proof.
     move=> s1 s2 e c1 c2 he _ hc ii m m' c' /= hrm s1' hval.
-    move: hrm; t_xrbindP => e' /(remove_glob_eP hval) -/(_ _ _ he) he'.
+    move: hrm; t_xrbindP => e' /(remove_glob_eP hval) -/(_ _ _ he) [] [] // [] // he' _.
     move=> [m1 c1'] h /= [m2 c2'] /hc -/(_ _ hval) [s2' [hval' hc1']] <- <-.
     exists s2'; split.
     + apply: valid_Mincl hval'; apply merge_incl_r.
@@ -761,7 +946,8 @@ Module RGP. Section PROOFS.
     have h2' := hc' _ _ _ h2.
     move=> ? [??] [??] hm hm1 ? <-;subst e1 m4 c4 m5 c5 m1.
     have /h1' [s2' [hs2 hc1]]: valid m3 s1 s1' by apply: valid_Mincl hval.
-    have he' := remove_glob_eP hs2 he1 he.
+    have := remove_glob_eP hs2 he1 he.
+    case => - [] // [] // he' _.
     have [s3' [hs3 hc2]]:= h2' _ hs2.
     have : remove_glob_i gd m3 (MkI ii (Cwhile a c e ei c')) =
              ok (m', [::MkI ii (Cwhile a c1' e' ei c2')]).
@@ -780,17 +966,18 @@ Module RGP. Section PROOFS.
     move=> ? [??] [??] hm hm1 ? <-;subst e1 m4 c4 m5 c5 m1.
     have h1' := hc _ _ _ h1.
     have /h1' [s2' [hs2 hc1]]: valid m3 s1 s1' by apply: valid_Mincl hval.
+    have := remove_glob_eP hs2 he1 he.
+    case => - [] // [] // he' _.
     exists s2';split => //.
-    apply sem_seq1;constructor;apply: Ewhile_false => //.
-    by apply: remove_glob_eP he1 he.
+    by apply sem_seq1;constructor;apply: Ewhile_false.
   Qed.
 
   Local Lemma Hfor : sem_Ind_for P ev Pi_r Pfor.
   Proof.
     move=> s1 s2 i d lo hi c vlo vhi hlo hhi _ hfor ii m m' c' /= hrn s1' hval.
     case : ifPn hrn => // hglob.
-    t_xrbindP => lo' /(remove_glob_eP hval) -/(_ _ _ hlo) hlo'.
-    move=> hi' /(remove_glob_eP hval) -/(_ _ _ hhi) hhi'.
+    t_xrbindP => lo' /(remove_glob_eP hval) -/(_ _ _ hlo) [] ? hlo' /value_uinclE ?; subst.
+    move=> hi' /(remove_glob_eP hval) -/(_ _ _ hhi) [] ? hhi' /value_uinclE ?; subst.
     move=> [m2 c2] /= /loopP [m1 [hc h1 h2]] [??];subst m2 c'.
     have hval': valid m' s1 s1' by apply: valid_Mincl hval.
     have [s2' [??]]:= hfor hglob _ _ _ hc h1 _ hval'.
@@ -818,11 +1005,17 @@ Module RGP. Section PROOFS.
     move=> s1 scs2 m2 s2 xs fn args vargs rvs hargs _ hfun hres ii m m' c' /=
       hrm s1' hval.
     move: hrm; t_xrbindP => xs' hxs es' hes ??;subst m' c'.
-    have hes' := remove_glob_esP hval hes hargs.
+    have := remove_glob_esP hval hes hargs.
+    case => vargs' hes' hvargs.
+    case: hfun => vres hvres /(sem_call_uincl hvargs).
+    case => vres' [] hfun' hvres'.
+    have := writes_uincl (vm_uincl_refl _) (values_uincl_trans hvres hvres') hres.
+    case => vm hres' le_vm.
     have hval' : valid m (with_scs (with_mem s1 m2) scs2) (with_scs (with_mem s1' m2) scs2).
     + by case: hval;split.
-    have [s2' [hs2' hxs']]:= remove_glob_lvsP hval' hxs hres.
-    exists s2';split => //.
+    have [s2' hxs' hs2' ]:= remove_glob_lvsP hval' hxs hres'.
+    exists s2';split.
+    + exact: vm_uincl_valid le_vm.
     apply sem_seq1;constructor;econstructor;eauto.
     by case: hval => <- <-.
   Qed.
@@ -835,11 +1028,17 @@ Module RGP. Section PROOFS.
     have hval: valid (Mvar.empty var) s1 s1 by split.
     have [s2' [hs2' ws2]] := hc _ _ _ hrm _ hval.
     subst m2; case: (hs2') => /= hscse hmem hm _ _.
-    have hres2 : get_var_is (~~ direct_call) (evm s2') (f_res f) = ok vres.
-    + elim: (f_res f) (vres) res1 hres1 hres => //= x xs hrec vres0 res1.
+    have : exists2 vres', get_var_is (~~ direct_call) (evm s2') (f_res f) = ok vres' & List.Forall2 value_uincl vres vres'.
+    + elim: (f_res f) (vres) res1 hres1 hres.
+      * by move => _ _ _ /ok_inj <-; exists [::]; constructor.
+      move => x xs hrec vres0 res1 /=.
       t_xrbindP; case: ifPn => hglob // _ ? /hrec hres1 ? v.
-      by rewrite /get_var hm // => -> vs /hres1 hxs <-; rewrite /= hxs.
-    subst scs2; econstructor; eauto.
+      case/(get_var_uincl_at (hm _ hglob)) => v' -> v_v' vs /hres1[] vs' -> vs_vs' <- /=; eauto.
+    case => vs ok_vs vres_vs.
+    have := mapM2_dc_truncate_val hres' vres_vs.
+    case => vs' ok_vs' vres_vs'.
+    subst scs2.
+    eexists; last econstructor; eauto.
   Qed.
 
   Local Lemma remove_glob_call scs1 m1 f vargs scs2 m2 vres :
@@ -888,41 +1087,53 @@ Module RGP. Section PROOFS.
      ; check_esP_rel := @check_esP_R_valid ii
     |}.
 
-  Lemma checker_validP ii : Checker_eq P P' (checker_valid ii).
+  Lemma checker_validP ii : Checker_uincl P P' (checker_valid ii).
   Proof.
     constructor.
     + move=> > /wdb_ok_eq <- [_ hes] s1 s2 vs hval hses.
-      by rewrite (remove_glob_esP hval hes hses); eexists.
-    move=> > /wdb_ok_eq <- [<- hxs] vs s1 s2 s1' hval hw.
-    have [s2' [??]]:= remove_glob_lvsP hval hxs hw; eexists; eauto.
+      exact: remove_glob_esP hval hes hses.
+    move=> > /wdb_ok_eq <- [<- hxs] vs vs' vs_vs' s1 s2 s1' hval hw.
+    have [ s2' hw' hval' ]  :=  remove_glob_lvsP hval hxs hw.
+    have := writes_uincl (vm_uincl_refl _) vs_vs' hw'.
+    rewrite with_vm_same => - [] vm -> le_vm.
+    eexists; first reflexivity.
+    exact: valid_vm_uincl.
   Qed.
   #[local] Hint Resolve checker_validP : core.
 
   Let Pi i :=
     forall d dc, remove_glob_i gd d i = ok dc ->
-    wequiv_rec P P' ev ev eq_spec (valid d) [::i] dc.2 (valid dc.1).
+    wequiv_rec P P' ev ev uincl_spec (valid d) [::i] dc.2 (valid dc.1).
 
   Let Pi_r i := forall ii, Pi (MkI ii i).
 
   Let Pc c :=
     forall d dc, remove_glob (remove_glob_i gd) d c = ok dc ->
-    wequiv_rec P P' ev ev eq_spec (valid d) c dc.2 (valid dc.1).
+    wequiv_rec P P' ev ev uincl_spec (valid d) c dc.2 (valid dc.1).
 
-  Lemma it_remove_glob_call fn : wiequiv_f P P' ev ev (rpreF (eS:= eq_spec)) fn fn (rpostF (eS:=eq_spec)).
+  Lemma it_remove_glob_call fn : wiequiv_f P P' ev ev (rpreF (eS:= uincl_spec)) fn fn (rpostF (eS:=uincl_spec)).
   Proof.
-    apply wequiv_fun_ind => {}fn _ fs _ [<- <-] fd hget.
+    apply wequiv_fun_ind => {}fn _ fs fs' [<-] hfs fd hget.
     have [fd' [hget' hfd']]:= get_fundefP hget.
+    have fsi := fs_uincl_initialize (fd := fd) (fd' := fd').
     exists fd' => //.
     move: hfd'; rewrite /remove_glob_fundef; t_xrbindP => _tt hparams res1 hres1 [m' c'] hrm ?;subst fd' => /=.
-    move=> s1 hinit.
-    exists s1 => //; exists (valid (Mvar.empty var)), (valid m'); split => // {s1 hinit fs hget}; last first.
-    + move=> s1 s2 fs [/= hscse hmem hm _ _]; rewrite /finalize_funcall /=; t_xrbindP.
+    move=> s1 /fsi /= /(_ _ _ erefl erefl erefl erefl hfs)[] s1' hinit hs1.
+    exists s1'; first exact: hinit.
+    exists (valid (Mvar.empty var)), (valid m'); split => // {hfs fsi hget hinit}; cycle -1.
+    + move=> {hs1} s1 s2 {} fs [/= hscse hmem hm _ _]; rewrite /finalize_funcall /=; t_xrbindP.
       move=> vs hget vs' htr <-.
-      have -> : get_var_is (~~ direct_call) (evm s2) (f_res fd) = ok vs.
-      + elim: (f_res fd) (vs) res1 hres1 hget => //= x xs hrec1 vres0 res1.
-        t_xrbindP; case: ifPn => hglob // _ ? /hrec1 hres1 ? v.
-        by rewrite /get_var hm // => -> vs1 /hres1 hxs <-; rewrite /= hxs.
-      by rewrite /= htr hscse hmem/=; eexists; eauto.
+      have : exists2 vres', get_var_is (~~ direct_call) (evm s2) (f_res fd) = ok vres' & List.Forall2 value_uincl vs vres'.
+      - elim: (f_res fd) (vs) res1 hres1 hget.
+        * by move => _ _ _ /ok_inj <-; exists [::]; constructor.
+        move => x xs hrec vres0 res1 /=.
+        t_xrbindP; case: ifPn => hglob // _ ? /hrec hres1 ? v.
+        case/(get_var_uincl_at (hm _ hglob)) => v' -> v_v' qs /hres1[] qs' -> qs_qs' <- /=; eauto.
+      case => vres' -> vs_vres' /=.
+      have := mapM2_dc_truncate_val htr vs_vres'.
+      case => vs'' -> vs'_vs'' /=.
+      by eexists; first reflexivity.
+    + by case: hs1 => ?? le_vm.
     move: hrm; set dc_ := (m', c'); have [-> ->] : m' = dc_.1 /\ c' = dc_.2 by done.
     move: (f_body fd) (Mvar.empty var) dc_ => {fn fd m' c' hget' _tt hparams res1 hres1}.
     apply (cmd_rect (Pr := Pi_r) (Pi:=Pi) (Pc:=Pc)) => //.
@@ -930,23 +1141,23 @@ Module RGP. Section PROOFS.
     + move=> i c hi hc d dc_ /=; t_xrbindP => dci /hi{}hi ? /hc{}hc <-.
       by rewrite -cat1s; apply wequiv_cat with (valid dci.1).
     + move=> x tg ty e ii d [d' c'] hrm.
-      apply wequiv_assgn_esem => s1 s2 s1' hval hsem.
+      apply wequiv_assgn_esem => {hs1} s1 s2 {} s1' hval hsem.
       by apply (Hassgn_aux hrm hval hsem).
     + move=> xs tg o es ii d dc_ /=; t_xrbindP => xs' hxs' es' hes' <- /=.
-      by apply wequiv_opn_rel_eq with (checker_valid ii) d.
+      by apply wequiv_opn_rel_uincl with (checker_valid ii) d.
     + move=> xs o es ii d dc_ /=; t_xrbindP => xs' hxs' es' hes' <- /=.
-      apply wequiv_syscall_rel_eq_core_R with (checker_valid ii) d d => //.
+      apply wequiv_syscall_rel_uincl_core_R with (checker_valid ii) d d => //.
       + by move=> > []. + by move=> > [?????].
-      by move=> ??? <- ->; eauto.
+      exact: fs_uincl_syscall.
     + move=> e c1 c2 hc1 hc2 ii d dc_ /=; t_xrbindP.
       move=> e' he' dc1 /hc1{}hc1 dc2 /hc2{}hc2 <- /=.
-      apply wequiv_if_rel_eq_R with (checker_valid ii) d dc1.1 dc2.1 => //.
+      apply wequiv_if_rel_uincl_R with (checker_valid ii) d dc1.1 dc2.1 => //.
       + by split => //=; rewrite he'.
       + by move=> >; apply/valid_Mincl/merge_incl_l.
       by move=> >; apply/valid_Mincl/merge_incl_r.
     + move=> v dir lo hi c hc ii d dc_ /=.
       case: ifP => // hv; t_xrbindP => lo' hlo hi' hhi [d' c'] /loopP [d1] [/hc{}hc hincl1 hincl2] [<-] /=.
-      apply wequiv_for_rel_eq_R with (checker_valid ii) d d' => //.
+      apply wequiv_for_rel_uincl_R with (checker_valid ii) d d' => //.
       + by split => //=; rewrite hlo /= hhi.
       + by move=> >; apply valid_Mincl.
       + by split => //=; rewrite hv.
@@ -958,14 +1169,14 @@ Module RGP. Section PROOFS.
       subst e_ d1_ c1_ d2_ c2_.
       apply wequiv_weaken with (valid d2) (valid d') => //.
       + by move=> >; apply valid_Mincl.
-      apply wequiv_while_rel_eq with (checker_valid ii) d' => //.
+      apply wequiv_while_rel_uincl with (checker_valid ii) d' => //.
       + by split => //=; rewrite he.
       apply wequiv_weaken with (valid d') (valid d1) => //.
       by move=> >; apply valid_Mincl.
     move=> xs fn es ii d dc_ /=; t_xrbindP => xs' hxs' es' hes' <- /=.
-    apply wequiv_call_rel_eq_R with (checker_valid ii) d d => //.
+    apply wequiv_call_rel_uincl_R with (checker_valid ii) d d => //.
     + by move=> > []. + by move=> > [?????].
-    by move=> ?? <-; apply: wequiv_fun_rec.
+    by move => ???; apply: wequiv_fun_rec.
   Qed.
 
   End IT.
@@ -975,11 +1186,13 @@ Module RGP. Section PROOFS.
   Lemma remove_globP P P' f ev scs mem scs' mem' va vr :
     remove_glob_prog fresh_id P = ok P' ->
     sem_call P ev scs mem f va scs' mem' vr ->
-    sem_call P' ev scs mem f va scs' mem' vr.
+    exists2 vr',
+     List.Forall2 value_uincl vr vr' &
+    sem_call P' ev scs mem f va scs' mem' vr'.
   Proof.
     rewrite /remove_glob_prog; t_xrbindP => gd' /extend_glob_progP hgd.
     case: ifP => // huniq; t_xrbindP => fds hfds <- h; have hf := gd_incl_fun hgd h.
-    apply: (remove_glob_call (P:={| p_globs := gd'; p_funcs := p_funcs P |}) hfds huniq hf).
+    exact: (remove_glob_call (P:={| p_globs := gd'; p_funcs := p_funcs P |}) hfds huniq hf).
   Qed.
 
   Section IT.
@@ -988,7 +1201,7 @@ Module RGP. Section PROOFS.
 
   Lemma it_remove_globP P P' ev fn:
     remove_glob_prog fresh_id P = ok P' ->
-    wiequiv_f P P' ev ev (rpreF (eS:= eq_spec)) fn fn (rpostF (eS:=eq_spec)).
+    wiequiv_f P P' ev ev (rpreF (eS:= eq_spec)) fn fn (rpostF (eS:= uincl_spec)).
   Proof.
     rewrite /remove_glob_prog; t_xrbindP => gd' /extend_glob_progP hgd.
     case: ifP => // huniq; t_xrbindP => fds hfds <-.
@@ -997,8 +1210,8 @@ Module RGP. Section PROOFS.
     have h2 := it_remove_glob_call (P:=P1) ev hfds huniq (wE:=wE) (rE:=rE0) (fn:=fn).
     move: h1 h2.
     apply wiequiv_f_trans => //.
-    + by move=> fs1 fs2 [_ <-]; exists fs1.
-    by move=> ??? fs1 fs3 _ _ [fs2] <- <-.
+    + by move=> fs1 fs2 [] _ <-; exists fs1 => //; split => //; exact: fs_uinclR.
+    by move=> ??? fs1 fs3 _ _ [fs2] <-.
   Qed.
 
   End IT.

From 9dd0f83c14948b67689574c521eef4982132f83b Mon Sep 17 00:00:00 2001
From: Vincent Laporte <Vincent.Laporte@inria.fr>
Date: Fri, 30 Jan 2026 11:40:03 +0100
Subject: [PATCH 5/5] Literal arrays: concrete syntax, tests & documentation

---
 changes/01-feature/1375-literal-arrays.md     |  3 +
 .../examples/extraction-unit-tests/.gitignore |  3 +
 .../examples/extraction-unit-tests/proofs.ec  |  6 ++
 .../extraction-unit-tests/string.jazz         | 13 ++++
 compiler/src/latex_printer.ml                 | 19 ++---
 compiler/src/parser.mly                       | 11 ++-
 compiler/src/pretyping.ml                     | 75 ++++++-------------
 compiler/src/printer.ml                       |  6 +-
 compiler/src/prog.ml                          |  6 +-
 compiler/src/prog.mli                         |  6 +-
 compiler/src/subst.ml                         | 25 +++----
 compiler/src/syntax.ml                        |  9 +--
 compiler/src/typing.ml                        | 35 +++++++--
 compiler/tests/exec/exec.expected             |  3 +
 compiler/tests/exec/exec.ml                   |  7 ++
 .../typing/x86-64/global_type_mismatch.jazz   |  1 +
 .../typing/x86-64/global_type_mismatch2.jazz  |  2 +
 compiler/tests/negative.expected              | 20 +++--
 compiler/tests/printing.ml                    |  8 +-
 .../tests/success/common/literal-arrays.jazz  | 32 ++++++++
 docs/source/language/syntax/expressions.md    |  3 +
 21 files changed, 168 insertions(+), 125 deletions(-)
 create mode 100644 changes/01-feature/1375-literal-arrays.md
 create mode 100644 compiler/examples/extraction-unit-tests/string.jazz
 create mode 100644 compiler/tests/fail/typing/x86-64/global_type_mismatch.jazz
 create mode 100644 compiler/tests/fail/typing/x86-64/global_type_mismatch2.jazz
 create mode 100644 compiler/tests/success/common/literal-arrays.jazz

diff --git a/changes/01-feature/1375-literal-arrays.md b/changes/01-feature/1375-literal-arrays.md
new file mode 100644
index 0000000000..5ac7cb3073
--- /dev/null
+++ b/changes/01-feature/1375-literal-arrays.md
@@ -0,0 +1,3 @@
+- Byte arrays can occur as literal values as string constants (`"abcd"`) or as
+  a sequence of expressions (e.g., `{ 1, 2, 3 }`)
+  ([PR 1375](https://github.com/jasmin-lang/jasmin/pull/1375)).
diff --git a/compiler/examples/extraction-unit-tests/.gitignore b/compiler/examples/extraction-unit-tests/.gitignore
index 200d98cbd8..986ed0ffc5 100644
--- a/compiler/examples/extraction-unit-tests/.gitignore
+++ b/compiler/examples/extraction-unit-tests/.gitignore
@@ -2,3 +2,6 @@ add_in_mem.ec
 gcd.ec
 loops.ec
 sdiv.ec
+string.ec
+Array2.ec
+BArray2.ec
diff --git a/compiler/examples/extraction-unit-tests/proofs.ec b/compiler/examples/extraction-unit-tests/proofs.ec
index 4625226374..249b0d398a 100644
--- a/compiler/examples/extraction-unit-tests/proofs.ec
+++ b/compiler/examples/extraction-unit-tests/proofs.ec
@@ -5,6 +5,7 @@ require Gcd.
 require Loops.
 require Sdiv.
 require Add_in_mem.
+require String.
 
 lemma loops_forty_correct : hoare [ Loops.M.forty: true ==> res = W32.of_int 40 ].
 proof. by proc; unroll for ^while; auto. qed.
@@ -42,6 +43,11 @@ proof.
   by rewrite gcd0z.
 qed.
 
+(* ------------------------------------------------ *)
+hoare string_correct :
+  String.M.main : true ==> res = W32.of_int 1075839235.
+proof. by proc; auto => />; rewrite to_uint_eq !(to_uintD, to_uint_shl, of_uintK). qed.
+
 (* ------------------------------------------------ *)
 
 op to_list (m:global_mem_t) (p len : int) =
diff --git a/compiler/examples/extraction-unit-tests/string.jazz b/compiler/examples/extraction-unit-tests/string.jazz
new file mode 100644
index 0000000000..03361e1c8d
--- /dev/null
+++ b/compiler/examples/extraction-unit-tests/string.jazz
@@ -0,0 +1,13 @@
+export fn main() -> reg u32 {
+  global u8[2] x = "@ ";
+  global u8[2] y = { 1, 3 };
+  reg u32 r = 0;
+  r += (32u)x[0];
+  r <<= 8;
+  r += (32u)x[1];
+  r <<= 8;
+  r += (32u)y[0];
+  r <<= 8;
+  r += (32u)y[1];
+  return r;
+}
diff --git a/compiler/src/latex_printer.ml b/compiler/src/latex_printer.ml
index c336001c53..9d68194352 100644
--- a/compiler/src/latex_printer.ml
+++ b/compiler/src/latex_printer.ml
@@ -55,8 +55,6 @@ let pp_string fmt s =
   | '^' -> caret fmt ()
   | c -> F.fprintf fmt "%c" c
 
-let pp_loc_string fmt s = L.unloc s |> pp_string fmt
-
 let pp_cc =
     pp_opt (fun fmt x -> F.fprintf fmt "%a " kw (match x with `Inline -> "inline" | `Export -> "export"))
 
@@ -195,6 +193,12 @@ and pp_expr_rec prio fmt pe =
   | PEFetch me -> pp_mem_access fmt me
   | PEpack (vs,es) ->
     F.fprintf fmt "(%a)[@[%a@]]" pp_svsize vs (pp_list ",@ " pp_expr) es
+  | PEarray es ->
+    F.fprintf fmt "%a @[%a@] %a"
+      openbrace ()
+      (pp_list ",@ " pp_expr) es
+      closebrace ()
+  | PEstring s -> pp_string fmt s
   | PEBool b -> F.fprintf fmt "%s" (if b then "true" else "false")
   | PEInt i -> F.fprintf fmt "%s" i
   | PECall (f, args) -> F.fprintf fmt "%a(%a)" pp_var f (pp_list ", " pp_expr) args
@@ -392,20 +396,11 @@ let pp_param fmt { ppa_ty ; ppa_name ; ppa_init } =
     dname (L.unloc ppa_name)
     pp_expr ppa_init
 
-let pp_pgexpr fmt = function
-  | GEword e -> pp_expr fmt e
-  | GEarray es ->
-    F.fprintf fmt "%a @[%a@] %a"
-      openbrace ()
-      (pp_list ",@ " pp_expr) es
-      closebrace ()
-  | GEstring e -> pp_loc_string fmt e
-
 let pp_global fmt { pgd_type ; pgd_name ; pgd_val } =
   F.fprintf fmt "%a %a = %a;"
     pp_type pgd_type
     dname (L.unloc pgd_name)
-    pp_pgexpr pgd_val
+    pp_expr pgd_val
 
 let pp_path fmt s =
   F.fprintf fmt "%S " (L.unloc s)
diff --git a/compiler/src/parser.mly b/compiler/src/parser.mly
index 1d62049ade..d370a6d269 100644
--- a/compiler/src/parser.mly
+++ b/compiler/src/parser.mly
@@ -289,6 +289,10 @@ pexpr_r:
 | ct=parens(svsize) LBRACKET es=rtuple1(pexpr) RBRACKET
     { PEpack(ct,es) }
 
+| e = STRING { PEstring e }
+
+| LBRACE es = rtuple1(pexpr) RBRACE { PEarray es }
+
 | ct=parens(cast) e=pexpr %prec BANG
     { PEOp1 (`Cast(ct), e) }
 
@@ -486,13 +490,8 @@ pparam:
     { { ppa_ty = ty; ppa_name = x; ppa_init = pe; } }
 
 (* -------------------------------------------------------------------- *)
-pgexpr:
-| e=pexpr { GEword e }
-| LBRACE es = rtuple1(pexpr) RBRACE { GEarray es }
-| e=loc(STRING) { GEstring e }
-
 pglobal:
-| pgd_type=ptype pgd_name=ident EQ pgd_val=pgexpr SEMICOLON
+| pgd_type=ptype pgd_name=ident EQ pgd_val=pexpr SEMICOLON
   { { pgd_type ; pgd_name ; pgd_val  } }
 
 (* -------------------------------------------------------------------- *)
diff --git a/compiler/src/pretyping.ml b/compiler/src/pretyping.ml
index 0197e30c3d..b3fb8318b3 100644
--- a/compiler/src/pretyping.ml
+++ b/compiler/src/pretyping.ml
@@ -35,9 +35,6 @@ type tyerror =
   | TypeNotFound        of A.symbol
   | InvalidTypeAlias    of A.symbol L.located option * P.epty
   | InvalidCast         of P.epty pair
-  | InvalidTypeForGlobal of P.epty
-  | GlobArrayNotWord
-  | GlobWordNotArray
   | EqOpWithNoLValue
   | CallNotAllowed
   | PrimNotAllowed
@@ -105,16 +102,6 @@ let pp_tyerror fmt (code : tyerror) =
     F.fprintf fmt "can not implicitly cast %a into %a"
       pp_eptype t1 pp_eptype t2
 
-  | InvalidTypeForGlobal ty ->
-      F.fprintf fmt "globals should have type word; found: ‘%a’"
-        pp_eptype ty
-
-  | GlobArrayNotWord ->
-    F.fprintf fmt "the definition is an array and not a word"
-
-  | GlobWordNotArray ->
-    F.fprintf fmt "the definition is a word and not an array"
-
   | InvalidOperator o ->
     F.fprintf fmt "invalid operator %s"
       (match o with
@@ -266,7 +253,7 @@ module Env : sig
   val exit_namespace : 'asm env -> 'asm env
 
   module Vars : sig
-    val push_global   : 'asm env -> (P.pvar * P.epty * P.pexpr_ P.ggexpr ) -> 'asm env
+    val push_global   : 'asm env -> (P.pvar * P.epty * P.pexpr) -> 'asm env
     val push_param    : 'asm env -> (P.pvar * P.epty * P.pexpr) -> 'asm env
     val push_local    : 'asm env -> P.pvar * P.epty -> 'asm env
     val push_implicit : 'asm env -> P.pvar * P.epty -> 'asm env
@@ -1225,6 +1212,12 @@ let word_of_wint wint_of_word ws (cast : W.signedness option) e =
     e, P.etwi s ws
 *)
 
+(* -------------------------------------------------------------------- *)
+let array_of_string s =
+  s |> String.to_list |> List.map @@ fun c ->
+  c |> Char.code |> Z.of_int |> fun z ->
+  P.(Papp1 (op_word_of_int(Word, W.Unsigned, W.U8), Pconst z))
+
 (* -------------------------------------------------------------------- *)
 let rec tt_expr pd ?(mode=`AllVar) (env : 'asm Env.env) pe =
   match L.unloc pe with
@@ -1357,6 +1350,18 @@ let rec tt_expr pd ?(mode=`AllVar) (env : 'asm Env.env) pe =
     if alen <> len then rs_tyerror ~loc (PackWrongLength (len, alen));
     P.PappN (E.Opack (sz, pz), args), P.etw sz
 
+  | S.PEarray es ->
+     let loc = L.loc pe in
+     let es = List.map (tt_expr ~mode pd env) es in
+     let es = List.map (fun (e, ty) -> cast loc e ty (ETword (None, U8))) es in
+     let len = Conv.pos_of_int (List.length es) in
+     P.PappN (E.Oarray len, es), P.(ETarr (U8, PE (Pconst (Conv.z_of_pos len))))
+
+  | S.PEstring s ->
+     let es = array_of_string s in
+     let len = Conv.pos_of_int (List.length es) in
+     P.PappN (E.Oarray len, es), P.(ETarr (U8, PE (Pconst (Conv.z_of_pos len))))
+
   | S.PEIf (pe1, pe2, pe3) ->
     let e1, ty1 = tt_expr ~mode pd env pe1 in
     let e2, ty2 = tt_expr ~mode pd env pe2 in
@@ -2315,47 +2320,11 @@ let tt_fundef arch_info (env0 : 'asm Env.env) loc (pf : S.pfundef) : 'asm Env.en
   Env.Funs.push env0 fdef {fs_tin; fs_tout}
 
 (* -------------------------------------------------------------------- *)
-let tt_global_def pd env (gd:S.gpexpr) =
-  let f e =
-    let pe,ety = tt_expr ~mode:`AllVar pd env e in
-    (L.mk_loc e.pl_loc pe, ety) in
-  let array_of_string s =
-    L.unloc s |> String.to_list |> List.map @@ fun c ->
-    c |> Char.code |> Z.of_int |> fun z ->
-    P.(L.mk_loc (L.loc s) (Papp1 (op_word_of_int(Word, W.Unsigned, W.U8), Pconst z)), P.etw U8) in
-  match gd with
-  | S.GEword e ->
-    `Word (f e)
-  | S.GEarray es ->
-    `Array (List.map f es)
-  | S.GEstring e ->
-    `Array (array_of_string e)
-
 let tt_global pd (env : 'asm Env.env) _loc (gd: S.pglobal) : 'asm Env.env =
 
-  let open P in
-  let mk_pe ws (pe,ety) =
-    match ety with
-    | P.ETword(wk, ews) when wk = None && Utils0.cmp_le Wsize.wsize_cmp ws ews ->
-      L.unloc pe
-    | P.ETint -> Papp1 (op_word_of_int(Word, W.Unsigned, ws), L.unloc pe)
-    | _ -> rs_tyerror ~loc:(L.loc pe) (TypeMismatch (ety, P.etw ws))
-    in
-
-  let ty, d =
-    match tt_type pd env gd.S.pgd_type, tt_global_def pd env gd.S.pgd_val with
-    | P.ETword(None, ws) as ty, `Word (pe,ety) ->
-      let pe = mk_pe ws (pe,ety) in
-      ty, P.GEword pe
-    | (P.ETint | P.ETbool | P.ETword _), `Array _ ->
-      rs_tyerror ~loc:(L.loc gd.S.pgd_type) GlobArrayNotWord
-    | P.ETarr(ws, _n) as ty, `Array es ->
-      let pes = List.map (mk_pe ws) es in
-      ty, P.GEarray pes
-    | P.ETarr _, `Word _ ->
-      rs_tyerror ~loc:(L.loc gd.S.pgd_type) GlobWordNotArray
-    | ty,_ -> rs_tyerror ~loc:(L.loc gd.S.pgd_type) (InvalidTypeForGlobal ty)
-  in
+  let ty = tt_type pd env gd.S.pgd_type in
+  let d, dty = tt_expr ~mode:`AllVar pd env gd.S.pgd_val in
+  let d = cast (L.loc gd.S.pgd_name) d dty ty in
 
   let x = mk_var (L.unloc gd.S.pgd_name) W.Global ty (L.loc gd.S.pgd_name) [] in
 
diff --git a/compiler/src/printer.ml b/compiler/src/printer.ml
index 59044f19f8..68894c49a5 100644
--- a/compiler/src/printer.ml
+++ b/compiler/src/printer.ml
@@ -270,10 +270,6 @@ let pp_gfun ~debug (pp_size:F.formatter -> 'size -> unit) pp_opn pp_var fmt fd =
 
 let pp_noinfo _ _ = ()
 
-let pp_gexpr ~debug pp_len pp_var fmt = function
-  | GEword e -> pp_ge ~debug pp_len pp_var fmt e
-  | GEarray es -> Format.fprintf fmt "{@[%a@]}" (pp_ges ~debug pp_len pp_var) es
-
 let pp_pitem ~debug pp_len pp_opn pp_var =
   let aux fmt = function
    | MIfun fd -> pp_gfun ~debug pp_len pp_opn pp_var fmt fd
@@ -285,7 +281,7 @@ let pp_pitem ~debug pp_len pp_opn pp_var =
       F.fprintf fmt "%a %a = %a;"
         (pp_gtype pp_len) x.v_ty
         pp_var x
-        (pp_gexpr ~debug pp_len pp_var) e
+        (pp_ge ~debug pp_len pp_var) e
  in
   aux
 
diff --git a/compiler/src/prog.ml b/compiler/src/prog.ml
index cbf97cfecb..3f71c64dd3 100644
--- a/compiler/src/prog.ml
+++ b/compiler/src/prog.ml
@@ -125,14 +125,10 @@ type ('len, 'info, 'asm) gfunc = {
     f_ret  : 'len gvar_i list
   }
 
-type 'len ggexpr =
-  | GEword of 'len gexpr
-  | GEarray of 'len gexprs
-
 type ('len, 'info, 'asm) gmod_item =
   | MIfun   of ('len, 'info, 'asm) gfunc
   | MIparam of ('len gvar * 'len gexpr)
-  | MIglobal of ('len gvar * 'len ggexpr)
+  | MIglobal of ('len gvar * 'len gexpr)
 
 type ('len, 'info, 'asm) gprog = ('len, 'info, 'asm) gmod_item list
    (* first declaration occur at the end (i.e reverse order) *)
diff --git a/compiler/src/prog.mli b/compiler/src/prog.mli
index 434e070918..8675c8ac7a 100644
--- a/compiler/src/prog.mli
+++ b/compiler/src/prog.mli
@@ -92,14 +92,10 @@ type ('len, 'info, 'asm) gfunc = {
     f_ret  : 'len gvar_i list
   }
 
-type 'len ggexpr =
-  | GEword of 'len gexpr
-  | GEarray of 'len gexprs
-
 type ('len, 'info, 'asm) gmod_item =
   | MIfun   of ('len, 'info, 'asm) gfunc
   | MIparam of ('len gvar * 'len gexpr)
-  | MIglobal of ('len gvar * 'len ggexpr)
+  | MIglobal of ('len gvar * 'len gexpr)
 
 type ('len, 'info, 'asm) gprog = ('len, 'info, 'asm) gmod_item list
    (* first declaration occur at the end (i.e reverse order) *)
diff --git a/compiler/src/subst.ml b/compiler/src/subst.ml
index cbd6c07ed3..6b7220dfe8 100644
--- a/compiler/src/subst.ml
+++ b/compiler/src/subst.ml
@@ -122,10 +122,6 @@ let psubst_v subst =
     | _      -> e in
   aux
 
-let psubst_ge f = function
-  | GEword e -> GEword (psubst_e f e)
-  | GEarray es -> GEarray (List.map (psubst_e f) es)
-
 let psubst_prog (prog:('info, 'asm) pprog) =
   let subst = ref (Mpv.empty : pexpr Mpv.t) in
   let rec aux = function
@@ -142,7 +138,7 @@ let psubst_prog (prog:('info, 'asm) pprog) =
         let v =
           gsubst_gvar f {gv = L.mk_loc L._dummy v; gs = Expr.Sglob} in
         assert (not (is_gkvar v)); L.unloc v.gv in
-      let e = psubst_ge f e in
+      let e = psubst_e f e in
       subst := Mpv.add v (Pvar (gkglob (L.mk_loc L._dummy v'))) !subst;
       (v', e) :: g, p
     | MIfun fc :: items ->
@@ -249,10 +245,7 @@ let isubst_prog glob prog =
         gsubst_gvar subst_v {gv = L.mk_loc L._dummy x; gs = Expr.Sglob} in
       assert (not (is_gkvar x)); L.unloc x.gv in
 
-    let gd =
-      match gd with
-      | GEword e -> GEword (gsubst_e isubst_len subst_v e)
-      | GEarray es -> GEarray (List.map (gsubst_e isubst_len subst_v) es) in
+    let gd = gsubst_e isubst_len subst_v gd in
     x, gd in
   let glob = List.map isubst_glob glob in
 
@@ -334,20 +327,20 @@ let remove_params (prog : ('info, 'asm) pprog) =
   let doglob (x, e) =
     let gv =
       match x.v_ty, e with
-      | Bty (U ws), GEword e ->
+      | Bty (U ws), e ->
         begin try Global.Gword (ws, mk_word ws e)
         with NotAConstantExpr ->
-          hierror ~loc:x.v_dloc "the expression assigned to global variable %a must evaluate to a constant"
+          hierror ~loc:x.v_dloc "the expression assigned to global variable %a must evaluate to a constant word"
             (Printer.pp_var ~debug:false) x
         end
-      | Arr (_ws, n), GEarray es when List.length es <> n ->
+      | Arr (_ws, n), PappN (E.Oarray _len, es) when List.length es <> n ->
          let m = List.length es in
          hierror ~loc:x.v_dloc "array size mismatch for global variable %a: %d %s given (%d expected)"
            (Printer.pp_var ~debug:false) x
            (List.length es)
            (if m > 1 then "values" else "value")
            n
-      | Arr (ws, n), GEarray es ->
+      | Arr (ws, n), PappN (E.Oarray _len, es) ->
         let p = Conv.pos_of_int (n * size_of_ws ws) in
         let mk_word_i i e =
           try mk_word ws e
@@ -358,7 +351,11 @@ let remove_params (prog : ('info, 'asm) pprog) =
         in
         let t = Warray_.WArray.of_list ws (List.mapi mk_word_i es) in
         Global.Garr(p, t)
-      | _, _ -> assert false in
+      | Arr _, _ -> hierror ~loc:x.v_dloc "ill-typed global array"
+      | Bty (Bool | Int), _ ->
+         hierror ~loc:x.v_dloc "globals should have type word; found: ‘%a’"
+           PrintCommon.pp_ty x.v_ty
+    in
     add_glob x gv;
     x, gv
   in
diff --git a/compiler/src/syntax.ml b/compiler/src/syntax.ml
index 490dd4cfe6..60256bd48d 100644
--- a/compiler/src/syntax.ml
+++ b/compiler/src/syntax.ml
@@ -172,6 +172,8 @@ type pexpr_r =
   | PEGet    of [`Aligned|`Unaligned] option * arr_access * swsize L.located option * pident * pexpr * pexpr option
   | PEFetch  of mem_access
   | PEpack   of svsize * pexpr list
+  | PEarray of pexpr list
+  | PEstring of string
   | PEBool   of bool
   | PEInt    of int_representation
   | PECall   of pident * pexpr list
@@ -318,12 +320,7 @@ type pfundef = {
 }
 
 (* -------------------------------------------------------------------- *)
-type gpexpr =
-  | GEword  of pexpr
-  | GEarray of pexpr list
-  | GEstring of string L.located
-
-type pglobal = { pgd_type: ptype; pgd_name: pident ; pgd_val: gpexpr }
+type pglobal = { pgd_type: ptype; pgd_name: pident ; pgd_val: pexpr }
 
 (* -------------------------------------------------------------------- *)
 type pexec = {
diff --git a/compiler/src/typing.ml b/compiler/src/typing.ml
index 5e50441ae7..15bc595465 100644
--- a/compiler/src/typing.ml
+++ b/compiler/src/typing.ml
@@ -16,20 +16,20 @@ let error loc fmt =
     bfmt fmt
 
 (* -------------------------------------------------------------------- *)
-let ty_var (x:var_i) =
-  let ty = (L.unloc x).v_ty in
+let ty_var (x: var) =
+  let ty = x.v_ty in
   begin match ty with
   | Arr(_, n) ->
       if (n < 1) then
-        error (L.i_loc0 (L.unloc x).v_dloc)
+        error (L.i_loc0 x.v_dloc)
           "the variable %a has type %a, its array size should be positive"
-          (Printer.pp_var ~debug:false) (L.unloc x) PrintCommon.pp_ty ty
+          (Printer.pp_var ~debug:false) x PrintCommon.pp_ty ty
   | _ -> ()
   end;
   ty
 
 
-let ty_gvar (x:int ggvar) = ty_var x.gv
+let ty_gvar (x: int ggvar) = ty_var (L.unloc x.gv)
 
 (* -------------------------------------------------------------------- *)
 
@@ -150,7 +150,7 @@ and ty_get_set_sub pd loc ws len x e =
 
 let ty_lval pd loc = function
   | Lnone (_, ty) -> ty
-  | Lvar x -> ty_var x
+  | Lvar x -> ty_var (L.unloc x)
   | Lmem(_, ws,_,e) -> ty_load_store pd loc ws e
   | Laset(_al,_aa,ws,x,e) -> ty_get_set pd loc ws (gkvar x) e
   | Lasub(_aa,ws,len,x,e) -> ty_get_set_sub pd loc ws len (gkvar x) e
@@ -218,6 +218,26 @@ let rec check_instr pd msfsz asmOp env i =
 and check_cmd pd msfsz asmOp env c =
   List.iter (check_instr pd msfsz asmOp env) c
 
+(* -------------------------------------------------------------------- *)
+let check_global_decl (g, d) =
+  let ty = ty_var g in
+  let error vty =
+    error (L.i_loc0 g.v_dloc)
+      "global variable %a has type %a but its value has type %a"
+      (Printer.pp_var ~debug:false)
+      g PrintCommon.pp_ty ty PrintCommon.pp_ty vty
+  in
+  match d with
+  | Global.Garr (len, _) ->
+      if
+        match ty with
+        | Arr (ws, len') -> Conv.int_of_pos len <> arr_size ws len'
+        | _ -> true
+      then error (Arr (U8, Conv.int_of_pos len))
+  | Gword (ws, _) ->
+      if match ty with Bty (U ws') -> not (wsize_le ws ws') | _ -> true then
+        error (Bty (U ws))
+
 (* -------------------------------------------------------------------- *)
 
 let check_fun pd msfsz asmOp env fd =
@@ -231,6 +251,7 @@ let check_fun pd msfsz asmOp env fd =
 
 (* -------------------------------------------------------------------- *)
 
-let check_prog pd msfsz asmOp (_,funcs) =
+let check_prog pd msfsz asmOp (gds, funcs) =
   let env = Hf.create 107 in
+  List.iter check_global_decl gds;
   List.iter (check_fun pd msfsz asmOp env) (List.rev funcs)
diff --git a/compiler/tests/exec/exec.expected b/compiler/tests/exec/exec.expected
index 4ed13e1a05..2fd2c82a34 100644
--- a/compiler/tests/exec/exec.expected
+++ b/compiler/tests/exec/exec.expected
@@ -29,3 +29,6 @@ main() = [0XC0; 0XE6; 0XC4; 0X8E; 0XA9; 0XEF; 0X82; 0X0; 0X1D; 0XF3; 0X99;
          0X39; 0XB8; 0X1; 0X17; 0XC5; 0X8C; 0X89; 0X69; 0X84; 0XD1; 0X42;
          0X44; 0XB5; 0X1F; 0X92; 0X2E; 0X8A; 0X19; 0X13; 0XD3; 0X8; 0XA3;
          0X85; 0X88; 0X6A; 0X3F; 0X24; 0X3; 0X73; 0X70; 0X3]
+test_string(0X0) = 0X6F6C6568
+test_array(0X0) = 0X1010100
+combine(0X0; 0X1) = 0X1
diff --git a/compiler/tests/exec/exec.ml b/compiler/tests/exec/exec.ml
index 8b457648f0..6f70386dde 100644
--- a/compiler/tests/exec/exec.ml
+++ b/compiler/tests/exec/exec.ml
@@ -67,3 +67,10 @@ let () =
 let () =
   let prog = load_file "wide_rotation.jazz" in
   exec prog [] "main" []
+
+let () =
+  let prog = load_file "../success/common/literal-arrays.jazz" in
+  let w z = Jasmin.(Values.Vword (U32, Conv.word_of_z U32 z)) in
+  exec prog [] "test_string" [ w Z.zero ];
+  exec prog [] "test_array" [ w Z.zero ];
+  exec prog [] "combine" [ w Z.zero; w Z.one ]
diff --git a/compiler/tests/fail/typing/x86-64/global_type_mismatch.jazz b/compiler/tests/fail/typing/x86-64/global_type_mismatch.jazz
new file mode 100644
index 0000000000..b92b195bd9
--- /dev/null
+++ b/compiler/tests/fail/typing/x86-64/global_type_mismatch.jazz
@@ -0,0 +1 @@
+u32 g = { 42 };
diff --git a/compiler/tests/fail/typing/x86-64/global_type_mismatch2.jazz b/compiler/tests/fail/typing/x86-64/global_type_mismatch2.jazz
new file mode 100644
index 0000000000..ee58ac7a47
--- /dev/null
+++ b/compiler/tests/fail/typing/x86-64/global_type_mismatch2.jazz
@@ -0,0 +1,2 @@
+u32[1] g = 42;
+
diff --git a/compiler/tests/negative.expected b/compiler/tests/negative.expected
index e7fb11384d..e0e02dfd9d 100644
--- a/compiler/tests/negative.expected
+++ b/compiler/tests/negative.expected
@@ -742,7 +742,7 @@ fail/param_expansion/x86-64/global_not_constant.jazz:
 
 "fail/param_expansion/x86-64/global_not_constant.jazz", line 2 (4-5):
 compilation error:
-param expansion: the expression assigned to global variable b must evaluate to a constant
+param expansion: the expression assigned to global variable b must evaluate to a constant word
 
 fail/param_expansion/x86-64/operator_arg.jazz:
 
@@ -1354,11 +1354,21 @@ typing error: x has kind stack, only reg or reg ptr are allowed in result of non
 
 fail/typing/x86-64/global_in_global_def.jazz:
 
-"fail/typing/x86-64/global_in_global_def.jazz", line 2 (10-19): the expression has type u8 instead of u16
+"fail/typing/x86-64/global_in_global_def.jazz", line 2 (4-7): can not implicitly cast u8 into u16
 
 fail/typing/x86-64/global_int.jazz:
 
-"fail/typing/x86-64/global_int.jazz", line 1 (0-3): globals should have type word; found: ‘int’
+"fail/typing/x86-64/global_int.jazz", line 1 (4-5):
+compilation error:
+param expansion: globals should have type word; found: ‘int’
+
+fail/typing/x86-64/global_type_mismatch.jazz:
+
+"fail/typing/x86-64/global_type_mismatch.jazz", line 1 (4-5): can not implicitly cast u8[1] into u32
+
+fail/typing/x86-64/global_type_mismatch2.jazz:
+
+"fail/typing/x86-64/global_type_mismatch2.jazz", line 1 (7-8): can not implicitly cast int into u32[1]
 
 fail/typing/x86-64/init_global.jazz:
 
@@ -1523,7 +1533,7 @@ Allowed args are:
 
 Statistics:
 	Annots:      0
-	Pretyping:  45
+	Pretyping:  46
 	Parsing:     4
 	Typing:      1
-	Compile:   190
+	Compile:   191
diff --git a/compiler/tests/printing.ml b/compiler/tests/printing.ml
index bd8cf7d017..e528f67eaa 100644
--- a/compiler/tests/printing.ml
+++ b/compiler/tests/printing.ml
@@ -109,12 +109,6 @@ and eq_pexpr x y =
 and eq_pexprs x y = List.for_all2 eq_pexpr x y
 and eq_pexpr_ (PE x) (PE y) = eq_pexpr x y
 
-let eq_pgexpr x y =
-  match (x, y) with
-  | GEword a, GEword b -> eq_pexpr a b
-  | GEarray a, GEarray b -> eq_pexprs a b
-  | (GEword _ | GEarray _), _ -> false
-
 let eq_prange (x : pexpr_ grange) (y : pexpr_ grange) =
   let a, b, c = x and d, e, f = y in
   a = d && eq_pexpr b e && eq_pexpr c f
@@ -167,7 +161,7 @@ let eq_pmod_item x y =
   match (x, y) with
   | MIfun f, MIfun g -> eq_pfunc f g
   | MIparam (x, i), MIparam (y, j) -> eq_pvar x y && eq_pexpr i j
-  | MIglobal (x, i), MIglobal (y, j) -> eq_pvar x y && eq_pgexpr i j
+  | MIglobal (x, i), MIglobal (y, j) -> eq_pvar x y && eq_pexpr i j
   | (MIfun _ | MIparam _ | MIglobal _), _ -> false
 
 let eq_pmod_items x y = List.for_all2 eq_pmod_item x y
diff --git a/compiler/tests/success/common/literal-arrays.jazz b/compiler/tests/success/common/literal-arrays.jazz
new file mode 100644
index 0000000000..7b929bfdfa
--- /dev/null
+++ b/compiler/tests/success/common/literal-arrays.jazz
@@ -0,0 +1,32 @@
+export fn test_string(reg u32 x) -> reg u32 {
+  global u8[4] g = "helo";
+  reg u32 y = g[:u32 0];
+  x += y;
+  return x;
+}
+
+inline fn from_parts(inline u8 a b c d) -> reg u32 {
+  global u8[4] u = { a, b, c, d };
+  reg u32 v = u[:u32 0];
+  return v;
+}
+
+export fn test_array(reg u32 x) -> reg u32 {
+  reg u32 y;
+  y = from_parts(1, 2, 3, 4);
+  x += y;
+  y = from_parts(-1, -2, -3, -4);
+  x += y;
+  return x;
+}
+
+export fn combine(reg u32 x y) -> reg u32 {
+  global u8[2] coefficients = { 0, 1 };
+  reg u32 coeff;
+  coeff = (32u)coefficients[0];
+  x *= coeff;
+  coeff = (32u)coefficients[1];
+  y *= coeff;
+  x += y;
+  return x;
+}
diff --git a/docs/source/language/syntax/expressions.md b/docs/source/language/syntax/expressions.md
index 1625abe10f..c8eb15e6d0 100644
--- a/docs/source/language/syntax/expressions.md
+++ b/docs/source/language/syntax/expressions.md
@@ -3,6 +3,8 @@
 <expr> ::=
   | <int>  // Integer constant.
   | <bool>  // Boolean constant.
+  | <string> // String constant.
+  | { <expr>, ..., <expr> } // Array.
   | <var>  // Variable.
   | [<expr>] // Memory access.
   | [:<wsize> <expr>] // Memory access.
@@ -27,6 +29,7 @@ Expressions are made of:
 
   - constants (`true`, `false`,  `42`, `0xabcd`);
   - packs (`(4u2)[0, 3, 2, 1]`);
+  - byte arrays (`"Hello World!"`, `{ x, 0o77 }`);
   - variables (`x`);
   - parenthesized subexpressions (`(e)`);
   - memory loads (`[:u16 p + 2 * i]`);