strata-org · fabiomadge · Apr 28, 2026 · Apr 29, 2026 · May 3, 2026 · May 3, 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
   | ⟨.TTypedField vt, _⟩ => collectTypeRefs vt
   | ⟨.Applied base args, _⟩ =>
@@ -88,6 +90,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
 
@@ -74,6 +74,8 @@ private partial def collectHighTypeNames (ty : HighTypeMd) : CollectM Unit := do
   | .TTypedField vt => collectHighTypeNames vt
   | .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
@@ -123,6 +125,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 _
   | .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"]
@@ -184,6 +186,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
@@ -247,11 +253,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.multiAssign, #[targetsSeq, valueArg] =>
       let targets ← match targetsSeq with
         | .seq _ .comma args => args.toList.mapM fun targ => do
@@ -359,6 +368,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,13 +3,12 @@
 
   SPDX-License-Identifier: Apache-2.0 OR MIT
 -/
--- Grammar updated: renamed Optional* categories (op names updated)
 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: block format uses indent(2) with leading spaces for vertical layout.
+-- 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;
@@ -211,3 +213,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 "]";
@@ -170,6 +170,37 @@ 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"
+  | .THeap => "heap"
+  | .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}"
+  | .TTypedField vt => s!"Field_{highTypeTag vt.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!". -/
@@ -184,6 +215,7 @@ def boxDestructorName (model : SemanticModel) (ty : HighType) : Identifier :=
       if isDatatype model name then s!"Box..{name.text}Val!"
       else "Box..compositeVal!"
   | .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.
@@ -200,6 +232,7 @@ def boxConstructorName (model : SemanticModel) (ty : HighType) : Identifier :=
       if isDatatype model name then s!"Box..{name.text}"
       else "BoxComposite"
   | .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 -/
@@ -217,6 +250,9 @@ private def boxConstructorDef (model : SemanticModel) (ty : HighType) : Option D
         some { name := "BoxComposite", args := [{ name := "compositeVal", type := ⟨.UserDefined "Composite", 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 -/
@@ -401,20 +437,24 @@ where
     | .PureFieldUpdate t f v => return [⟨ .PureFieldUpdate (← recurseOne t) f (← recurseOne v), source ⟩]
     | .PrimitiveOp op args _ =>
       let args' ← args.mapM (recurseOne ·)
-      -- For == and != on Composite types, compare refs instead
+      -- For == and != on Composite types, compare refs instead. Note
+      -- `.UserDefined` covers BOTH composites (heap references — `ref!` is
+      -- correct) and datatypes (values — `ref!` is wrong and would unify a
+      -- datatype value against `Composite`). Only ref-compare composites;
+      -- datatype equality falls through to structural comparison.
       match op, args with
       | .Eq, [e1, _e2] =>
-        let ty := (computeExprType model e1).val
-        match ty with
-        | .UserDefined _ =>
+        match (computeExprType model e1).val with
+        | .UserDefined name =>
+          if isDatatype model name then return [⟨ .PrimitiveOp op args', source ⟩]
           let ref1 := mkMd (.StaticCall "Composite..ref!" [args'[0]!])
           let ref2 := mkMd (.StaticCall "Composite..ref!" [args'[1]!])
           return [⟨ .PrimitiveOp .Eq [ref1, ref2], source ⟩]
         | _ => return [⟨ .PrimitiveOp op args', source ⟩]
       | .Neq, [e1, _e2] =>
-        let ty := (computeExprType model e1).val
-        match ty with
-        | .UserDefined _ =>
+        match (computeExprType model e1).val with
+        | .UserDefined name =>
+          if isDatatype model name then return [⟨ .PrimitiveOp op args', source ⟩]
           let ref1 := mkMd (.StaticCall "Composite..ref!" [args'[0]!])
           let ref2 := mkMd (.StaticCall "Composite..ref!" [args'[1]!])
           return [⟨ .PrimitiveOp .Neq [ref1, ref2], source ⟩]