Core.formatProgram to produce round-trip-parseable output for all constructs

Examples/expected/IrrelevantAxioms.removeIrrelevantAxioms.core.st

@@ -1,11 +1,11 @@
 program Core;
 
 function f (x : int) : int;
-axiom [f_positive]: forall __q0 : int :: f(__q0) > 0;
-axiom [f_monotone]: forall __q0 : int :: forall __q1 : int :: __q0 < __q1 ==> f(__q0) < f(__q1);
+axiom [f_positive]: forall x : int :: f(x) > 0;
+axiom [f_monotone]: forall x : int :: forall y : int :: x < y ==> f(x) < f(y);
 function g (x : int) : int;
 function h (x : int) : int;
-axiom [h_def]: forall __q0 : int :: h(__q0) == f(__q0) + 1;
+axiom [h_def]: forall x : int :: h(x) == f(x) + 1;
 procedure TestF (x : int, out result : int)
 spec {
   ensures [result_positive]: result > 0;

Strata/Languages/Core/DDMTransform/ASTtoCST.lean

@@ -195,7 +195,9 @@ def funcToCST {M} [Inhabited M]
     -- Convert preconditions
     let preconds ← precondsToSpecElts func.preconditions
     let bodyExpr ← lexprToExpr body 0
-    let inline? : Ann (Option (Inline M)) M := ⟨default, none⟩
+    let inline? : Ann (Option (Inline M)) M :=
+      if func.attr.any (· == .inline) then ⟨default, some (.inline default)⟩
+      else ⟨default, none⟩
     pure (.command_fndef default name typeArgs b r preconds bodyExpr inline?)
   modify ToCSTContext.popScope
   -- Register function name as free variable.

Strata/Languages/Core/DDMTransform/FormatCore.lean

@@ -37,8 +37,6 @@ Known issues:
   translation in the latter's metadata field and recover them in the future.
 
 - Misc. formatting issues
-  -- Remove extra parentheses around constructors in datatypes, assignments,
-  etc.
   -- Remove extra indentation from the last brace of a block or the `end`
   keyword of a mutual block.
 -/
@@ -295,11 +293,21 @@ def handleZeroaryOps {M} [Inhabited M] (name : String)
   | .re .All => pure (.re_all default)
   | .re .AllChar => pure (.re_allchar default)
   | .re .None => pure (.re_none default)
-  -- TODO: seq_empty is not yet parseable (see Grammar.lean); handle here when added.
   | _ => do
     ToCSTM.logError "lopToExpr" "0-ary op not found" name
     pure (.re_none default)
 
+/-- Convert a bitvector width to the corresponding CoreType, logging an error and
+    falling back to bv64 for unsupported widths. -/
+def bvTypeOfWidth {M} [Inhabited M] (caller : String) (w : Nat) : ToCSTM M (CoreType M) :=
+  match w with
+  | 1 => pure (CoreType.bv1 default) | 8 => pure (.bv8 default)
+  | 16 => pure (.bv16 default) | 32 => pure (.bv32 default)
+  | 64 => pure (.bv64 default)
+  | _ => do
+    ToCSTM.logError caller s!"unsupported BV width {w}" (toString w)
+    pure (.bv64 default)
+
 /-- Handle unary operations -/
 def handleUnaryOps {M} [Inhabited M] (name : String) (arg : CoreDDM.Expr M)
     : ToCSTM M (CoreDDM.Expr M) :=
@@ -338,8 +346,13 @@ def handleUnaryOps {M} [Inhabited M] (name : String) (arg : CoreDDM.Expr M)
   | .bv ⟨16, .SafeNeg⟩ | .bv ⟨16, .SafeUNeg⟩ => pure (.safeneg_expr default (.bv16 default) arg)
   | .bv ⟨32, .SafeNeg⟩ | .bv ⟨32, .SafeUNeg⟩ => pure (.safeneg_expr default (.bv32 default) arg)
   | .bv ⟨64, .SafeNeg⟩ | .bv ⟨64, .SafeUNeg⟩ => pure (.safeneg_expr default (.bv64 default) arg)
-  -- Overflow predicates: approximated as Bool.Not for CST printing
-  | .bv ⟨_, .SNegOverflow⟩ | .bv ⟨_, .UNegOverflow⟩ => pure (.not default arg)
+  -- Overflow predicates
+  | .bv ⟨w, .SNegOverflow⟩ => do
+    let bvTy ← bvTypeOfWidth "handleUnaryOps" w
+    pure (.bv_neg_overflow default bvTy arg)
+  | .bv ⟨w, .UNegOverflow⟩ => do
+    let bvTy ← bvTypeOfWidth "handleUnaryOps" w
+    pure (.bv_uneg_overflow default bvTy arg)
   -- Bitvector extract ops
   | .bvExtract 8 7 7 => pure (.bvextract_7_7 default arg)
   | .bvExtract 16 15 15 => pure (.bvextract_15_15 default arg)
@@ -386,14 +399,14 @@ def bvBinaryOpMap {M} [Inhabited M] :
   (.SafeUAdd, fun ty arg1 arg2 => .safeadd_expr default ty arg1 arg2),
   (.SafeUSub, fun ty arg1 arg2 => .safesub_expr default ty arg1 arg2),
   (.SafeUMul, fun ty arg1 arg2 => .safemul_expr default ty arg1 arg2),
-  -- Overflow predicates: approximated as boolean ops for CST printing
-  (.SAddOverflow, fun _ty arg1 arg2 => .le default _ty arg1 arg2),
-  (.SSubOverflow, fun _ty arg1 arg2 => .le default _ty arg1 arg2),
-  (.SMulOverflow, fun _ty arg1 arg2 => .le default _ty arg1 arg2),
-  (.SDivOverflow, fun _ty arg1 arg2 => .le default _ty arg1 arg2),
-  (.UAddOverflow, fun _ty arg1 arg2 => .le default _ty arg1 arg2),
-  (.USubOverflow, fun _ty arg1 arg2 => .le default _ty arg1 arg2),
-  (.UMulOverflow, fun _ty arg1 arg2 => .le default _ty arg1 arg2)
+  -- Overflow predicates
+  (.SAddOverflow, fun ty arg1 arg2 => .bv_sadd_overflow default ty arg1 arg2),
+  (.SSubOverflow, fun ty arg1 arg2 => .bv_ssub_overflow default ty arg1 arg2),
+  (.SMulOverflow, fun ty arg1 arg2 => .bv_smul_overflow default ty arg1 arg2),
+  (.SDivOverflow, fun ty arg1 arg2 => .bv_sdiv_overflow default ty arg1 arg2),
+  (.UAddOverflow, fun ty arg1 arg2 => .bv_uadd_overflow default ty arg1 arg2),
+  (.USubOverflow, fun ty arg1 arg2 => .bv_usub_overflow default ty arg1 arg2),
+  (.UMulOverflow, fun ty arg1 arg2 => .bv_umul_overflow default ty arg1 arg2)
 ]
 
 /-- Map from bitvector sizes to their corresponding type constructors -/
@@ -551,11 +564,19 @@ partial def lexprToExpr {M} [Inhabited M]
         pure (.fvar default (ctx.allFreeVars.size))
   | .ite _ c t f => liteToExpr c t f qLevel
   | .eq _ e1 e2 => leqToExpr e1 e2 qLevel
-  | .op _ name _ => lopToExpr name.name []
+  | .op _ name ty => do
+    -- seq_empty needs the type annotation to render the explicit type parameter
+    if name.name == "Sequence.empty" then
+      let tyCST ← match ty with
+        | some (.tcons "Sequence" [ety]) => lmonoTyToCoreType ety
+        | _ => pure (CoreType.tvar default unknownTypeVar)
+      pure (.seq_empty default tyCST)
+    else
+      lopToExpr name.name []
   | .app _ _ _ => lappToExpr e qLevel
   | .abs _ prettyName ty body => labsToExpr prettyName ty body (qLevel + 1)
-  | .quant _ qkind _ ty trigger body =>
-    lquantToExpr qkind ty trigger body (qLevel + 1)
+  | .quant _ qkind prettyName ty trigger body =>
+    lquantToExpr qkind prettyName ty trigger body (qLevel + 1)
 
 /-- Extract trigger patterns from Lambda's trigger expression representation -/
 partial def extractTriggerPatterns {M} [Inhabited M]
@@ -609,11 +630,13 @@ partial def labsToExpr {M} [Inhabited M]
   pure (.lambda default tyExpr dl bodyExpr)
 
 partial def lquantToExpr {M} [Inhabited M]
-    (qkind : Lambda.QuantifierKind) (ty : Option Lambda.LMonoTy)
+    (qkind : Lambda.QuantifierKind) (prettyName : String)
+    (ty : Option Lambda.LMonoTy)
     (trigger : Lambda.LExpr CoreLParams.mono) (body : Lambda.LExpr CoreLParams.mono)
     (qLevel : Nat)
     : ToCSTM M (CoreDDM.Expr M) := do
-  let name : Ann String M := ⟨default, mkQuantVarName (qLevel - 1)⟩
+  let varName := if prettyName.isEmpty then mkQuantVarName (qLevel - 1) else prettyName
+  let name : Ann String M := ⟨default, varName⟩
   modify ToCSTContext.pushScope
   modify (·.addScopedBoundVars #[name.val])
   let tyExpr ← match ty with
@@ -661,23 +684,23 @@ partial def leqToExpr {M} [Inhabited M]
 
 partial def lappToExpr {M} [Inhabited M]
     (e : Lambda.LExpr CoreLParams.mono)
-    (qLevel : Nat) (acc : List (CoreDDM.Expr M) := [])
-    : ToCSTM M (CoreDDM.Expr M) :=
-  match e with
-  | .app _ (.app m fn e1) e2 => do
-    let e2Expr ← lexprToExpr e2 qLevel
-    lappToExpr (.app m fn e1) qLevel (e2Expr :: acc)
-  | .app _ (.op _ fn _) e1 => do
-    let e1Expr ← lexprToExpr e1 qLevel
-    lopToExpr fn.name (e1Expr :: acc)
-  | .app _ fn e1 => do
+    (qLevel : Nat)
+    : ToCSTM M (CoreDDM.Expr M) := do
+  let (head, args) := Lambda.getLFuncCall e
+  match head with
+  | .op _ fn _ =>
+    let argExprs ← args.mapM (lexprToExpr · qLevel)
+    lopToExpr fn.name argExprs
+  | .app _ fn arg =>
+    -- getLFuncCall couldn't decompose further (fn is not .app or .op)
     let fnCST ← lexprToExpr fn qLevel
-    let e1Expr ← lexprToExpr e1 qLevel
-    pure <| (e1Expr :: acc).foldl (fun fnAcc arg => .app default fnAcc arg) fnCST
-  | _ => do
-    -- Non-application head (e.g. lambda applied to arguments)
-    let eCST ← lexprToExpr e qLevel
-    pure <| acc.foldl (fun fnAcc arg => .app default fnAcc arg) eCST
+    let argCST ← lexprToExpr arg qLevel
+    let argExprs ← args.mapM (lexprToExpr · qLevel)
+    pure <| (argCST :: argExprs).foldl (fun fnAcc a => .app default fnAcc a) fnCST
+  | _ =>
+    let fnCST ← lexprToExpr head qLevel
+    let argExprs ← args.mapM (lexprToExpr · qLevel)
+    pure <| argExprs.foldl (fun fnAcc arg => .app default fnAcc arg) fnCST
 end
 
 /-- Convert preconditions to CST spec elements -/
@@ -717,7 +740,9 @@ def funcDeclToStatement {M} [Inhabited M] (decl : Imperative.PureFunc Expression
   let paramNames := results.map (·.2)
   let b : Bindings M := .mkBindings default ⟨default, bindings⟩
   let r ← lTyToCoreType decl.output
-  let inline? : Ann (Option (Inline M)) M := ⟨default, none⟩
+  let inline? : Ann (Option (Inline M)) M :=
+    if decl.attr.any (· == .inline) then ⟨default, some (.inline default)⟩
+    else ⟨default, none⟩
   -- Add formals to the context
   modify (·.addScopedBoundVars (reverse? := false) paramNames)
   -- Convert preconditions
@@ -735,6 +760,24 @@ def funcDeclToStatement {M} [Inhabited M] (decl : Imperative.PureFunc Expression
   modify (·.pushBoundVar name.val)
   pure (.funcDecl_statement default name typeArgs b r preconds bodyExpr inline?)
 
+/-- Decompose a single-level `map_update(base, idx, val)` where `base` is (or starts
+    with) an fvar matching `varName`. Returns `(indices, innerVal)` with indices
+    in left-to-right order, or `none` if the expression is not this pattern. -/
+private def decomposeMapUpdate (varName : String)
+    (e : Lambda.LExpr CoreLParams.mono)
+    : Option (List (Lambda.LExpr CoreLParams.mono) × Lambda.LExpr CoreLParams.mono) :=
+  let (head, args) := Lambda.getLFuncCall e
+  match head, args with
+  | .op _ opName _, [base, idx, val] =>
+    if opName.name == "update" then
+      match base with
+      | .fvar _ ident _ =>
+        if ident.name == varName then some ([idx], val)
+        else none
+      | _ => none
+    else none
+  | _, _ => none
+
 mutual
 /-- Convert `Core.Statement` to `CoreDDM.Statement` -/
 partial def stmtToCST {M} [Inhabited M] (s : Core.Statement)
@@ -758,9 +801,20 @@ partial def stmtToCST {M} [Inhabited M] (s : Core.Statement)
     modify (·.pushBoundVar name.toPretty)
     pure result
   | .set name expr _md => do
-    let lhs := Lhs.lhsIdent default ⟨default, name.name⟩
-    let exprCST ← lexprToExpr expr 0
-    -- Type annotation required by CST but not semantically used.
+    -- Detect map_update(name, idx, val) pattern to produce lhsArray syntax
+    let (lhs, exprCST) ← match decomposeMapUpdate name.name expr with
+      | some (idxs, val) => do
+        let baseLhs := Lhs.lhsIdent default ⟨default, name.name⟩
+        let lhs ← idxs.foldlM (init := baseLhs) fun acc idx => do
+          let idxCST ← lexprToExpr idx 0
+          let tyCST := CoreType.tvar default unknownTypeVar
+          pure (Lhs.lhsArray default tyCST acc idxCST)
+        let valCST ← lexprToExpr val 0
+        pure (lhs, valCST)
+      | none => do
+        let lhs := Lhs.lhsIdent default ⟨default, name.name⟩
+        let exprCST ← lexprToExpr expr 0
+        pure (lhs, exprCST)
     let tyCST := CoreType.tvar default unknownTypeVar
     pure (.assign default tyCST lhs exprCST)
   | .havoc name _md => do

Strata/Languages/Core/DDMTransform/Grammar.lean

@@ -103,9 +103,9 @@ fn map_get (K : Type, V : Type, m : Map K V, k : K) : V => m "[" k "]";
 fn map_set (K : Type, V : Type, m : Map K V, k : K, v : V) : Map K V =>
   m "[" k ":=" v "]";
 
-// TODO: seq_empty is not yet supported in the grammar because the DDM parser
-// cannot currently handle 0-ary polymorphic functions (no arguments to infer
-// the type parameter from). The Factory definition exists for programmatic use.
+// seq_empty uses explicit type annotation syntax since there are no value
+// arguments to infer the type parameter from.
+fn seq_empty (A : Type) : Sequence A => "Sequence.empty" "<" A ">" "(" ")";
 fn seq_length (A : Type, s : Sequence A) : int => "Sequence.length" "(" s ")";
 fn seq_select (A : Type, s : Sequence A, i : int) : A => "Sequence.select" "(" s ", " i ")";
 fn seq_append (A : Type, s1 : Sequence A, s2 : Sequence A) : Sequence A =>
@@ -188,6 +188,16 @@ fn bvsle (tp : Type, a : tp, b : tp) : bool => @[prec(20), leftassoc] a " <=s "
 fn bvsgt (tp : Type, a : tp, b : tp) : bool => @[prec(20), leftassoc] a " >s " b;
 fn bvsge (tp : Type, a : tp, b : tp) : bool => @[prec(20), leftassoc] a " >=s " b;
 
+fn bv_neg_overflow (tp : Type, a : tp) : bool => "Bv.SNegOverflow" "(" a ")";
+fn bv_uneg_overflow (tp : Type, a : tp) : bool => "Bv.UNegOverflow" "(" a ")";
+fn bv_sadd_overflow (tp : Type, a : tp, b : tp) : bool => "Bv.SAddOverflow" "(" a ", " b ")";
+fn bv_ssub_overflow (tp : Type, a : tp, b : tp) : bool => "Bv.SSubOverflow" "(" a ", " b ")";
+fn bv_smul_overflow (tp : Type, a : tp, b : tp) : bool => "Bv.SMulOverflow" "(" a ", " b ")";
+fn bv_sdiv_overflow (tp : Type, a : tp, b : tp) : bool => "Bv.SDivOverflow" "(" a ", " b ")";
+fn bv_uadd_overflow (tp : Type, a : tp, b : tp) : bool => "Bv.UAddOverflow" "(" a ", " b ")";
+fn bv_usub_overflow (tp : Type, a : tp, b : tp) : bool => "Bv.USubOverflow" "(" a ", " b ")";
+fn bv_umul_overflow (tp : Type, a : tp, b : tp) : bool => "Bv.UMulOverflow" "(" a ", " b ")";
+
 fn bvconcat8 (a : bv8, b : bv8) : bv16 => "bvconcat{8}{8}" "(" a ", " b ")";
 fn bvconcat16 (a : bv16, b : bv16) : bv32 => "bvconcat{16}{16}" "(" a ", " b ")";
 fn bvconcat32 (a : bv32, b : bv32) : bv64 => "bvconcat{32}{32}" "(" a ", " b ")";
@@ -354,7 +364,7 @@ op command_fndecl (name : Ident,
   "function " name typeArgs b " : " r ";\n";
 
 category Inline;
-op inline () : Inline => "inline";
+op inline () : Inline => "inline ";
 
 // Note: when editing command_fndef, consider whether recfn_decl needs
 // matching edits.