From 1214ab71b713cdb5467092075f8c2bb059938fca Mon Sep 17 00:00:00 2001
From: Josh Berdine <jjb@fb.com>
Date: Mon, 15 Jun 2020 15:41:59 -0700
Subject: [PATCH] [sledge] Refactor: Rename to use terminology for "sized
 sequences"

Summary:
Logically there is nothing specific to memory contents (as
byte-arrays) or aggregate (struct/array) values, the theory is for
sequences of non-fixed sized elements.

Reviewed By: jvillard

Differential Revision: D21721019

fbshipit-source-id: b2b730a50
---
 sledge/src/domain_sh.ml   | 14 +++---
 sledge/src/equality.ml    | 66 ++++++++++++++---------------
 sledge/src/exec.ml        | 80 +++++++++++++++++------------------
 sledge/src/llair/exp.ml   |  2 +-
 sledge/src/llair/exp.mli  |  2 +-
 sledge/src/sh.ml          | 24 +++++------
 sledge/src/sh.mli         |  7 ++-
 sledge/src/sh_test.ml     |  6 +--
 sledge/src/solver.ml      | 76 ++++++++++++++++-----------------
 sledge/src/solver_test.ml | 58 ++++++++++++-------------
 sledge/src/term.ml        | 89 +++++++++++++++++++--------------------
 sledge/src/term.mli       | 16 +++----
 12 files changed, 219 insertions(+), 221 deletions(-)

diff --git a/sledge/src/domain_sh.ml b/sledge/src/domain_sh.ml
index f8514800d..86070e330 100644
--- a/sledge/src/domain_sh.ml
+++ b/sledge/src/domain_sh.ml
@@ -18,11 +18,11 @@ let simplify q = if !simplify_states then Sh.simplify q else q
 
 let init globals =
   IArray.fold globals ~init:Sh.emp ~f:(fun q -> function
-    | {Llair.Global.reg; init= Some (arr, siz)} ->
+    | {Llair.Global.reg; init= Some (seq, siz)} ->
         let loc = Term.var (Var.of_reg reg) in
         let len = Term.integer (Z.of_int siz) in
-        let arr = Term.of_exp arr in
-        Sh.star q (Sh.seg {loc; bas= loc; len; siz= len; arr})
+        let seq = Term.of_exp seq in
+        Sh.star q (Sh.seg {loc; bas= loc; len; siz= len; seq})
     | _ -> q )
 
 let join p q =
@@ -105,7 +105,7 @@ let garbage_collect (q : t) ~wrt =
       let new_set =
         List.fold ~init:current q.heap ~f:(fun current seg ->
             if term_eq_class_has_only_vars_in current q.cong seg.loc then
-              List.fold (Equality.class_of q.cong seg.arr) ~init:current
+              List.fold (Equality.class_of q.cong seg.seq) ~init:current
                 ~f:(fun c e -> Var.Set.union c (Term.fv e))
             else current )
       in
@@ -335,9 +335,9 @@ let%test_module _ =
     let b = Term.var b_
     let n = Term.var n_
     let endV = Term.var end_
-    let seg_main = Sh.seg {loc= main; bas= b; len= n; siz= n; arr= a}
-    let seg_a = Sh.seg {loc= a; bas= b; len= n; siz= n; arr= endV}
-    let seg_cycle = Sh.seg {loc= a; bas= b; len= n; siz= n; arr= main}
+    let seg_main = Sh.seg {loc= main; bas= b; len= n; siz= n; seq= a}
+    let seg_a = Sh.seg {loc= a; bas= b; len= n; siz= n; seq= endV}
+    let seg_cycle = Sh.seg {loc= a; bas= b; len= n; siz= n; seq= main}
 
     let%expect_test _ =
       pp (garbage_collect seg_main ~wrt:(Var.Set.of_list [])) ;
diff --git a/sledge/src/equality.ml b/sledge/src/equality.ml
index aeb1a95e5..4dd80b120 100644
--- a/sledge/src/equality.ml
+++ b/sledge/src/equality.ml
@@ -14,7 +14,7 @@ type kind = Interpreted | Atomic | Uninterpreted
 
 let classify e =
   match (e : Term.t) with
-  | Add _ | Ap2 (Memory, _, _) | Ap3 (Extract, _, _, _) | ApN (Concat, _) ->
+  | Add _ | Ap2 (Sized, _, _) | Ap3 (Extract, _, _, _) | ApN (Concat, _) ->
       Interpreted
   | Mul _ | Ap1 _ | Ap2 _ | Ap3 _ | ApN _ | And _ | Or _ -> Uninterpreted
   | Var _ | Integer _ | Rational _ | Float _ | Label _ | RecRecord _ ->
@@ -178,13 +178,13 @@ end
 (** Theory Solver *)
 
 (** prefer representative terms that are minimal in the order s.t. Var <
-    Memory < Extract < Concat < others, then using height of aggregate
+    Sized < Extract < Concat < others, then using height of sequence
     nesting, and then using Term.compare *)
 let prefer e f =
   let rank e =
     match (e : Term.t) with
     | Var _ -> 0
-    | Ap2 (Memory, _, _) -> 1
+    | Ap2 (Sized, _, _) -> 1
     | Ap3 (Extract, _, _, _) -> 2
     | ApN (Concat, _) -> 3
     | _ -> 4
@@ -229,16 +229,16 @@ let solve_poly ?f p q s =
 (* α[o,l) = β ==> l = |β| ∧ α = (⟨n,c⟩[0,o) ^ β ^ ⟨n,c⟩[o+l,n-o-l)) where n
    = |α| and c fresh *)
 let rec solve_extract ?f a o l b s =
-  let n = Term.agg_size_exn a in
+  let n = Term.seq_size_exn a in
   let c, s = fresh "c" s in
-  let n_c = Term.memory ~siz:n ~arr:c in
+  let n_c = Term.sized ~siz:n ~seq:c in
   let o_l = Term.add o l in
   let n_o_l = Term.sub n o_l in
-  let c0 = Term.extract ~agg:n_c ~off:Term.zero ~len:o in
-  let c1 = Term.extract ~agg:n_c ~off:o_l ~len:n_o_l in
+  let c0 = Term.extract ~seq:n_c ~off:Term.zero ~len:o in
+  let c1 = Term.extract ~seq:n_c ~off:o_l ~len:n_o_l in
   let b, s =
-    match Term.agg_size b with
-    | None -> (Term.memory ~siz:l ~arr:b, Some s)
+    match Term.seq_size b with
+    | None -> (Term.sized ~siz:l ~seq:b, Some s)
     | Some m -> (b, solve_ ?f l m s)
   in
   s >>= solve_ ?f a (Term.concat [|c0; b; c1|])
@@ -248,9 +248,9 @@ let rec solve_extract ?f a o l b s =
 and solve_concat ?f a0V b m s =
   IArray.fold_until a0V ~init:(s, Term.zero)
     ~f:(fun (s, oI) aJ ->
-      let nJ = Term.agg_size_exn aJ in
+      let nJ = Term.seq_size_exn aJ in
       let oJ = Term.add oI nJ in
-      match solve_ ?f aJ (Term.extract ~agg:b ~off:oI ~len:nJ) s with
+      match solve_ ?f aJ (Term.extract ~seq:b ~off:oI ~len:nJ) s with
       | Some s -> Continue (s, oJ)
       | None -> Stop None )
     ~finish:(fun (s, n0V) -> solve_ ?f n0V m s)
@@ -266,18 +266,18 @@ and solve_ ?f d e s =
   (* i = j ==> false when i ≠ j *)
   | Some (Integer _, Integer _) | Some (Rational _, Rational _) -> None
   (* ⟨0,a⟩ = β ==> a = β = ⟨⟩ *)
-  | Some (Ap2 (Memory, n, a), b) when Term.equal n Term.zero ->
+  | Some (Ap2 (Sized, n, a), b) when Term.equal n Term.zero ->
       s |> solve_ ?f a (Term.concat [||]) >>= solve_ ?f b (Term.concat [||])
-  | Some (b, Ap2 (Memory, n, a)) when Term.equal n Term.zero ->
+  | Some (b, Ap2 (Sized, n, a)) when Term.equal n Term.zero ->
       s |> solve_ ?f a (Term.concat [||]) >>= solve_ ?f b (Term.concat [||])
   (* v = ⟨n,a⟩ ==> v = a *)
-  | Some ((Var _ as v), Ap2 (Memory, _, a)) -> s |> solve_ ?f v a
+  | Some ((Var _ as v), Ap2 (Sized, _, a)) -> s |> solve_ ?f v a
   (* ⟨n,a⟩ = ⟨m,b⟩ ==> n = m ∧ a = β *)
-  | Some (Ap2 (Memory, n, a), Ap2 (Memory, m, b)) ->
+  | Some (Ap2 (Sized, n, a), Ap2 (Sized, m, b)) ->
       s |> solve_ ?f n m >>= solve_ ?f a b
   (* ⟨n,a⟩ = β ==> n = |β| ∧ a = β *)
-  | Some (Ap2 (Memory, n, a), b) ->
-      ( match Term.agg_size b with
+  | Some (Ap2 (Sized, n, a), b) ->
+      ( match Term.seq_size b with
       | None -> Some s
       | Some m -> solve_ ?f n m s )
       >>= solve_ ?f a b
@@ -287,19 +287,19 @@ and solve_ ?f d e s =
         compose1 ?f ~var:v ~rep:e s
       else
         (* v = α[o,l) ==> α[o,l) ↦ ⟨l,v⟩ when v ∈ fv(α[o,l)) *)
-        compose1 ?f ~var:e ~rep:(Term.memory ~siz:l ~arr:v) s
+        compose1 ?f ~var:e ~rep:(Term.sized ~siz:l ~seq:v) s
   | Some ((Var _ as v), (ApN (Concat, a0V) as c)) ->
       if not (Var.Set.mem (Term.fv c) (Var.of_ v)) then
         (* v = α₀^…^αᵥ ==> v ↦ α₀^…^αᵥ when v ∉ fv(α₀^…^αᵥ) *)
         compose1 ?f ~var:v ~rep:c s
       else
         (* v = α₀^…^αᵥ ==> ⟨|α₀^…^αᵥ|,v⟩ = α₀^…^αᵥ when v ∈ fv(α₀^…^αᵥ) *)
-        let m = Term.agg_size_exn c in
-        solve_concat ?f a0V (Term.memory ~siz:m ~arr:v) m s
+        let m = Term.seq_size_exn c in
+        solve_concat ?f a0V (Term.sized ~siz:m ~seq:v) m s
   | Some ((Ap3 (Extract, _, _, l) as e), ApN (Concat, a0V)) ->
       solve_concat ?f a0V e l s
   | Some (ApN (Concat, a0V), (ApN (Concat, _) as c)) ->
-      solve_concat ?f a0V c (Term.agg_size_exn c) s
+      solve_concat ?f a0V c (Term.seq_size_exn c) s
   | Some (Ap3 (Extract, a, o, l), e) -> solve_extract ?f a o l e s
   (* p = q ==> p-q = 0 *)
   | Some
@@ -772,7 +772,7 @@ let solve_poly_eq us p' q' subst =
   [%Trace.retn fun {pf} subst' ->
     pf "@[%a@]" Subst.pp_diff (subst, Option.value subst' ~default:subst)]
 
-let solve_memory_eq us e' f' subst =
+let solve_seq_eq us e' f' subst =
   [%Trace.call fun {pf} -> pf "%a = %a" Term.pp e' Term.pp f']
   ;
   let f x u =
@@ -781,9 +781,9 @@ let solve_memory_eq us e' f' subst =
   in
   let solve_concat ms n a =
     let a, n =
-      match Term.agg_size a with
+      match Term.seq_size a with
       | Some n -> (a, n)
-      | None -> (Term.memory ~siz:n ~arr:a, n)
+      | None -> (Term.sized ~siz:n ~seq:a, n)
     in
     let+ _, xs, s = solve_concat ~f ms a n (us, Var.Set.empty, subst) in
     assert (Var.Set.is_empty xs) ;
@@ -791,12 +791,12 @@ let solve_memory_eq us e' f' subst =
   in
   ( match ((e' : Term.t), (f' : Term.t)) with
   | (ApN (Concat, ms) as c), a when f c a ->
-      solve_concat ms (Term.agg_size_exn c) a
+      solve_concat ms (Term.seq_size_exn c) a
   | a, (ApN (Concat, ms) as c) when f c a ->
-      solve_concat ms (Term.agg_size_exn c) a
-  | (Ap2 (Memory, _, (Var _ as v)) as m), u when f m u ->
+      solve_concat ms (Term.seq_size_exn c) a
+  | (Ap2 (Sized, _, (Var _ as v)) as m), u when f m u ->
       Some (Subst.compose1 ~key:v ~data:u subst)
-  | u, (Ap2 (Memory, _, (Var _ as v)) as m) when f m u ->
+  | u, (Ap2 (Sized, _, (Var _ as v)) as m) when f m u ->
       Some (Subst.compose1 ~key:v ~data:u subst)
   | _ -> None )
   |>
@@ -810,7 +810,7 @@ let solve_interp_eq us e' (cls, subst) =
   ;
   List.find_map cls ~f:(fun f ->
       let f' = Subst.norm subst f in
-      match solve_memory_eq us e' f' subst with
+      match solve_seq_eq us e' f' subst with
       | Some subst -> Some subst
       | None -> solve_poly_eq us e' f' subst )
   |>
@@ -853,7 +853,7 @@ type cls_solve_state =
 
 let dom_trm e =
   match (e : Term.t) with
-  | Ap2 (Memory, _, (Var _ as v)) -> Some v
+  | Ap2 (Sized, _, (Var _ as v)) -> Some v
   | _ when non_interpreted e -> Some e
   | _ -> None
 
@@ -960,7 +960,7 @@ let solve_concat_extracts_eq r x =
   ;
   let uses =
     fold_uses_of r x ~init:[] ~f:(fun uses -> function
-      | Ap2 (Memory, _, _) as m ->
+      | Ap2 (Sized, _, _) as m ->
           fold_uses_of r m ~init:uses ~f:(fun uses -> function
             | Ap3 (Extract, _, _, _) as e -> e :: uses | _ -> uses )
       | _ -> uses )
@@ -975,7 +975,7 @@ let solve_concat_extracts_eq r x =
     List.fold (find_extracts_at_off off) ~init:full_rev_extracts
       ~f:(fun full_rev_extracts e ->
         match e with
-        | Ap3 (Extract, Ap2 (Memory, n, _), o, l) ->
+        | Ap3 (Extract, Ap2 (Sized, n, _), o, l) ->
             let o_l = Term.add o l in
             if entails_eq r n o_l then
               (e :: rev_prefix) :: full_rev_extracts
@@ -999,7 +999,7 @@ let solve_concat_extracts r us x (classes, subst, us_xs) =
                       Some trm
                   | _ -> rep_ito_us )
             in
-            Term.memory ~siz:(Term.agg_size_exn e) ~arr:rep_ito_us :: suffix ) )
+            Term.sized ~siz:(Term.seq_size_exn e) ~seq:rep_ito_us :: suffix ) )
     |> List.min_elt ~compare:[%compare: Term.t list]
   with
   | Some extracts ->
diff --git a/sledge/src/exec.ml b/sledge/src/exec.ml
index 7ec93c083..f0ebec935 100644
--- a/sledge/src/exec.ml
+++ b/sledge/src/exec.ml
@@ -19,7 +19,7 @@ let fresh_var nam us xs =
   let var, us = Var.fresh nam ~wrt:us in
   (Term.var var, us, Var.Set.add xs var)
 
-let fresh_seg ~loc ?bas ?len ?siz ?arr ?(xs = Var.Set.empty) us =
+let fresh_seg ~loc ?bas ?len ?siz ?seq ?(xs = Var.Set.empty) us =
   let freshen term nam us xs =
     match term with
     | Some term -> (term, us, xs)
@@ -28,15 +28,15 @@ let fresh_seg ~loc ?bas ?len ?siz ?arr ?(xs = Var.Set.empty) us =
   let bas, us, xs = freshen bas "b" us xs in
   let len, us, xs = freshen len "m" us xs in
   let siz, us, xs = freshen siz "n" us xs in
-  let arr, us, xs = freshen arr "a" us xs in
-  {us; xs; seg= {loc; bas; len; siz; arr}}
+  let seq, us, xs = freshen seq "a" us xs in
+  {us; xs; seg= {loc; bas; len; siz; seq}}
 
 let null_eq ptr = Sh.pure (Term.eq Term.zero ptr)
 
-let eq_concat (siz, arr) ms =
+let eq_concat (siz, seq) ms =
   Term.(
-    eq (memory ~siz ~arr)
-      (concat (Array.map ~f:(fun (siz, arr) -> memory ~siz ~arr) ms)))
+    eq (sized ~siz ~seq)
+      (concat (Array.map ~f:(fun (siz, seq) -> sized ~siz ~seq) ms)))
 
 (* Overwritten variables renaming and remaining modified variables. [ws] are
    the written variables; [rs] are the variables read or in the
@@ -82,7 +82,7 @@ let load_spec us reg ptr len =
   let sub, ms, _ = assign ~ws:(Var.Set.of_ reg) ~rs:foot.us ~us in
   let post =
     Sh.and_
-      (Term.eq (Term.var reg) (Term.rename sub seg.arr))
+      (Term.eq (Term.var reg) (Term.rename sub seg.seq))
       (Sh.rename sub foot)
   in
   {xs; foot; sub; ms; post}
@@ -94,7 +94,7 @@ let load_spec us reg ptr len =
 let store_spec us ptr exp len =
   let {us= _; xs; seg} = fresh_seg ~loc:ptr ~siz:len us in
   let foot = Sh.seg seg in
-  let post = Sh.seg {seg with arr= exp} in
+  let post = Sh.seg {seg with seq= exp} in
   {xs; foot; sub= Var.Subst.empty; ms= Var.Set.empty; post}
 
 (* { d-[b;m)->⟨l,α⟩ }
@@ -104,7 +104,7 @@ let store_spec us ptr exp len =
 let memset_spec us dst byt len =
   let {us= _; xs; seg} = fresh_seg ~loc:dst ~siz:len us in
   let foot = Sh.seg seg in
-  let post = Sh.seg {seg with arr= Term.splat byt} in
+  let post = Sh.seg {seg with seq= Term.splat byt} in
   {xs; foot; sub= Var.Subst.empty; ms= Var.Set.empty; post}
 
 (* { d=s * l=0 * d-[b;m)->⟨l,α⟩ }
@@ -129,7 +129,7 @@ let memcpy_dj_spec us dst src len =
   let dst_heap = Sh.seg dst_seg in
   let {us= _; xs; seg= src_seg} = fresh_seg ~loc:src ~siz:len ~xs us in
   let src_heap = Sh.seg src_seg in
-  let dst_seg' = {dst_seg with arr= src_seg.arr} in
+  let dst_seg' = {dst_seg with seq= src_seg.seq} in
   let dst_heap' = Sh.seg dst_seg' in
   let foot = Sh.star dst_heap src_heap in
   let post = Sh.star dst_heap' src_heap in
@@ -160,23 +160,23 @@ let memmov_foot us dst src len =
   let xs = Var.Set.empty in
   let bas, us, xs = fresh_var "b" us xs in
   let siz, us, xs = fresh_var "m" us xs in
-  let arr_dst, us, xs = fresh_var "a" us xs in
-  let arr_mid, us, xs = fresh_var "a" us xs in
-  let arr_src, us, xs = fresh_var "a" us xs in
+  let seq_dst, us, xs = fresh_var "a" us xs in
+  let seq_mid, us, xs = fresh_var "a" us xs in
+  let seq_src, us, xs = fresh_var "a" us xs in
   let src_dst = Term.sub src dst in
-  let mem_dst = (src_dst, arr_dst) in
+  let mem_dst = (src_dst, seq_dst) in
   let siz_mid = Term.sub len src_dst in
-  let mem_mid = (siz_mid, arr_mid) in
-  let mem_src = (src_dst, arr_src) in
+  let mem_mid = (siz_mid, seq_mid) in
+  let mem_src = (src_dst, seq_src) in
   let mem_dst_mid_src = [|mem_dst; mem_mid; mem_src|] in
   let siz_dst_mid_src, us, xs = fresh_var "m" us xs in
-  let arr_dst_mid_src, us, xs = fresh_var "a" us xs in
+  let seq_dst_mid_src, us, xs = fresh_var "a" us xs in
   let eq_mem_dst_mid_src =
-    eq_concat (siz_dst_mid_src, arr_dst_mid_src) mem_dst_mid_src
+    eq_concat (siz_dst_mid_src, seq_dst_mid_src) mem_dst_mid_src
   in
   let seg =
     Sh.seg
-      {loc= dst; bas; len= siz; siz= siz_dst_mid_src; arr= arr_dst_mid_src}
+      {loc= dst; bas; len= siz; siz= siz_dst_mid_src; seq= seq_dst_mid_src}
   in
   let foot =
     Sh.and_ eq_mem_dst_mid_src
@@ -195,9 +195,9 @@ let memmov_dn_spec us dst src len =
   in
   let mem_mid_src_src = [|mem_mid; mem_src; mem_src|] in
   let siz_mid_src_src, us, xs = fresh_var "m" us xs in
-  let arr_mid_src_src, _, xs = fresh_var "a" us xs in
+  let seq_mid_src_src, _, xs = fresh_var "a" us xs in
   let eq_mem_mid_src_src =
-    eq_concat (siz_mid_src_src, arr_mid_src_src) mem_mid_src_src
+    eq_concat (siz_mid_src_src, seq_mid_src_src) mem_mid_src_src
   in
   let post =
     Sh.and_ eq_mem_mid_src_src
@@ -206,7 +206,7 @@ let memmov_dn_spec us dst src len =
          ; bas
          ; len= siz
          ; siz= siz_mid_src_src
-         ; arr= arr_mid_src_src })
+         ; seq= seq_mid_src_src })
   in
   {xs; foot; sub= Var.Subst.empty; ms= Var.Set.empty; post}
 
@@ -220,9 +220,9 @@ let memmov_up_spec us dst src len =
   in
   let mem_src_src_mid = [|mem_src; mem_src; mem_mid|] in
   let siz_src_src_mid, us, xs = fresh_var "m" us xs in
-  let arr_src_src_mid, _, xs = fresh_var "a" us xs in
+  let seq_src_src_mid, _, xs = fresh_var "a" us xs in
   let eq_mem_src_src_mid =
-    eq_concat (siz_src_src_mid, arr_src_src_mid) mem_src_src_mid
+    eq_concat (siz_src_src_mid, seq_src_src_mid) mem_src_src_mid
   in
   let post =
     Sh.and_ eq_mem_src_src_mid
@@ -231,7 +231,7 @@ let memmov_up_spec us dst src len =
          ; bas
          ; len= siz
          ; siz= siz_src_src_mid
-         ; arr= arr_src_src_mid })
+         ; seq= seq_src_src_mid })
   in
   {xs; foot; sub= Var.Subst.empty; ms= Var.Set.empty; post}
 
@@ -317,8 +317,8 @@ let calloc_spec us reg num len =
   let sub, ms, us = assign ~ws:(Var.Set.of_ reg) ~rs:(Term.fv siz) ~us in
   let loc = Term.var reg in
   let siz = Term.rename sub siz in
-  let arr = Term.splat Term.zero in
-  let {us= _; xs; seg} = fresh_seg ~loc ~bas:loc ~len:siz ~siz ~arr us in
+  let seq = Term.splat Term.zero in
+  let {us= _; xs; seg} = fresh_seg ~loc ~bas:loc ~len:siz ~siz ~seq us in
   let post = Sh.or_ (null_eq (Term.var reg)) (Sh.seg seg) in
   {xs; foot; sub; ms; post}
 
@@ -339,7 +339,7 @@ let posix_memalign_spec us reg ptr siz =
       ~us
   in
   let q, us, xs = fresh_var "q" us xs in
-  let pseg' = {pseg with arr= q} in
+  let pseg' = {pseg with seq= q} in
   let {us= _; xs; seg= qseg} =
     fresh_seg ~loc:q ~bas:q ~len:siz ~siz ~xs us
   in
@@ -374,8 +374,8 @@ let realloc_spec us reg ptr siz =
   let loc = Term.var reg in
   let siz = Term.rename sub siz in
   let {us; xs; seg= rseg} = fresh_seg ~loc ~bas:loc ~len:siz ~siz ~xs us in
-  let a0 = pseg.arr in
-  let a1 = rseg.arr in
+  let a0 = pseg.seq in
+  let a1 = rseg.seq in
   let a2, _, xs = fresh_var "a" us xs in
   let post =
     Sh.or_
@@ -406,8 +406,8 @@ let rallocx_spec us reg ptr siz =
   let loc = Term.var reg in
   let siz = Term.rename sub siz in
   let {us; xs; seg= rseg} = fresh_seg ~loc ~bas:loc ~len:siz ~siz ~xs us in
-  let a0 = pseg.arr in
-  let a1 = rseg.arr in
+  let a0 = pseg.seq in
+  let a1 = rseg.seq in
   let a2, _, xs = fresh_var "a" us xs in
   let post =
     Sh.or_
@@ -442,8 +442,8 @@ let xallocx_spec us reg ptr siz ext =
   let {us; xs; seg= seg'} =
     fresh_seg ~loc:ptr ~bas:ptr ~len:reg ~siz:reg ~xs us
   in
-  let a0 = seg.arr in
-  let a1 = seg'.arr in
+  let a0 = seg.seq in
+  let a1 = seg'.seq in
   let a2, _, xs = fresh_var "a" us xs in
   let post =
     Sh.and_
@@ -502,14 +502,14 @@ let size_of_int_mul = Term.mulq (Q.of_int Llair.Typ.(size_of siz))
  *)
 let mallctl_read_spec us r i w n =
   let {us; xs; seg= iseg} = fresh_seg ~loc:i us in
-  let {us; xs; seg= rseg} = fresh_seg ~loc:r ~siz:iseg.arr ~xs us in
+  let {us; xs; seg= rseg} = fresh_seg ~loc:r ~siz:iseg.seq ~xs us in
   let a, _, xs = fresh_var "a" us xs in
   let foot =
     Sh.and_
       Term.(eq w zero)
       (Sh.and_ Term.(eq n zero) (Sh.star (Sh.seg iseg) (Sh.seg rseg)))
   in
-  let rseg' = {rseg with arr= a} in
+  let rseg' = {rseg with seq= a} in
   let post = Sh.star (Sh.seg rseg') (Sh.seg iseg) in
   {xs; foot; sub= Var.Subst.empty; ms= Var.Set.empty; post}
 
@@ -522,7 +522,7 @@ let mallctlbymib_read_spec us p l r i w n =
   let wl = size_of_int_mul l in
   let {us; xs; seg= pseg} = fresh_seg ~loc:p ~siz:wl us in
   let {us; xs; seg= iseg} = fresh_seg ~loc:i ~xs us in
-  let m = iseg.arr in
+  let m = iseg.seq in
   let {us; xs; seg= rseg} = fresh_seg ~loc:r ~siz:m ~xs us in
   let const = Sh.star (Sh.seg pseg) (Sh.seg iseg) in
   let a, _, xs = fresh_var "a" us xs in
@@ -531,7 +531,7 @@ let mallctlbymib_read_spec us p l r i w n =
       Term.(eq w zero)
       (Sh.and_ Term.(eq n zero) (Sh.star const (Sh.seg rseg)))
   in
-  let rseg' = {rseg with arr= a} in
+  let rseg' = {rseg with seq= a} in
   let post = Sh.star (Sh.seg rseg') const in
   {xs; foot; sub= Var.Subst.empty; ms= Var.Set.empty; post}
 
@@ -577,12 +577,12 @@ let mallctlbymib_specs us p j r i w n =
  *)
 let mallctlnametomib_spec us p o =
   let {us; xs; seg= oseg} = fresh_seg ~loc:o us in
-  let n = oseg.arr in
+  let n = oseg.seq in
   let wn = size_of_int_mul n in
   let {us; xs; seg= pseg} = fresh_seg ~loc:p ~siz:wn ~xs us in
   let a, _, xs = fresh_var "a" us xs in
   let foot = Sh.star (Sh.seg oseg) (Sh.seg pseg) in
-  let pseg' = {pseg with arr= a} in
+  let pseg' = {pseg with seq= a} in
   let post = Sh.star (Sh.seg pseg') (Sh.seg oseg) in
   {xs; foot; sub= Var.Subst.empty; ms= Var.Set.empty; post}
 
diff --git a/sledge/src/llair/exp.ml b/sledge/src/llair/exp.ml
index 99ea77cd7..11330cac0 100644
--- a/sledge/src/llair/exp.ml
+++ b/sledge/src/llair/exp.ml
@@ -389,7 +389,7 @@ let conditional ?typ ~cnd ~thn ~els =
   let typ = match typ with Some typ -> typ | None -> typ_of thn in
   Ap3 (Conditional, typ, cnd, thn, els) |> check invariant
 
-(* memory *)
+(* sequences *)
 
 let splat typ byt = Ap1 (Splat, typ, byt) |> check invariant
 
diff --git a/sledge/src/llair/exp.mli b/sledge/src/llair/exp.mli
index b203191bc..e0c14e50b 100644
--- a/sledge/src/llair/exp.mli
+++ b/sledge/src/llair/exp.mli
@@ -172,7 +172,7 @@ val ashr : ?typ:Typ.t -> t -> t -> t
 (* if-then-else *)
 val conditional : ?typ:Typ.t -> cnd:t -> thn:t -> els:t -> t
 
-(* memory *)
+(* sequences *)
 val splat : Typ.t -> t -> t
 
 (* records (struct / array values) *)
diff --git a/sledge/src/sh.ml b/sledge/src/sh.ml
index 368b12581..3192cc857 100644
--- a/sledge/src/sh.ml
+++ b/sledge/src/sh.ml
@@ -9,7 +9,7 @@
 
 [@@@warning "+9"]
 
-type seg = {loc: Term.t; bas: Term.t; len: Term.t; siz: Term.t; arr: Term.t}
+type seg = {loc: Term.t; bas: Term.t; len: Term.t; siz: Term.t; seq: Term.t}
 [@@deriving compare, equal, sexp]
 
 type starjunction =
@@ -44,15 +44,15 @@ let map_seg ~f h =
   let bas = f h.bas in
   let len = f h.len in
   let siz = f h.siz in
-  let arr = f h.arr in
+  let seq = f h.seq in
   if
     loc == h.loc
     && bas == h.bas
     && len == h.len
     && siz == h.siz
-    && arr == h.arr
+    && seq == h.seq
   then h
-  else {loc; bas; len; siz; arr}
+  else {loc; bas; len; siz; seq}
 
 let map ~f_sjn ~f_cong ~f_trm ({us; xs= _; cong; pure; heap; djns} as q) =
   let exception Unsat in
@@ -72,9 +72,9 @@ let map ~f_sjn ~f_cong ~f_trm ({us; xs= _; cong; pure; heap; djns} as q) =
     else {q with cong; pure; heap; djns}
   with Unsat -> false_ us
 
-let fold_terms_seg {loc; bas; len; siz; arr} ~init ~f =
+let fold_terms_seg {loc; bas; len; siz; seq} ~init ~f =
   let f b s = f s b in
-  f loc (f bas (f len (f siz (f arr init))))
+  f loc (f bas (f len (f siz (f seq init))))
 
 let fold_vars_seg seg ~init ~f =
   fold_terms_seg seg ~init ~f:(fun init -> Term.fold_vars ~f ~init)
@@ -130,15 +130,15 @@ let var_strength ?(xs = Var.Set.empty) q =
   in
   var_strength_ xs m q
 
-let pp_memory x fs (siz, arr) = Term.ppx x fs (Term.memory ~siz ~arr)
+let pp_chunk x fs (siz, seq) = Term.ppx x fs (Term.sized ~siz ~seq)
 
-let pp_seg x fs {loc; bas; len; siz; arr} =
+let pp_seg x fs {loc; bas; len; siz; seq} =
   let term_pp = Term.ppx x in
   Format.fprintf fs "@[<2>%a@ @[@[-[%a)->@]@ %a@]@]" term_pp loc
     (fun fs (bas, len) ->
       if (not (Term.equal loc bas)) || not (Term.equal len siz) then
         Format.fprintf fs " %a, %a " term_pp bas term_pp len )
-    (bas, len) (pp_memory x) (siz, arr)
+    (bas, len) (pp_chunk x) (siz, seq)
 
 let pp_seg_norm cong fs seg =
   let x _ = None in
@@ -164,8 +164,8 @@ let pp_block x fs segs =
     | [] -> false
   in
   let term_pp = Term.ppx x in
-  let pp_mems =
-    List.pp "@,^" (fun fs seg -> pp_memory x fs (seg.siz, seg.arr))
+  let pp_chunks =
+    List.pp "@,^" (fun fs seg -> pp_chunk x fs (seg.siz, seg.seq))
   in
   match segs with
   | {loc; bas; len; _} :: _ ->
@@ -173,7 +173,7 @@ let pp_block x fs segs =
         (fun fs ->
           if not (is_full_alloc segs) then
             Format.fprintf fs " %a, %a " term_pp bas term_pp len )
-        pp_mems segs
+        pp_chunks segs
   | [] -> ()
 
 let pp_heap x ?pre cong fs heap =
diff --git a/sledge/src/sh.mli b/sledge/src/sh.mli
index c99d38dfe..1f36dd55d 100644
--- a/sledge/src/sh.mli
+++ b/sledge/src/sh.mli
@@ -7,11 +7,10 @@
 
 (** Symbolic Heap Formulas *)
 
-(** Segment of memory starting at [loc] containing a byte-array [arr] of
+(** Segment of memory starting at [loc] containing [seq] (a byte-array) of
     size [siz], contained in an enclosing allocation-block starting at [bas]
-    of length [len]. Byte-array expressions are either [Var]iables or
-    [Splat] vectors. *)
-type seg = {loc: Term.t; bas: Term.t; len: Term.t; siz: Term.t; arr: Term.t}
+    of length [len]. *)
+type seg = {loc: Term.t; bas: Term.t; len: Term.t; siz: Term.t; seq: Term.t}
 
 type starjunction = private
   { us: Var.Set.t  (** vocabulary / variable context of formula *)
diff --git a/sledge/src/sh_test.ml b/sledge/src/sh_test.ml
index 5b2f7435a..de53b2f60 100644
--- a/sledge/src/sh_test.ml
+++ b/sledge/src/sh_test.ml
@@ -41,10 +41,10 @@ let%test_module _ =
     let x = Term.var x_
     let y = Term.var y_
 
-    let eq_concat (siz, arr) ms =
+    let eq_concat (siz, seq) ms =
       Term.(
-        eq (memory ~siz ~arr)
-          (concat (Array.map ~f:(fun (siz, arr) -> memory ~siz ~arr) ms)))
+        eq (sized ~siz ~seq)
+          (concat (Array.map ~f:(fun (siz, seq) -> sized ~siz ~seq) ms)))
 
     let of_eqs l =
       List.fold ~init:emp ~f:(fun q (a, b) -> and_ (Term.eq a b) q) l
diff --git a/sledge/src/solver.ml b/sledge/src/solver.ml
index 9f28e25f5..bf352f885 100644
--- a/sledge/src/solver.ml
+++ b/sledge/src/solver.ml
@@ -132,10 +132,10 @@ end
 
 open Goal
 
-let eq_concat (siz, arr) ms =
+let eq_concat (siz, seq) ms =
   Term.(
-    eq (memory ~siz ~arr)
-      (concat (Array.map ~f:(fun (siz, arr) -> memory ~siz ~arr) ms)))
+    eq (sized ~siz ~seq)
+      (concat (Array.map ~f:(fun (siz, seq) -> sized ~siz ~seq) ms)))
 
 let fresh_var name vs zs ~wrt =
   let v, wrt = Var.fresh name ~wrt in
@@ -212,8 +212,8 @@ let excise_seg_same ({com; min; sub} as goal) msg ssg =
   excise (fun {pf} ->
       pf "@[<hv 2>excise_seg_same@ %a@ \\- %a@]" (Sh.pp_seg_norm sub.cong)
         msg (Sh.pp_seg_norm sub.cong) ssg ) ;
-  let {Sh.bas= b; len= m; arr= a} = msg in
-  let {Sh.bas= b'; len= m'; arr= a'} = ssg in
+  let {Sh.bas= b; len= m; seq= a} = msg in
+  let {Sh.bas= b'; len= m'; seq= a'} = ssg in
   let com = Sh.star (Sh.seg msg) com in
   let min = Sh.rem_seg msg min in
   let sub =
@@ -240,18 +240,18 @@ let excise_seg_sub_prefix ({us; com; min; xs; sub; zs} as goal) msg ssg o_n
   excise (fun {pf} ->
       pf "@[<hv 2>excise_seg_sub_prefix@ %a@ \\- %a@]"
         (Sh.pp_seg_norm sub.cong) msg (Sh.pp_seg_norm sub.cong) ssg ) ;
-  let {Sh.loc= k; bas= b; len= m; siz= o; arr= a} = msg in
-  let {Sh.bas= b'; len= m'; siz= n; arr= a'} = ssg in
+  let {Sh.loc= k; bas= b; len= m; siz= o; seq= a} = msg in
+  let {Sh.bas= b'; len= m'; siz= n; seq= a'} = ssg in
   let o_n = Term.integer o_n in
   let a0, us, zs, wrt = fresh_var "a0" us zs ~wrt:(Var.Set.union us xs) in
   let a1, us, zs, _ = fresh_var "a1" us zs ~wrt in
   let xs = Var.Set.diff xs (Term.fv n) in
-  let com = Sh.star (Sh.seg {msg with siz= n; arr= a0}) com in
+  let com = Sh.star (Sh.seg {msg with siz= n; seq= a0}) com in
   let min =
     Sh.and_
       (eq_concat (o, a) [|(n, a0); (o_n, a1)|])
       (Sh.star
-         (Sh.seg {loc= Term.add k n; bas= b; len= m; siz= o_n; arr= a1})
+         (Sh.seg {loc= Term.add k n; bas= b; len= m; siz= o_n; seq= a1})
          (Sh.rem_seg msg min))
   in
   let sub =
@@ -280,8 +280,8 @@ let excise_seg_min_prefix ({us; com; min; xs; sub; zs} as goal) msg ssg n_o
   excise (fun {pf} ->
       pf "@[<hv 2>excise_seg_min_prefix@ %a@ \\- %a@]"
         (Sh.pp_seg_norm sub.cong) msg (Sh.pp_seg_norm sub.cong) ssg ) ;
-  let {Sh.bas= b; len= m; siz= o; arr= a} = msg in
-  let {Sh.loc= l; bas= b'; len= m'; siz= n; arr= a'} = ssg in
+  let {Sh.bas= b; len= m; siz= o; seq= a} = msg in
+  let {Sh.loc= l; bas= b'; len= m'; siz= n; seq= a'} = ssg in
   let n_o = Term.integer n_o in
   let com = Sh.star (Sh.seg msg) com in
   let min = Sh.rem_seg msg min in
@@ -293,7 +293,7 @@ let excise_seg_min_prefix ({us; com; min; xs; sub; zs} as goal) msg ssg n_o
             (eq_concat (n, a') [|(o, a); (n_o, a1')|])
             (Sh.star
                (Sh.seg
-                  {loc= Term.add l o; bas= b'; len= m'; siz= n_o; arr= a1'})
+                  {loc= Term.add l o; bas= b'; len= m'; siz= n_o; seq= a1'})
                (Sh.rem_seg ssg sub))))
   in
   goal |> with_ ~com ~min ~xs ~sub ~zs
@@ -316,20 +316,20 @@ let excise_seg_sub_suffix ({us; com; min; xs; sub; zs} as goal) msg ssg l_k
   excise (fun {pf} ->
       pf "@[<hv 2>excise_seg_sub_suffix@ %a@ \\- %a@]"
         (Sh.pp_seg_norm sub.cong) msg (Sh.pp_seg_norm sub.cong) ssg ) ;
-  let {Sh.loc= k; bas= b; len= m; siz= o; arr= a} = msg in
-  let {Sh.loc= l; bas= b'; len= m'; siz= n; arr= a'} = ssg in
+  let {Sh.loc= k; bas= b; len= m; siz= o; seq= a} = msg in
+  let {Sh.loc= l; bas= b'; len= m'; siz= n; seq= a'} = ssg in
   let l_k = Term.integer l_k in
   let a0, us, zs, wrt = fresh_var "a0" us zs ~wrt:(Var.Set.union us xs) in
   let a1, us, zs, _ = fresh_var "a1" us zs ~wrt in
   let xs = Var.Set.diff xs (Term.fv n) in
   let com =
-    Sh.star (Sh.seg {loc= l; bas= b; len= m; siz= n; arr= a1}) com
+    Sh.star (Sh.seg {loc= l; bas= b; len= m; siz= n; seq= a1}) com
   in
   let min =
     Sh.and_
       (eq_concat (o, a) [|(l_k, a0); (n, a1)|])
       (Sh.star
-         (Sh.seg {loc= k; bas= b; len= m; siz= l_k; arr= a0})
+         (Sh.seg {loc= k; bas= b; len= m; siz= l_k; seq= a0})
          (Sh.rem_seg msg min))
   in
   let sub =
@@ -358,8 +358,8 @@ let excise_seg_sub_infix ({us; com; min; xs; sub; zs} as goal) msg ssg l_k
   excise (fun {pf} ->
       pf "@[<hv 2>excise_seg_sub_infix@ %a@ \\- %a@]"
         (Sh.pp_seg_norm sub.cong) msg (Sh.pp_seg_norm sub.cong) ssg ) ;
-  let {Sh.loc= k; bas= b; len= m; siz= o; arr= a} = msg in
-  let {Sh.loc= l; bas= b'; len= m'; siz= n; arr= a'} = ssg in
+  let {Sh.loc= k; bas= b; len= m; siz= o; seq= a} = msg in
+  let {Sh.loc= l; bas= b'; len= m'; siz= n; seq= a'} = ssg in
   let l_k = Term.integer l_k in
   let ko_ln = Term.integer ko_ln in
   let ln = Term.add l n in
@@ -368,15 +368,15 @@ let excise_seg_sub_infix ({us; com; min; xs; sub; zs} as goal) msg ssg l_k
   let a2, us, zs, _ = fresh_var "a2" us zs ~wrt in
   let xs = Var.Set.diff xs (Var.Set.union (Term.fv l) (Term.fv n)) in
   let com =
-    Sh.star (Sh.seg {loc= l; bas= b; len= m; siz= n; arr= a1}) com
+    Sh.star (Sh.seg {loc= l; bas= b; len= m; siz= n; seq= a1}) com
   in
   let min =
     Sh.and_
       (eq_concat (o, a) [|(l_k, a0); (n, a1); (ko_ln, a2)|])
       (Sh.star
-         (Sh.seg {loc= k; bas= b; len= m; siz= l_k; arr= a0})
+         (Sh.seg {loc= k; bas= b; len= m; siz= l_k; seq= a0})
          (Sh.star
-            (Sh.seg {loc= ln; bas= b; len= m; siz= ko_ln; arr= a2})
+            (Sh.seg {loc= ln; bas= b; len= m; siz= ko_ln; seq= a2})
             (Sh.rem_seg msg min)))
   in
   let sub =
@@ -405,8 +405,8 @@ let excise_seg_min_skew ({us; com; min; xs; sub; zs} as goal) msg ssg l_k
   excise (fun {pf} ->
       pf "@[<hv 2>excise_seg_min_skew@ %a@ \\- %a@]"
         (Sh.pp_seg_norm sub.cong) msg (Sh.pp_seg_norm sub.cong) ssg ) ;
-  let {Sh.loc= k; bas= b; len= m; siz= o; arr= a} = msg in
-  let {Sh.loc= l; bas= b'; len= m'; siz= n; arr= a'} = ssg in
+  let {Sh.loc= k; bas= b; len= m; siz= o; seq= a} = msg in
+  let {Sh.loc= l; bas= b'; len= m'; siz= n; seq= a'} = ssg in
   let l_k = Term.integer l_k in
   let ko_l = Term.integer ko_l in
   let ln_ko = Term.integer ln_ko in
@@ -416,13 +416,13 @@ let excise_seg_min_skew ({us; com; min; xs; sub; zs} as goal) msg ssg l_k
   let a2', xs, zs, _ = fresh_var "a2" xs zs ~wrt in
   let xs = Var.Set.diff xs (Term.fv l) in
   let com =
-    Sh.star (Sh.seg {loc= l; bas= b; len= m; siz= ko_l; arr= a1}) com
+    Sh.star (Sh.seg {loc= l; bas= b; len= m; siz= ko_l; seq= a1}) com
   in
   let min =
     Sh.and_
       (eq_concat (o, a) [|(l_k, a0); (ko_l, a1)|])
       (Sh.star
-         (Sh.seg {loc= k; bas= b; len= m; siz= l_k; arr= a0})
+         (Sh.seg {loc= k; bas= b; len= m; siz= l_k; seq= a0})
          (Sh.rem_seg msg min))
   in
   let sub =
@@ -431,7 +431,7 @@ let excise_seg_min_skew ({us; com; min; xs; sub; zs} as goal) msg ssg l_k
          (Sh.and_
             (eq_concat (n, a') [|(ko_l, a1); (ln_ko, a2')|])
             (Sh.star
-               (Sh.seg {loc= ko; bas= b'; len= m'; siz= ln_ko; arr= a2'})
+               (Sh.seg {loc= ko; bas= b'; len= m'; siz= ln_ko; seq= a2'})
                (Sh.rem_seg ssg sub))))
   in
   goal |> with_ ~us ~com ~min ~xs ~sub ~zs
@@ -455,8 +455,8 @@ let excise_seg_min_suffix ({us; com; min; xs; sub; zs} as goal) msg ssg k_l
   excise (fun {pf} ->
       pf "@[<hv 2>excise_seg_min_suffix@ %a@ \\- %a@]"
         (Sh.pp_seg_norm sub.cong) msg (Sh.pp_seg_norm sub.cong) ssg ) ;
-  let {Sh.bas= b; len= m; siz= o; arr= a} = msg in
-  let {Sh.loc= l; bas= b'; len= m'; siz= n; arr= a'} = ssg in
+  let {Sh.bas= b; len= m; siz= o; seq= a} = msg in
+  let {Sh.loc= l; bas= b'; len= m'; siz= n; seq= a'} = ssg in
   let k_l = Term.integer k_l in
   let a0', xs, zs, _ = fresh_var "a0" xs zs ~wrt:(Var.Set.union us xs) in
   let com = Sh.star (Sh.seg msg) com in
@@ -467,7 +467,7 @@ let excise_seg_min_suffix ({us; com; min; xs; sub; zs} as goal) msg ssg k_l
          (Sh.and_
             (eq_concat (n, a') [|(k_l, a0'); (o, a)|])
             (Sh.star
-               (Sh.seg {loc= l; bas= b'; len= m'; siz= k_l; arr= a0'})
+               (Sh.seg {loc= l; bas= b'; len= m'; siz= k_l; seq= a0'})
                (Sh.rem_seg ssg sub))))
   in
   goal |> with_ ~com ~min ~xs ~sub ~zs
@@ -492,8 +492,8 @@ let excise_seg_min_infix ({us; com; min; xs; sub; zs} as goal) msg ssg k_l
   excise (fun {pf} ->
       pf "@[<hv 2>excise_seg_min_infix@ %a@ \\- %a@]"
         (Sh.pp_seg_norm sub.cong) msg (Sh.pp_seg_norm sub.cong) ssg ) ;
-  let {Sh.loc= k; bas= b; len= m; siz= o; arr= a} = msg in
-  let {Sh.loc= l; bas= b'; len= m'; siz= n; arr= a'} = ssg in
+  let {Sh.loc= k; bas= b; len= m; siz= o; seq= a} = msg in
+  let {Sh.loc= l; bas= b'; len= m'; siz= n; seq= a'} = ssg in
   let k_l = Term.integer k_l in
   let ln_ko = Term.integer ln_ko in
   let ko = Term.add k o in
@@ -507,9 +507,9 @@ let excise_seg_min_infix ({us; com; min; xs; sub; zs} as goal) msg ssg k_l
          (Sh.and_
             (eq_concat (n, a') [|(k_l, a0'); (o, a); (ln_ko, a2')|])
             (Sh.star
-               (Sh.seg {loc= l; bas= b'; len= m'; siz= k_l; arr= a0'})
+               (Sh.seg {loc= l; bas= b'; len= m'; siz= k_l; seq= a0'})
                (Sh.star
-                  (Sh.seg {loc= ko; bas= b'; len= m'; siz= ln_ko; arr= a2'})
+                  (Sh.seg {loc= ko; bas= b'; len= m'; siz= ln_ko; seq= a2'})
                   (Sh.rem_seg ssg sub)))))
   in
   goal |> with_ ~com ~min ~xs ~sub ~zs
@@ -533,8 +533,8 @@ let excise_seg_sub_skew ({us; com; min; xs; sub; zs} as goal) msg ssg k_l
   excise (fun {pf} ->
       pf "@[<hv 2>excise_seg_sub_skew@ %a@ \\- %a@]"
         (Sh.pp_seg_norm sub.cong) msg (Sh.pp_seg_norm sub.cong) ssg ) ;
-  let {Sh.loc= k; bas= b; len= m; siz= o; arr= a} = msg in
-  let {Sh.loc= l; bas= b'; len= m'; siz= n; arr= a'} = ssg in
+  let {Sh.loc= k; bas= b; len= m; siz= o; seq= a} = msg in
+  let {Sh.loc= l; bas= b'; len= m'; siz= n; seq= a'} = ssg in
   let k_l = Term.integer k_l in
   let ln_k = Term.integer ln_k in
   let ko_ln = Term.integer ko_ln in
@@ -543,13 +543,13 @@ let excise_seg_sub_skew ({us; com; min; xs; sub; zs} as goal) msg ssg k_l
   let a1, us, zs, wrt = fresh_var "a1" us zs ~wrt in
   let a2, us, zs, _ = fresh_var "a2" us zs ~wrt in
   let com =
-    Sh.star (Sh.seg {loc= k; bas= b; len= m; siz= ln_k; arr= a1}) com
+    Sh.star (Sh.seg {loc= k; bas= b; len= m; siz= ln_k; seq= a1}) com
   in
   let min =
     Sh.and_
       (eq_concat (o, a) [|(ln_k, a1); (ko_ln, a2)|])
       (Sh.star
-         (Sh.seg {loc= ln; bas= b; len= m; siz= ko_ln; arr= a2})
+         (Sh.seg {loc= ln; bas= b; len= m; siz= ko_ln; seq= a2})
          (Sh.rem_seg msg min))
   in
   let sub =
@@ -558,7 +558,7 @@ let excise_seg_sub_skew ({us; com; min; xs; sub; zs} as goal) msg ssg k_l
          (Sh.and_
             (eq_concat (n, a') [|(k_l, a0'); (ln_k, a1)|])
             (Sh.star
-               (Sh.seg {loc= l; bas= b'; len= m'; siz= k_l; arr= a0'})
+               (Sh.seg {loc= l; bas= b'; len= m'; siz= k_l; seq= a0'})
                (Sh.rem_seg ssg sub))))
   in
   goal |> with_ ~us ~com ~min ~xs ~sub ~zs
diff --git a/sledge/src/solver_test.ml b/sledge/src/solver_test.ml
index f7362763c..014b71cd9 100644
--- a/sledge/src/solver_test.ml
+++ b/sledge/src/solver_test.ml
@@ -75,7 +75,7 @@ let%test_module _ =
 
     let%expect_test _ =
       check_frame
-        (Sh.seg {loc= l; bas= b; len= m; siz= n; arr= a})
+        (Sh.seg {loc= l; bas= b; len= m; siz= n; seq= a})
         [] Sh.emp ;
       [%expect
         {|
@@ -84,9 +84,9 @@ let%test_module _ =
 
     let%expect_test _ =
       check_frame
-        (Sh.seg {loc= l; bas= b; len= m; siz= n; arr= a})
+        (Sh.seg {loc= l; bas= b; len= m; siz= n; seq= a})
         []
-        (Sh.seg {loc= l; bas= b; len= m; siz= n; arr= a}) ;
+        (Sh.seg {loc= l; bas= b; len= m; siz= n; seq= a}) ;
       [%expect
         {|
         ( infer_frame:
@@ -95,8 +95,8 @@ let%test_module _ =
         ) infer_frame:   emp |}]
 
     let%expect_test _ =
-      let common = Sh.seg {loc= l2; bas= b; len= !10; siz= !10; arr= a2} in
-      let seg1 = Sh.seg {loc= l; bas= b; len= !10; siz= !10; arr= a} in
+      let common = Sh.seg {loc= l2; bas= b; len= !10; siz= !10; seq= a2} in
+      let seg1 = Sh.seg {loc= l; bas= b; len= !10; siz= !10; seq= a} in
       let minued = Sh.star common seg1 in
       let subtrahend =
         Sh.and_ (Term.eq m n)
@@ -117,10 +117,10 @@ let%test_module _ =
     let%expect_test _ =
       check_frame
         (Sh.star
-           (Sh.seg {loc= l; bas= b; len= m; siz= n; arr= a})
-           (Sh.seg {loc= l2; bas= b; len= m; siz= n; arr= a2}))
+           (Sh.seg {loc= l; bas= b; len= m; siz= n; seq= a})
+           (Sh.seg {loc= l2; bas= b; len= m; siz= n; seq= a2}))
         []
-        (Sh.seg {loc= l; bas= b; len= m; siz= n; arr= a}) ;
+        (Sh.seg {loc= l; bas= b; len= m; siz= n; seq= a}) ;
       [%expect
         {|
         ( infer_frame:
@@ -132,10 +132,10 @@ let%test_module _ =
     let%expect_test _ =
       check_frame
         (Sh.star
-           (Sh.seg {loc= l; bas= l; len= !16; siz= !8; arr= a})
-           (Sh.seg {loc= l + !8; bas= l; len= !16; siz= !8; arr= a2}))
+           (Sh.seg {loc= l; bas= l; len= !16; siz= !8; seq= a})
+           (Sh.seg {loc= l + !8; bas= l; len= !16; siz= !8; seq= a2}))
         [a3_]
-        (Sh.seg {loc= l; bas= l; len= !16; siz= !16; arr= a3}) ;
+        (Sh.seg {loc= l; bas= l; len= !16; siz= !16; seq= a3}) ;
       [%expect
         {|
         ( infer_frame:
@@ -145,10 +145,10 @@ let%test_module _ =
     let%expect_test _ =
       check_frame
         (Sh.star
-           (Sh.seg {loc= l; bas= l; len= !16; siz= !8; arr= a})
-           (Sh.seg {loc= l + !8; bas= l; len= !16; siz= !8; arr= a2}))
+           (Sh.seg {loc= l; bas= l; len= !16; siz= !8; seq= a})
+           (Sh.seg {loc= l + !8; bas= l; len= !16; siz= !8; seq= a2}))
         [a3_; m_]
-        (Sh.seg {loc= l; bas= l; len= m; siz= !16; arr= a3}) ;
+        (Sh.seg {loc= l; bas= l; len= m; siz= !16; seq= a3}) ;
       [%expect
         {|
         ( infer_frame:
@@ -161,10 +161,10 @@ let%test_module _ =
     let%expect_test _ =
       check_frame
         (Sh.star
-           (Sh.seg {loc= l; bas= l; len= !16; siz= !8; arr= a})
-           (Sh.seg {loc= l + !8; bas= l; len= !16; siz= !8; arr= a2}))
+           (Sh.seg {loc= l; bas= l; len= !16; siz= !8; seq= a})
+           (Sh.seg {loc= l + !8; bas= l; len= !16; siz= !8; seq= a2}))
         [a3_; m_]
-        (Sh.seg {loc= l; bas= l; len= m; siz= m; arr= a3}) ;
+        (Sh.seg {loc= l; bas= l; len= m; siz= m; seq= a3}) ;
       [%expect
         {|
         ( infer_frame:
@@ -177,12 +177,12 @@ let%test_module _ =
     let%expect_test _ =
       check_frame
         (Sh.star
-           (Sh.seg {loc= k; bas= k; len= !16; siz= !32; arr= a})
-           (Sh.seg {loc= l; bas= l; len= !8; siz= !8; arr= !16}))
+           (Sh.seg {loc= k; bas= k; len= !16; siz= !32; seq= a})
+           (Sh.seg {loc= l; bas= l; len= !8; siz= !8; seq= !16}))
         [a2_; m_; n_]
         (Sh.star
-           (Sh.seg {loc= l; bas= l; len= !8; siz= !8; arr= n})
-           (Sh.seg {loc= k; bas= k; len= m; siz= n; arr= a2})) ;
+           (Sh.seg {loc= l; bas= l; len= !8; siz= !8; seq= n})
+           (Sh.seg {loc= k; bas= k; len= m; siz= n; seq= a2})) ;
       [%expect
         {|
         ( infer_frame:
@@ -199,12 +199,12 @@ let%test_module _ =
     let%expect_test _ =
       infer_frame
         (Sh.star
-           (Sh.seg {loc= k; bas= k; len= !16; siz= !32; arr= a})
-           (Sh.seg {loc= l; bas= l; len= !8; siz= !8; arr= !16}))
+           (Sh.seg {loc= k; bas= k; len= !16; siz= !32; seq= a})
+           (Sh.seg {loc= l; bas= l; len= !8; siz= !8; seq= !16}))
         [a2_; m_; n_]
         (Sh.star
-           (Sh.seg {loc= k; bas= k; len= m; siz= n; arr= a2})
-           (Sh.seg {loc= l; bas= l; len= !8; siz= !8; arr= n})) ;
+           (Sh.seg {loc= k; bas= k; len= m; siz= n; seq= a2})
+           (Sh.seg {loc= l; bas= l; len= !8; siz= !8; seq= n})) ;
       [%expect
         {|
         ( infer_frame:
@@ -220,9 +220,9 @@ let%test_module _ =
 
     let seg_split_symbolically =
       Sh.star
-        (Sh.seg {loc= l; bas= l; len= !16; siz= 8 * n; arr= a2})
+        (Sh.seg {loc= l; bas= l; len= !16; siz= 8 * n; seq= a2})
         (Sh.seg
-           {loc= l + (8 * n); bas= l; len= !16; siz= !16 - (8 * n); arr= a3})
+           {loc= l + (8 * n); bas= l; len= !16; siz= !16 - (8 * n); seq= a3})
 
     let%expect_test _ =
       check_frame
@@ -230,7 +230,7 @@ let%test_module _ =
            Term.(or_ (or_ (eq n !0) (eq n !1)) (eq n !2))
            seg_split_symbolically)
         [m_; a_]
-        (Sh.seg {loc= l; bas= l; len= m; siz= m; arr= a}) ;
+        (Sh.seg {loc= l; bas= l; len= m; siz= m; seq= a}) ;
       [%expect
         {|
         ( infer_frame:
@@ -263,7 +263,7 @@ let%test_module _ =
       infer_frame
         (Sh.and_ (Term.le n !2) seg_split_symbolically)
         [m_; a_]
-        (Sh.seg {loc= l; bas= l; len= m; siz= m; arr= a}) ;
+        (Sh.seg {loc= l; bas= l; len= m; siz= m; seq= a}) ;
       [%expect
         {|
         ( infer_frame:
diff --git a/sledge/src/term.ml b/sledge/src/term.ml
index 3cd7e98e1..d9e39b5e5 100644
--- a/sledge/src/term.ml
+++ b/sledge/src/term.ml
@@ -30,7 +30,7 @@ type op2 =
   | Shl
   | Lshr
   | Ashr
-  | Memory
+  | Sized
   | Update of int
 [@@deriving compare, equal, hash, sexp]
 
@@ -186,9 +186,9 @@ let rec ppx strength fs term =
     | Ap2 (Ashr, x, y) -> pf "(%a@ ashr %a)" pp x pp y
     | Ap3 (Conditional, cnd, thn, els) ->
         pf "(%a@ ? %a@ : %a)" pp cnd pp thn pp els
-    | Ap3 (Extract, agg, off, len) -> pf "%a[%a,%a)" pp agg pp off pp len
+    | Ap3 (Extract, seq, off, len) -> pf "%a[%a,%a)" pp seq pp off pp len
     | Ap1 (Splat, byt) -> pf "%a^" pp byt
-    | Ap2 (Memory, siz, arr) -> pf "@<1>⟨%a,%a@<1>⟩" pp siz pp arr
+    | Ap2 (Sized, siz, arr) -> pf "@<1>⟨%a,%a@<1>⟩" pp siz pp arr
     | ApN (Concat, args) when IArray.is_empty args -> pf "@<2>⟨⟩"
     | ApN (Concat, args) -> pf "(%a)" (IArray.pp "@,^" pp) args
     | ApN (Record, elts) -> pf "{%a}" (pp_record strength) elts
@@ -285,14 +285,14 @@ let assert_polynomial poly =
       Qset.iter args ~f:(fun m c -> assert_poly_term m c |> Fn.id)
   | _ -> assert false
 
-(* aggregate args of Extract and Concat must be aggregate terms, in
+(* sequence args of Extract and Concat must be sequence terms, in
    particular, not variables *)
-let rec assert_aggregate = function
-  | Ap2 (Memory, _, _) -> ()
-  | Ap3 (Extract, a, _, _) -> assert_aggregate a
+let rec assert_sequence = function
+  | Ap2 (Sized, _, _) -> ()
+  | Ap3 (Extract, a, _, _) -> assert_sequence a
   | ApN (Concat, a0N) ->
       assert (IArray.length a0N <> 1) ;
-      IArray.iter ~f:assert_aggregate a0N
+      IArray.iter ~f:assert_sequence a0N
   | _ -> assert false
 
 let invariant e =
@@ -302,8 +302,8 @@ let invariant e =
   | Or _ -> assert_disjunction e |> Fn.id
   | Add _ -> assert_polynomial e |> Fn.id
   | Mul _ -> assert_monomial e |> Fn.id
-  | Ap2 (Memory, _, _) | Ap3 (Extract, _, _, _) | ApN (Concat, _) ->
-      assert_aggregate e
+  | Ap2 (Sized, _, _) | Ap3 (Extract, _, _, _) | ApN (Concat, _) ->
+      assert_sequence e
   | ApN (Record, elts) -> assert (not (IArray.is_empty elts))
   | Ap1 (Convert {src= Integer _; dst= Integer _}, _) -> assert false
   | Ap1 (Convert {src; dst}, _) ->
@@ -595,27 +595,27 @@ let rec simp_or2 x y =
 
 let simp_or xs = Set.fold xs ~init:false_ ~f:simp_or2
 
-(* aggregate sizes *)
+(* sequence sizes *)
 
-let rec agg_size_exn = function
-  | Ap2 (Memory, n, _) | Ap3 (Extract, _, _, n) -> n
+let rec seq_size_exn = function
+  | Ap2 (Sized, n, _) | Ap3 (Extract, _, _, n) -> n
   | ApN (Concat, a0U) ->
       IArray.fold a0U ~init:zero ~f:(fun a0I aJ ->
-          simp_add2 a0I (agg_size_exn aJ) )
-  | _ -> invalid_arg "agg_size_exn"
+          simp_add2 a0I (seq_size_exn aJ) )
+  | _ -> invalid_arg "seq_size_exn"
 
-let agg_size e = try Some (agg_size_exn e) with Invalid_argument _ -> None
+let seq_size e = try Some (seq_size_exn e) with Invalid_argument _ -> None
 
-(* memory *)
+(* sequences *)
 
-let empty_agg = ApN (Concat, IArray.of_array [||])
+let empty_seq = ApN (Concat, IArray.of_array [||])
 let simp_splat byt = Ap1 (Splat, byt)
 
-let simp_memory siz arr =
+let simp_sized siz arr =
   (* ⟨n,α⟩ ==> α when n ≡ |α| *)
-  match agg_size arr with
+  match seq_size arr with
   | Some n when equal siz n -> arr
-  | _ -> Ap2 (Memory, siz, arr)
+  | _ -> Ap2 (Sized, siz, arr)
 
 type pcmp = Lt | Eq | Gt | Unknown
 
@@ -630,22 +630,22 @@ let partial_compare x y : pcmp =
 let partial_ge x y =
   match partial_compare x y with Gt | Eq -> true | Lt | Unknown -> false
 
-let rec simp_extract agg off len =
-  [%Trace.call fun {pf} -> pf "%a" pp (Ap3 (Extract, agg, off, len))]
+let rec simp_extract seq off len =
+  [%Trace.call fun {pf} -> pf "%a" pp (Ap3 (Extract, seq, off, len))]
   ;
   (* _[_,0) ==> ⟨⟩ *)
-  ( if equal len zero then empty_agg
+  ( if equal len zero then empty_seq
   else
     let o_l = simp_add2 off len in
-    match agg with
+    match seq with
     (* α[m,k)[o,l) ==> α[m+o,l) when k ≥ o+l *)
     | Ap3 (Extract, a, m, k) when partial_ge k o_l ->
         simp_extract a (simp_add2 m off) len
     (* ⟨n,E^⟩[o,l) ==> ⟨l,E^⟩ when n ≥ o+l *)
-    | Ap2 (Memory, n, (Ap1 (Splat, _) as e)) when partial_ge n o_l ->
-        simp_memory len e
+    | Ap2 (Sized, n, (Ap1 (Splat, _) as e)) when partial_ge n o_l ->
+        simp_sized len e
     (* ⟨n,a⟩[0,n) ==> ⟨n,a⟩ *)
-    | Ap2 (Memory, n, _) when equal off zero && equal n len -> agg
+    | Ap2 (Sized, n, _) when equal off zero && equal n len -> seq
     (* For (α₀^α₁)[o,l) there are 3 cases:
      *
      * ⟨...⟩^⟨...⟩
@@ -671,7 +671,7 @@ let rec simp_extract agg off len =
       | Integer {data= l} ->
           IArray.fold_map_until na1N ~init:(l, off)
             ~f:(fun (l, oI) naI ->
-              let nI = agg_size_exn naI in
+              let nI = seq_size_exn naI in
               if Z.equal Z.zero l then
                 Continue ((l, oI), simp_extract naI oI zero)
               else
@@ -682,11 +682,11 @@ let rec simp_extract agg off len =
                     let lI = Z.(max zero (min l (neg data))) in
                     let l = Z.(l - lI) in
                     Continue ((l, oJ), simp_extract naI oI (integer lI))
-                | _ -> Stop (Ap3 (Extract, agg, off, len)) )
+                | _ -> Stop (Ap3 (Extract, seq, off, len)) )
             ~finish:(fun (_, e1N) -> simp_concat e1N)
-      | _ -> Ap3 (Extract, agg, off, len) )
+      | _ -> Ap3 (Extract, seq, off, len) )
     (* α[o,l) *)
-    | _ -> Ap3 (Extract, agg, off, len) )
+    | _ -> Ap3 (Extract, seq, off, len) )
   |>
   [%Trace.retn fun {pf} -> pf "%a" pp]
 
@@ -710,16 +710,16 @@ and simp_concat xs =
   let simp_adjacent e f =
     match (e, f) with
     (* ⟨n,a⟩[o,k)^⟨n,a⟩[o+k,l) ==> ⟨n,a⟩[o,k+l) when n ≥ o+k+l *)
-    | ( Ap3 (Extract, (Ap2 (Memory, n, _) as na), o, k)
+    | ( Ap3 (Extract, (Ap2 (Sized, n, _) as na), o, k)
       , Ap3 (Extract, na', o_k, l) )
       when equal na na'
            && equal o_k (simp_add2 o k)
            && partial_ge n (simp_add2 o_k l) ->
         Some (simp_extract na o (simp_add2 k l))
     (* ⟨m,E^⟩^⟨n,E^⟩ ==> ⟨m+n,E^⟩ *)
-    | Ap2 (Memory, m, (Ap1 (Splat, _) as a)), Ap2 (Memory, n, a')
+    | Ap2 (Sized, m, (Ap1 (Splat, _) as a)), Ap2 (Sized, n, a')
       when equal a a' ->
-        Some (simp_memory (simp_add2 m n) a)
+        Some (simp_sized (simp_add2 m n) a)
     | _ -> None
   in
   let xs = flatten xs in
@@ -791,17 +791,16 @@ let rec simp_eq x y =
           let a = IArray.sub ~pos ~len:(m - length_common) a in
           let b = IArray.sub ~pos ~len:(n - length_common) b in
           simp_eq (simp_concat a) (simp_concat b)
-    | ( (Ap2 (Memory, _, _) | Ap3 (Extract, _, _, _) | ApN (Concat, _))
-      , (Ap2 (Memory, _, _) | Ap3 (Extract, _, _, _) | ApN (Concat, _)) ) ->
+    | ( (Ap2 (Sized, _, _) | Ap3 (Extract, _, _, _) | ApN (Concat, _))
+      , (Ap2 (Sized, _, _) | Ap3 (Extract, _, _, _) | ApN (Concat, _)) ) ->
         Ap2 (Eq, x, y)
     (* x = α ==> ⟨x,|α|⟩ = α *)
     | ( x
-      , ( (Ap2 (Memory, _, _) | Ap3 (Extract, _, _, _) | ApN (Concat, _)) as
-        a ) )
-     |( ( (Ap2 (Memory, _, _) | Ap3 (Extract, _, _, _) | ApN (Concat, _)) as
-        a )
+      , ((Ap2 (Sized, _, _) | Ap3 (Extract, _, _, _) | ApN (Concat, _)) as a)
+      )
+     |( ((Ap2 (Sized, _, _) | Ap3 (Extract, _, _, _) | ApN (Concat, _)) as a)
       , x ) ->
-        simp_eq (Ap2 (Memory, agg_size_exn a, x)) a
+        simp_eq (Ap2 (Sized, seq_size_exn a, x)) a
     | x, y -> Ap2 (Eq, x, y) )
 
 and simp_dq x y =
@@ -904,7 +903,7 @@ let norm1 op x =
 
 let norm2 op x y =
   ( match op with
-  | Memory -> simp_memory x y
+  | Sized -> simp_sized x y
   | Eq -> simp_eq x y
   | Dq -> simp_dq x y
   | Lt -> simp_lt x y
@@ -965,8 +964,8 @@ let lshr = norm2 Lshr
 let ashr = norm2 Ashr
 let conditional ~cnd ~thn ~els = norm3 Conditional cnd thn els
 let splat byt = norm1 Splat byt
-let memory ~siz ~arr = norm2 Memory siz arr
-let extract ~agg ~off ~len = norm3 Extract agg off len
+let sized ~seq ~siz = norm2 Sized siz seq
+let extract ~seq ~off ~len = norm3 Extract seq off len
 let concat xs = normN Concat (IArray.of_array xs)
 let record elts = normN Record elts
 let select ~rcd ~idx = norm1 (Select idx) rcd
diff --git a/sledge/src/term.mli b/sledge/src/term.mli
index 8043f3acf..cefe113ae 100644
--- a/sledge/src/term.mli
+++ b/sledge/src/term.mli
@@ -43,13 +43,13 @@ type op2 =
   | Shl  (** Shift left, bitwise *)
   | Lshr  (** Logical shift right, bitwise *)
   | Ashr  (** Arithmetic shift right, bitwise *)
-  | Memory  (** Size-tagged byte-array *)
+  | Sized  (** Size-tagged sequence *)
   | Update of int  (** Constant record with updated index *)
 [@@deriving compare, equal, hash, sexp]
 
 type op3 =
   | Conditional  (** If-then-else *)
-  | Extract  (** Extract a slice of an aggregate value *)
+  | Extract  (** Extract a slice of an sequence value *)
 [@@deriving compare, equal, hash, sexp]
 
 type opN =
@@ -217,14 +217,14 @@ val ashr : t -> t -> t
 (* if-then-else *)
 val conditional : cnd:t -> thn:t -> els:t -> t
 
-(* aggregate sizes *)
-val agg_size_exn : t -> t
-val agg_size : t -> t option
+(* sequence sizes *)
+val seq_size_exn : t -> t
+val seq_size : t -> t option
 
-(* aggregates (memory contents) *)
+(* sequences *)
 val splat : t -> t
-val memory : siz:t -> arr:t -> t
-val extract : agg:t -> off:t -> len:t -> t
+val sized : seq:t -> siz:t -> t
+val extract : seq:t -> off:t -> len:t -> t
 val concat : t array -> t
 
 (* records (struct / array values) *)