strata-org · fabiomadge · Jun 13, 2026 · Jun 23, 2026 · Jun 23, 2026 · Jun 23, 2026
@@ -111,17 +111,35 @@ private def renameOutputsInPostExpr (outputNames : List String) (expr : StmtExpr
       | _ => e)
     expr
 
+/-- Conjoin a list of conditions into a single expression with `&&`. -/
+private def conjoin (conds : List Condition) : Option StmtExprMd :=
+  match conds.map (·.condition) with
+  | [] => none
+  | e :: rest => some (rest.foldl (fun acc x => mkMd (.PrimitiveOp .And [acc, x])) e)
+
 /-- Build a postcondition helper function over the procedure's inputs and outputs.
     Output parameters are renamed (see `outParamSuffix`) to avoid colliding with
     identically-named inputs, and the condition body is rewritten to match. -/
 private def mkPostConditionProc (name : String) (inputs outputs : List Parameter)
-    (condition : Condition) : Procedure :=
+    (assumedConditions : List Condition) (condition : Condition) : Procedure :=
   let outputNames := outputs.map (·.name.text)
   let renamedOutputs := outputs.map (fun p => { p with name := mkId (p.name.text ++ outParamSuffix) })
+  -- `assumedConditions` are the procedure's preconditions plus the *earlier*
+  -- postconditions. We carry them as *free* preconditions of the helper (not as
+  -- an `assumedConditions ==> condition` body). Core's function-WF generation
+  -- assumes a function's preconditions, in order, before asserting the WF of its
+  -- body, so a partial op in `condition` is still checked with that context in
+  -- scope — and, unlike the implication form, a call site that applies the helper
+  -- learns `condition` directly rather than `assumedConditions ==> condition`.
+  -- `free` keeps them assumption-only: each condition is asserted by its own
+  -- helper, never re-asserted here. Output-rename so earlier postconditions
+  -- resolve against this helper's `$out` parameters (preconditions reference
+  -- inputs only, so the rename is a no-op for them).
   { name := mkId name
     inputs := inputs ++ renamedOutputs
     outputs := [⟨mkId "$result", { val := .TBool, source := none }⟩]
-    preconditions := []
+    preconditions := assumedConditions.map (fun (c : Condition) =>
+      { c with condition := renameOutputsInPostExpr outputNames c.condition, free := true })
     decreases := none
     isFunctional := true
     body := .Transparent (renameOutputsInPostExpr outputNames condition.condition) }
@@ -136,7 +154,23 @@ private structure ContractInfo where
 private def ContractInfo.hasPreCondition (info : ContractInfo) : Bool := !info.preNames.isEmpty
 private def ContractInfo.hasPostCondition (info : ContractInfo) : Bool := !info.postNames.isEmpty
 
-/-- Collect contract info for all procedures with contracts. -/
+/-- Whether a contract condition calls one of the given (non-functional)
+    procedures. Used to decide which preconditions can be retained on the lowered
+    procedure: a precondition that calls a procedure cannot survive as a contract
+    expression (illegal in a pure context), so it is dropped from the spec and
+    enforced only through its `$pre` helper. -/
+private def conditionCallsProc (procNames : Std.HashSet String) (c : Condition) : Bool :=
+  let detect : StateM Bool StmtExprMd :=
+    mapStmtExprM (m := StateM Bool) (fun e => do
+      match e.val with
+      | .StaticCall callee _ =>
+        if procNames.contains callee.text then set true
+        pure e
+      | _ => pure e) c.condition
+  (detect.run false).2
+
+/-- Collect contract info for every non-functional procedure that has a contract.
+    Each such procedure's pre/postconditions are lowered into helper functions. -/
 private def collectContractInfo (procs : List Procedure) : Std.HashMap String ContractInfo :=
   procs.foldl (fun m proc =>
     let postconds := getPostconditions proc.body
@@ -332,12 +366,6 @@ private def rewriteCallSitesInProc (contractInfoMap : Std.HashMap String Contrac
     return { proc with body := Body.Opaque posts' impl' mods' }
   | _ => return proc
 
-/-- Conjoin a list of conditions into a single expression with `&&`. -/
-private def conjoin (conds : List Condition) : Option StmtExprMd :=
-  match conds.map (·.condition) with
-  | [] => none
-  | e :: rest => some (rest.foldl (fun acc x => mkMd (.PrimitiveOp .And [acc, x])) e)
-
 /-- Build an axiom expression from `invokeOn` trigger and ensures clauses.
     Produces `∀ p1, ∀ p2, ..., ∀ pn :: { trigger } (preconds => ensures)`.
     The trigger controls when the SMT solver instantiates the axiom. -/
@@ -407,17 +435,23 @@ private def invokeOnOutputRefError (proc : Procedure) : Option DiagnosticModel :
     All procedures with contracts are transformed. -/
 def lowerContracts (program : Program) : Program × List DiagnosticModel :=
   let contractInfoMap := collectContractInfo program.staticProcedures
+  let procNames : Std.HashSet String :=
+    Std.HashSet.ofList (program.staticProcedures.filterMap fun p =>
+      if p.isFunctional then none else some p.name.text)
 
   -- Check for output-referencing ensures in invokeOn procedures
   let diagnostics := program.staticProcedures.filterMap invokeOnOutputRefError
 
-  -- Generate helper procedures for all procedures with contracts
-  let helperProcs := (program.staticProcedures.filter (fun proc => !proc.isFunctional)).flatMap fun proc =>
+  -- Generate the pre/postcondition helper functions for every contracted
+  -- procedure (those in `contractInfoMap`).
+  let helperProcs := (program.staticProcedures.filter
+      (fun proc => !proc.isFunctional && contractInfoMap.contains proc.name.text)).flatMap fun proc =>
     let postconds := getPostconditions proc.body
     let preProcs := proc.preconditions.zipIdx.map fun (c, i) =>
       mkConditionProc (preCondProcName proc.name.text i) proc.inputs c
     let postProcs := postconds.zipIdx.map fun (c, i) =>
-      mkPostConditionProc (postCondProcName proc.name.text i) proc.inputs proc.outputs c
+      mkPostConditionProc (postCondProcName proc.name.text i) proc.inputs proc.outputs
+        (proc.preconditions ++ postconds.take i) c
     preProcs ++ postProcs
 
   -- Transform procedures: strip contracts, add assume/assert, rewrite call sites
@@ -440,7 +474,23 @@ def lowerContracts (program : Program) : Program × List DiagnosticModel :=
       let proc : Procedure := match contractInfoMap.get? proc.name.text with
         | some info =>
           { proc with
-            preconditions := []
+            -- Only an opaque/abstract procedure retains its postconditions natively
+            -- in `spec.postconditions` (a transparent one lowers them to in-body
+            -- asserts via `transformProcBody`, ending with `spec.postconditions = []`).
+            -- Core's `mkContractWFProc` checks the partial-op WF of those native
+            -- postconditions assuming `spec.preconditions` in order first, so an
+            -- opaque proc must keep its preconditions in scope; a transparent proc
+            -- needs none (its postcondition asserts run after the in-body `$pre`
+            -- assumes, which already supply the context). So for opaque/abstract
+            -- procs we keep the non-procedure-calling preconditions as *free*
+            -- (assumed, never re-asserted — the `$pre` helpers check them at call
+            -- sites); for transparent procs we strip them. Procedure-calling
+            -- preconditions are always dropped (illegal as a contract expression;
+            -- handled solely by their `$pre` helper).
+            preconditions :=
+              if proc.body.isTransparent then []
+              else proc.preconditions.filterMap (fun (c : Condition) =>
+                if conditionCallsProc procNames c then none else some { c with free := true })
             body := transformProcBody proc info }
         | none => proc
       -- Rewrite call sites in the procedure body

@@ -44,6 +44,44 @@ function update(map: int, key: int, value: int) : Box
 function const(value: int) : Box
   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
 
 /--

@@ -35,6 +35,8 @@ open Std (Format ToFormat)
 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
@@ -90,6 +92,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"]
@@ -199,6 +201,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
@@ -265,11 +271,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
@@ -396,6 +405,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

@@ -8,7 +8,7 @@ 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: fieldAccess prec raised 90 -> 95 (paren-free `c#n++`); shares prec(95) with `call`.
+-- Last grammar change: added Seq<T>, Array<T>, subscript, and seqLiteral productions (merged with base's fieldAccess-prec 90->95, doWhile, and array-theory changes).
 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;
@@ -231,3 +233,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 "]";