diff --git a/Strata/Languages/Laurel/ContractPass.lean b/Strata/Languages/Laurel/ContractPass.lean index 2d9b98ffb0..b95892fbb6 100644 --- a/Strata/Languages/Laurel/ContractPass.lean +++ b/Strata/Languages/Laurel/ContractPass.lean @@ -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 diff --git a/Strata/Languages/Laurel/CoreDefinitionsForLaurel.lean b/Strata/Languages/Laurel/CoreDefinitionsForLaurel.lean index dfe3e09782..bb132b76e1 100644 --- a/Strata/Languages/Laurel/CoreDefinitionsForLaurel.lean +++ b/Strata/Languages/Laurel/CoreDefinitionsForLaurel.lean @@ -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 /-- diff --git a/Strata/Languages/Laurel/CoreGroupingAndOrdering.lean b/Strata/Languages/Laurel/CoreGroupingAndOrdering.lean index 85303d227e..4238a6c903 100644 --- a/Strata/Languages/Laurel/CoreGroupingAndOrdering.lean +++ b/Strata/Languages/Laurel/CoreGroupingAndOrdering.lean @@ -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 diff --git a/Strata/Languages/Laurel/FilterPrelude.lean b/Strata/Languages/Laurel/FilterPrelude.lean index 52fd25fcbc..9c735e6ade 100644 --- a/Strata/Languages/Laurel/FilterPrelude.lean +++ b/Strata/Languages/Laurel/FilterPrelude.lean @@ -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 () diff --git a/Strata/Languages/Laurel/Grammar/AbstractToConcreteTreeTranslator.lean b/Strata/Languages/Laurel/Grammar/AbstractToConcreteTreeTranslator.lean index 145c39694f..5455ff535f 100644 --- a/Strata/Languages/Laurel/Grammar/AbstractToConcreteTreeTranslator.lean +++ b/Strata/Languages/Laurel/Grammar/AbstractToConcreteTreeTranslator.lean @@ -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" #[ diff --git a/Strata/Languages/Laurel/Grammar/ConcreteToAbstractTreeTranslator.lean b/Strata/Languages/Laurel/Grammar/ConcreteToAbstractTreeTranslator.lean index bf5e10dd12..3e853dafb8 100644 --- a/Strata/Languages/Laurel/Grammar/ConcreteToAbstractTreeTranslator.lean +++ b/Strata/Languages/Laurel/Grammar/ConcreteToAbstractTreeTranslator.lean @@ -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) or `ValidateSubscriptUsage` rejects it (Seq). + 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 diff --git a/Strata/Languages/Laurel/Grammar/LaurelGrammar.lean b/Strata/Languages/Laurel/Grammar/LaurelGrammar.lean index dc54d7617a..70b090d8e8 100644 --- a/Strata/Languages/Laurel/Grammar/LaurelGrammar.lean +++ b/Strata/Languages/Laurel/Grammar/LaurelGrammar.lean @@ -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, Array, 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 diff --git a/Strata/Languages/Laurel/Grammar/LaurelGrammar.st b/Strata/Languages/Laurel/Grammar/LaurelGrammar.st index 53f0c33f99..97ed47faaa 100644 --- a/Strata/Languages/Laurel/Grammar/LaurelGrammar.st +++ b/Strata/Languages/Laurel/Grammar/LaurelGrammar.st @@ -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 "]"; diff --git a/Strata/Languages/Laurel/HeapParameterization.lean b/Strata/Languages/Laurel/HeapParameterization.lean index daf9e9f4b7..c3a6159dfe 100644 --- a/Strata/Languages/Laurel/HeapParameterization.lean +++ b/Strata/Languages/Laurel/HeapParameterization.lean @@ -173,6 +173,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..Val!"; for Composite types, uses "Box..compositeVal!". @@ -193,6 +222,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. @@ -210,6 +240,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 -/ @@ -229,6 +260,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 -/ diff --git a/Strata/Languages/Laurel/LaurelAST.lean b/Strata/Languages/Laurel/LaurelAST.lean index fb02d7cd59..5bf3c12c4b 100644 --- a/Strata/Languages/Laurel/LaurelAST.lean +++ b/Strata/Languages/Laurel/LaurelAST.lean @@ -156,6 +156,10 @@ inductive HighType : Type where | TSet (elementType : AstNode HighType) /-- Map type. -/ | TMap (keyType : AstNode HighType) (valueType : AstNode HighType) + /-- Immutable sequence type, e.g. `Seq`. Maps to Core's polymorphic `Sequence` type. -/ + | TSeq (elementType : AstNode HighType) + /-- Mutable heap-backed array type, e.g. `Array`. Has reference (aliasing) semantics. -/ + | TArray (elementType : AstNode HighType) /-- A Identifier to a user-defined composite or constrained type by name. -/ | UserDefined (name : Identifier) /-- A generic type application, e.g. `List`. -/ @@ -395,6 +399,17 @@ inductive StmtExpr : Type where - `type`: this property is used internally by Laurel and can be left to its default value. Internal usage: inferred by the hole type inference pass; `none` means not yet inferred. -/ | Hole (deterministic : Bool := true) (type : Option (AstNode HighType) := none) + /-- Subscript read `s[i]` or functional update `s[i := v]`, both *values*. + `update = none` is a read; `update = some v` is a functional update that + produces a new sequence (it does not mutate `target`). Eliminated by + `SubscriptElim`. Destructive in-place writes are `.SubscriptWrite`. -/ + | Subscript (target : AstNode StmtExpr) (index : AstNode StmtExpr) (update : Option (AstNode StmtExpr)) + /-- Destructive in-place subscript write `a[i] := v` on a mutable `Array`, + a *statement* (not a value). Distinct from `.Subscript t i (some v)` + (functional update) so the two need not be disambiguated by syntactic + position. Produced by the grammar translator for `a[i] := v`; eliminated + by `SubscriptElim`. -/ + | SubscriptWrite (target : AstNode StmtExpr) (index : AstNode StmtExpr) (value : AstNode StmtExpr) inductive ContractType where | Reads | Modifies | Precondition | PostCondition @@ -433,6 +448,8 @@ def StmtExpr.constrName : StmtExpr → String | .Assume .. => "assume" | .ProveBy .. => "by" | .ContractOf .. => "contractOf" + | .Subscript .. => "subscript" + | .SubscriptWrite .. => "subscript write" | .Abstract => "abstract" | .All => "all" | .Hole .. => "hole" @@ -459,6 +476,14 @@ def bodyLabel : String := "$body" theorem AstNode.sizeOf_val_lt {t : Type} [SizeOf t] (e : AstNode t) : sizeOf e.val < sizeOf e := by cases e; grind +/-- Termination helper for AST walkers that recurse on a child of `n.val`, +where the match arm bound a hypothesis `h : n.val = Constructor … child …`. +From `sizeOf n.val < sizeOf n` (`AstNode.sizeOf_val_lt`), rewrite via `h` and +let `simp` expand the constructor's `sizeOf`, closing `sizeOf child < sizeOf n`. +Use as `all_goals (try (term_by_val n h))`. -/ +macro "term_by_val" n:term "," h:ident : tactic => + `(tactic| (have hlt := AstNode.sizeOf_val_lt $n; rw [$h:ident] at hlt; simp at hlt; omega)) + theorem Condition.sizeOf_condition_lt (c : Condition) : sizeOf c.condition < 1 + sizeOf c := by cases c; grind @@ -540,6 +565,8 @@ def highEq (a : HighTypeMd) (b : HighTypeMd) : Bool := match _a: a.val, _b: b.va | HighType.TBv n1, HighType.TBv n2 => n1 == n2 | HighType.TSet t1, HighType.TSet t2 => highEq t1 t2 | HighType.TMap k1 v1, HighType.TMap k2 v2 => highEq k1 k2 && highEq v1 v2 + | HighType.TSeq t1, HighType.TSeq t2 => highEq t1 t2 + | HighType.TArray t1, HighType.TArray t2 => highEq t1 t2 | HighType.UserDefined r1, HighType.UserDefined r2 => r1.text == r2.text | HighType.TCore s1, HighType.TCore s2 => s1 == s2 | HighType.Applied b1 args1, HighType.Applied b2 args2 => @@ -663,6 +690,17 @@ def isSubtype (ctx : TypeLattice) (sub sup : HighTypeMd) : Bool := `highEq` arm zips element-wise IN DECLARATION ORDER, so `A & B ≠ B & A` even though intersection is conceptually unordered. Known limitation, to fix with bespoke subtyping rules when intersections become live. -/ + +/-- Name of the synthetic composite `SubscriptElim` injects to model `Array` + (the `$` prefix avoids colliding with user types). Defined here, rather than + with the other array names below, so the consistency relation can name it. -/ +def arrayCompositeName := "$Array" + +/-- Name of the flattened composite reference type that `TypeHierarchy`'s + `compositeRefToComposite` collapses every composite (including `$Array`) + into. After that pass all composite values share this single static type. -/ +def compositeTypeName := "Composite" + /-- Consistency `~` (Siek–Taha): the symmetric gradual relation. `Unknown` is the dynamic type and is consistent with everything; otherwise structural equality after unfolding aliases / constrained types. @@ -686,15 +724,35 @@ def isConsistent (ctx : TypeLattice) (a b : HighTypeMd) : Bool := | _, _ => let a' := ctx.unfold a let b' := ctx.unfold b + -- A surface `Array` is mutually consistent with its lowered forms + -- (`$Array`, then `Composite`): the declaration type is never rewritten, so + -- re-resolution after lowering compares the two (e.g. a modifies clause's + -- `$obj != a` guard). `isArrayInitCompatible` covers the related init case. + let isLoweredArrayName (n : String) : Bool := + n == arrayCompositeName || n == compositeTypeName match a'.val, b'.val with | .Unknown, _ | _, .Unknown => true | .TCore _, _ | _, .TCore _ => true + | .TArray _, .UserDefined n | .UserDefined n, .TArray _ => isLoweredArrayName n.text | _, _ => highEq a' b' termination_by (SizeOf.sizeOf a) decreasing_by all_goals (cases a; cases b; try term_by_mem) cases t1; term_by_mem +/-- A `Seq` flows into an `Array` slot when `U <: T` — an array is + *initialized* from a sequence literal (`var a: Array := [1, 2, 3]`). + The element types are checked, so `Array := [true]` is rejected. + + `isConsistent` does *not* admit this (it is element-invariant), so it needs + its own rule; the complementary `Array`/lowered-form consistency lives in + `isConsistent`. Uses `isConsistent`/`isSubtype` directly to stay + non-recursive. -/ +def isArrayInitCompatible (ctx : TypeLattice) (sub sup : HighTypeMd) : Bool := + match (ctx.unfold sup).val, (ctx.unfold sub).val with + | .TArray et, .TSeq st => isConsistent ctx st et || isSubtype ctx st et + | _, _ => false + /-- Consistent subtyping: `∃ R. sub ~ R ∧ R <: sup`. For our flat lattice this collapses to `sub ~ sup ∨ sub <: sup` — the standard collapse. @@ -711,14 +769,25 @@ def isConsistent (ctx : TypeLattice) (a b : HighTypeMd) : Bool := user type was ever rejected. The bidirectional design retires that carve-out — user-defined types are now a regular participant in `<:`, with `isSubtype` walking inheritance chains and unwrapping aliases - and constrained types to deliver real checking on user-defined code. -/ + and constrained types to deliver real checking on user-defined code. + + The `isArrayInitCompatible` disjunct adds the narrow `Array` surface-vs- + lowered carve-out documented on that helper. -/ def isConsistentSubtype (ctx : TypeLattice) (sub sup : HighTypeMd) : Bool := - isConsistent ctx sub sup || isSubtype ctx sub sup + isConsistent ctx sub sup || isSubtype ctx sub sup || isArrayInitCompatible ctx sub sup def HighType.isBool : HighType → Bool | TBool => true | _ => false +def HighType.isArray : HighType → Bool + | TArray _ => true + | _ => false + +def HighType.isSeq : HighType → Bool + | TSeq _ => true + | _ => false + /-- Return the constructor name of a `StmtExprMd` as a `String`. -/ def StmtExpr.constructorName (e : StmtExpr) : String := match e with @@ -751,6 +820,8 @@ def StmtExpr.constructorName (e : StmtExpr) : String := | .Assume .. => "Assume" | .ProveBy .. => "ProveBy" | .ContractOf .. => "ContractOf" + | .Subscript .. => "Subscript" + | .SubscriptWrite .. => "SubscriptWrite" | .Abstract => "Abstract" | .All => "All" | .Hole .. => "Hole" @@ -940,6 +1011,50 @@ structure Program where constants : List Constant := [] deriving Inhabited +/-! ## Sequence and Array well-known names + +`SubscriptElim` and `ConcreteToAbstractTreeTranslator` reference these names +when lowering `Seq` and `Array` to Core. They are collected here so +changes do not silently diverge between passes. +-/ + +/-- `Sequence.empty() : Seq` — the empty sequence. -/ +def SeqOp.empty := "Sequence.empty" +/-- `Sequence.build(s, v) : Seq` — append `v` to the end of `s`. -/ +def SeqOp.build := "Sequence.build" +/-- `Sequence.select(s, i) : T` — read the element at index `i`. -/ +def SeqOp.select := "Sequence.select" +/-- `Sequence.update(s, i, v) : Seq` — functional update. -/ +def SeqOp.update := "Sequence.update" +/-- `Sequence.length(s) : int` — length of the sequence. -/ +def SeqOp.length := "Sequence.length" +/-- `Sequence.append(s1, s2) : Seq` — concatenation. -/ +def SeqOp.append := "Sequence.append" +/-- `Sequence.contains(s, v) : bool` — membership test. -/ +def SeqOp.contains := "Sequence.contains" +/-- `Sequence.take(s, n) : Seq` — prefix of length `n`. -/ +def SeqOp.take := "Sequence.take" +/-- `Sequence.drop(s, n) : Seq` — suffix after dropping `n`. -/ +def SeqOp.drop := "Sequence.drop" + +/-- Name of the `$data` field on the synthetic `$Array` composite. + This is a field name, not a `Sequence.*` operation — kept out of the + `SeqOp.*` namespace since it's semantically different from the entries + above. -/ +def arrayDataField := "$data" + +-- `arrayCompositeName` ("$Array") is defined earlier, alongside the +-- consistency relation that also needs it. + +/-- Name of the `Array.length` function. Calls to this name are desugared by + `SubscriptElim` into `Sequence.length(a.$data)`. -/ +def arrayLengthName := "Array.length" + +/-- Name of the `Sequence.fromArray` function. Takes a snapshot of an array's + contents as an immutable `Seq`. Calls are desugared by `SubscriptElim` + into `a#$data`. -/ +def sequenceFromArrayName := "Sequence.fromArray" + end -- public section end Laurel diff --git a/Strata/Languages/Laurel/LaurelCompilationPipeline.lean b/Strata/Languages/Laurel/LaurelCompilationPipeline.lean index 4e048572c5..d9df8a640f 100644 --- a/Strata/Languages/Laurel/LaurelCompilationPipeline.lean +++ b/Strata/Languages/Laurel/LaurelCompilationPipeline.lean @@ -27,6 +27,7 @@ import Strata.Languages.Laurel.PushOldInward import Strata.Languages.Laurel.LiftInstanceProcedures import Strata.Languages.Laurel.TypeAliasElim public import Strata.Languages.Laurel.LaurelPass +import Strata.Languages.Laurel.SubscriptElim public import Strata.Languages.Core import Strata.Languages.Core.DDMTransform.ASTtoCST import Strata.Languages.Core.Verifier @@ -98,6 +99,7 @@ abbrev TranslateResultWithLaurel := (Option Core.Program) × (List DiagnosticMod /-- The ordered sequence of Laurel-to-Laurel lowering passes. -/ def laurelPipeline : Array LoweringPass := #[ + subscriptElimPass, eliminateDoWhilePass, eliminateIncrDecrPass, typeAliasElimPass, @@ -147,6 +149,13 @@ private def runLaurelPasses let mut allDiags : List DiagnosticModel := result.errors.toList let mut allStats : Statistics := {} + -- Whether the program was already rejected before lowering began (any + -- non-verification error from `resolve`, which now includes subscript-usage + -- and diamond-access validation). Its diagnostics are collected into + -- `allDiags` above; the flag additionally disarms the StrataBug guard below + -- (see there). + let programIsKnownInvalid := !result.errors.isEmpty + for pass in laurelPipeline do let (program', diags, stats) ← pctx.withPhase pass.name do pure (pass.run options program model) program := program' @@ -157,12 +166,21 @@ private def runLaurelPasses let result := resolve program (some model) let newErrors := result.errors.filter fun e => !resolutionErrors.contains e if !newErrors.isEmpty then + emit pass.name "laurel.st" program + if programIsKnownInvalid then + -- The program was already rejected before lowering, so a pass + -- transforming it into something that no longer re-resolves is + -- expected fallout, not a compiler bug. Stop here and report only the + -- diagnostics already collected (the real, user-facing errors), + -- dropping the downstream noise rather than mislabeling it `StrataBug`. + return (program, model, allDiags, allStats) + -- The program resolved cleanly before this pass, so a newly-introduced + -- error means the pass itself corrupted the program: a compiler bug. let newDiags := newErrors.toList.map fun d => { d with message := s!"Internal error: resolution after '{pass.name}' introduced this diagnostic: {d}. Existing diagnostics were: {resolutionErrors.toList}" type := .StrataBug } - emit pass.name "laurel.st" program return (program, model, allDiags ++ newDiags, allStats) program := result.program model := result.model diff --git a/Strata/Languages/Laurel/LaurelToCoreSchemaPass.lean b/Strata/Languages/Laurel/LaurelToCoreSchemaPass.lean index e5a62a87dd..c4916eb273 100644 --- a/Strata/Languages/Laurel/LaurelToCoreSchemaPass.lean +++ b/Strata/Languages/Laurel/LaurelToCoreSchemaPass.lean @@ -88,6 +88,8 @@ def translateType (ty : HighTypeMd) : TranslateM LMonoTy := do | .TVoid => return LMonoTy.bool -- Using bool as placeholder for void | .TSet elementType => return Core.mapTy (← translateType elementType) LMonoTy.bool | .TMap keyType valueType => return Core.mapTy (← translateType keyType) (← translateType valueType) + | .TSeq elementType => return Core.seqTy (← translateType elementType) + | .TArray _ => return .tcons compositeTypeName [] | .UserDefined name => match model.get? name with | some (.datatypeDefinition dt) => return .tcons dt.name.text [] @@ -331,6 +333,7 @@ def translateExpr (expr : StmtExprMd) | .InstanceCall target callee args => throwExprDiagnostic $ diagnosticFromSource expr.source "instance call expression translation" DiagnosticType.NotYetImplemented | .PureFieldUpdate _ _ _ => throwExprDiagnostic $ diagnosticFromSource expr.source "pure field update expression translation" DiagnosticType.NotYetImplemented | .This => throwExprDiagnostic $ diagnosticFromSource expr.source "this expression translation" DiagnosticType.NotYetImplemented + | .Subscript _ _ _ | .SubscriptWrite _ _ _ => throwExprDiagnostic $ diagnosticFromSource expr.source "Subscript should have been eliminated by SubscriptElim" DiagnosticType.StrataBug termination_by expr decreasing_by all_goals (have := AstNode.sizeOf_val_lt expr; term_by_mem) diff --git a/Strata/Languages/Laurel/LaurelTypes.lean b/Strata/Languages/Laurel/LaurelTypes.lean index d462f5242e..8700a2289b 100644 --- a/Strata/Languages/Laurel/LaurelTypes.lean +++ b/Strata/Languages/Laurel/LaurelTypes.lean @@ -52,6 +52,18 @@ def computeExprType (model : SemanticModel) (expr : StmtExprMd) : HighTypeMd := | .Var (.Declare _) => ⟨ .TVoid, source ⟩ -- Field access | .Var (.Field _ fieldName) => (model.get fieldName).getType + -- Subscript read returns the element type; functional update `s[i := v]` + -- returns a new sequence of the same type as the target. + | .Subscript target _ update => + match update with + | some _ => computeExprType model target + | none => + match (computeExprType model target).val with + | .TSeq et => et + | .TArray et => et + | _ => ⟨ HighType.Unknown, source ⟩ + -- Destructive write `a[i] := v` is a statement. + | .SubscriptWrite _ _ _ => ⟨ .TVoid, source ⟩ -- Pure field update returns the same type as the target | .PureFieldUpdate target _ _ => computeExprType model target -- Calls — return the declared output type when available, fall back to Unknown otherwise @@ -120,6 +132,7 @@ non-heap-relevant types. Single source of truth for which types participate in modifies clauses and heap parameterization. -/ def classifyModifiesHighType : HighType → Option ModifiesTypeKind | .UserDefined _ => some .composite + | .TArray _ => some .composite | .TSet _ => some .compositeSet | _ => none diff --git a/Strata/Languages/Laurel/MapStmtExpr.lean b/Strata/Languages/Laurel/MapStmtExpr.lean index 2ba11ebea7..af2cf42b08 100644 --- a/Strata/Languages/Laurel/MapStmtExpr.lean +++ b/Strata/Languages/Laurel/MapStmtExpr.lean @@ -120,6 +120,12 @@ def mapStmtExprUsedM [Monad m] (f : Bool → StmtExprMd → m StmtExprMd) pure ⟨.ProveBy (← mapStmtExprUsedM f true value) (← mapStmtExprUsedM f true proof), source⟩ | .ContractOf ty func => pure ⟨.ContractOf ty (← mapStmtExprUsedM f true func), source⟩ + | .Subscript target index update => + pure ⟨.Subscript (← mapStmtExprUsedM f true target) (← mapStmtExprUsedM f true index) + (← update.attach.mapM fun ⟨e, _⟩ => mapStmtExprUsedM f true e), source⟩ + | .SubscriptWrite target index value => + pure ⟨.SubscriptWrite (← mapStmtExprUsedM f true target) (← mapStmtExprUsedM f true index) + (← mapStmtExprUsedM f true value), source⟩ -- Leaves: no StmtExprMd children. -- ⚠ If a new StmtExpr constructor with StmtExprMd children is added, -- it must get its own arm above; otherwise all passes will silently @@ -231,6 +237,12 @@ def mapStmtExprFlattenM [Monad m] (pre : Bool → StmtExprMd → m (Option (List | .ProveBy value proof => pure ⟨.ProveBy (collapse (← go true value) value.source) (collapse (← go true proof) proof.source), source⟩ | .ContractOf ty func => pure ⟨.ContractOf ty (collapse (← go true func) func.source), source⟩ + | .Subscript target index update => + pure ⟨.Subscript (collapse (← go true target) target.source) (collapse (← go true index) index.source) + (← update.attach.mapM fun ⟨x, _⟩ => do pure (collapse (← go true x) x.source)), source⟩ + | .SubscriptWrite target index value => + pure ⟨.SubscriptWrite (collapse (← go true target) target.source) (collapse (← go true index) index.source) + (collapse (← go true value) value.source), source⟩ | .Exit _ | .LiteralInt _ | .LiteralBool _ | .LiteralString _ | .LiteralDecimal _ | .LiteralBv _ _ | .Var (.Local _) | .Var (.Declare _) | .New _ | .This | .Abstract | .All | .Hole .. => pure e post used rebuilt @@ -314,6 +326,12 @@ def mapStmtExprPrePostM [Monad m] (pre : StmtExprMd → m (Option StmtExprMd)) pure ⟨.ProveBy (← mapStmtExprPrePostM pre post value) (← mapStmtExprPrePostM pre post proof), source⟩ | .ContractOf ty func => pure ⟨.ContractOf ty (← mapStmtExprPrePostM pre post func), source⟩ + | .Subscript target index update => + pure ⟨.Subscript (← mapStmtExprPrePostM pre post target) (← mapStmtExprPrePostM pre post index) + (← update.attach.mapM fun ⟨e, _⟩ => mapStmtExprPrePostM pre post e), source⟩ + | .SubscriptWrite target index value => + pure ⟨.SubscriptWrite (← mapStmtExprPrePostM pre post target) (← mapStmtExprPrePostM pre post index) + (← mapStmtExprPrePostM pre post value), source⟩ -- Leaves: no StmtExprMd children. -- ⚠ If a new StmtExpr constructor with StmtExprMd children is added, -- it must get its own arm above; otherwise all passes will silently diff --git a/Strata/Languages/Laurel/Resolution.lean b/Strata/Languages/Laurel/Resolution.lean index a3e3e5090d..e66f7fbcea 100644 --- a/Strata/Languages/Laurel/Resolution.lean +++ b/Strata/Languages/Laurel/Resolution.lean @@ -11,6 +11,7 @@ public import Strata.Languages.Laurel.Grammar.AbstractToConcreteTreeTranslator import Strata.Util.Tactics public import Strata.Languages.Laurel.SemanticModel public import Strata.Languages.Laurel.LaurelTypes +import Strata.Languages.Laurel.MapStmtExpr import Strata.Languages.Laurel.Grammar.AbstractToConcreteTreeTranslator /-! @@ -260,6 +261,7 @@ private def targetTypeName (target : StmtExprMd) : ResolveM (Option String) := d | some (_, node) => match node.getType.val with | .UserDefined typRef => pure (some typRef.text) + | .TArray _ => pure (some arrayCompositeName) | _ => pure none | none => pure none | .Var (.Field inner fieldName) => do @@ -354,6 +356,12 @@ def resolveHighType (ty : HighTypeMd) : ResolveM HighTypeMd := do let kt' ← resolveHighType kt let vt' ← resolveHighType vt pure (.TMap kt' vt') + | .TSeq et => + let et' ← resolveHighType et + pure (.TSeq et') + | .TArray et => + let et' ← resolveHighType et + pure (.TArray et') | .Applied base args => let base' ← resolveHighType base let args' ← args.mapM resolveHighType @@ -440,6 +448,21 @@ private def isReference (ctx : TypeLattice) (ty : HighTypeMd) : Bool := | .UserDefined _ | .Unknown => true | _ => false +/-- Element type of a subscript target, enforcing that it is indexable: + `Seq`/`Array` yields `U`; a concrete non-collection is rejected + (`expected a sequence or array`, as `Fresh`/`ReferenceEquals` reject a + non-reference); a gradual `Unknown`/`TCore` is tolerated silently. The + rejected and gradual cases both return `Unknown` to suppress cascades. + `construct` only prefixes the diagnostic with the surrounding form. -/ +private def checkSubscriptTarget (ctx : TypeLattice) (construct : StmtExpr) + (targetTy : HighTypeMd) (source : Option FileRange) : ResolveM HighTypeMd := do + match (ctx.unfold targetTy).val with + | .TSeq et | .TArray et => pure et + | .Unknown | .TCore _ => pure { val := .Unknown, source := source } + | _ => + typeMismatch source (some construct) "expected a sequence or array" targetTy + pure { val := .Unknown, source := source } + /-- Get the type of a resolved reference. Prefers the resolved definition by `uniqueId` (the post-resolution ground truth, populated as definitions are registered and never shadowed): a field reference carries its field's @@ -700,6 +723,11 @@ def Synth.resolveStmtExpr (exprMd : StmtExprMd) : ResolveM (StmtExprMd × HighTy Synth.proveBy exprMd val proof source (by rw [h_node]) | .ContractOf ty fn => Synth.contractOf exprMd ty fn source (by rw [h_node]) + | .Subscript target index update => + Synth.subscript exprMd target index update source (by rw [h_node]) + | .SubscriptWrite target index value => do + let r ← Check.subscriptWrite exprMd target index value source (by rw [h_node]) + return (r, ⟨ .TVoid, source ⟩) | .Abstract => pure (Synth.abstract source) | .All => pure (Synth.all source) | .IfThenElse cond thenBr elseBr => @@ -1638,30 +1666,51 @@ def Synth.staticCall (exprMd : StmtExprMd) (h : exprMd.val = .StaticCall callee args) : ResolveM (StmtExpr × HighTypeMd) := do - -- Hack because we use these polymorphic map primitives but Laurel does not - -- support polymorphism yet, so they cannot be type-checked against their - -- placeholder `int` signatures. Instead we resolve the arguments and infer the - -- result type structurally from them, keeping a concrete `HighType` flowing into - -- Core translation: - -- * `select(map, key)` ⇒ the map's value type - -- * `update(map, key, val)` ⇒ the map type itself - -- * `const(val)` ⇒ `Map _ (typeof val)` (key type is not recoverable) - if callee == "select" || callee == "update" || callee == "const" then + -- Polymorphic Map/Sequence/Array primitives: Laurel has no polymorphism, so + -- these can't be checked against their placeholder `int` signatures. Instead + -- we resolve the arguments and infer the result type structurally, keeping a + -- concrete `HighType` flowing into Core translation. `Seq` literals and + -- subscripts desugar into the Sequence ops (`SubscriptElim` lowers `s[i]` / + -- `s[i := v]` to `Sequence.select` / `Sequence.update`), so they ride the + -- same path. + -- + -- `primInfer?` names each op exactly once: it maps the callee to the function + -- that computes the result type from the (resolved) argument types, or `none` + -- for a non-primitive callee. The `some`/`none` doubles as the "is this a + -- prim?" test — keyed on `callee.text` alone, so it's decided before args are + -- resolved (a non-prim must take the normal checking path below, not be + -- re-resolved here) and there's no separate, drift-prone list of prim names. + let unknown : HighTypeMd := ⟨ .Unknown, source ⟩ + let ctx := (← get).typeLattice + let elemOf (ty : HighTypeMd) : HighTypeMd := + match (ctx.unfold ty).val with + | .TSeq et | .TArray et => et + | _ => unknown + let primInfer? : Option (List HighTypeMd → HighTypeMd) := + let arg0 (argTys : List HighTypeMd) := argTys.headD unknown + match callee.text with + -- Map ops. + | "select" => some fun argTys => match (arg0 argTys).val with | .TMap _ v => v | _ => unknown + | "update" => some fun argTys => arg0 argTys + | "const" => some fun argTys => ⟨ .TMap ⟨.UserDefined "TypeTag", source⟩ (arg0 argTys), source ⟩ + -- Sequence/Array ops. `empty` (and any unmatched arg shape) is `Unknown`, + -- a top-level wildcard so `[]` flows into any `Seq`. + | t => + if t == SeqOp.empty then some fun _ => unknown + else if t == SeqOp.build then + some fun argTys => match argTys with | _ :: v :: _ => ⟨ .TSeq v, source ⟩ | _ => unknown + else if t == SeqOp.select then some fun argTys => elemOf (arg0 argTys) + else if t == sequenceFromArrayName then some fun argTys => ⟨ .TSeq (elemOf (arg0 argTys)), source ⟩ + else if t == SeqOp.update || t == SeqOp.append + || t == SeqOp.take || t == SeqOp.drop then some fun argTys => arg0 argTys + else if t == SeqOp.length || t == arrayLengthName then some fun _ => ⟨ .TInt, source ⟩ + else if t == SeqOp.contains then some fun _ => ⟨ .TBool, source ⟩ + else none + if let some infer := primInfer? then let resolved ← args.attach.mapM (fun ⟨a, hMem⟩ => do have := hMem Synth.resolveStmtExpr a) - let args' := resolved.map (·.1) - let argTys := resolved.map (·.2) - let resultTy : HighTypeMd ← - match callee, argTys with - | "select", mapTy :: _ => - match mapTy.val with - | .TMap _ valueTy => pure valueTy - | _ => pure ⟨ .Unknown, source ⟩ - | "update", mapTy :: _ => pure mapTy - | "const", valTy :: _ => pure ⟨ .TMap ⟨.UserDefined "TypeTag", source⟩ valTy, source ⟩ - | _, _ => pure ⟨ .Unknown, source ⟩ - return (.StaticCall callee args', resultTy) + return (.StaticCall callee (resolved.map (·.1)), infer (resolved.map (·.2))) let callee' ← resolveRef callee source (expected := #[.parameter, .staticProcedure, .datatypeConstructor, .datatypeDestructor, .constant]) @@ -2190,6 +2239,85 @@ def Synth.pureFieldUpdate (exprMd : StmtExprMd) rw [h] at hsz term_by_mem +-- ### Subscript + +/-- (Subscript) + ``` + Γ ⊢ target ⇒ T Γ ⊢ i ⇐ TInt (Subscript-Read) + ──────────────────────────────────────────── + Γ ⊢ Subscript target i none ⇒ elem(T) + + Γ ⊢ target ⇒ T Γ ⊢ i ⇐ TInt Γ ⊢ v ⇐ elem(T) (Subscript-Update) + ──────────────────────────────────────────── + Γ ⊢ Subscript target i (some v) ⇒ T + ``` + `s[i]` reads element `elem(T)`; `s[i := v]` is a *functional* update that + yields a new collection of the same type `T` (it does not mutate `target`). + Both are values. The index is checked against `TInt` and the update value + against the element type (so `s[0 := "x"]` on a `Seq` is rejected). The + element type and indexability are decided by `checkSubscriptTarget`: a + `Seq`/`Array` gives its element type; a concrete non-collection is rejected + (`expected a sequence or array`); a gradual `Unknown`/`TCore` target yields + `Unknown`, making the index/value checks vacuous. The Seq-vs-Array-misuse + rules (functional update is only valid on `Seq`) are left to the separate + `ValidateSubscriptUsage` pass. -/ +def Synth.subscript (exprMd : StmtExprMd) + (target index : StmtExprMd) (update : Option StmtExprMd) (source : Option FileRange) + (h : exprMd.val = .Subscript target index update) : + ResolveM (StmtExpr × HighTypeMd) := do + let (target', targetTy) ← Synth.resolveStmtExpr target + let ctx := (← get).typeLattice + let elemTy ← checkSubscriptTarget ctx (.Subscript target' index update) targetTy source + let index' ← Check.resolveStmtExpr index { val := .TInt, source := index.source } + let update' ← update.attach.mapM (fun a => have := a.property; + Check.resolveStmtExpr a.val elemTy) + let resultTy := match update' with + | none => elemTy + | some _ => targetTy + pure (.Subscript target' index' update', resultTy) + termination_by (exprMd, 1) + decreasing_by + all_goals + apply Prod.Lex.left + have hsz := exprMd.sizeOf_val_lt + rw [h] at hsz + simp only [StmtExpr.Subscript.sizeOf_spec] at hsz + try (rw [Option.mem_def.mp ‹_ ∈ update›, Option.some.sizeOf_spec] at hsz) + omega + +/-- (SubscriptWrite) + ``` + Γ ⊢ target ⇒ T Γ ⊢ i ⇐ TInt Γ ⊢ v ⇐ elem(T) + ────────────────────────────────────────────── + Γ ⊢ SubscriptWrite target i v ⇒ TVoid + ``` + `a[i] := v` is a destructive in-place write on a mutable `Array`, a + statement. The index is checked against `TInt` and the value against the + element type (so `a[0] := true` on an `Array` is rejected). As in + `Synth.subscript`, `checkSubscriptTarget` supplies the element type and + rejects a concrete non-collection target, while a gradual `Unknown`/`TCore` + target makes the value check vacuous. The Seq-vs-Array-misuse rule + (destructive update is only valid on `Array`, not `Seq`) is left to + `ValidateSubscriptUsage`. It yields no value, so it synthesizes `TVoid`. -/ +def Check.subscriptWrite (exprMd : StmtExprMd) + (target index value : StmtExprMd) (source : Option FileRange) + (h : exprMd.val = .SubscriptWrite target index value) : + ResolveM StmtExprMd := do + let (target', targetTy) ← Synth.resolveStmtExpr target + let ctx := (← get).typeLattice + let elemTy ← checkSubscriptTarget ctx (.SubscriptWrite target' index value) targetTy source + let index' ← Check.resolveStmtExpr index { val := .TInt, source := index.source } + let value' ← Check.resolveStmtExpr value elemTy + pure { val := .SubscriptWrite target' index' value', source := source } + termination_by (exprMd, 0) + decreasing_by + all_goals + apply Prod.Lex.left + have hsz := exprMd.sizeOf_val_lt + rw [h] at hsz + simp only [StmtExpr.SubscriptWrite.sizeOf_spec] at hsz + omega + -- ### Verification expressions /-- (Quantifier) @@ -2789,6 +2917,8 @@ private def collectHighType (map : Std.HashMap Nat ResolvedNode) (ty : HighTypeM | .TMap kt vt => let map := collectHighType map kt collectHighType map vt + | .TSeq et => collectHighType map et + | .TArray et => collectHighType map et | .Applied base args => let map := collectHighType map base args.foldl collectHighType map @@ -2861,6 +2991,16 @@ private def collectStmtExpr (map : Std.HashMap Nat ResolvedNode) (expr : StmtExp let map := collectStmtExpr map val collectStmtExpr map proof | .ContractOf _ fn => collectStmtExpr map fn + | .Subscript target index update => + let map := collectStmtExpr map target + let map := collectStmtExpr map index + match update with + | some u => collectStmtExpr map u + | none => map + | .SubscriptWrite target index value => + let map := collectStmtExpr map target + let map := collectStmtExpr map index + collectStmtExpr map value | .New _ | .This | .Exit _ | .LiteralInt _ | .LiteralBool _ | .LiteralString _ | .LiteralDecimal _ | .LiteralBv _ _ | .Abstract | .All | .Hole _ _ => map @@ -3113,6 +3253,164 @@ private def preRegisterTopLevel (program : Program) : ResolveM Unit := do for proc in program.staticProcedures do let _ ← defineNameCheckDup proc.name (.staticProcedure proc) +/-! ## Subscript usage validation + +Reports misuses of `Seq` and `Array` that would otherwise surface as +confusing downstream errors. Run from `resolve` (below), alongside +`validateDiamondFieldAccesses`, so that — like every other non-verification +diagnostic — these are produced by resolution rather than a separate pipeline +pass. The diagnostics are: + +1. `a[i := v]` on `Array` — arrays are mutable; functional update is only + valid for sequences. +2. `s[i] := v` on `Seq` — sequences are immutable; destructive update is + only valid for arrays. +3. `Array.length(x)` where `x` is not an `Array`. +4. `Array` where `T ≠ int` (not yet implemented at the Laurel layer). +5. `Sequence.fromArray(x)` where `x` is not an `Array`. +-/ + +private def fmtSubscriptType (t : HighType) : String := (Std.format t).pretty + +/-- Message wording. Substrings of these strings appear in the + `// ^^^ error: ...` annotations of the Seq/Array example tests; + update both sides together if you reword. -/ +private def msgArrayFuncUpdate : String := + "`a[i := v]` is not supported on `Array`: arrays are mutable. " ++ + "Use `a[i] := v` to update in place, or declare `a` as `Seq` to use `s[i := v]`." + +private def msgSeqDestructiveUpdate : String := + "`s[i] := v` is not allowed: sequences (`Seq`) are immutable. " ++ + "Use `s[i := v]` to produce a new sequence with index `i` set to `v`, " ++ + "or declare `s` as `Array` to update in place." + +private def msgArrayLengthArg (actual : String) : String := + s!"`Array.length` requires an argument of type `Array`, got `{actual}`." + +private def msgSequenceFromArrayArg (actual : String) : String := + s!"`Sequence.fromArray` requires an argument of type `Array`, got `{actual}`." + +private def msgArrayElementNotInt (actual : String) : String := + s!"`Array` is currently only supported for `T = int`. " ++ + s!"Support for other element types is not yet implemented. Found: `Array<{actual}>`." + +private def msgArrayLengthArity (got : Nat) : String := + s!"`Array.length` takes exactly one argument of type `Array`, got {got}." + +private def msgSequenceFromArrayArity (got : Nat) : String := + s!"`Sequence.fromArray` takes exactly one argument of type `Array`, got {got}." + +/-- Collect diagnostics for any `Array` whose element type is not `int`. + + Each constructor has its own arm so adding a new `HighType` variant produces + a missing-cases error. `Unknown` and `MultiValuedExpr` are explicit no-op + arms (they cannot carry user-declared types that need validating). -/ +def validateHighType (ty : HighTypeMd) : List DiagnosticModel := + match _hht : ty.val with + | .TArray et => + let here : List DiagnosticModel := + match et.val with + | .TInt => [] + | other => + [diagnosticFromSource ty.source (msgArrayElementNotInt (fmtSubscriptType other))] + -- Recurse into the element type — rare but a nested `Array>` + -- should still complain about the outer not being int. + here ++ validateHighType et + | .TSet et => validateHighType et + | .TSeq et => validateHighType et + | .TMap kt vt => validateHighType kt ++ validateHighType vt + | .Applied base args => + validateHighType base ++ args.flatMap validateHighType + | .Pure base => validateHighType base + | .Intersection tys => tys.flatMap validateHighType + | .Unknown | .MultiValuedExpr _ => [] + | .TVoid | .TBool | .TInt | .TFloat64 | .TReal | .TString + | .TBv _ | .UserDefined _ | .TCore _ => [] +termination_by sizeOf ty +decreasing_by + all_goals simp_wf + all_goals (try term_by_mem) + -- Single-child recursion (TArray/TSet/TSeq/TMap/Applied-base/Pure). + all_goals (try term_by_val ty, _hht) + -- List-member recursion (Applied args / Intersection types): also chain + -- through `List.sizeOf_lt_of_mem`. + all_goals (have := List.sizeOf_lt_of_mem ‹_›; term_by_val ty, _hht) + +/-- Diagnostics for a *single* `StmtExpr` node — the Subscript/SubscriptWrite + misuse and `Array.length`/`Sequence.fromArray` argument/arity checks. Only + the constructors this validator is actually about are named; recursion into + children, and into the type-carrying constructors, is handled by the generic + `MapStmtExpr` traversals in `validateSubscriptUsage`, so a new unrelated + `StmtExpr` constructor needs no change here. -/ +private def validateSubscriptNode (model : SemanticModel) (expr : StmtExprMd) : List DiagnosticModel := + match expr.val with + -- Diagnostic 1: functional update `a[i := v]` on Array (not supported). + | .Subscript target _ (some _) => + if (computeExprType model target).val.isArray then + [diagnosticFromSource expr.source msgArrayFuncUpdate] + else [] + -- Diagnostic 2: destructive write `s[i] := v` on Seq (immutable). + | .SubscriptWrite target _ _ => + if (computeExprType model target).val.isSeq then + [diagnosticFromSource expr.source msgSeqDestructiveUpdate] + else [] + -- Diagnostics 3 and 5: Array.length(x) / Sequence.fromArray(x) with x not Array. + | .StaticCall callee args => + if callee.text == arrayLengthName then + match args with + | [a] => + let actualTy := (computeExprType model a).val + if actualTy.isArray then [] + else [diagnosticFromSource expr.source (msgArrayLengthArg (fmtSubscriptType actualTy))] + | _ => [diagnosticFromSource expr.source (msgArrayLengthArity args.length)] + else if callee.text == sequenceFromArrayName then + match args with + | [a] => + let actualTy := (computeExprType model a).val + if actualTy.isArray then [] + else [diagnosticFromSource expr.source (msgSequenceFromArrayArg (fmtSubscriptType actualTy))] + | _ => [diagnosticFromSource expr.source (msgSequenceFromArrayArity args.length)] + else [] + | _ => [] + +/-- Run the Subscript/Array-length usage validator on the whole program. + + Two generic collects over `MapStmtExpr`, rather than a hand-written walker + that enumerates every `StmtExpr`/`HighType` constructor: + + * `validateHighType` is driven over *every* embedded type annotation by + `mapProgramHighTypesM` (the single source of truth for "where types live"). + * `validateSubscriptNode` is driven over *every* expression node by + `mapStmtExprM`. Only the program-level expr-bearing slots are named + explicitly here (procedures via `mapProcedureM`, constrained-type + constraint/witness, constant initializers) — there is no whole-program + `StmtExpr` collect — but no `StmtExpr`/`HighType` *constructor* is + enumerated, so a new unrelated one needs no change. + + Collects only: both hooks return their argument unchanged, so + `computeExprType` still sees the original (un-rewritten) children and the + program is left untouched. -/ +def validateSubscriptUsage (model : SemanticModel) (program : Program) : List DiagnosticModel := + let M := StateM (Array DiagnosticModel) + -- Visit every node of one expression, collecting node-level diagnostics. + let collectExpr (e : StmtExprMd) : M PUnit := do + let _ ← mapStmtExprM (m := M) (fun n => do + modify (· ++ (validateSubscriptNode model n).toArray); pure n) e + let run : M PUnit := do + -- Expression positions, program-wide: procedure bodies/pre/decreases/invokeOn, + -- constant initializers, and constrained-type constraint/witness. + let _ ← mapProgramProceduresM (mapProcedureM (m := M) (fun e => do collectExpr e; pure e)) program + for c in program.constants do + match c.initializer with | some i => collectExpr i | none => pure () + for td in program.types do + match td with + | .Constrained ct => collectExpr ct.constraint; collectExpr ct.witness + | _ => pure () + -- Type positions, program-wide. + let _ ← mapProgramHighTypesM (m := M) (fun t => do + modify (· ++ (validateHighType t).toArray); pure t) program + (run.run #[]).2.toList + /-! ## Entry point -/ /-- Run the full resolution pass on a Laurel program. -/ @@ -3137,9 +3435,10 @@ public def resolve (program : Program) (existingModel: Option SemanticModel := n nextId := finalState.nextId } let diamondErrors := validateDiamondFieldAccesses semanticModel program' + let subscriptErrors := validateSubscriptUsage semanticModel program' { program := program', model := semanticModel, - errors := finalState.errors ++ diamondErrors + errors := finalState.errors ++ diamondErrors ++ subscriptErrors } /-! ## Resolution for UnorderedCoreWithLaurelTypes -/ diff --git a/Strata/Languages/Laurel/SubscriptElim.lean b/Strata/Languages/Laurel/SubscriptElim.lean new file mode 100644 index 0000000000..0111fc7a59 --- /dev/null +++ b/Strata/Languages/Laurel/SubscriptElim.lean @@ -0,0 +1,449 @@ +/- + Copyright Strata Contributors + + SPDX-License-Identifier: Apache-2.0 OR MIT +-/ +module + +public import Strata.Languages.Laurel.Resolution +public import Strata.Languages.Laurel.LaurelTypes +public import Strata.Languages.Laurel.LaurelPass +public import Strata.Languages.Laurel.SubscriptElimConstants +import Strata.Util.Tactics + +/-! +# Subscript Elimination + +Type-aware pass that desugars `Subscript` nodes based on the target type: + +- `Seq` (immutable): read `s[i]` → `Sequence.select(s, i)`; + functional update `s[i := v]` → `Sequence.update(s, i, v)`. +- `Array` (mutable, heap-backed): read `a[i]` → `Sequence.select(a#$data, i)`; + destructive update `a[i] := v` → `a#$data := Sequence.update(a#$data, i, v)`. + +Also: +- Rewrites `Array.length(a)` to `Sequence.length(a#$data)`. +- Rewrites `Sequence.fromArray(a)` to `a#$data` (a snapshot read of + the array's current Seq contents). +- Splits `var a: Array := ` (where `init` is a `Seq` literal, not + another Array) into `var a: Array := new $Array; a#$data := `. +- Conditionally injects the synthetic `$Array` composite (containing a single + `$data: Seq` field) when the program uses `Array` anywhere. + +After this pass, no `Subscript` nodes remain in the program. + +Out-of-bounds access produces a proof obligation at the call site: +the Core-level bounds preconditions on `Sequence.select` / `update` / `take` / +`drop` propagate through `PrecondElim`, and the verification backend is +responsible for discharging them. +-/ + +namespace Strata.Laurel + +open Strata + +public section + +/-! ## Detecting whether `Array` is used anywhere -/ + +/-- Return `true` if `ty` contains a `TArray` anywhere. + + Each `HighType` constructor gets its own arm so that adding a new + constructor produces a missing-cases error rather than silently + falling through. `Unknown` and `MultiValuedExpr` are explicitly + `false`: the former is an unresolved-type marker that aborts + compilation before we'd care whether it contains a TArray, and the + latter is an internal-only computeExprType output that never carries + user-declared types. -/ +def containsTArray (ty : HighTypeMd) : Bool := match _hht : ty.val with + | .TArray _ => true + | .TSet et => containsTArray et + | .TSeq et => containsTArray et + | .TMap kt vt => containsTArray kt || containsTArray vt + | .Applied base args => containsTArray base || args.attach.any (fun ⟨x, _⟩ => containsTArray x) + | .Pure base => containsTArray base + | .Intersection types => types.attach.any (fun ⟨x, _⟩ => containsTArray x) + | .Unknown | .MultiValuedExpr _ => false + | .TVoid | .TBool | .TInt | .TFloat64 | .TReal | .TString + | .TBv _ | .UserDefined _ | .TCore _ => false +termination_by sizeOf ty +decreasing_by + all_goals simp_wf + -- Single-child recursion on an `AstNode HighType` field. + all_goals (try term_by_val ty, _hht) + -- List-member recursion (Applied args / Intersection types). + all_goals (have := List.sizeOf_lt_of_mem ‹_›; term_by_val ty, _hht) + +/-- Walk a `StmtExprMd` and return `true` if any embedded `HighType` contains `TArray`. -/ +def stmtExprUsesTArray (expr : StmtExprMd) : Bool := + match _h : expr.val with + | .Var (.Declare p) => containsTArray p.type + | .Var (.Field t _) => stmtExprUsesTArray t + | .Var (.Local _) => false + | .Quantifier _ p trig body => + containsTArray p.type || + (trig.attach.any (fun ⟨x, _⟩ => stmtExprUsesTArray x)) || + stmtExprUsesTArray body + | .AsType t ty => stmtExprUsesTArray t || containsTArray ty + | .IsType t ty => stmtExprUsesTArray t || containsTArray ty + | .Hole _ (some ty) => containsTArray ty + | .IfThenElse c th el => + stmtExprUsesTArray c || stmtExprUsesTArray th || + (el.attach.any (fun ⟨x, _⟩ => stmtExprUsesTArray x)) + | .Block stmts _ => stmts.attach.any (fun ⟨x, _⟩ => stmtExprUsesTArray x) + | .While c invs dec body _ => + stmtExprUsesTArray c || + invs.attach.any (fun ⟨x, _⟩ => stmtExprUsesTArray x) || + (dec.attach.any (fun ⟨x, _⟩ => stmtExprUsesTArray x)) || + stmtExprUsesTArray body + | .Return v => v.attach.any (fun ⟨x, _⟩ => stmtExprUsesTArray x) + | .Assign targets v => + targets.attach.any (fun ⟨t, _⟩ => match _htv : t.val with + | .Declare p => containsTArray p.type + | .Field target _ => stmtExprUsesTArray target + | .Local _ => false) + || stmtExprUsesTArray v + | .PureFieldUpdate t _ v => stmtExprUsesTArray t || stmtExprUsesTArray v + | .StaticCall _ args => args.attach.any (fun ⟨x, _⟩ => stmtExprUsesTArray x) + | .InstanceCall t _ args => + stmtExprUsesTArray t || args.attach.any (fun ⟨x, _⟩ => stmtExprUsesTArray x) + | .PrimitiveOp _ args => args.attach.any (fun ⟨x, _⟩ => stmtExprUsesTArray x) + | .ReferenceEquals l r => stmtExprUsesTArray l || stmtExprUsesTArray r + | .Assigned n => stmtExprUsesTArray n + | .Old v | .Fresh v => stmtExprUsesTArray v + | .Assert c => stmtExprUsesTArray c.condition + | .Assume c => stmtExprUsesTArray c + | .ProveBy v p => stmtExprUsesTArray v || stmtExprUsesTArray p + | .ContractOf _ f => stmtExprUsesTArray f + | .Subscript t i u => + stmtExprUsesTArray t || stmtExprUsesTArray i || + (u.attach.any (fun ⟨x, _⟩ => stmtExprUsesTArray x)) + | _ => false +termination_by sizeOf expr +decreasing_by + all_goals simp_wf + all_goals (try have := AstNode.sizeOf_val_lt expr) + all_goals (try have := Condition.sizeOf_condition_lt ‹_›) + all_goals (try term_by_mem) + -- Assign-target list, .Field inner + all_goals (try ( + have := List.sizeOf_lt_of_mem ‹_› + have := Variable.sizeOf_field_target_lt_of_eq _htv + simp_all; omega)) + -- Top-level .Subscript (target/index/value children). + all_goals (try term_by_val expr, _h) + +/-- Check whether a parameter's type involves `TArray`. -/ +private def parameterUsesTArray (p : Parameter) : Bool := containsTArray p.type + +/-- Check whether a procedure body involves `TArray`. -/ +private def bodyUsesTArray (body : Body) : Bool := + match body with + | .Transparent b => stmtExprUsesTArray b + | .Opaque posts impl mods => + posts.any (stmtExprUsesTArray ·.condition) || + (impl.map stmtExprUsesTArray).getD false || + mods.any stmtExprUsesTArray + | .Abstract posts => posts.any (stmtExprUsesTArray ·.condition) + | .External => false + +/-- Check whether a procedure involves `TArray` in signature, contracts, or body. -/ +private def procedureUsesTArray (proc : Procedure) : Bool := + proc.inputs.any parameterUsesTArray || + proc.outputs.any parameterUsesTArray || + proc.preconditions.any (stmtExprUsesTArray ·.condition) || + (proc.decreases.map stmtExprUsesTArray).getD false || + bodyUsesTArray proc.body + +/-- Check whether a type definition involves `TArray` in its fields or methods. -/ +private def typeDefinitionUsesTArray (td : TypeDefinition) : Bool := + match td with + | .Composite ct => + ct.fields.any (fun f => containsTArray f.type) || + ct.instanceProcedures.any procedureUsesTArray + | .Constrained ct => + containsTArray ct.base || stmtExprUsesTArray ct.constraint || + stmtExprUsesTArray ct.witness + | .Datatype dt => + dt.constructors.any fun c => c.args.any parameterUsesTArray + | .Alias ta => containsTArray ta.target + +/-- Return `true` if the program uses `Array` anywhere. -/ +def usesTArray (program : Program) : Bool := + program.staticProcedures.any procedureUsesTArray || + program.staticFields.any (fun f => containsTArray f.type) || + program.types.any typeDefinitionUsesTArray || + program.constants.any fun c => + containsTArray c.type || (c.initializer.map stmtExprUsesTArray).getD false + +/-! ## Rewrite helpers -/ + +private def mkCall (name : String) (args : List StmtExprMd) (src : Option FileRange) : StmtExprMd := + ⟨.StaticCall (mkId name) args, src⟩ + +/-- Build a `Variable.Field` read as a StmtExpr (expression position). -/ +private def mkFieldExpr (target : StmtExprMd) (field : String) (src : Option FileRange) : StmtExprMd := + ⟨.Var (.Field target (mkId field)), src⟩ + +/-- Build a `Variable.Field` as an Assign target (target position). -/ +private def mkFieldVariable (target : StmtExprMd) (field : String) (src : Option FileRange) : VariableMd := + ⟨.Field target (mkId field), src⟩ + +/-- Is the expression's computed type an `Array`? -/ +private def isArrayType (model : SemanticModel) (target : StmtExprMd) : Bool := + (computeExprType model target).val.isArray + +/-- Build the destructive-update statement for `a[i] := v` on an `Array`: + `a#$data := Sequence.update(a#$data, i, v)`. + + The arguments are *already-rewritten* children so this helper does not + recurse — it simply constructs the result shape used by `elimExpr`'s + `.SubscriptWrite` arm. -/ +private def mkArrayUpdateStmt (target' index' value' : StmtExprMd) + (src : Option FileRange) : StmtExprMd := + let data := mkFieldExpr target' arrayDataField src + ⟨.Assign [mkFieldVariable target' arrayDataField src] + (mkCall SeqOp.update [data, index', value'] src), src⟩ + +/-- Build the two-statement split for `var a: Array := ` where + `init` is a non-Array (i.e. needs the synthetic `$Array` allocation): + `var a: Array := new $Array; a#$data := `. + + The arguments are *already-rewritten* (`initExpr'` is the rewritten + initialiser); this helper does not recurse. Used by `splitArrayInit`. -/ +private def mkArrayInitSplit (param : Parameter) (dsrc : Option FileRange) + (initExpr' : StmtExprMd) (src : Option FileRange) : List StmtExprMd := + [⟨.Assign [⟨.Declare param, dsrc⟩] ⟨.New (mkId arrayCompositeName), src⟩, src⟩, + ⟨.Assign [mkFieldVariable ⟨.Var (.Local param.name), src⟩ arrayDataField src] + initExpr', src⟩] + +/-- Collapse a list of statements into a single `StmtExprMd`, wrapping + multi-statement results in `.Block`. Singleton results pass through + unchanged. Used at non-Block container sites (If/While branches) + where the surrounding AST expects exactly one `StmtExprMd`. -/ +private def collapseStmts (stmts : List StmtExprMd) (src : Option FileRange) : StmtExprMd := + match stmts with + | [s] => s + | _ => ⟨.Block stmts none, src⟩ + +/-! ## Main rewrite + +`elimExpr` is a structural top-down rewrite. The one place a single statement +expands 1→N is `var a: Array := ` (allocate `$Array`, then store): +`splitArrayInit` applies that split as a non-recursive post-pass over +`elimExpr`'s output at the four statement-position container arms (`.Block`, +`.IfThenElse` then/else, `.While` body). Keeping the split out of `elimExpr` +itself lets `elimExpr` stay a plain (non-mutual) structural recursion. +-/ + +/-- Apply the Array-init 1→N split to an already-`elimExpr`'d statement. + `var a: Array := ` becomes `var a := new $Array; a#$data := `; + every other statement passes through unchanged. Non-recursive: it inspects + `s` but does not recurse, so callers run `elimExpr` first. -/ +private def splitArrayInit (model : SemanticModel) (s : StmtExprMd) : List StmtExprMd := + match s.val with + | .Assign [⟨.Declare param, dsrc⟩] initExpr => + if param.type.val.isArray && !isArrayType model initExpr then + mkArrayInitSplit param dsrc initExpr s.source + else [s] + | _ => [s] + +/-- Recursively eliminate Subscript nodes and desugar `Array.length`. -/ +def elimExpr (model : SemanticModel) (expr : StmtExprMd) : StmtExprMd := + let src := expr.source + match _h : expr.val with + | .Subscript target index none => + let target' := elimExpr model target + let index' := elimExpr model index + if isArrayType model target then + mkCall SeqOp.select [mkFieldExpr target' arrayDataField src, index'] src + else + mkCall SeqOp.select [target', index'] src + | .Subscript target index (some value) => + -- Functional update `s[i := v]` (a value). Desugars to Sequence.update. + let target' := elimExpr model target + let index' := elimExpr model index + let value' := elimExpr model value + if isArrayType model target then + -- `a[i := v]` on Array: not supported (the `ValidateSubscriptUsage` + -- pass has already surfaced a diagnostic for this misuse). + -- Desugar the read-side to keep downstream typecheck simple. + let data := mkFieldExpr target' arrayDataField src + mkCall SeqOp.update [data, index', value'] src + else + mkCall SeqOp.update [target', index', value'] src + | .SubscriptWrite target index value => + if isArrayType model target then + -- `a[i] := v` on Array: `a#$data := Sequence.update(a#$data, i, v)`. + mkArrayUpdateStmt (elimExpr model target) (elimExpr model index) + (elimExpr model value) src + else + -- Seq: user error. COUPLING: `ValidateSubscriptUsage` MUST have + -- reported `msgSeqDestructiveUpdate` first (translation halts before + -- Core). Emit an empty block rather than a `$data` access that a Seq + -- target does not have. + ⟨.Block [] none, src⟩ + | .Block stmts label => + ⟨.Block (stmts.attach.flatMap fun ⟨s, _⟩ => splitArrayInit model (elimExpr model s)) label, src⟩ + | .Assign targets value => + -- Assign targets are VariableMd; we only need to recurse into .Field sub-expressions. + let targets' := targets.attach.map fun ⟨t, _⟩ => match _htv : t.val with + | .Field subTarget fieldName => (⟨.Field (elimExpr model subTarget) fieldName, t.source⟩ : VariableMd) + | .Local _ | .Declare _ => t + ⟨.Assign targets' (elimExpr model value), src⟩ + | .StaticCall callee args => + let args' := args.attach.map fun ⟨a, _⟩ => elimExpr model a + -- `Array.length(a)` → `Sequence.length(a#$data)` — only when `a` is an Array. + -- When the argument is not an Array (a user error caught by the validator), + -- replace the call with `0` so downstream Core type checking doesn't emit + -- confusing unification errors on top of the validator's helpful message. + if callee.text == arrayLengthName then + match args' with + | [a] => + if isArrayType model a then + mkCall SeqOp.length [mkFieldExpr a arrayDataField src] src + else + ⟨.LiteralInt 0, src⟩ + | _ => + -- Wrong arity — leave alone (validator/resolver will flag). + ⟨.StaticCall callee args', src⟩ + else if callee.text == sequenceFromArrayName then + -- `Sequence.fromArray(a)` → `a#$data` — only when `a` is an Array. + -- When the argument is not an Array the validator has flagged it; we + -- rewrite defensively to `Sequence.empty()` so Core type checking + -- does not add confusing follow-on errors. + match args' with + | [a] => + if isArrayType model a then + mkFieldExpr a arrayDataField src + else + mkCall SeqOp.empty [] src + | _ => + ⟨.StaticCall callee args', src⟩ + else + ⟨.StaticCall callee args', src⟩ + | .IfThenElse c t e => + let t' := collapseStmts (splitArrayInit model (elimExpr model t)) t.source + let e' := e.attach.map fun ⟨y, _⟩ => collapseStmts (splitArrayInit model (elimExpr model y)) y.source + ⟨.IfThenElse (elimExpr model c) t' e', src⟩ + | .While c invs dec body postTest => + let body' := collapseStmts (splitArrayInit model (elimExpr model body)) body.source + ⟨.While (elimExpr model c) (invs.attach.map fun ⟨i, _⟩ => elimExpr model i) + (dec.attach.map fun ⟨d, _⟩ => elimExpr model d) body' postTest, src⟩ + | .Return v => ⟨.Return (v.attach.map fun ⟨x, _⟩ => elimExpr model x), src⟩ + | .PrimitiveOp op args skipProof => + ⟨.PrimitiveOp op (args.attach.map fun ⟨a, _⟩ => elimExpr model a) skipProof, src⟩ + | .Quantifier mode p trig body => + ⟨.Quantifier mode p (trig.attach.map fun ⟨t, _⟩ => elimExpr model t) (elimExpr model body), src⟩ + | .Assert c => ⟨.Assert { c with condition := elimExpr model c.condition }, src⟩ + | .Assume c => ⟨.Assume (elimExpr model c), src⟩ + | .Old v => ⟨.Old (elimExpr model v), src⟩ + | .Fresh v => ⟨.Fresh (elimExpr model v), src⟩ + | .Assigned v => ⟨.Assigned (elimExpr model v), src⟩ + | .ProveBy v p => ⟨.ProveBy (elimExpr model v) (elimExpr model p), src⟩ + | .ReferenceEquals l r => ⟨.ReferenceEquals (elimExpr model l) (elimExpr model r), src⟩ + | .InstanceCall t c args => + ⟨.InstanceCall (elimExpr model t) c (args.attach.map fun ⟨a, _⟩ => elimExpr model a), src⟩ + | .Var (.Field t f) => ⟨.Var (.Field (elimExpr model t) f), src⟩ + | .IncrDecr mode op ⟨.Field t f, vs⟩ => + ⟨.IncrDecr mode op ⟨.Field (elimExpr model t) f, vs⟩, src⟩ + | .IncrDecr _ _ ⟨.Local _, _⟩ | .IncrDecr _ _ ⟨.Declare _, _⟩ => expr + | .PureFieldUpdate t f v => ⟨.PureFieldUpdate (elimExpr model t) f (elimExpr model v), src⟩ + | .AsType t ty => ⟨.AsType (elimExpr model t) ty, src⟩ + | .IsType t ty => ⟨.IsType (elimExpr model t) ty, src⟩ + | .ContractOf ty fn => ⟨.ContractOf ty (elimExpr model fn), src⟩ + -- Leaves: no StmtExprMd children that need eliminating. + -- ⚠ If a new StmtExpr constructor with StmtExprMd children is added, + -- it must get its own arm above; otherwise this walker will silently + -- skip recursion into those children. + | .Exit _ | .LiteralInt _ | .LiteralBool _ | .LiteralString _ | .LiteralDecimal _ | .LiteralBv _ _ + | .Var (.Local _) | .Var (.Declare _) | .New _ | .This | .Abstract | .All | .Hole .. => expr +termination_by sizeOf expr +decreasing_by + all_goals simp_wf + all_goals (try have := AstNode.sizeOf_val_lt expr) + all_goals (try have := Condition.sizeOf_condition_lt ‹_›) + all_goals (try term_by_mem) + -- For subTarget inside .Assign target list .Field — uses the match + -- hypothesis _htv : t.val = Variable.Field ... + all_goals (try ( + have := List.sizeOf_lt_of_mem ‹_› + have := Variable.sizeOf_field_target_lt_of_eq _htv + simp_all; omega)) + -- For target/index/value inside .Subscript at the top level (expression + -- position). + all_goals (try term_by_val expr, _h) + +private def elimBody (model : SemanticModel) (body : Body) : Body := + match body with + | .Transparent b => .Transparent (elimExpr model b) + | .Opaque posts impl mods => + .Opaque (posts.map (·.mapCondition (elimExpr model))) + (impl.map (elimExpr model)) (mods.map (elimExpr model)) + | .Abstract posts => .Abstract (posts.map (·.mapCondition (elimExpr model))) + | .External => .External + +private def elimProcedure (model : SemanticModel) (proc : Procedure) : Procedure := + { proc with + preconditions := proc.preconditions.map (·.mapCondition (elimExpr model)) + body := elimBody model proc.body + decreases := proc.decreases.map (elimExpr model) + invokeOn := proc.invokeOn.map (elimExpr model) } + +/-- The synthetic `$Array` composite. Defined in Laurel source in + `SubscriptElimConstants` (see `arrayComposite`) rather than built as a Lean + AST value, so the declaration reads as ordinary Laurel. -/ +private def arrayCompositeDef : TypeDefinition := arrayComposite + +/-- Eliminate `Subscript` nodes and desugar `Array.length` across a program. + Conditionally injects the `$Array` synthetic composite when the program + uses `Array` anywhere. + + The `_model` parameter is accepted to satisfy `LaurelPass.run`'s + `Program → SemanticModel → ...` signature but is intentionally unused: + the caller's model predates our `$Array` injection, and `elimProcedure`'s + `computeExprType` queries need a model that includes the synthetic + composite's `$data` field. We therefore rebuild the model via `resolve` + below. The pipeline's `needsResolves := true` flag re-resolves after + this pass for all downstream consumers. -/ +public def subscriptElim (_model : SemanticModel) (program : Program) + : Program × List DiagnosticModel := + -- Inject the `$Array` composite only when the program actually uses + -- `Array`. This guard is load-bearing, not just tidiness: the synthetic + -- composite's elaboration consumes fresh type-variable ids, which perturbs + -- the elaboration of *every* program (e.g. the `$__tyNN` numbering in Core + -- type errors) if injected unconditionally. Gating on `usesTArray` keeps + -- array-free programs byte-identical to their feature-absent output. + let program := + if usesTArray program then + { program with types := arrayCompositeDef :: program.types } + else program + -- Build a fresh resolution model so that `computeExprType` sees the injected + -- `$Array` composite. The pipeline's `needsResolves := true` flag will take + -- care of re-resolving after this pass; but we need the local type lookups + -- below to already see the new type. We rely on the caller to run `resolve` + -- again afterwards (driven by `LaurelPass.needsResolves`). + let model := (resolve program).model + let types' := program.types.map fun td => + match td with + | .Composite ct => + .Composite { ct with instanceProcedures := ct.instanceProcedures.map (elimProcedure model) } + | other => other + let program' := { program with + types := types' + staticProcedures := program.staticProcedures.map (elimProcedure model) + constants := program.constants.map fun c => + { c with initializer := c.initializer.map (elimExpr model) } } + (program', []) + +/-- Pipeline pass: subscript elimination. -/ +public def subscriptElimPass : LoweringPass where + name := "SubscriptElim" + documentation := "Lowers `Seq`/`Array` subscript reads and writes into the underlying map/composite operations. Injects the synthetic `$Array` composite (only when the program uses `Array`) and rewrites subscript expressions in procedures, composite instance procedures, and constant initializers." + needsResolves := true + run := fun _ p m => + let (p', diags) := subscriptElim m p + (p', diags, {}) + +end -- public section +end Strata.Laurel diff --git a/Strata/Languages/Laurel/SubscriptElimConstants.lean b/Strata/Languages/Laurel/SubscriptElimConstants.lean new file mode 100644 index 0000000000..4ddd4604e5 --- /dev/null +++ b/Strata/Languages/Laurel/SubscriptElimConstants.lean @@ -0,0 +1,84 @@ +/- + Copyright Strata Contributors + + SPDX-License-Identifier: Apache-2.0 OR MIT +-/ +module + +public import StrataDDM.AST +public import Strata.Languages.Laurel.LaurelAST +import Strata.Languages.Laurel.Grammar.ConcreteToAbstractTreeTranslator +import Strata.Languages.Laurel.Grammar.LaurelGrammar +import StrataDDM.Integration.Lean.HashCommands -- shake: keep + +namespace Strata.Laurel + +public section + +/-- +The synthetic backing type for `Array`, expressed in Laurel source (like +`HeapParameterizationConstants`) rather than built as a Lean AST value, so the +definition reads as ordinary Laurel. + +`SubscriptElim`/`ArrayElim` injects this composite into a program (when +`Array` is used) and lowers array operations onto its single mutable `$data` +field: `a[i]` → `Sequence.select(a#$data, i)`, +`a[i] := v` → `a#$data := Sequence.update(...)`, +`Array.length(a)` → `Sequence.length(a#$data)`. + +The composite name and field name must match `arrayCompositeName` and +`arrayDataField` (the constants the rest of the pass uses to read/write the +field); the `initialize` check below enforces this at module-load time. The +element type is hardcoded as `int`: `Array` with `T ≠ int` is rejected during +resolution, so every program reaching the pass uses only `Array`. +-/ +private def arrayCompositeDDM := +#strata +program Laurel; +composite $Array { + var $data: Seq +} +#end + +/-- The synthetic `$Array` composite, parsed from `arrayCompositeDDM`. + Mirrors `HeapParameterizationConstants.heapConstants` / `coreDefinitionsForLaurel`: + a parse failure is a bug in the source literal above, reported via `dbg_trace`. + The structural invariants (name/field/mutability matching the constants) are + checked at module load by the `initialize` block below. -/ +def arrayComposite : TypeDefinition := + match Laurel.TransM.run none (Laurel.parseProgram arrayCompositeDDM) with + | .ok program => + match program.types with + | [td] => td + | _ => dbg_trace s!"BUG: $Array prelude has unexpected type count"; default + | .error e => dbg_trace s!"BUG: $Array prelude parse error: {e}"; default + +/-- Whether `arrayComposite` is a `Composite` named `arrayCompositeName` with a + single mutable field named `arrayDataField` — the shape the pass relies on + when it reads/writes `a#$data`. Returns an error message on mismatch. -/ +private def arrayCompositeError : Option String := + match arrayComposite with + | .Composite ct => + if ct.name.text != arrayCompositeName then + some s!"composite is named '{ct.name.text}', expected '{arrayCompositeName}'" + else match ct.fields with + | [f] => + if f.name.text != arrayDataField then + some s!"field is named '{f.name.text}', expected '{arrayDataField}'" + else if !f.isMutable then + some s!"field '{arrayDataField}' must be mutable" + else none + | fs => some s!"has {fs.length} fields, expected exactly 1 ('{arrayDataField}')" + | _ => some "did not parse to a Composite" + +-- Enforce at module-load time that the `$Array` Laurel source above stays in +-- sync with the `arrayCompositeName` / `arrayDataField` constants the pass uses. +-- (`initialize` rather than `#guard`, which needs interpreter IR unavailable in +-- `module` files — same reason as `LaurelCompilationPipeline`'s ordering check.) +initialize do + if let some err := arrayCompositeError then + throw <| .userError s!"SubscriptElimConstants: synthetic $Array composite {err}" + +end -- public section + +end Strata.Laurel diff --git a/Strata/Languages/Laurel/TransparencyPass.lean b/Strata/Languages/Laurel/TransparencyPass.lean index 9ed040c98a..2a01b7606a 100644 --- a/Strata/Languages/Laurel/TransparencyPass.lean +++ b/Strata/Languages/Laurel/TransparencyPass.lean @@ -127,7 +127,15 @@ private def mkFunctionCopy (asFunctionNames : Std.HashSet String) (proc : Proced | .Transparent b => .Transparent (rewriteCallsToFunctional asFunctionNames (if hasProcedureTwin then stripAssertAssume b else b)) | .Opaque _ _ _ => if hasProcedureTwin then .Opaque [] none [] else proc.body | x => x - { proc with name := funcName, isFunctional := true, body := body } + -- The `$asFunction` twin models only the procedure's input/output relation + -- (used in the free postcondition `r == foo$asFunction(args)`); it must not + -- carry the procedure's preconditions. The procedure already checks those, so a + -- precondition on the twin would fire a *duplicate* well-formedness obligation + -- at every application. ContractPass retains a procedure's preconditions (as + -- free, for the native postcondition WF check), so without this strip the twin + -- would inherit them. Genuine functions are not twins and keep their preconditions. + let preconditions := if hasProcedureTwin then [] else proc.preconditions + { proc with name := funcName, isFunctional := true, body := body, preconditions := preconditions } /-- Append a free postcondition to a procedure's body postconditions. For Opaque and Abstract bodies, the free condition is appended to the diff --git a/Strata/Languages/Laurel/TypeAliasElim.lean b/Strata/Languages/Laurel/TypeAliasElim.lean index a3af677f35..720bc85988 100644 --- a/Strata/Languages/Laurel/TypeAliasElim.lean +++ b/Strata/Languages/Laurel/TypeAliasElim.lean @@ -40,6 +40,8 @@ partial def resolveAliasType (amap : AliasMap) (ty : HighTypeMd) | some target => resolveAliasType amap target (visited.insert name.text) | none => ty | .TSet et => { val := .TSet (resolveAliasType amap et visited), source := ty.source } + | .TSeq et => { val := .TSeq (resolveAliasType amap et visited), source := ty.source } + | .TArray et => { val := .TArray (resolveAliasType amap et visited), source := ty.source } | .TMap kt vt => { val := .TMap (resolveAliasType amap kt visited) (resolveAliasType amap vt visited), source := ty.source } | .Applied base args => diff --git a/StrataPython/StrataPythonTest/ToLaurelTest.lean b/StrataPython/StrataPythonTest/ToLaurelTest.lean index f44e423ba5..85b5ef6c04 100644 --- a/StrataPython/StrataPythonTest/ToLaurelTest.lean +++ b/StrataPython/StrataPythonTest/ToLaurelTest.lean @@ -66,6 +66,8 @@ private def fmtHighType : HighType → String | .TString => "TString" | .TSet _ => "TSet" | .TMap _ _ => "TMap" + | .TSeq _ => "TSeq" + | .TArray _ => "TArray" | .UserDefined name => s!"UserDefined({name})" | .Applied _ _ => "Applied" | .Pure _ => "Pure" diff --git a/StrataPython/StrataPythonTest/expected_laurel/test_class_methods.expected b/StrataPython/StrataPythonTest/expected_laurel/test_class_methods.expected index f0601e776e..30d29081f5 100644 --- a/StrataPython/StrataPythonTest/expected_laurel/test_class_methods.expected +++ b/StrataPython/StrataPythonTest/expected_laurel/test_class_methods.expected @@ -5,6 +5,7 @@ test_class_methods.py(34, 4): ✔️ always true if reached - get_owner should r test_class_methods.py(34, 4): ✔️ always true if reached - main_assert(564)_35 test_class_methods.py(34, 4): ✔️ always true if reached - get_balance should return 100 test_class_methods.py(34, 4): ✔️ always true if reached - (Account@set_balance requires) Type constraint of amount +test_class_methods.py(34, 4): ✔️ always true if reached - assume_main_assume(653)_38_calls_Account@set_balance$post0_0 test_class_methods.py(34, 4): ✔️ always true if reached - main_assert(678)_40 test_class_methods.py(34, 4): ✔️ always true if reached - set_balance should update balance test_class_methods.py(34, 4): ✔️ always true if reached - (Origin_test_helper_procedure_Requires)req_name_is_foo @@ -13,5 +14,8 @@ test_class_methods.py(34, 4): ✔️ always true if reached - (Origin_test_helpe test_class_methods.py(31, 4): ✔️ always true if reached - assert_name_is_foo test_class_methods.py(31, 4): ✔️ always true if reached - assert_opt_name_none_or_str test_class_methods.py(31, 4): ✔️ always true if reached - assert_opt_name_none_or_bar -DETAIL: 15 passed, 0 failed, 0 inconclusive +test_class_methods.py(34, 4): ✔️ always true if reached - assume_main_assume(773)_45_calls_test_helper_procedure$post0_0 +test_class_methods.py(34, 4): ✔️ always true if reached - assume_main_assume(773)_45_calls_test_helper_procedure$post0_1 +test_class_methods.py(34, 4): ✔️ always true if reached - assume_main_assume(773)_45_calls_test_helper_procedure$post0_2 +DETAIL: 19 passed, 0 failed, 0 inconclusive RESULT: Analysis success diff --git a/StrataPython/StrataPythonTest/expected_laurel/test_class_with_methods.expected b/StrataPython/StrataPythonTest/expected_laurel/test_class_with_methods.expected index 3f5ddaf665..bf6d2d15f8 100644 --- a/StrataPython/StrataPythonTest/expected_laurel/test_class_with_methods.expected +++ b/StrataPython/StrataPythonTest/expected_laurel/test_class_with_methods.expected @@ -1,6 +1,8 @@ test_class_with_methods.py(32, 4): ✔️ always true if reached - (DataStore@__init__ requires) Type constraint of name test_class_with_methods.py(32, 4): ✔️ always true if reached - (DataStore@add requires) Type constraint of amount +test_class_with_methods.py(32, 4): ✔️ always true if reached - assume_main_assume(447)_30_calls_DataStore@add$post0_0 test_class_with_methods.py(32, 4): ✔️ always true if reached - (DataStore@add requires) Type constraint of amount +test_class_with_methods.py(32, 4): ✔️ always true if reached - assume_main_assume(465)_32_calls_DataStore@add$post0_0 test_class_with_methods.py(32, 4): ✔️ always true if reached - main_assert(484)_34 test_class_with_methods.py(32, 4): ✔️ always true if reached - get_count should return 30 test_class_with_methods.py(32, 4): ✔️ always true if reached - main_assert(569)_37 @@ -11,5 +13,8 @@ test_class_with_methods.py(32, 4): ✔️ always true if reached - (Origin_test_ test_class_with_methods.py(29, 4): ✔️ always true if reached - assert_name_is_foo test_class_with_methods.py(29, 4): ✔️ always true if reached - assert_opt_name_none_or_str test_class_with_methods.py(29, 4): ✔️ always true if reached - assert_opt_name_none_or_bar -DETAIL: 13 passed, 0 failed, 0 inconclusive +test_class_with_methods.py(32, 4): ✔️ always true if reached - assume_main_assume(666)_42_calls_test_helper_procedure$post0_0 +test_class_with_methods.py(32, 4): ✔️ always true if reached - assume_main_assume(666)_42_calls_test_helper_procedure$post0_1 +test_class_with_methods.py(32, 4): ✔️ always true if reached - assume_main_assume(666)_42_calls_test_helper_procedure$post0_2 +DETAIL: 18 passed, 0 failed, 0 inconclusive RESULT: Analysis success diff --git a/StrataPython/StrataPythonTest/expected_laurel/test_datetime.expected b/StrataPython/StrataPythonTest/expected_laurel/test_datetime.expected index f627b50117..eb9f6843b5 100644 --- a/StrataPython/StrataPythonTest/expected_laurel/test_datetime.expected +++ b/StrataPython/StrataPythonTest/expected_laurel/test_datetime.expected @@ -1,8 +1,13 @@ test_datetime.py(13, 0): ✅ pass - (Origin_datetime_date_Requires)d_type +test_datetime.py(13, 0): ✅ pass - assume_assume(394)_calls_datetime_date$post0_0 test_datetime.py(14, 0): ✅ pass - (Origin_timedelta_Requires) test_datetime.py(14, 0): ✅ pass - (Origin_timedelta_Requires)hours_type test_datetime.py(14, 0): ✅ pass - (Origin_timedelta_Requires)days_pos test_datetime.py(14, 0): ✅ pass - (Origin_timedelta_Requires)hours_pos +test_datetime.py(14, 0): ✅ pass - assume_assume(430)_calls_timedelta_func$post0_0 +test_datetime.py(14, 0): ✅ pass - assume_assume(430)_calls_timedelta_func$post0_1 +test_datetime.py(14, 0): ✅ pass - assume_assume(430)_calls_timedelta_func$post0_2 +test_datetime.py(14, 0): ✅ pass - assume_assume(430)_calls_timedelta_func$post0_3 test_datetime.py(15, 19): ✅ pass - Check PSub exception test_datetime.py(21, 7): ✅ pass - Check PLe exception test_datetime.py(21, 0): ✅ pass - assert(554) @@ -10,5 +15,5 @@ test_datetime.py(25, 0): ✅ pass - assert(673) test_datetime.py(27, 0): ✅ pass - assert(758) test_datetime.py(30, 7): ✅ pass - Check PLe exception test_datetime.py(30, 0): ✅ pass - assert(859) -DETAIL: 12 passed, 0 failed, 0 inconclusive +DETAIL: 17 passed, 0 failed, 0 inconclusive RESULT: Analysis success diff --git a/StrataPython/StrataPythonTest/expected_laurel/test_datetime_now_tz.expected b/StrataPython/StrataPythonTest/expected_laurel/test_datetime_now_tz.expected index 4ef6e80e7b..a3b64d5ff9 100644 --- a/StrataPython/StrataPythonTest/expected_laurel/test_datetime_now_tz.expected +++ b/StrataPython/StrataPythonTest/expected_laurel/test_datetime_now_tz.expected @@ -2,8 +2,12 @@ test_datetime_now_tz.py(4, 0): ✅ pass - (Origin_timedelta_Requires) test_datetime_now_tz.py(4, 0): ✅ pass - (Origin_timedelta_Requires)hours_type test_datetime_now_tz.py(4, 0): ✅ pass - (Origin_timedelta_Requires)days_pos test_datetime_now_tz.py(4, 0): ✅ pass - (Origin_timedelta_Requires)hours_pos +test_datetime_now_tz.py(4, 0): ✅ pass - assume_assume(95)_calls_timedelta_func$post0_0 +test_datetime_now_tz.py(4, 0): ✅ pass - assume_assume(95)_calls_timedelta_func$post0_1 +test_datetime_now_tz.py(4, 0): ✅ pass - assume_assume(95)_calls_timedelta_func$post0_2 +test_datetime_now_tz.py(4, 0): ✅ pass - assume_assume(95)_calls_timedelta_func$post0_3 test_datetime_now_tz.py(5, 18): ✅ pass - Check PSub exception test_datetime_now_tz.py(6, 7): ✅ pass - Check PLe exception test_datetime_now_tz.py(6, 0): ✅ pass - assert(162) -DETAIL: 7 passed, 0 failed, 0 inconclusive +DETAIL: 11 passed, 0 failed, 0 inconclusive RESULT: Analysis success diff --git a/StrataPython/StrataPythonTest/expected_laurel/test_deep_inline.expected b/StrataPython/StrataPythonTest/expected_laurel/test_deep_inline.expected index bc3395d77d..880b798c57 100644 --- a/StrataPython/StrataPythonTest/expected_laurel/test_deep_inline.expected +++ b/StrataPython/StrataPythonTest/expected_laurel/test_deep_inline.expected @@ -2,14 +2,18 @@ test_deep_inline.py(21, 4): ✔️ always true if reached - (triple_apply requir test_deep_inline.py(15, 4): ✔️ always true if reached - (double_inc requires) Type constraint of x test_deep_inline.py(10, 4): ✔️ always true if reached - (inc requires) Type constraint of x test_deep_inline.py(6, 4): ✔️ always true if reached - Check PAdd exception +test_deep_inline.py(10, 4): ✔️ always true if reached - assume_double_inc_assume(135)_53_calls_inc$post0_0 test_deep_inline.py(10, 4): ✔️ always true if reached - double_inc_assert(135)_54 test_deep_inline.py(10, 4): ✔️ always true if reached - Check PMul exception +test_deep_inline.py(15, 4): ✔️ always true if reached - assume_triple_apply_assume(206)_26_calls_double_inc$post0_0 test_deep_inline.py(15, 4): ✔️ always true if reached - triple_apply_assert(206)_27 test_deep_inline.py(15, 4): ✔️ always true if reached - (inc requires) Type constraint of x test_deep_inline.py(11, 4): ✔️ always true if reached - Check PAdd exception +test_deep_inline.py(15, 4): ✔️ always true if reached - assume_triple_apply_assume(233)_29_calls_inc$post0_0 test_deep_inline.py(15, 4): ✔️ always true if reached - triple_apply_assert(233)_30 +test_deep_inline.py(21, 4): ✔️ always true if reached - assume_main_assume(279)_8_calls_triple_apply$post0_0 test_deep_inline.py(21, 4): ✔️ always true if reached - main_assert(279)_9 test_deep_inline.py(21, 4): ✔️ always true if reached - triple_apply(3) should be 9 test_deep_inline.py(21, 4): ✖️ always false if reached - triple_apply(3) should not be 10 -DETAIL: 12 passed, 1 failed, 0 inconclusive +DETAIL: 16 passed, 1 failed, 0 inconclusive RESULT: Failures found diff --git a/StrataPython/StrataPythonTest/expected_laurel/test_default_params.expected b/StrataPython/StrataPythonTest/expected_laurel/test_default_params.expected index 395575a21c..ef0d4cfb9b 100644 --- a/StrataPython/StrataPythonTest/expected_laurel/test_default_params.expected +++ b/StrataPython/StrataPythonTest/expected_laurel/test_default_params.expected @@ -9,19 +9,27 @@ test_default_params.py(10, 12): ❓ unknown - Check PAdd exception test_default_params.py(5, 38): ❓ unknown - (power ensures) Return type constraint test_default_params.py(14, 4): ✅ pass - (greet requires) Type constraint of name test_default_params.py(14, 4): ✅ pass - (greet requires) Type constraint of greeting +test_default_params.py(14, 4): ✅ pass - assume_assume(294)_calls_greet$post0_0 +test_default_params.py(14, 4): ✅ pass - assume_assume(294)_calls_greet$post0_1 test_default_params.py(14, 4): ✅ pass - assert(294) test_default_params.py(15, 4): ❓ unknown - default greeting failed test_default_params.py(17, 4): ✅ pass - (greet requires) Type constraint of name test_default_params.py(17, 4): ✅ pass - (greet requires) Type constraint of greeting +test_default_params.py(17, 4): ✅ pass - assume_assume(386)_calls_greet$post0_0 +test_default_params.py(17, 4): ✅ pass - assume_assume(386)_calls_greet$post0_1 test_default_params.py(17, 4): ✅ pass - assert(386) test_default_params.py(18, 4): ❓ unknown - explicit greeting failed test_default_params.py(20, 4): ✅ pass - (power requires) Type constraint of base test_default_params.py(20, 4): ✅ pass - (power requires) Type constraint of exp +test_default_params.py(20, 4): ✅ pass - assume_assume(478)_calls_power$post0_0 +test_default_params.py(20, 4): ✅ pass - assume_assume(478)_calls_power$post0_1 test_default_params.py(20, 4): ✅ pass - assert(478) test_default_params.py(21, 4): ❓ unknown - default power failed test_default_params.py(23, 4): ✅ pass - (power requires) Type constraint of base test_default_params.py(23, 4): ✅ pass - (power requires) Type constraint of exp +test_default_params.py(23, 4): ✅ pass - assume_assume(545)_calls_power$post0_0 +test_default_params.py(23, 4): ✅ pass - assume_assume(545)_calls_power$post0_1 test_default_params.py(23, 4): ✅ pass - assert(545) test_default_params.py(24, 4): ❓ unknown - explicit power failed -DETAIL: 18 passed, 0 failed, 7 inconclusive +DETAIL: 26 passed, 0 failed, 7 inconclusive RESULT: Inconclusive diff --git a/StrataPython/StrataPythonTest/expected_laurel/test_func_input_type_constraints.expected b/StrataPython/StrataPythonTest/expected_laurel/test_func_input_type_constraints.expected index 014be579f7..f752317484 100644 --- a/StrataPython/StrataPythonTest/expected_laurel/test_func_input_type_constraints.expected +++ b/StrataPython/StrataPythonTest/expected_laurel/test_func_input_type_constraints.expected @@ -7,10 +7,17 @@ test_func_input_type_constraints.py(12, 4): ❓ unknown - set_LaurelResult_calls test_func_input_type_constraints.py(11, 65): ❓ unknown - (List_Dict_index ensures) Return type constraint test_func_input_type_constraints.py(15, 0): ✅ pass - (Mul requires) Type constraint of x test_func_input_type_constraints.py(15, 0): ✅ pass - (Mul requires) Type constraint of y +test_func_input_type_constraints.py(15, 0): ✅ pass - assume_assume(315)_calls_Mul$post0_0 +test_func_input_type_constraints.py(15, 0): ✅ pass - assume_assume(315)_calls_Mul$post0_1 test_func_input_type_constraints.py(16, 0): ✅ pass - (Sum requires) Type constraint of x test_func_input_type_constraints.py(16, 0): ✅ pass - (Sum requires) Type constraint of y +test_func_input_type_constraints.py(16, 0): ✅ pass - assume_assume(332)_calls_Sum$post0_0 +test_func_input_type_constraints.py(16, 0): ✅ pass - assume_assume(332)_calls_Sum$post0_1 test_func_input_type_constraints.py(17, 0): ✅ pass - (List_Dict_index requires) Type constraint of l test_func_input_type_constraints.py(17, 0): ✅ pass - (List_Dict_index requires) Type constraint of i test_func_input_type_constraints.py(17, 0): ✅ pass - (List_Dict_index requires) Type constraint of s -DETAIL: 11 passed, 0 failed, 3 inconclusive +test_func_input_type_constraints.py(17, 0): ✅ pass - assume_assume(349)_calls_List_Dict_index$post0_0 +test_func_input_type_constraints.py(17, 0): ✅ pass - assume_assume(349)_calls_List_Dict_index$post0_1 +test_func_input_type_constraints.py(17, 0): ✅ pass - assume_assume(349)_calls_List_Dict_index$post0_2 +DETAIL: 18 passed, 0 failed, 3 inconclusive RESULT: Inconclusive diff --git a/StrataPython/StrataPythonTest/expected_laurel/test_function_def_calls.expected b/StrataPython/StrataPythonTest/expected_laurel/test_function_def_calls.expected index 62499427b9..ec353257e9 100644 --- a/StrataPython/StrataPythonTest/expected_laurel/test_function_def_calls.expected +++ b/StrataPython/StrataPythonTest/expected_laurel/test_function_def_calls.expected @@ -1,6 +1,9 @@ test_function_def_calls.py(6, 4): ❓ unknown - (Origin_test_helper_procedure_Requires)req_name_is_foo test_function_def_calls.py(6, 4): ✅ pass - (Origin_test_helper_procedure_Requires)req_opt_name_none_or_str test_function_def_calls.py(6, 4): ✅ pass - (Origin_test_helper_procedure_Requires)req_opt_name_none_or_bar +test_function_def_calls.py(6, 4): ❓ unknown - assume_assume(64)_calls_test_helper_procedure$post0_0 +test_function_def_calls.py(6, 4): ✅ pass - assume_assume(64)_calls_test_helper_procedure$post0_1 +test_function_def_calls.py(6, 4): ✅ pass - assume_assume(64)_calls_test_helper_procedure$post0_2 test_function_def_calls.py(9, 4): ✅ pass - (my_f requires) Type constraint of s -DETAIL: 3 passed, 0 failed, 1 inconclusive +DETAIL: 5 passed, 0 failed, 2 inconclusive RESULT: Inconclusive diff --git a/StrataPython/StrataPythonTest/expected_laurel/test_if_elif.expected b/StrataPython/StrataPythonTest/expected_laurel/test_if_elif.expected index 2c4b59ca73..b7fddd0ed9 100644 --- a/StrataPython/StrataPythonTest/expected_laurel/test_if_elif.expected +++ b/StrataPython/StrataPythonTest/expected_laurel/test_if_elif.expected @@ -3,16 +3,20 @@ test_if_elif.py(1, 24): ✅ pass - (classify ensures) Return type constraint test_if_elif.py(6, 9): ✅ pass - Check PLt exception test_if_elif.py(12, 23): ✅ pass - Check PNeg exception test_if_elif.py(12, 4): ✅ pass - (classify requires) Type constraint of x +test_if_elif.py(12, 4): ✅ pass - assume_assume(198)_calls_classify$post0_0 test_if_elif.py(12, 4): ✅ pass - assert(198) test_if_elif.py(13, 4): ❓ unknown - should be negative test_if_elif.py(15, 4): ✅ pass - (classify requires) Type constraint of x +test_if_elif.py(15, 4): ✅ pass - assume_assume(276)_calls_classify$post0_0 test_if_elif.py(15, 4): ✅ pass - assert(276) test_if_elif.py(16, 4): ❓ unknown - should be zero test_if_elif.py(18, 4): ✅ pass - (classify requires) Type constraint of x +test_if_elif.py(18, 4): ✅ pass - assume_assume(345)_calls_classify$post0_0 test_if_elif.py(18, 4): ✅ pass - assert(345) test_if_elif.py(19, 4): ❓ unknown - should be small test_if_elif.py(21, 4): ✅ pass - (classify requires) Type constraint of x +test_if_elif.py(21, 4): ✅ pass - assume_assume(416)_calls_classify$post0_0 test_if_elif.py(21, 4): ✅ pass - assert(416) test_if_elif.py(22, 4): ❓ unknown - should be large -DETAIL: 12 passed, 0 failed, 4 inconclusive +DETAIL: 16 passed, 0 failed, 4 inconclusive RESULT: Inconclusive diff --git a/StrataPython/StrataPythonTest/expected_laurel/test_method_call_with_kwargs.expected b/StrataPython/StrataPythonTest/expected_laurel/test_method_call_with_kwargs.expected index 315f62f13d..249ee0019c 100644 --- a/StrataPython/StrataPythonTest/expected_laurel/test_method_call_with_kwargs.expected +++ b/StrataPython/StrataPythonTest/expected_laurel/test_method_call_with_kwargs.expected @@ -5,5 +5,8 @@ test_method_call_with_kwargs.py(8, 0): ✅ pass - (MyClass@__init__ requires) Ty test_method_call_with_kwargs.py(9, 0): ✅ pass - (MyClass@some_method requires) Type constraint of ip1 test_method_call_with_kwargs.py(9, 0): ✅ pass - (MyClass@some_method requires) Type constraint of ip2 test_method_call_with_kwargs.py(9, 0): ✅ pass - (MyClass@some_method requires) Type constraint of ip3 -DETAIL: 7 passed, 0 failed, 0 inconclusive +test_method_call_with_kwargs.py(9, 0): ✅ pass - assume_assume(250)_calls_MyClass@some_method$post0_0 +test_method_call_with_kwargs.py(9, 0): ✅ pass - assume_assume(250)_calls_MyClass@some_method$post0_1 +test_method_call_with_kwargs.py(9, 0): ✅ pass - assume_assume(250)_calls_MyClass@some_method$post0_2 +DETAIL: 10 passed, 0 failed, 0 inconclusive RESULT: Analysis success diff --git a/StrataPython/StrataPythonTest/expected_laurel/test_method_kwargs_no_hierarchy.expected b/StrataPython/StrataPythonTest/expected_laurel/test_method_kwargs_no_hierarchy.expected index 56de827e26..c34ed4becf 100644 --- a/StrataPython/StrataPythonTest/expected_laurel/test_method_kwargs_no_hierarchy.expected +++ b/StrataPython/StrataPythonTest/expected_laurel/test_method_kwargs_no_hierarchy.expected @@ -5,8 +5,10 @@ unknown location: ✅ pass - assert(0) test_method_kwargs_no_hierarchy.py(11, 18): ✅ pass - init_calls_Any_get_or_none_0 test_method_kwargs_no_hierarchy.py(11, 18): ✅ pass - (Calculator@add requires) Type constraint of x test_method_kwargs_no_hierarchy.py(11, 18): ✅ pass - (Calculator@add requires) Type constraint of y +test_method_kwargs_no_hierarchy.py(11, 18): ✅ pass - assume_assume(268)_calls_Calculator@add$post0_0 +test_method_kwargs_no_hierarchy.py(11, 18): ✅ pass - assume_assume(268)_calls_Calculator@add$post0_1 test_method_kwargs_no_hierarchy.py(11, 4): ✅ pass - assert(254) test_method_kwargs_no_hierarchy.py(12, 4): ❓ unknown - assert(286) test_method_kwargs_no_hierarchy.py(8, 14): ✅ pass - (main ensures) Return type constraint -DETAIL: 8 passed, 0 failed, 2 inconclusive +DETAIL: 10 passed, 0 failed, 2 inconclusive RESULT: Inconclusive diff --git a/StrataPython/StrataPythonTest/expected_laurel/test_missing_models.expected b/StrataPython/StrataPythonTest/expected_laurel/test_missing_models.expected index 0cd54248ab..0eac8f72ec 100644 --- a/StrataPython/StrataPythonTest/expected_laurel/test_missing_models.expected +++ b/StrataPython/StrataPythonTest/expected_laurel/test_missing_models.expected @@ -3,11 +3,20 @@ test_missing_models.py(8, 4): ❓ unknown - init_calls_Any_get_1 test_missing_models.py(9, 4): ❓ unknown - (Origin_test_helper_procedure_Requires)req_name_is_foo test_missing_models.py(9, 4): ✅ pass - (Origin_test_helper_procedure_Requires)req_opt_name_none_or_str test_missing_models.py(9, 4): ✅ pass - (Origin_test_helper_procedure_Requires)req_opt_name_none_or_bar +test_missing_models.py(9, 4): ❓ unknown - assume_assume(226)_calls_test_helper_procedure$post0_0 +test_missing_models.py(9, 4): ✅ pass - assume_assume(226)_calls_test_helper_procedure$post0_1 +test_missing_models.py(9, 4): ✅ pass - assume_assume(226)_calls_test_helper_procedure$post0_2 test_missing_models.py(12, 4): ✅ pass - (Origin_test_helper_procedure_Requires)req_name_is_foo test_missing_models.py(12, 4): ✅ pass - (Origin_test_helper_procedure_Requires)req_opt_name_none_or_str test_missing_models.py(12, 4): ✅ pass - (Origin_test_helper_procedure_Requires)req_opt_name_none_or_bar +test_missing_models.py(12, 4): ✅ pass - assume_assume(330)_calls_test_helper_procedure$post0_0 +test_missing_models.py(12, 4): ✅ pass - assume_assume(330)_calls_test_helper_procedure$post0_1 +test_missing_models.py(12, 4): ✅ pass - assume_assume(330)_calls_test_helper_procedure$post0_2 test_missing_models.py(15, 4): ✅ pass - (Origin_test_helper_procedure_Requires)req_name_is_foo test_missing_models.py(15, 4): ✅ pass - (Origin_test_helper_procedure_Requires)req_opt_name_none_or_str test_missing_models.py(15, 4): ✅ pass - (Origin_test_helper_procedure_Requires)req_opt_name_none_or_bar -DETAIL: 8 passed, 0 failed, 3 inconclusive +test_missing_models.py(15, 4): ✅ pass - assume_assume(411)_calls_test_helper_procedure$post0_0 +test_missing_models.py(15, 4): ✅ pass - assume_assume(411)_calls_test_helper_procedure$post0_1 +test_missing_models.py(15, 4): ✅ pass - assume_assume(411)_calls_test_helper_procedure$post0_2 +DETAIL: 16 passed, 0 failed, 4 inconclusive RESULT: Inconclusive diff --git a/StrataPython/StrataPythonTest/expected_laurel/test_multi_function.expected b/StrataPython/StrataPythonTest/expected_laurel/test_multi_function.expected index 1408f7cb98..27b41cac48 100644 --- a/StrataPython/StrataPythonTest/expected_laurel/test_multi_function.expected +++ b/StrataPython/StrataPythonTest/expected_laurel/test_multi_function.expected @@ -4,7 +4,10 @@ test_multi_function.py(8, 47): ✅ pass - (validate_config ensures) Return type test_multi_function.py(11, 4): ✅ pass - ite_cond_calls_PNotIn_0 test_multi_function.py(16, 4): ✅ pass - (create_config requires) Type constraint of name test_multi_function.py(16, 4): ✅ pass - (create_config requires) Type constraint of value +test_multi_function.py(16, 4): ✅ pass - assume_assume(429)_calls_create_config$post0_0 +test_multi_function.py(16, 4): ✅ pass - assume_assume(429)_calls_create_config$post0_1 test_multi_function.py(17, 4): ✅ pass - (validate_config requires) Type constraint of config +test_multi_function.py(17, 4): ✅ pass - assume_assume(485)_calls_validate_config$post0_0 test_multi_function.py(17, 4): ✅ pass - assert(485) test_multi_function.py(18, 7): ✅ pass - Check PNot exception test_multi_function.py(20, 4): ❓ unknown - set_LaurelResult_calls_Any_get_0 @@ -14,5 +17,8 @@ test_multi_function.py(24, 4): ❓ unknown - process_config should return value test_multi_function.py(26, 4): ✅ pass - (Origin_test_helper_procedure_Requires)req_name_is_foo test_multi_function.py(26, 4): ✅ pass - (Origin_test_helper_procedure_Requires)req_opt_name_none_or_str test_multi_function.py(26, 4): ✅ pass - (Origin_test_helper_procedure_Requires)req_opt_name_none_or_bar -DETAIL: 14 passed, 0 failed, 2 inconclusive +test_multi_function.py(26, 4): ✅ pass - assume_assume(715)_calls_test_helper_procedure$post0_0 +test_multi_function.py(26, 4): ✅ pass - assume_assume(715)_calls_test_helper_procedure$post0_1 +test_multi_function.py(26, 4): ✅ pass - assume_assume(715)_calls_test_helper_procedure$post0_2 +DETAIL: 20 passed, 0 failed, 2 inconclusive RESULT: Inconclusive diff --git a/StrataPython/StrataPythonTest/expected_laurel/test_nested_calls.expected b/StrataPython/StrataPythonTest/expected_laurel/test_nested_calls.expected index 0f4bb96d26..6ab4adc4ce 100644 --- a/StrataPython/StrataPythonTest/expected_laurel/test_nested_calls.expected +++ b/StrataPython/StrataPythonTest/expected_laurel/test_nested_calls.expected @@ -3,19 +3,25 @@ test_nested_calls.py(1, 22): ✅ pass - (double ensures) Return type constraint test_nested_calls.py(5, 11): ✅ pass - Check PAdd exception test_nested_calls.py(4, 23): ✅ pass - (add_one ensures) Return type constraint test_nested_calls.py(8, 4): ✅ pass - (double requires) Type constraint of x +test_nested_calls.py(8, 4): ✅ pass - assume_assume(107)_calls_double$post0_0 test_nested_calls.py(8, 4): ✅ pass - assert(107) test_nested_calls.py(9, 4): ✅ pass - (double requires) Type constraint of x +test_nested_calls.py(9, 4): ✅ pass - assume_assume(130)_calls_double$post0_0 test_nested_calls.py(9, 4): ✅ pass - assert(130) test_nested_calls.py(10, 4): ❓ unknown - double(double(3)) should be 12 test_nested_calls.py(12, 4): ✅ pass - (double requires) Type constraint of x +test_nested_calls.py(12, 4): ✅ pass - assume_assume(207)_calls_double$post0_0 test_nested_calls.py(12, 4): ✅ pass - assert(207) test_nested_calls.py(13, 4): ✅ pass - (add_one requires) Type constraint of x +test_nested_calls.py(13, 4): ✅ pass - assume_assume(230)_calls_add_one$post0_0 test_nested_calls.py(13, 4): ✅ pass - assert(230) test_nested_calls.py(14, 4): ❓ unknown - add_one(double(5)) should be 11 test_nested_calls.py(16, 4): ✅ pass - (add_one requires) Type constraint of x +test_nested_calls.py(16, 4): ✅ pass - assume_assume(309)_calls_add_one$post0_0 test_nested_calls.py(16, 4): ✅ pass - assert(309) test_nested_calls.py(17, 4): ✅ pass - (double requires) Type constraint of x +test_nested_calls.py(17, 4): ✅ pass - assume_assume(333)_calls_double$post0_0 test_nested_calls.py(17, 4): ✅ pass - assert(333) test_nested_calls.py(18, 4): ❓ unknown - double(add_one(4)) should be 10 -DETAIL: 16 passed, 0 failed, 3 inconclusive +DETAIL: 22 passed, 0 failed, 3 inconclusive RESULT: Inconclusive diff --git a/StrataPython/StrataPythonTest/expected_laurel/test_param_reassign.expected b/StrataPython/StrataPythonTest/expected_laurel/test_param_reassign.expected index 57dfaf7a9e..f9eabace5c 100644 --- a/StrataPython/StrataPythonTest/expected_laurel/test_param_reassign.expected +++ b/StrataPython/StrataPythonTest/expected_laurel/test_param_reassign.expected @@ -12,22 +12,30 @@ test_param_reassign.py(18, 8): ✅ pass - Check PAdd exception test_param_reassign.py(19, 8): ✅ pass - Check PMul exception test_param_reassign.py(17, 36): ✅ pass - (param_reassign_twice ensures) Return type constraint test_param_reassign.py(23, 4): ✅ pass - (single_param_reassign requires) Type constraint of x +test_param_reassign.py(23, 4): ✅ pass - assume_assume(422)_calls_single_param_reassign$post0_0 test_param_reassign.py(23, 4): ✅ pass - assert(422) test_param_reassign.py(24, 4): ❓ unknown - single reassign test_param_reassign.py(26, 4): ✅ pass - (multi_param_reassign requires) Type constraint of a test_param_reassign.py(26, 4): ✅ pass - (multi_param_reassign requires) Type constraint of b +test_param_reassign.py(26, 4): ✅ pass - assume_assume(500)_calls_multi_param_reassign$post0_0 +test_param_reassign.py(26, 4): ✅ pass - assume_assume(500)_calls_multi_param_reassign$post0_1 test_param_reassign.py(26, 4): ✅ pass - assert(500) test_param_reassign.py(27, 4): ❓ unknown - multi reassign test_param_reassign.py(29, 4): ✅ pass - (no_param_reassign requires) Type constraint of x test_param_reassign.py(29, 4): ✅ pass - (no_param_reassign requires) Type constraint of y +test_param_reassign.py(29, 4): ✅ pass - assume_assume(580)_calls_no_param_reassign$post0_0 +test_param_reassign.py(29, 4): ✅ pass - assume_assume(580)_calls_no_param_reassign$post0_1 test_param_reassign.py(29, 4): ✅ pass - assert(580) test_param_reassign.py(30, 4): ❓ unknown - no reassign test_param_reassign.py(32, 4): ✅ pass - (partial_param_reassign requires) Type constraint of x test_param_reassign.py(32, 4): ✅ pass - (partial_param_reassign requires) Type constraint of y +test_param_reassign.py(32, 4): ✅ pass - assume_assume(653)_calls_partial_param_reassign$post0_0 +test_param_reassign.py(32, 4): ✅ pass - assume_assume(653)_calls_partial_param_reassign$post0_1 test_param_reassign.py(32, 4): ✅ pass - assert(653) test_param_reassign.py(33, 4): ❓ unknown - partial reassign test_param_reassign.py(35, 4): ✅ pass - (param_reassign_twice requires) Type constraint of x +test_param_reassign.py(35, 4): ✅ pass - assume_assume(738)_calls_param_reassign_twice$post0_0 test_param_reassign.py(35, 4): ✅ pass - assert(738) test_param_reassign.py(36, 4): ❓ unknown - reassign twice -DETAIL: 26 passed, 0 failed, 5 inconclusive +DETAIL: 34 passed, 0 failed, 5 inconclusive RESULT: Inconclusive diff --git a/StrataPython/StrataPythonTest/expected_laurel/test_param_reassign_kwargs.expected b/StrataPython/StrataPythonTest/expected_laurel/test_param_reassign_kwargs.expected index 330fc8092f..28fe9446e8 100644 --- a/StrataPython/StrataPythonTest/expected_laurel/test_param_reassign_kwargs.expected +++ b/StrataPython/StrataPythonTest/expected_laurel/test_param_reassign_kwargs.expected @@ -2,7 +2,9 @@ test_param_reassign_kwargs.py(2, 11): ✅ pass - Check PAdd exception test_param_reassign_kwargs.py(1, 59): ✅ pass - (greet ensures) Return type constraint test_param_reassign_kwargs.py(6, 4): ✅ pass - (greet requires) Type constraint of name test_param_reassign_kwargs.py(6, 4): ✅ pass - (greet requires) Type constraint of greeting +test_param_reassign_kwargs.py(6, 4): ✅ pass - assume_assume(137)_calls_greet$post0_0 +test_param_reassign_kwargs.py(6, 4): ✅ pass - assume_assume(137)_calls_greet$post0_1 test_param_reassign_kwargs.py(6, 4): ✅ pass - assert(137) test_param_reassign_kwargs.py(7, 4): ❓ unknown - kwargs call -DETAIL: 5 passed, 0 failed, 1 inconclusive +DETAIL: 7 passed, 0 failed, 1 inconclusive RESULT: Inconclusive diff --git a/StrataPython/StrataPythonTest/expected_laurel/test_precondition_verification.expected b/StrataPython/StrataPythonTest/expected_laurel/test_precondition_verification.expected index 30acce18e1..1dc375e596 100644 --- a/StrataPython/StrataPythonTest/expected_laurel/test_precondition_verification.expected +++ b/StrataPython/StrataPythonTest/expected_laurel/test_precondition_verification.expected @@ -1,14 +1,26 @@ test_precondition_verification.py(8, 4): ✅ pass - (Origin_test_helper_procedure_Requires)req_name_is_foo test_precondition_verification.py(8, 4): ✅ pass - (Origin_test_helper_procedure_Requires)req_opt_name_none_or_str test_precondition_verification.py(8, 4): ✅ pass - (Origin_test_helper_procedure_Requires)req_opt_name_none_or_bar +test_precondition_verification.py(8, 4): ✅ pass - assume_assume(104)_calls_test_helper_procedure$post0_0 +test_precondition_verification.py(8, 4): ✅ pass - assume_assume(104)_calls_test_helper_procedure$post0_1 +test_precondition_verification.py(8, 4): ✅ pass - assume_assume(104)_calls_test_helper_procedure$post0_2 test_precondition_verification.py(11, 4): ✅ pass - (Origin_test_helper_procedure_Requires)req_name_is_foo test_precondition_verification.py(11, 4): ✅ pass - (Origin_test_helper_procedure_Requires)req_opt_name_none_or_str test_precondition_verification.py(11, 4): ✅ pass - (Origin_test_helper_procedure_Requires)req_opt_name_none_or_bar +test_precondition_verification.py(11, 4): ✅ pass - assume_assume(159)_calls_test_helper_procedure$post0_0 +test_precondition_verification.py(11, 4): ✅ pass - assume_assume(159)_calls_test_helper_procedure$post0_1 +test_precondition_verification.py(11, 4): ✅ pass - assume_assume(159)_calls_test_helper_procedure$post0_2 test_precondition_verification.py(14, 4): ❓ unknown - (Origin_test_helper_procedure_Requires)req_name_is_foo test_precondition_verification.py(14, 4): ✅ pass - (Origin_test_helper_procedure_Requires)req_opt_name_none_or_str test_precondition_verification.py(14, 4): ✅ pass - (Origin_test_helper_procedure_Requires)req_opt_name_none_or_bar +test_precondition_verification.py(14, 4): ❓ unknown - assume_assume(230)_calls_test_helper_procedure$post0_0 +test_precondition_verification.py(14, 4): ✅ pass - assume_assume(230)_calls_test_helper_procedure$post0_1 +test_precondition_verification.py(14, 4): ✅ pass - assume_assume(230)_calls_test_helper_procedure$post0_2 test_precondition_verification.py(17, 4): ✅ pass - (Origin_test_helper_procedure_Requires)req_name_is_foo test_precondition_verification.py(17, 4): ✅ pass - (Origin_test_helper_procedure_Requires)req_opt_name_none_or_str test_precondition_verification.py(17, 4): ❓ unknown - (Origin_test_helper_procedure_Requires)req_opt_name_none_or_bar -DETAIL: 10 passed, 0 failed, 2 inconclusive +test_precondition_verification.py(17, 4): ✅ pass - assume_assume(283)_calls_test_helper_procedure$post0_0 +test_precondition_verification.py(17, 4): ✅ pass - assume_assume(283)_calls_test_helper_procedure$post0_1 +test_precondition_verification.py(17, 4): ❓ unknown - assume_assume(283)_calls_test_helper_procedure$post0_2 +DETAIL: 20 passed, 0 failed, 4 inconclusive RESULT: Inconclusive diff --git a/StrataPython/StrataPythonTest/expected_laurel/test_procedure_in_assert.expected b/StrataPython/StrataPythonTest/expected_laurel/test_procedure_in_assert.expected index 8d71e8b122..4547094ebf 100644 --- a/StrataPython/StrataPythonTest/expected_laurel/test_procedure_in_assert.expected +++ b/StrataPython/StrataPythonTest/expected_laurel/test_procedure_in_assert.expected @@ -3,9 +3,13 @@ test_procedure_in_assert.py(5, 4): ✅ pass - (Origin_timedelta_Requires) test_procedure_in_assert.py(5, 4): ✅ pass - (Origin_timedelta_Requires)hours_type test_procedure_in_assert.py(5, 4): ✅ pass - (Origin_timedelta_Requires)days_pos test_procedure_in_assert.py(5, 4): ✅ pass - (Origin_timedelta_Requires)hours_pos +test_procedure_in_assert.py(5, 4): ✅ pass - assume_assume(75)_calls_timedelta_func$post0_0 +test_procedure_in_assert.py(5, 4): ✅ pass - assume_assume(75)_calls_timedelta_func$post0_1 +test_procedure_in_assert.py(5, 4): ✅ pass - assume_assume(75)_calls_timedelta_func$post0_2 +test_procedure_in_assert.py(5, 4): ✅ pass - assume_assume(75)_calls_timedelta_func$post0_3 test_procedure_in_assert.py(5, 17): ✅ pass - Check PSub exception test_procedure_in_assert.py(6, 4): ✅ pass - assert(117) test_procedure_in_assert.py(7, 4): ✅ pass - should pass test_procedure_in_assert.py(3, 14): ✅ pass - (main ensures) Return type constraint -DETAIL: 9 passed, 0 failed, 0 inconclusive +DETAIL: 13 passed, 0 failed, 0 inconclusive RESULT: Analysis success diff --git a/StrataPython/StrataPythonTest/expected_laurel/test_return_types.expected b/StrataPython/StrataPythonTest/expected_laurel/test_return_types.expected index ba027981f3..699d478671 100644 --- a/StrataPython/StrataPythonTest/expected_laurel/test_return_types.expected +++ b/StrataPython/StrataPythonTest/expected_laurel/test_return_types.expected @@ -14,7 +14,9 @@ test_return_types.py(25, 4): ✅ pass - assert(449) test_return_types.py(26, 4): ❓ unknown - get_flag returned wrong value test_return_types.py(28, 4): ✅ pass - (add requires) Type constraint of a test_return_types.py(28, 4): ✅ pass - (add requires) Type constraint of b +test_return_types.py(28, 4): ✅ pass - assume_assume(529)_calls_add$post0_0 +test_return_types.py(28, 4): ✅ pass - assume_assume(529)_calls_add$post0_1 test_return_types.py(28, 4): ✅ pass - assert(529) test_return_types.py(29, 4): ❓ unknown - add returned wrong value -DETAIL: 14 passed, 0 failed, 4 inconclusive +DETAIL: 16 passed, 0 failed, 4 inconclusive RESULT: Inconclusive diff --git a/StrataPython/StrataPythonTest/expected_laurel/test_timedelta_expr.expected b/StrataPython/StrataPythonTest/expected_laurel/test_timedelta_expr.expected index 270b1ae3c0..7136cea712 100644 --- a/StrataPython/StrataPythonTest/expected_laurel/test_timedelta_expr.expected +++ b/StrataPython/StrataPythonTest/expected_laurel/test_timedelta_expr.expected @@ -2,8 +2,12 @@ test_timedelta_expr.py(4, 0): ✅ pass - (Origin_timedelta_Requires) test_timedelta_expr.py(4, 0): ✅ pass - (Origin_timedelta_Requires)hours_type test_timedelta_expr.py(4, 0): ✅ pass - (Origin_timedelta_Requires)days_pos test_timedelta_expr.py(4, 0): ✅ pass - (Origin_timedelta_Requires)hours_pos +test_timedelta_expr.py(4, 0): ✅ pass - assume_assume(73)_calls_timedelta_func$post0_0 +test_timedelta_expr.py(4, 0): ✅ pass - assume_assume(73)_calls_timedelta_func$post0_1 +test_timedelta_expr.py(4, 0): ✅ pass - assume_assume(73)_calls_timedelta_func$post0_2 +test_timedelta_expr.py(4, 0): ✅ pass - assume_assume(73)_calls_timedelta_func$post0_3 test_timedelta_expr.py(5, 18): ✅ pass - Check PSub exception test_timedelta_expr.py(6, 7): ✅ pass - Check PLe exception test_timedelta_expr.py(6, 0): ✅ pass - assert(140) -DETAIL: 7 passed, 0 failed, 0 inconclusive +DETAIL: 11 passed, 0 failed, 0 inconclusive RESULT: Analysis success diff --git a/StrataPython/StrataPythonTest/expected_laurel/test_try_except_nested.expected b/StrataPython/StrataPythonTest/expected_laurel/test_try_except_nested.expected index bc5270d557..f979e50112 100644 --- a/StrataPython/StrataPythonTest/expected_laurel/test_try_except_nested.expected +++ b/StrataPython/StrataPythonTest/expected_laurel/test_try_except_nested.expected @@ -1,7 +1,8 @@ test_try_except_nested.py(5, 26): ✅ pass - (might_fail ensures) Return type constraint test_try_except_nested.py(9, 4): ✅ pass - assert(256) test_try_except_nested.py(12, 12): ✅ pass - (might_fail requires) Type constraint of x +test_try_except_nested.py(12, 12): ✅ pass - assume_assume(310)_calls_might_fail$post0_0 test_try_except_nested.py(15, 4): ❓ unknown - should succeed test_try_except_nested.py(8, 28): ✅ pass - (test_nested_except ensures) Return type constraint -DETAIL: 4 passed, 0 failed, 1 inconclusive +DETAIL: 5 passed, 0 failed, 1 inconclusive RESULT: Inconclusive diff --git a/StrataPython/StrataPythonTest/expected_laurel/test_var_shadow_func.expected b/StrataPython/StrataPythonTest/expected_laurel/test_var_shadow_func.expected index 7aee788a67..6cf06871fe 100644 --- a/StrataPython/StrataPythonTest/expected_laurel/test_var_shadow_func.expected +++ b/StrataPython/StrataPythonTest/expected_laurel/test_var_shadow_func.expected @@ -2,8 +2,9 @@ test_var_shadow_func.py(2, 8): ✅ pass - Check PAdd exception test_var_shadow_func.py(1, 17): ✅ pass - (f ensures) Return type constraint test_var_shadow_func.py(6, 4): ✅ pass - assert(83) test_var_shadow_func.py(7, 4): ✅ pass - (f requires) Type constraint of x +test_var_shadow_func.py(7, 4): ✅ pass - assume_assume(98)_calls_f$post0_0 test_var_shadow_func.py(7, 4): ✅ pass - assert(98) test_var_shadow_func.py(8, 4): ❓ unknown - param modified inside test_var_shadow_func.py(9, 4): ✅ pass - original unchanged -DETAIL: 6 passed, 0 failed, 1 inconclusive +DETAIL: 7 passed, 0 failed, 1 inconclusive RESULT: Inconclusive diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T24_Sequences.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T24_Sequences.lean new file mode 100644 index 0000000000..0eae31c62c --- /dev/null +++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T24_Sequences.lean @@ -0,0 +1,293 @@ +/- + Copyright Strata Contributors + + SPDX-License-Identifier: Apache-2.0 OR MIT +-/ + +import StrataTest.Util.TestLaurel + +open StrataTest.Util +open Strata + +#eval testLaurel +#strata +program Laurel; +// Literal construction and select +procedure literalSelect() returns (r: int) + opaque +{ + var s: Seq := [10, 20, 30]; + r := Sequence.select(s, 1); + assert r == 20 +}; + +// Empty sequence has length 0 +procedure emptyLength() + opaque +{ + var s: Seq := []; + assert Sequence.length(s) == 0 +}; + +// Build and length +procedure buildLength() + opaque +{ + var s: Seq := [1, 2, 3]; + assert Sequence.length(s) == 3 +}; + +// Functional update preserves length +procedure updateLength() + opaque +{ + var s: Seq := [1, 2, 3]; + var t: Seq := s[0 := 99]; + assert Sequence.length(t) == 3 +}; + +// Functional update changes element +procedure updateSelect() + opaque +{ + var s: Seq := [1, 2, 3]; + var t: Seq := s[0 := 99]; + assert Sequence.select(t, 0) == 99 +}; + +// Subscript read sugar +procedure subscriptRead(s: Seq) + requires Sequence.length(s) > 0 + opaque +{ + var x: int := s[0]; + assert x == Sequence.select(s, 0) +}; + +// Subscript update sugar +procedure subscriptUpdate(s: Seq) + requires Sequence.length(s) > 0 + opaque +{ + var t: Seq := s[0 := 42]; + assert Sequence.select(t, 0) == 42 +}; + +// Sequence in requires/ensures +procedure contractSeq(s: Seq) returns (r: int) + requires Sequence.length(s) > 0 + opaque + ensures r == Sequence.select(s, 0) +{ + r := s[0] +}; + +// Sequence in quantifiers +procedure quantifierSeq(s: Seq) + requires Sequence.length(s) > 0 + requires forall(i: int) => 0 <= i && i < Sequence.length(s) ==> s[i] >= 0 + opaque +{ + assert s[0] >= 0 +}; + +// Bool element type +procedure seqBool() + opaque +{ + var s: Seq := [true, false]; + assert Sequence.select(s, 0) == true +}; + +// Nested sequences +procedure seqNested() + opaque +{ + var s: Seq> := [[1, 2], [3, 4]]; + assert Sequence.select(Sequence.select(s, 0), 1) == 2 +}; + +// Append length +procedure appendLength() + opaque +{ + var a: Seq := [1, 2]; + var b: Seq := [3, 4, 5]; + var c: Seq := Sequence.append(a, b); + assert Sequence.length(c) == 5 +}; + +// Append select from first half +procedure appendSelectFirst() + opaque +{ + var a: Seq := [10, 20]; + var b: Seq := [30]; + var c: Seq := Sequence.append(a, b); + assert c[0] == 10; + assert c[1] == 20 +}; + +// Append select from second half +procedure appendSelectSecond() + opaque +{ + var a: Seq := [10, 20]; + var b: Seq := [30]; + var c: Seq := Sequence.append(a, b); + assert c[2] == 30 +}; + +// Take length +procedure takeLength() + opaque +{ + var s: Seq := [10, 20, 30, 40]; + var t: Seq := Sequence.take(s, 2); + assert Sequence.length(t) == 2 +}; + +// Take preserves elements +procedure takeSelect() + opaque +{ + var s: Seq := [10, 20, 30, 40]; + var t: Seq := Sequence.take(s, 2); + assert t[0] == 10; + assert t[1] == 20 +}; + +// Drop length +procedure dropLength() + opaque +{ + var s: Seq := [10, 20, 30, 40]; + var d: Seq := Sequence.drop(s, 2); + assert Sequence.length(d) == 2 +}; + +// Drop selects from offset +procedure dropSelect() + opaque +{ + var s: Seq := [10, 20, 30, 40]; + var d: Seq := Sequence.drop(s, 2); + assert d[0] == 30; + assert d[1] == 40 +}; +#end + +/-! Negative cases: misuses of Seq flagged by ValidateSubscriptUsage. -/ + +#eval testLaurel +#strata +program Laurel; +// Diagnostic 2: destructive update on Seq +procedure seqDestructiveUpdate() + opaque +{ + var s: Seq := [1, 2, 3]; + s[0] := 42 +//^^^^^^^^^^ error: immutable +}; +#end + +/-! Out-of-bounds: verification fails when an index cannot be shown to be in +range. Pins the end-to-end wiring of the bounds preconditions on +`Sequence.select` (Lt bound) and `Sequence.take` (Le bound). +Error ranges are wider than the offending expression because Core does +not yet propagate expression-level source locations through PrecondElim +(same caveat as `DivisionByZeroCheckTest.lean`). -/ + +#eval testLaurel +#strata +program Laurel; +procedure outOfBoundsRead() + opaque +{ + var s: Seq := [10, 20]; + var x: int := s[5] +//^^^^^^^^^^^^^^^^^^ error: could not be proved +}; +#end + +#eval testLaurel +#strata +program Laurel; +procedure outOfBoundsTake() + opaque +{ + var s: Seq := [10, 20]; + var t: Seq := Sequence.take(s, 3) +//^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ error: could not be proved +}; +#end + +/-! Negative-test grid: ensure the validator's stmt-position dispatch arms +for IfThenElse and While bodies fire correctly. The expression-position +diagnostics are covered by the existing tests above; these exercise the +separate `_htsub` / `_hbsub` arms in `validateStmtExpr`. -/ + +#eval testLaurel +#strata +program Laurel; +procedure seqDestructiveInIf(c: bool) + opaque +{ + var s: Seq := [1, 2, 3]; + if c then s[0] := 42 +// ^^^^^^^^^^ error: immutable +}; +#end + +#eval testLaurel +#strata +program Laurel; +procedure seqDestructiveInWhile() + opaque +{ + var s: Seq := [1, 2, 3]; + var i: int := 0; + while (i < 3) s[i] := 0 +// ^^^^^^^^^ error: immutable +}; +#end + +#eval testLaurel +#strata +program Laurel; +// A non-int subscript index is a type error (index is checked against int). +procedure seqIndexNotInt(s: Seq) returns (r: int) + opaque +{ + r := s[true] +// ^^^^ error: expected 'int' +}; +#end + +#eval testLaurel +#strata +program Laurel; +// A functional update whose value disagrees with the element type is a type +// error (the value is checked against the sequence's element type). +procedure seqUpdateWrongElem(s: Seq) returns (t: Seq) + opaque +{ + t := s[0 := true] +// ^^^^ error: expected 'int' +}; +#end + +#eval testLaurel +#strata +program Laurel; +// Subscripting a concrete non-collection target is a type error: the element +// type only exists for Seq/Array, so the target must be one of those. +procedure subscriptNonCollection() returns (r: int) + opaque +{ + var x: int := 5; + r := x[0] +// ^^^^ error: expected a sequence or array +}; +#end diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T25_Arrays.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T25_Arrays.lean new file mode 100644 index 0000000000..47c0e54183 --- /dev/null +++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T25_Arrays.lean @@ -0,0 +1,261 @@ +/- + Copyright Strata Contributors + + SPDX-License-Identifier: Apache-2.0 OR MIT +-/ + +import StrataTest.Util.TestLaurel + +open StrataTest.Util +open Strata + +#eval testLaurel +#strata +program Laurel; +// Basic read/write +procedure basicReadWrite() + opaque +{ + var a: Array := [1, 2, 3]; + a[0] := 42; + assert a[0] == 42 +}; + +// Length +procedure length() + opaque +{ + var a: Array := [10, 20, 30]; + assert Array.length(a) == 3 +}; + +// Empty array +procedure emptyArray() + opaque +{ + var a: Array := []; + assert Array.length(a) == 0 +}; + +// Array in contracts +procedure arrayContract(a: Array) + requires Array.length(a) > 0 + opaque +{ + var x: int := a[0]; + assert x == a[0] +}; + +// Multiple writes +procedure multipleWrites() + opaque +{ + var a: Array := [0, 0, 0]; + a[0] := 10; + a[1] := 20; + a[2] := 30; + assert a[0] == 10; + assert a[1] == 20; + assert a[2] == 30 +}; + +// Aliasing: mutation through one reference visible through another +procedure aliasing() + opaque +{ + var a: Array := [1, 2, 3]; + var b: Array := a; + b[0] := 99; + assert a[0] == 99 +}; + +// Array in a loop: zero-fill +procedure arrayLoop() + opaque + modifies * +{ + var a: Array := [1, 2, 3]; + var i: int := 0; + while (i < 3) + invariant 0 <= i && i <= 3 + invariant Array.length(a) == 3 + invariant forall(j: int) => 0 <= j && j < i ==> a[j] == 0 + { + a[i] := 0; + i := i + 1 + }; + assert a[0] == 0; + assert a[1] == 0; + assert a[2] == 0 +}; + +// Inter-procedural: callee modifies array +procedure setFirst(a: Array, v: int) + requires Array.length(a) > 0 + opaque + ensures Array.length(a) > 0 + ensures a[0] == v + modifies a +{ + a[0] := v +}; + +procedure callSetFirst() + opaque +{ + var a: Array := [1, 2, 3]; + setFirst(a, 42); + assert a[0] == 42 +}; + +// Sequence.fromArray takes a snapshot of the array's current contents. +procedure fromArrayBasic() + opaque +{ + var a: Array := [10, 20, 30]; + var s: Seq := Sequence.fromArray(a); + assert Sequence.length(s) == 3; + assert s[0] == 10 +}; + +// Snapshot semantics: mutating the array after extraction does not +// affect the previously-taken sequence. +procedure fromArraySnapshot() + opaque +{ + var a: Array := [1, 2, 3]; + var s: Seq := Sequence.fromArray(a); + a[0] := 99; + assert s[0] == 1; + assert a[0] == 99 +}; +#end + +/-! Negative cases: misuses of Array flagged by ValidateSubscriptUsage. -/ + +#eval testLaurel +#strata +program Laurel; +// Diagnostic 1: functional update on Array +procedure arrayFuncUpdate() + opaque +{ + var a: Array := [1, 2, 3]; + var b: Array := a[0 := 99] +// ^^^^^^^^^^ error: not supported on `Array +}; +#end + +#eval testLaurel +#strata +program Laurel; +// Diagnostic 3: Array.length on a non-Array argument +procedure arrayLengthWrongArg() + opaque +{ + var s: Seq := [1, 2, 3]; + assert Array.length(s) == 3 +// ^^^^^^^^^^^^^^^ error: requires an argument of type +}; +#end + +#eval testLaurel +#strata +program Laurel; +// Diagnostic 4: Array with T other than int +procedure arrayNonIntElement() + opaque +{ + var a: Array := [true, false] +// ^^^^^^^^^^^ error: currently only supported +}; +#end + +#eval testLaurel +#strata +program Laurel; +// Sequence.fromArray on a non-Array argument +procedure fromArrayWrongArg() + opaque +{ + var s: Seq := [1, 2, 3]; + var t: Seq := Sequence.fromArray(s) +// ^^^^^^^^^^^^^^^^^^^^^ error: requires an argument of type +}; +#end + +/-! Diagnostic 4 in *parameter* position. The variable-declaration form is +already covered by `arrayNonIntElement`; this exercises the separate +`validateProcedure → validateHighType` entry on `proc.inputs`. -/ + +#eval testLaurel +#strata +program Laurel; +procedure arrayNonIntParameter(a: Array) +// ^^^^^^^^^^^ error: currently only supported + opaque +{ +}; +#end + +/-! Arity diagnostics: `Array.length` and `Sequence.fromArray` each take +exactly one argument. Calls with a different arity get a dedicated +diagnostic before the user sees a Core type-checker unification error. -/ + +#eval testLaurel +#strata +program Laurel; +procedure arrayLengthWrongArity() + opaque +{ + var a: Array := [1, 2, 3]; + assert Array.length(a, a) == 3 +// ^^^^^^^^^^^^^^^^^^ error: takes exactly one argument +}; +#end + +#eval testLaurel +#strata +program Laurel; +procedure fromArrayWrongArity() + opaque +{ + var a: Array := [1, 2, 3]; + var t: Seq := Sequence.fromArray(a, a) +// ^^^^^^^^^^^^^^^^^^^^^^^^ error: takes exactly one argument +}; +#end + +/-! A `while` whose body is a single `a[i] := v` (no braces) takes the +`_hbsub` dispatch arm in `SubscriptElim.elimExpr.While`. With braces +the body is a `.Block` and goes through the `.Block` arm instead. +Pinning this case ensures the bare-stmt path stays correct. -/ + +#eval testLaurel +#strata +program Laurel; +procedure arraySingleStmtWhile() + opaque + modifies * +{ + var a: Array := [1, 2, 3]; + var i: int := 0; + while (i < 3) invariant 0 <= i && i <= 3 invariant Array.length(a) == 3 a[i] := 0; + assert a[0] == 0 +}; +#end + +#eval testLaurel +#strata +program Laurel; +// A destructive write whose value disagrees with the element type is a type +// error (the value is checked against the array's element type). +procedure arrayWriteWrongElem() + opaque + modifies * +{ + var a: Array := [1, 2, 3]; + a[0] := true +// ^^^^ error: expected 'int' +}; +#end diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T26_MixedSeqFields.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T26_MixedSeqFields.lean new file mode 100644 index 0000000000..03dcda1ad8 --- /dev/null +++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T26_MixedSeqFields.lean @@ -0,0 +1,33 @@ +/- + Copyright Strata Contributors + + SPDX-License-Identifier: Apache-2.0 OR MIT +-/ + +import StrataTest.Util.TestLaurel + +open StrataTest.Util +open Strata + +/-! Regression: two `Seq` fields with different `T` on the same composite +must produce distinct Box constructor names in HeapParameterization. +Before the fix, both shared the name "BoxSeq" and Core type-checking +failed on the element-type mismatch. After the fix the name encodes the +element type (`BoxSeq_int`, `BoxSeq_bool`, ...). -/ + +#eval testLaurel +#strata +program Laurel; +composite Both { + var a: Seq + var b: Seq +} + +procedure touch(x: Both) + opaque + modifies x +{ + x#a := [1]; + x#b := [true] +}; +#end diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T27_ArrayInDatatype.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T27_ArrayInDatatype.lean new file mode 100644 index 0000000000..34dd33d530 --- /dev/null +++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T27_ArrayInDatatype.lean @@ -0,0 +1,78 @@ +/- + Copyright Strata Contributors + + SPDX-License-Identifier: Apache-2.0 OR MIT +-/ + +import StrataTest.Util.TestLaurel + +open StrataTest.Util +open Strata + +/-! `Array` is allowed as a datatype constructor argument. Because an array +is a heap reference, a datatype that stores one compares by reference on +that field: two datatype values built from the *same* array are equal, +while two values built from *different* arrays are not — even if those +arrays have identical contents. + +Same array in both wrappers ⇒ the datatype values are equal. -/ + +#eval testLaurel +#strata +program Laurel; +datatype Wrapped { + Wrap(arr: Array) +} + +procedure cmp() + opaque +{ + var a: Array := [1, 2, 3]; + var w1: Wrapped := Wrap(a); + var w2: Wrapped := Wrap(a); + assert w1 == w2 +}; +#end + +/-! Different arrays, even with identical contents, are distinct references, so +the wrapping datatype values are not equal. -/ + +#eval testLaurel +#strata +program Laurel; +datatype Wrapped { + Wrap(arr: Array) +} + +procedure cmp() + opaque +{ + var a1: Array := [1, 2, 3]; + var a2: Array := [1, 2, 3]; + var w1: Wrapped := Wrap(a1); + var w2: Wrapped := Wrap(a2); + assert w1 != w2 +}; +#end + +/-! Contrast: a `Seq` constructor argument has value semantics — two +datatype values built from equal sequences are equal regardless of how the +sequences were constructed. -/ + +#eval testLaurel +#strata +program Laurel; +datatype WrappedSeq { + WrapSeq(items: Seq) +} + +procedure constructAndCompare() + opaque +{ + var s1: Seq := [1, 2, 3]; + var s2: Seq := [1, 2, 3]; + var w1: WrappedSeq := WrapSeq(s1); + var w2: WrappedSeq := WrapSeq(s2); + assert w1 == w2 +}; +#end diff --git a/StrataTest/Languages/Laurel/SubscriptElimConstantsTest.lean b/StrataTest/Languages/Laurel/SubscriptElimConstantsTest.lean new file mode 100644 index 0000000000..2fab233c7f --- /dev/null +++ b/StrataTest/Languages/Laurel/SubscriptElimConstantsTest.lean @@ -0,0 +1,76 @@ +/- + Copyright Strata Contributors + + SPDX-License-Identifier: Apache-2.0 OR MIT +-/ +module + +/- +Tests that `subscriptElim` walks `program.constants` initializers, +rewriting subscripts there in addition to procedure bodies. + +Constants with subscript-bearing initializers cannot currently be parsed +from Laurel grammar text, so this test constructs a program +programmatically — same pattern as `TypeAliasElimTest.lean`. + +Latent today (no grammar path produces such constants), but defensive: the +walk was added to address a review comment, and this test pins that +contract so future grammar additions cannot regress it silently. +-/ + +meta import Strata.Languages.Laurel.SubscriptElim +meta import Strata.Languages.Laurel.Resolution + +meta section + +open Strata.Laurel + +private def mkTy (ty : HighType) : HighTypeMd := { val := ty, source := none } +private def mkE (e : StmtExpr) : StmtExprMd := { val := e, source := none } + +-- A constant `c : int := s[0]` where `s` is a sequence built inline. +-- After `subscriptElim`, the initializer should no longer contain a +-- `.Subscript` — it should be rewritten to `Sequence.select(..., 0)`. +private def constantWithSubscript : Program := + let buildEmpty := mkE (.StaticCall (mkId SeqOp.empty) []) + let buildOne := mkE (.StaticCall (mkId SeqOp.build) [buildEmpty, mkE (.LiteralInt 10)]) + let seqLit := mkE (.StaticCall (mkId SeqOp.build) [buildOne, mkE (.LiteralInt 20)]) + -- Subscript: seqLit[0] + let subscriptInit := mkE (.Subscript seqLit (mkE (.LiteralInt 0)) none) + { staticProcedures := [] + staticFields := [] + types := [] + constants := [{ + name := mkId "c" + type := mkTy .TInt + initializer := some subscriptInit }] } + +/-- Returns `true` if any `.Subscript` survives in the initializer. -/ +private partial def hasSubscript (e : StmtExprMd) : Bool := + match e.val with + | .Subscript _ _ _ => true + | .StaticCall _ args => args.any hasSubscript + | .Block stmts _ => stmts.any hasSubscript + | .Var (.Field t _) => hasSubscript t + | .IfThenElse c t e => + hasSubscript c || hasSubscript t || (e.map hasSubscript).getD false + | _ => false + +-- The initializer should still be a `.StaticCall` to `Sequence.select`, +-- and `hasSubscript` should report `false`. +/-- +info: subscript eliminated +-/ +#guard_msgs in +#eval! do + let model := (resolve constantWithSubscript).model + let (program', _) := subscriptElim model constantWithSubscript + match program'.constants with + | [{ initializer := some init, .. }] => + if hasSubscript init then + IO.println "BUG: subscript still present" + else + IO.println "subscript eliminated" + | _ => IO.println "BUG: unexpected constants shape" + +end diff --git a/docs/verso/LaurelDoc.lean b/docs/verso/LaurelDoc.lean index 4de8a96ba4..5ca7eb7b7e 100644 --- a/docs/verso/LaurelDoc.lean +++ b/docs/verso/LaurelDoc.lean @@ -275,6 +275,222 @@ type. Algebraic datatypes can be encoded using composite and constrained types. {docstring Strata.Laurel.TypeDefinition} +# Sequences and Arrays +%%% +tag := "sec-sequences-arrays" +%%% + +Laurel provides two collection types that share a subscript syntax but differ in their +semantics: + +- `Seq` — immutable value sequences. Operations like functional update produce new + sequences, leaving the input unchanged. +- `Array` — mutable, heap-backed arrays. + +Their equality and aliasing behaviour is covered under [Equality and aliasing](#equality-and-aliasing) below. + +Currently `Array` is supported only for `T = int`; other element types are +rejected by the pre-pass validator. `Seq` supports any element type. + +## Sequence literals + +Square-bracket literals construct a `Seq`: + +``` +var s: Seq := [1, 2, 3]; +``` + +The empty literal `[]` produces `Sequence.empty()`. + +## Subscript syntax + +The expression `s[i]` reads the element at index `i`: + +``` +assert s[0] == 1; +``` + +On a `Seq`, `s[i := v]` produces a new sequence with index `i` set to `v`: + +``` +var t: Seq := s[0 := 99]; // t differs from s at index 0 +``` + +On an `Array`, `a[i] := v` updates the array in place: + +``` +var a: Array := [1, 2, 3]; +a[0] := 42; +assert a[0] == 42; +``` + +Out-of-bounds access is a proof obligation. `Sequence.select`, +`Sequence.update`, `Sequence.take`, and `Sequence.drop` carry preconditions +that the index or length argument is in range; the subscript sugar inherits +them. A proof obligation is generated at each subscript site — both +in imperative code and in pure positions like `requires`/`ensures` clauses, +quantifier bodies, and function bodies. If the index cannot be shown to be +in bounds, verification fails with an `outOfBoundsAccess` diagnostic. This +matches how division by zero is checked. + +## Sequence operations + +The `Sequence` namespace exposes the following operations: + +- `Sequence.empty()` — the empty sequence +- `Sequence.build(s, v)` — append `v` to the end of `s` +- `Sequence.select(s, i)` — read index `i`; equivalent to `s[i]` +- `Sequence.update(s, i, v)` — functional update; equivalent to `s[i := v]` +- `Sequence.length(s)` — length +- `Sequence.append(s1, s2)` — concatenate two sequences +- `Sequence.contains(s, v)` — membership test +- `Sequence.take(s, n)` — prefix of length `n` +- `Sequence.drop(s, n)` — suffix after the first `n` elements + +## Array length + +`Array.length(a)` returns the length of an array. It requires its argument to be +of type `Array`. + +## Array to sequence conversion + +`Sequence.fromArray(a)` returns a `Seq` snapshot of an `Array`'s current +contents. The snapshot is independent: subsequent mutations to the array are +not reflected in the returned sequence. + +``` +var a: Array := [1, 2, 3]; +var s: Seq := Sequence.fromArray(a); +a[0] := 99; +assert s[0] == 1; // the snapshot still holds the original value +assert a[0] == 99; +``` + +This is the supported idiom for extracting values out of an array. Laurel does +not support implicit `Array` → `Seq` conversion, nor the reverse: there is +no `Seq` → `Array` conversion. Construct an array directly from a literal, +e.g. `var a: Array := [1, 2, 3]`. + +## Common mistakes + +A pre-pass validator flags five common misuses with helpful messages: + +- Using `a[i := v]` (functional update) on an `Array`: + + ``` + var a: Array := [1, 2, 3]; + var b: Array := a[0 := 99]; + // ~~~~~~~~~~ + // error: `a[i := v]` is not supported on `Array`: arrays are mutable. + ``` + +- Using `s[i] := v` (destructive update) on a `Seq`: + + ``` + var s: Seq := [1, 2, 3]; + s[0] := 42; + // ~~~~ + // error: `s[i] := v` is not allowed: sequences (`Seq`) are immutable. + ``` + +- Calling `Array.length` on something that is not an `Array`: + + ``` + var s: Seq := [1, 2, 3]; + assert Array.length(s) == 3; + // ~~~~~~~~~~~~~~~ + // error: `Array.length` requires an argument of type `Array`, got `Seq`. + ``` + +- Calling `Sequence.fromArray` on something that is not an `Array`: + + ``` + var s: Seq := [1, 2, 3]; + var t: Seq := Sequence.fromArray(s); + // ~~~~~~~~~~~~~~~~~~~~~ + // error: `Sequence.fromArray` requires an argument of type `Array`, + // got `Seq`. + ``` + +- Declaring `Array` with a `T` other than `int` (not yet implemented at the + Laurel layer): + + ``` + var a: Array := [true, false]; + // ~~~~~~~~~~~ + // error: `Array` is currently only supported for `T = int`. + ``` + +## Internal representation + +Arrays are represented internally by a synthetic `$Array` composite with a single +`$data: Seq` field (the `int` element type matches the current +`Array`-only restriction). The `$` prefix is a naming convention used for +compiler-internal names to avoid collisions with user-declared types. The +`$Array` composite is only injected into programs that actually use `Array`. + +## Equality and aliasing +%%% +tag := "equality-and-aliasing" +%%% + +`Seq` has *value* semantics and `Array` has *reference* semantics, and +this is what distinguishes the two types. + +A `Seq` is compared by content: two sequences are equal exactly when they +hold the same elements, regardless of how each was constructed. Sequences are +immutable, so there is no aliasing to worry about. + +An `Array` is a heap reference. Assigning an array to a new variable creates +an *alias* — both names refer to the same underlying array, so a mutation +through one is visible through the other — and `==` compares *identity*, not +contents: + +``` +var a1: Array := [1, 2, 3]; +var b: Array := a1; // alias of a1 +b[0] := 99; +assert a1[0] == 99; // mutation visible through a1 +assert a1 == b; // holds: same reference + +var a2: Array := [1, 2, 3]; +assert a1 != a2; // holds: distinct references, equal contents +``` + +### Arrays in datatypes + +`Array` may be used as a datatype constructor argument: + +``` +datatype Wrapped { Wrap(arr: Array) } +``` + +Reference semantics carry through the field: a datatype value that stores an +array compares by reference on that field. Two values built from the same +array are equal; two built from distinct arrays are not, even with identical +contents: + +``` +var a1: Array := [1, 2, 3]; +var a2: Array := [1, 2, 3]; +var w1: Wrapped := Wrap(a1); +var w2: Wrapped := Wrap(a1); // same array as w1 +var w3: Wrapped := Wrap(a2); // distinct array, equal contents +assert w1 == w2; // holds: same reference +assert w1 != w3; // holds: different references +``` + +For a datatype field with value semantics, store a `Seq` instead — take a +snapshot of the array's contents with `Sequence.fromArray(arr)`: + +``` +datatype WrappedSeq { WrapSeq(items: Seq) } +// ... +var w1: WrappedSeq := WrapSeq(Sequence.fromArray(a1)); +var w2: WrappedSeq := WrapSeq(Sequence.fromArray(a2)); +assert w1 == w2; // holds when a1, a2 have equal contents +``` + # Expressions and Statements Laurel uses a unified `StmtExpr` type that contains both expression-like and statement-like @@ -419,6 +635,7 @@ The Index below links to each construct's subsection. \[⇒\] Op-Arith, \[⇒\] Op-Concat; \[⇐\] Op-Arith, \[⇐\] Op-Bool - {ref "rules-object-forms"}[*Object forms*] — \[⇒\] New-Ok, \[⇒\] New-Fallback; \[⇒\] AsType; \[⇒\] IsType; \[⇒\] RefEq; \[⇒\] PureFieldUpdate +- {ref "rules-subscript"}[*Subscript*] — \[⇒\] Subscript-Read, \[⇒\] Subscript-Update, \[⇒\] SubscriptWrite - {ref "rules-verification-expressions"}[*Verification expressions*] — \[⇒\] Quantifier, \[⇒\] Assigned, \[⇐\] Old, \[⇒\] Old-Synth, \[⇒\] Fresh, \[⇐\] ProveBy, \[⇒\] ProveBy-Synth - {ref "rules-self-reference"}[*Self reference*] — \[⇒\] This-Inside, \[⇒\] This-Outside @@ -829,6 +1046,60 @@ $$`\frac{\Gamma \vdash \mathit{target} \Rightarrow T_t \quad \Gamma(f) = T_f \qu {docstring Strata.Laurel.Resolution.Synth.pureFieldUpdate} +### Subscript +%%% +tag := "rules-subscript" +%%% + +The {ref "sec-sequences-arrays"}[*sequence and array*] subscript forms. The +read `s[i]` and functional update `s[i := v]` are values; the destructive write +`a[i] := v` is a statement. In each, the *element type* $`U` is the only thing +needed from the target: the index is checked against $`\mathsf{TInt}` and the +update/written value against $`U`, so `a[0] := true` on an `Array` is +rejected here. The remaining $`\mathsf{Seq}`/$`\mathsf{Array}` misuse rules and +bounds-safety obligations are handled by +{name Strata.Laurel.validateSubscriptUsage}`ValidateSubscriptUsage` and +{name Strata.Laurel.subscriptElimPass}`SubscriptElim`, not here. + +The element type is computed by a total $`\mathsf{elem}(T)` metafunction that +also decides whether the target is indexable at all. Three cases: + +- $`\mathsf{unfold}\;T` is $`\mathsf{Seq}\;U` or $`\mathsf{Array}\;U`: + $`\mathsf{elem}(T) = U`. +- $`T` is *gradual* — $`\mathsf{Unknown}` (an unresolved name or hole) or + $`\mathsf{TCore}` — : $`\mathsf{elem}(T) = \mathsf{Unknown}`, tolerated + silently. The index and value checks are then vacuous (anything is consistent + with $`\mathsf{Unknown}`) and a read synthesizes $`\mathsf{Unknown}`, so no + cascading error piles on top of the name-resolution error that was already + reported. +- $`T` is any *concrete* non-collection (e.g. $`\mathsf{TInt}`, a composite, a + $`\mathsf{Map}`): the subscript is rejected with `expected a sequence or + array`, and $`\mathsf{elem}(T) = \mathsf{Unknown}` is returned only to + suppress follow-on errors on the index and value. This mirrors how + $`\mathsf{Fresh}` / $`\mathsf{RefEq}` reject a concrete non-reference target + while letting $`\mathsf{Unknown}` flow. + +Only the concrete-non-collection case emits a diagnostic; the gradual case is +the $`\mathsf{New}`-$`\mathsf{Fallback}`-style escape hatch. + +$$`\frac{\Gamma \vdash \mathit{target} \Rightarrow T \quad \Gamma \vdash i \Leftarrow \mathsf{TInt}}{\Gamma \vdash \mathsf{Subscript}\;\mathit{target}\;i\;\mathsf{none} \Rightarrow \mathsf{elem}(T)} \quad \text{([⇒] Subscript-Read)}` + +$$`\frac{\Gamma \vdash \mathit{target} \Rightarrow T \quad \Gamma \vdash i \Leftarrow \mathsf{TInt} \quad \Gamma \vdash v \Leftarrow \mathsf{elem}(T)}{\Gamma \vdash \mathsf{Subscript}\;\mathit{target}\;i\;(\mathsf{some}\;v) \Rightarrow T} \quad \text{([⇒] Subscript-Update)}` + +{docstring Strata.Laurel.Resolution.Synth.subscript} + +$$`\frac{\Gamma \vdash \mathit{target} \Rightarrow T \quad \Gamma \vdash i \Leftarrow \mathsf{TInt} \quad \Gamma \vdash v \Leftarrow \mathsf{elem}(T)}{\Gamma \vdash \mathsf{SubscriptWrite}\;\mathit{target}\;i\;v \Rightarrow \mathsf{TVoid}} \quad \text{([⇒] SubscriptWrite)}` + +{docstring Strata.Laurel.Resolution.Check.subscriptWrite} + +Sequence/array literals and operations (`[…]`, `Sequence.select`, +`Array.length`, …) desugar to calls on polymorphic primitives, typed by the +{ref "rules-calls"}[*Calls*] escape hatch in +{name Strata.Laurel.Resolution.Synth.staticCall}`Synth.staticCall`: their result +type is inferred structurally from the arguments rather than checked against the +primitives' placeholder `int` signatures (so `[1, 2, 3]` synthesizes +`Seq`). + ### Verification expressions %%% tag := "rules-verification-expressions"