strata-org · fabiomadge · Jun 13, 2026 · Jun 23, 2026 · Jun 23, 2026 · Jun 23, 2026
@@ -39,6 +39,44 @@ function update(map: int, key: int, value: int) : int
 function const(value: int) : int
   external;
 
+// Sequence operations. Parameter types and Seq-valued results use int as a
+// placeholder (like Map operations); Core infers the real polymorphic types
+// via WFFactory. Sequence.contains is declared bool because its result is
+// boolean regardless of element type.
+function Sequence.empty() : int
+  external;
+
+function Sequence.build(s: int, v: int) : int
+  external;
+
+function Sequence.select(s: int, i: int) : int
+  external;
+
+function Sequence.update(s: int, i: int, v: int) : int
+  external;
+
+function Sequence.length(s: int) : int
+  external;
+
+function Sequence.append(s1: int, s2: int) : int
+  external;
+
+function Sequence.contains(s: int, v: int) : bool
+  external;
+
+function Sequence.take(s: int, n: int) : int
+  external;
+
+function Sequence.drop(s: int, n: int) : int
+  external;
+
+// Array operations. Desugared by SubscriptElim into Sequence operations on $data.
+function Array.length(a: int) : int
+  external;
+
+function Sequence.fromArray(a: int) : int
+  external;
+
 #end
 
 /--

@@ -32,6 +32,8 @@ open Lambda (LMonoTy LExpr)
 def collectTypeRefs : HighTypeMd → List String
   | ⟨.UserDefined name, _⟩ => [name.text]
   | ⟨.TSet elem, _⟩ => collectTypeRefs elem
+  | ⟨.TSeq elem, _⟩ => collectTypeRefs elem
+  | ⟨.TArray elem, _⟩ => collectTypeRefs elem
   | ⟨.TMap k v, _⟩ => collectTypeRefs k ++ collectTypeRefs v
   | ⟨.Applied base args, _⟩ =>
       collectTypeRefs base ++ args.flatMap collectTypeRefs
@@ -87,6 +89,11 @@ def collectStaticCallNames (expr : StmtExprMd) : List String :=
       collectStaticCallNames body
   | .Var (.Field t _) => collectStaticCallNames t
   | .PureFieldUpdate t _ v => collectStaticCallNames t ++ collectStaticCallNames v
+  | .Subscript target index update =>
+      collectStaticCallNames target ++ collectStaticCallNames index ++
+      (match update with
+      | some u => collectStaticCallNames u
+      | none => [])
   | .InstanceCall t _ args =>
       collectStaticCallNames t ++ args.flatMap (fun a => collectStaticCallNames a)
   | .Old v | .Fresh v | .Assume v => collectStaticCallNames v

@@ -12,7 +12,7 @@ import Strata.Languages.Core.Factory
 
 Restrict the Laurel prelude to only the `staticProcedures` and `types`
 transitively needed by the user program, reducing the Core program size
-for SMT verification.
+handed to verification.
 
 #### Name collection
 
@@ -73,6 +73,8 @@ private partial def collectHighTypeNames (ty : HighTypeMd) : CollectM Unit := do
   | .TCore _ => pure ()
   | .TSet et => collectHighTypeNames et
   | .TMap kt vt => collectHighTypeNames kt; collectHighTypeNames vt
+  | .TSeq et => collectHighTypeNames et
+  | .TArray et => collectHighTypeNames et
   | .Applied base args =>
     collectHighTypeNames base; args.forM collectHighTypeNames
   | .Pure base => collectHighTypeNames base
@@ -127,6 +129,14 @@ private partial def collectExprNames (expr : StmtExprMd) : CollectM Unit := do
   | .ContractOf _ func => collectExprNames func
   | .ReferenceEquals lhs rhs => collectExprNames lhs; collectExprNames rhs
   | .Hole _ ty => ty.forM collectHighTypeNames
+  | .Subscript target index update =>
+    collectExprNames target
+    collectExprNames index
+    update.forM collectExprNames
+  | .SubscriptWrite target index value =>
+    collectExprNames target
+    collectExprNames index
+    collectExprNames value
   | .Exit _ | .LiteralInt _ | .LiteralBool _ | .LiteralString _ | .LiteralDecimal _ | .LiteralBv _ _
   | .Var (.Local _) | .This | .Abstract | .All => pure ()
 

@@ -46,6 +46,8 @@ partial def highTypeValToArg : HighType → Arg
   | .TString => laurelOp "stringType"
   | .TBv n => laurelOp "bvType" #[.num sr n]
   | .TMap k v => laurelOp "mapType" #[highTypeToArg k, highTypeToArg v]
+  | .TSeq et => laurelOp "seqType" #[highTypeToArg et]
+  | .TArray et => laurelOp "arrayType" #[highTypeToArg et]
   | .UserDefined name => laurelOp "compositeType" #[ident name.text]
   | .TCore s => laurelOp "coreType" #[ident s]
   | .TVoid => laurelOp "compositeType" #[ident "void"]
@@ -195,6 +197,15 @@ where
     | .ContractOf _type fn => stmtExprValToArg fn.val
     | .Abstract => laurelOp "identifier" #[ident "abstract"]
     | .All => laurelOp "identifier" #[ident "all"]
+    | .Subscript target index update =>
+      let updateOpt := optionArg (update.map fun v => laurelOp "seqUpdateValue" #[stmtExprToArg v])
+      laurelOp "subscript" #[stmtExprToArg target, stmtExprToArg index, updateOpt]
+    | .SubscriptWrite target index value =>
+      -- `a[i] := v`: assignment whose target is a (read-shaped) subscript.
+      laurelOp "assign" #[
+        laurelOp "subscript" #[stmtExprToArg target, stmtExprToArg index, optionArg none],
+        stmtExprToArg value
+      ]
     | .PureFieldUpdate target field value =>
       -- Not directly in grammar; emit as assignment to field
       laurelOp "assign" #[

@@ -108,6 +108,12 @@ partial def translateHighType (arg : Arg) : TransM HighTypeMd := do
       let keyType ← translateHighType keyArg
       let valType ← translateHighType valArg
       return mkHighTypeMd (.TMap keyType valType) src
+    | q`Laurel.seqType, #[elemArg] =>
+      let elemType ← translateHighType elemArg
+      return mkHighTypeMd (.TSeq elemType) src
+    | q`Laurel.arrayType, #[elemArg] =>
+      let elemType ← translateHighType elemArg
+      return mkHighTypeMd (.TArray elemType) src
     | q`Laurel.compositeType, #[nameArg] =>
       let name ← translateIdent nameArg
       return mkHighTypeMd (.UserDefined name) src
@@ -251,11 +257,14 @@ partial def translateStmtExpr (arg : Arg) : TransM StmtExprMd := do
     | q`Laurel.parenthesis, #[arg0] => translateStmtExpr arg0
     | q`Laurel.assign, #[arg0, arg1] =>
       let target ← translateStmtExpr arg0
-      let targetVar : VariableMd ← match target.val with
-        | .Var v => pure ⟨v, target.source⟩
-        | _ => TransM.error s!"assign target must be a variable or field access"
       let value ← translateStmtExpr arg1
-      return mkStmtExprMd (.Assign [targetVar] value) src
+      match target.val with
+      | .Subscript subTarget index none =>
+        -- `a[i] := v` is a destructive in-place write. SubscriptElim rewrites
+        -- it (Array<T>) or `ValidateSubscriptUsage` rejects it (Seq<T>).
+        return mkStmtExprMd (.SubscriptWrite subTarget index value) src
+      | .Var v => return mkStmtExprMd (.Assign [⟨v, target.source⟩] value) src
+      | _ => TransM.error s!"assign target must be a variable or field access"
     | q`Laurel.preIncr, #[arg0] =>
       let target ← translateIncrDecrTarget arg0 "preIncr"
       return mkStmtExprMd (.IncrDecr .Pre .Incr target) src
@@ -387,6 +396,21 @@ partial def translateStmtExpr (arg : Arg) : TransM StmtExprMd := do
         | _ => pure none
       let body ← translateStmtExpr bodyArg
       return mkStmtExprMd (.Quantifier .Exists { name := name, type := ty } trigger body) src
+    | q`Laurel.seqLiteral, #[elementsSeq] =>
+      let elements ← match elementsSeq with
+        | .seq _ .comma args => args.toList.mapM translateStmtExpr
+        | _ => pure []
+      let empty := mkStmtExprMd (.StaticCall (mkId SeqOp.empty) []) src
+      return elements.foldl (fun acc e => mkStmtExprMd (.StaticCall (mkId SeqOp.build) [acc, e]) src) empty
+    | q`Laurel.subscript, #[targetArg, indexArg, updateArg] =>
+      let target ← translateStmtExpr targetArg
+      let index ← translateStmtExpr indexArg
+      let update ← match updateArg with
+        | .option _ (some (.op updateOp)) => match updateOp.name, updateOp.args with
+          | q`Laurel.seqUpdateValue, #[valArg] => some <$> translateStmtExpr valArg
+          | _, _ => pure none
+        | _ => pure none
+      return mkStmtExprMd (.Subscript target index update) src
     | _, #[arg0] => match getUnaryOp? op.name with
       | some primOp =>
         let inner ← translateStmtExpr arg0

@@ -3,16 +3,11 @@
 
   SPDX-License-Identifier: Apache-2.0 OR MIT
 -/
--- Grammar updated: renamed Optional* categories (op names updated)
--- Grammar updated: `call` callee at prec 89 to accept fieldAccess (prec 90) chains
--- Grammar updated: `fieldAccess` is leftassoc so `a#b#c` parses as `(a#b)#c`
--- Grammar updated: added bitvector literal support (bvLiteral)
-
 module
 -- Laurel dialect definition, loaded from LaurelGrammar.st
 -- NOTE: Changes to LaurelGrammar.st are not automatically tracked by the build system.
 -- Update this file (e.g. this comment) to trigger a recompile after modifying LaurelGrammar.st.
--- Last grammar change: renamed strConcat token to `^`; added preIncr/preDecr/postIncr/postDecr; `return` value is now Option StmtExpr (supports a valueless return).
+-- Last grammar change: added Seq<T>, Array<T>, subscript, and seqLiteral productions.
 public import StrataDDM.AST
 import StrataDDM.BuiltinDialects.Init
 import StrataDDM.Integration.Lean.HashCommands

@@ -13,6 +13,8 @@ op bvType (width: Num): LaurelType => "bv" width;
 // Core type passthrough: parsed as Ident, translated to HighType.TCore
 op coreType (name: Ident): LaurelType => "Core " name;
 op mapType (keyType: LaurelType, valueType: LaurelType): LaurelType => "Map " keyType " " valueType;
+op seqType (elemType: LaurelType): LaurelType => "Seq<" elemType ">";
+op arrayType (elemType: LaurelType): LaurelType => "Array<" elemType ">";
 op compositeType (name: Ident): LaurelType => name;
 
 category StmtExpr;
@@ -226,3 +228,11 @@ op procedureCommand(procedure: Procedure): Command => procedure;
 op datatypeCommand(datatype: Datatype): Command => datatype;
 op constrainedTypeCommand(ct: ConstrainedType): Command => ct;
 
+
+// Sequence and Array operations
+category Update;
+op seqUpdateValue(value: StmtExpr): Update => ":=" value;
+// index:11 excludes assign (prec 10) so `:=` in s[i := v] is parsed by Update, not assign
+op subscript(target: StmtExpr, index: StmtExpr, update: Option Update): StmtExpr
+  => target "[" index:11 update "]";
+op seqLiteral(elements: CommaSepBy StmtExpr): StmtExpr => "[" elements "]";
@@ -174,6 +174,35 @@ private def isDatatype (model : SemanticModel) (name : Identifier) : Bool :=
   | .datatypeDefinition _ => true
   | _ => false
 
+/-- Compute a stable string tag for a `HighType`, used to derive per-type
+    Box constructor / destructor names. Designed so two structurally distinct
+    types never produce the same tag. -/
+private partial def highTypeTag : HighType → String
+  | .TVoid => "void"
+  | .TBool => "bool"
+  | .TInt => "int"
+  | .TFloat64 => "float64"
+  | .TReal => "real"
+  | .TString => "string"
+  | .TBv n => s!"bv{n}"
+  | .UserDefined name => name.text
+  | .TCore name => name
+  | .TSeq et => s!"Seq_{highTypeTag et.val}"
+  | .TArray et => s!"Array_{highTypeTag et.val}"
+  | .TSet et => s!"Set_{highTypeTag et.val}"
+  | .TMap k v => s!"Map_{highTypeTag k.val}_{highTypeTag v.val}"
+  | .Pure base => s!"Pure_{highTypeTag base.val}"
+  | .Intersection types =>
+    "Intersection_" ++ String.intercalate "_" (types.map (highTypeTag ·.val))
+  | .Applied base args =>
+    "Applied_" ++ String.intercalate "_"
+      (highTypeTag base.val :: args.map (highTypeTag ·.val))
+  | .Unknown => "unknown"
+  | .MultiValuedExpr types =>
+    -- Internal-only type for multi-return procedure calls; never a Box field
+    -- type in practice, but include for exhaustiveness.
+    "MultiValuedExpr_" ++ String.intercalate "_" (types.map (highTypeTag ·.val))
+
 /-- Get the Box destructor name for a given Laurel HighType.
     For UserDefined datatypes, uses "Box..<datatypeName>Val!";
     for Composite types, uses "Box..compositeVal!". -/
@@ -189,6 +218,7 @@ def boxDestructorName (model : SemanticModel) (ty : HighType) : Identifier :=
       else "Box..compositeVal!"
   | .TBv n => s!"Box..bv{n}Val!"
   | .TCore name => s!"Box..{name}Val!"
+  | .TSeq et => s!"Box..Seq_{highTypeTag et.val}Val!"
   | _ => dbg_trace f!"BUG, boxDestructorName bad type {ty}"; "boxDestructorNameError"
 
 /-- Get the Box constructor name for a given Laurel HighType.
@@ -206,6 +236,7 @@ def boxConstructorName (model : SemanticModel) (ty : HighType) : Identifier :=
       else "BoxComposite"
   | .TBv n => s!"BoxBv{n}"
   | .TCore name => s!"Box..{name}"
+  | .TSeq et => s!"BoxSeq_{highTypeTag et.val}"
   | ty => dbg_trace s!"BUG, boxConstructorName bad type: {repr ty}"; "boxConstructorNameError"
 
 /-- Build the DatatypeConstructor for a Box variant from a HighType, for datatype generation -/
@@ -225,6 +256,9 @@ private def boxConstructorDef (model : SemanticModel) (ty : HighType) : Option D
         some { name := s!"BoxBv{n}", args := [{ name := s!"bv{n}Val", type := ⟨.TBv n, none⟩ }] }
   | .TCore name =>
         some { name := s!"Box..{name}", args := [{ name := s!"{name}Val", type := ⟨.TCore name, none⟩ }] }
+  | .TSeq et =>
+        let tag := highTypeTag et.val
+        some { name := s!"BoxSeq_{tag}", args := [{ name := s!"Seq_{tag}Val", type := ⟨ty, none⟩ }] }
   | ty => dbg_trace s!"BUG, boxConstructorDef bad type: {repr ty}"; none
 
 /-- Record a Box constructor use in the transform state -/