Add more operators, while statement and quantifiers

Strata/DDM/Parser.lean

@@ -227,17 +227,19 @@ private partial def whitespace : ParserFn := fun c s =>
       let j    := c.next' i h
       let curr := c.get j
       match curr with
-      | '/' =>
-        match c.tokens.matchPrefix c.inputString i with
-        | some _ => s
-        | none =>
-          andthenFn (takeUntilFn (fun c => c = '\n')) whitespace c (s.next c j)
-      | '*' =>
-        match c.tokens.matchPrefix c.inputString i with
-        | some _ => s
-        | none =>
-          let j := c.next j
-          andthenFn (finishCommentBlock (pushMissingOnError := false)) whitespace c (s.next c j)
+      | '/' => Id.run do
+        -- Treat // as comment unless a token covering both chars exists (e.g., //@pre)
+        if let some tk := c.tokens.matchPrefix c.inputString i then
+          if tk.utf8ByteSize >= 2 then
+            return s
+        andthenFn (takeUntilFn (fun c => c = '\n')) whitespace c (s.next c j)
+      | '*' => Id.run do
+        -- Treat /* as comment unless a token covering both chars exists
+        if let some tk := c.tokens.matchPrefix c.inputString i then
+          if tk.utf8ByteSize >= 2 then
+            return s
+        andthenFn (finishCommentBlock (pushMissingOnError := false))
+          whitespace c (s.next c (c.next j))
       | _ =>
         s
     else s

Strata/DL/Lambda/IntBoolFactory.lean

@@ -118,6 +118,38 @@ def intModFunc : LFunc T :=
   binaryOp "Int.Mod" .int
   (some cevalIntMod)
 
+-- Truncating division: rounds toward zero (unlike Euclidean division which floors)
+-- Int.tdiv in Lean4
+def cevalIntDivT (m:T.Metadata) (args : List (LExpr T.mono)) : Option (LExpr T.mono) :=
+  match args with
+  | [e1, e2] =>
+    let e1i := LExpr.denoteInt e1
+    let e2i := LExpr.denoteInt e2
+    match e1i, e2i with
+    | some x, some y =>
+      if y == 0 then .none else .some (.intConst m (x.tdiv y))
+    | _, _ => .none
+  | _ => .none
+
+def cevalIntModT (m:T.Metadata) (args : List (LExpr T.mono)) : Option (LExpr T.mono) :=
+  match args with
+  | [e1, e2] =>
+    let e1i := LExpr.denoteInt e1
+    let e2i := LExpr.denoteInt e2
+    match e1i, e2i with
+    | some x, some y =>
+      if y == 0 then .none else .some (.intConst m (x.tmod y))
+    | _, _ => .none
+  | _ => .none
+
+def intDivTFunc : LFunc T :=
+  binaryOp "Int.DivT" .int
+  (some cevalIntDivT)
+
+def intModTFunc : LFunc T :=
+  binaryOp "Int.ModT" .int
+  (some cevalIntModT)
+
 def intNegFunc : LFunc T :=
   unaryOp "Int.Neg" .int
   (some (unOpCeval Int Int (@intConst T.mono) LExpr.denoteInt Int.neg))
@@ -166,6 +198,8 @@ def IntBoolFactory : @Factory T :=
     intMulFunc,
     intDivFunc,
     intModFunc,
+    intDivTFunc,
+    intModTFunc,
     intNegFunc,
     intLtFunc,
     intLeFunc,

Strata/Languages/Core/Factory.lean

@@ -403,6 +403,8 @@ def Factory : @Factory CoreLParams := #[
   @intMulFunc CoreLParams _,
   @intDivFunc CoreLParams _,
   @intModFunc CoreLParams _,
+  @intDivTFunc CoreLParams _,
+  @intModTFunc CoreLParams _,
   @intNegFunc CoreLParams _,
 
   @intLtFunc CoreLParams _,
@@ -508,6 +510,8 @@ def intSubOp : Expression.Expr := (@intSubFunc CoreLParams _).opExpr
 def intMulOp : Expression.Expr := (@intMulFunc CoreLParams _).opExpr
 def intDivOp : Expression.Expr := (@intDivFunc CoreLParams _).opExpr
 def intModOp : Expression.Expr := (@intModFunc CoreLParams _).opExpr
+def intDivTOp : Expression.Expr := (@intDivTFunc CoreLParams _).opExpr
+def intModTOp : Expression.Expr := (@intModTFunc CoreLParams _).opExpr
 def intNegOp : Expression.Expr := (@intNegFunc CoreLParams _).opExpr
 def intLtOp : Expression.Expr := (@intLtFunc CoreLParams _).opExpr
 def intLeOp : Expression.Expr := (@intLeFunc CoreLParams _).opExpr

Strata/Languages/Core/FactoryWF.lean

@@ -48,6 +48,8 @@ theorem Factory_wf :
             try unfold binOpCeval
             try unfold cevalIntDiv
             try unfold cevalIntMod
+            try unfold cevalIntDivT
+            try unfold cevalIntModT
             try unfold bvUnaryOp
             try unfold bvBinaryOp
             try unfold bvShiftOp

Strata/Languages/Core/SMTEncoder.lean

@@ -350,6 +350,39 @@ partial def toSMTOp (E : Env) (fn : CoreIdent) (fnty : LMonoTy) (ctx : SMT.Conte
     | "Int.Mul"      => .ok (.app Op.mul,        .int ,   ctx)
     | "Int.Div"      => .ok (.app Op.div,        .int ,   ctx)
     | "Int.Mod"      => .ok (.app Op.mod,        .int ,   ctx)
+    -- Truncating division: tdiv(a,b) = let q = ediv(abs(a), abs(b)) in ite(a*b >= 0, q, -q)
+    | "Int.DivT"     =>
+      let divTApp := fun (args : List Term) (retTy : TermType) =>
+        match args with
+        | [a, b] =>
+          let zero := Term.prim (.int 0)
+          let ab := Term.app Op.mul [a, b] retTy
+          let abGeZero := Term.app Op.ge [ab, zero] .bool
+          let absA := Term.app Op.abs [a] retTy
+          let absB := Term.app Op.abs [b] retTy
+          let q := Term.app Op.div [absA, absB] retTy
+          let negQ := Term.app Op.neg [q] retTy
+          Factory.ite abGeZero q negQ
+        | _ => Term.app Op.div args retTy
+      .ok (divTApp, .int, ctx)
+    -- Truncating modulo: tmod(a,b) = a - b * tdiv(a,b)
+    -- tdiv(a,b) = let q = ediv(abs(a), abs(b)) in ite(a*b >= 0, q, -q)
+    | "Int.ModT"     =>
+      let modTApp := fun (args : List Term) (retTy : TermType) =>
+        match args with
+        | [a, b] =>
+          let zero := Term.prim (.int 0)
+          let ab := Term.app Op.mul [a, b] retTy
+          let abGeZero := Term.app Op.ge [ab, zero] .bool
+          let absA := Term.app Op.abs [a] retTy
+          let absB := Term.app Op.abs [b] retTy
+          let q := Term.app Op.div [absA, absB] retTy
+          let negQ := Term.app Op.neg [q] retTy
+          let tdivAB := Term.app Op.ite [abGeZero, q, negQ] retTy
+          let bTimesTdiv := Term.app Op.mul [b, tdivAB] retTy
+          Term.app Op.sub [a, bTimesTdiv] retTy
+        | _ => Term.app Op.mod args retTy
+      .ok (modTApp, .int, ctx)
     | "Int.Lt"       => .ok (.app Op.lt,         .bool,   ctx)
     | "Int.Le"       => .ok (.app Op.le,         .bool,   ctx)
     | "Int.Gt"       => .ok (.app Op.gt,         .bool,   ctx)

Strata/Languages/Laurel/Grammar/ConcreteToAbstractTreeTranslator.lean

@@ -136,6 +136,12 @@ instance : Inhabited Procedure where
 def getBinaryOp? (name : QualifiedIdent) : Option Operation :=
   match name with
   | q`Laurel.add => some Operation.Add
+  | q`Laurel.sub => some Operation.Sub
+  | q`Laurel.mul => some Operation.Mul
+  | q`Laurel.div => some Operation.Div
+  | q`Laurel.mod => some Operation.Mod
+  | q`Laurel.divT => some Operation.DivT
+  | q`Laurel.modT => some Operation.ModT
   | q`Laurel.eq => some Operation.Eq
   | q`Laurel.neq => some Operation.Neq
   | q`Laurel.gt => some Operation.Gt
@@ -144,6 +150,13 @@ def getBinaryOp? (name : QualifiedIdent) : Option Operation :=
   | q`Laurel.ge => some Operation.Geq
   | q`Laurel.and => some Operation.And
   | q`Laurel.or => some Operation.Or
+  | q`Laurel.implies => some Operation.Implies
+  | _ => none
+
+def getUnaryOp? (name : QualifiedIdent) : Option Operation :=
+  match name with
+  | q`Laurel.not => some Operation.Not
+  | q`Laurel.neg => some Operation.Neg
   | _ => none
 
 mutual
@@ -215,6 +228,32 @@ partial def translateStmtExpr (arg : Arg) : TransM StmtExprMd := do
       let obj ← translateStmtExpr objArg
       let field ← translateIdent fieldArg
       return mkStmtExprMd (.FieldSelect obj field) md
+    | q`Laurel.while, #[condArg, invSeqArg, bodyArg] =>
+      let cond ← translateStmtExpr condArg
+      let invariants ← match invSeqArg with
+        | .seq _ _ clauses => clauses.toList.mapM fun arg => match arg with
+            | .op invOp => match invOp.name, invOp.args with
+              | q`Laurel.invariantClause, #[exprArg] => translateStmtExpr exprArg
+              | _, _ => TransM.error "Expected invariantClause"
+            | _ => TransM.error "Expected operation"
+        | _ => pure []
+      let body ← translateStmtExpr bodyArg
+      return mkStmtExprMd (.While cond invariants none body) md
+    | q`Laurel.forallExpr, #[nameArg, tyArg, bodyArg] =>
+      let name ← translateIdent nameArg
+      let ty ← translateHighType tyArg
+      let body ← translateStmtExpr bodyArg
+      return mkStmtExprMd (.Forall name ty body) md
+    | q`Laurel.existsExpr, #[nameArg, tyArg, bodyArg] =>
+      let name ← translateIdent nameArg
+      let ty ← translateHighType tyArg
+      let body ← translateStmtExpr bodyArg
+      return mkStmtExprMd (.Exists name ty body) md
+    | _, #[arg0] => match getUnaryOp? op.name with
+      | some primOp =>
+        let inner ← translateStmtExpr arg0
+        return mkStmtExprMd (.PrimitiveOp primOp [inner]) md
+      | none => TransM.error s!"Unknown unary operation: {op.name}"
     | _, #[arg0, arg1] => match getBinaryOp? op.name with
       | some primOp =>
         let lhs ← translateStmtExpr arg0

Strata/Languages/Laurel/Grammar/LaurelGrammar.lean

@@ -9,4 +9,5 @@ import Strata.DDM.Integration.Lean
 
 namespace Strata.Laurel
 
+
 #load_dialect "./LaurelGrammar.st"

Strata/Languages/Laurel/Grammar/LaurelGrammar.st

@@ -1,3 +1,5 @@
+// Changes in this file are not automatically discovered by the build. 
+// Touch LaurelGrammar.lean to trigger the build
 dialect Laurel;
 
 // Types
@@ -36,16 +38,31 @@ op assign (target: StmtExpr, value: StmtExpr): StmtExpr => @[prec(10)] target ":
 
 // Binary operators
 op add (lhs: StmtExpr, rhs: StmtExpr): StmtExpr => @[prec(60), leftassoc] lhs " + " rhs;
-op eq (lhs: StmtExpr, rhs: StmtExpr): StmtExpr => @[prec(40), leftassoc] lhs " == " rhs;
-op neq (lhs: StmtExpr, rhs: StmtExpr): StmtExpr => @[prec(40), leftassoc] lhs " != " rhs;
-op gt (lhs: StmtExpr, rhs: StmtExpr): StmtExpr => @[prec(40), leftassoc] lhs " > " rhs;
-op lt (lhs: StmtExpr, rhs: StmtExpr): StmtExpr => @[prec(40), leftassoc] lhs " < " rhs;
-op le (lhs: StmtExpr, rhs: StmtExpr): StmtExpr => @[prec(40), leftassoc] lhs " <= " rhs;
-op ge (lhs: StmtExpr, rhs: StmtExpr): StmtExpr => @[prec(40), leftassoc] lhs " >= " rhs;
-
-// Logical operators
+op sub (lhs: StmtExpr, rhs: StmtExpr): StmtExpr => @[prec(60), leftassoc] lhs " - " rhs;
+op mul (lhs: StmtExpr, rhs: StmtExpr): StmtExpr => @[prec(70), leftassoc] lhs " * " rhs;
+op div (lhs: StmtExpr, rhs: StmtExpr): StmtExpr => @[prec(70), leftassoc] lhs " / " rhs;
+op mod (lhs: StmtExpr, rhs: StmtExpr): StmtExpr => @[prec(70), leftassoc] lhs " % " rhs;
+op divT (lhs: StmtExpr, rhs: StmtExpr): StmtExpr => @[prec(70), leftassoc] lhs " /t " rhs;
+op modT (lhs: StmtExpr, rhs: StmtExpr): StmtExpr => @[prec(70), leftassoc] lhs " %t " rhs;
+op eq (lhs: StmtExpr, rhs: StmtExpr): StmtExpr => @[prec(40)] lhs " == " rhs;
+op neq (lhs: StmtExpr, rhs: StmtExpr): StmtExpr => @[prec(40)] lhs " != " rhs;
+op gt (lhs: StmtExpr, rhs: StmtExpr): StmtExpr => @[prec(40)] lhs " > " rhs;
+op lt (lhs: StmtExpr, rhs: StmtExpr): StmtExpr => @[prec(40)] lhs " < " rhs;
+op le (lhs: StmtExpr, rhs: StmtExpr): StmtExpr => @[prec(40)] lhs " <= " rhs;
+op ge (lhs: StmtExpr, rhs: StmtExpr): StmtExpr => @[prec(40)] lhs " >= " rhs;
 op and (lhs: StmtExpr, rhs: StmtExpr): StmtExpr => @[prec(30), leftassoc] lhs " && " rhs;
-op or (lhs: StmtExpr, rhs: StmtExpr): StmtExpr => @[prec(25), leftassoc] lhs " || " rhs;
+op or (lhs: StmtExpr, rhs: StmtExpr): StmtExpr => @[prec(20), leftassoc] lhs " || " rhs;
+op implies (lhs: StmtExpr, rhs: StmtExpr): StmtExpr => @[prec(15), rightassoc] lhs " ==> " rhs;
+
+// Unary operators
+op not (inner: StmtExpr): StmtExpr => @[prec(80)] "!" inner;
+op neg (inner: StmtExpr): StmtExpr => @[prec(80)] "-" inner;
+
+// Quantifiers
+op forallExpr (name: Ident, ty: LaurelType, body: StmtExpr): StmtExpr
+  => "forall(" name ": " ty ") => " body:0;
+op existsExpr (name: Ident, ty: LaurelType, body: StmtExpr): StmtExpr
+  => "exists(" name ": " ty ") => " body:0;
 
 // If-else
 category OptionalElse;
@@ -59,6 +76,13 @@ op assume (cond : StmtExpr) : StmtExpr => "assume " cond ";";
 op return (value : StmtExpr) : StmtExpr => "return " value ";";
 op block (stmts : Seq StmtExpr) : StmtExpr => @[prec(1000)] "{" stmts "}";
 
+// While loops
+category InvariantClause;
+op invariantClause (cond: StmtExpr): InvariantClause => "\n  invariant " cond:0;
+
+op while (cond: StmtExpr, invariants: Seq InvariantClause, body: StmtExpr): StmtExpr
+  => "while" "(" cond ")" invariants body:0;
+
 category Parameter;
 op parameter (name: Ident, paramType: LaurelType): Parameter => name ":" paramType;
 

Strata/Languages/Laurel/HeapParameterization.lean

@@ -59,7 +59,7 @@ def collectExpr (expr : StmtExpr) : StateM AnalysisResult Unit := do
   | .IfThenElse c t e => collectExprMd c; collectExprMd t; if let some x := e then collectExprMd x
   | .Block stmts _ => for s in stmts do collectExprMd s
   | .LocalVariable _ _ i => if let some x := i then collectExprMd x
-  | .While c i d b => collectExprMd c; collectExprMd b; if let some x := i then collectExprMd x; if let some x := d then collectExprMd x
+  | .While c invs d b => collectExprMd c; collectExprMd b; for inv in invs do collectExprMd inv; if let some x := d then collectExprMd x
   | .Return v => if let some x := v then collectExprMd x
   | .Assign assignTargets v =>
       -- Check if any target is a field assignment (heap write)
@@ -251,9 +251,9 @@ where
     | .LocalVariable n ty i =>
         let i' ← match i with | some x => some <$> recurse x | none => pure none
         return ⟨ .LocalVariable n ty i', md ⟩
-    | .While c i d b =>
-        let i' ← match i with | some x => some <$> recurse x | none => pure none
-        return ⟨ .While (← recurse c) i' d (← recurse b false), md ⟩
+    | .While c invs d b =>
+        let invs' ← invs.mapM (recurse ·)
+        return ⟨ .While (← recurse c) invs' d (← recurse b false), md ⟩
     | .Return v =>
         let v' ← match v with | some x => some <$> recurse x | none => pure none
         return ⟨ .Return v', md ⟩

Strata/Languages/Laurel/Laurel.lean

@@ -55,7 +55,7 @@ inductive Operation : Type where
   | Eq | Neq
   | And | Or | Not | Implies
   /- Works on Int/Float64 -/
-  | Neg | Add | Sub | Mul | Div | Mod
+  | Neg | Add | Sub | Mul | Div | Mod | DivT | ModT
   | Lt | Leq | Gt | Geq
   deriving Repr
 
@@ -130,9 +130,9 @@ inductive StmtExpr : Type where
   /- The initializer must be set if this StmtExpr is pure -/
   | LocalVariable (name : Identifier) (type : WithMetadata HighType) (initializer : Option (WithMetadata StmtExpr))
   /- While is only allowed in an impure context
-    The invariant and decreases are always pure
+    The invariants and decreases are always pure
   -/
-  | While (cond : WithMetadata StmtExpr) (invariant : Option (WithMetadata StmtExpr))
+  | While (cond : WithMetadata StmtExpr) (invariants : List (WithMetadata StmtExpr))
     (decreases : Option (WithMetadata StmtExpr))
     (body : WithMetadata StmtExpr)
   | Exit (target : Identifier)

Strata/Languages/Laurel/LaurelEval.lean

@@ -252,20 +252,20 @@ partial def eval (expr : StmtExpr) : Eval TypedValue :=
     let tv ← eval valExpr
     withResult (EvalResult.Return tv.val)
   | StmtExpr.Return none => fun env => (EvalResult.Success { val := Value.VVoid, ty := env.returnType }, env)
-  | StmtExpr.While _ none _ _  => withResult <| EvalResult.TypeError "While invariant was not derived"
+  | StmtExpr.While _ [] none _  => withResult <| EvalResult.TypeError "While invariant was not derived"
   | StmtExpr.While _ _ none _  => withResult <| EvalResult.TypeError "While decreases was not derived"
-  | StmtExpr.While condExpr (some invariantExpr) (some decreasedExpr) bodyExpr => do
+  | StmtExpr.While condExpr invariantExprs (some decreasedExpr) bodyExpr => do
     let rec loop : Eval TypedValue := do
       let cond ← eval condExpr
       if (cond.ty.isBool) then
         withResult <| EvalResult.TypeError "Condition must be boolean"
       else if cond.val.asBool! then
-        let invariant ← eval invariantExpr
-        if (invariant.ty.isBool) then
-          withResult <| EvalResult.TypeError "Invariant must be boolean"
-        else if (!invariant.val.asBool!) then
-          withResult <| EvalResult.VerficationError VerificationErrorType.InvariantFailed "While invariant does not hold"
-        else
+        for invariantExpr in invariantExprs do
+          let invariant ← eval invariantExpr
+          if (invariant.ty.isBool) then
+            withResult <| EvalResult.TypeError "Invariant must be boolean"
+          else if (!invariant.val.asBool!) then
+            withResult <| EvalResult.VerficationError VerificationErrorType.InvariantFailed "While invariant does not hold"
         -- TODO handle decreases
           fun env => match eval bodyExpr env with
             | (EvalResult.Success _, env') => loop env'

Strata/Languages/Laurel/LaurelFormat.lean

@@ -24,6 +24,8 @@ def formatOperation : Operation → Format
   | .Mul => "*"
   | .Div => "/"
   | .Mod => "%"
+  | .DivT => "/t"
+  | .ModT => "%t"
   | .Lt => "<"
   | .Leq => "<="
   | .Gt => ">"
@@ -75,8 +77,10 @@ def formatStmtExprVal (s : StmtExpr) : Format :=
       match init with
       | none => ""
       | some e => " := " ++ formatStmtExpr e
-  | .While cond _ _ body =>
-      "while " ++ formatStmtExpr cond ++ " " ++ formatStmtExpr body
+  | .While cond invs _ body =>
+      "while " ++ formatStmtExpr cond ++
+      (if invs.isEmpty then Format.nil else " invariant " ++ Format.joinSep (invs.map formatStmtExpr) "; ") ++
+      " " ++ formatStmtExpr body
   | .Exit target => "exit " ++ Format.text target
   | .Return value =>
       "return" ++