From 523ad02b5c317757061e4ce4fdd6266d923b5f76 Mon Sep 17 00:00:00 2001 From: Lydia Kondylidou <33327056+kondylidou@users.noreply.github.com> Date: Wed, 6 May 2026 08:55:24 +0200 Subject: [PATCH] records --- Strata/DDM/AST.lean | 74 ++++++++- Strata/DDM/Elab/Core.lean | 51 +++++- Strata/DDM/Integration/Lean/ToExpr.lean | 12 ++ Strata/Languages/Boole/Grammar.lean | 9 ++ Strata/Languages/Boole/Verify.lean | 55 +++++-- .../Languages/Core/DDMTransform/Grammar.lean | 10 ++ .../Core/DDMTransform/Translate.lean | 26 +++- .../FeatureRequests/struct_field_access.lean | 146 ++++++++++++------ docs/BooleFeatureRequests.md | 20 ++- 9 files changed, 337 insertions(+), 66 deletions(-) diff --git a/Strata/DDM/AST.lean b/Strata/DDM/AST.lean index 786ac648cc..b2d2e6c090 100644 --- a/Strata/DDM/AST.lean +++ b/Strata/DDM/AST.lean @@ -937,6 +937,21 @@ structure DatatypeBindingSpec (argDecls : ArgDecls) where functionTemplates : Array FunctionTemplate := #[] deriving Repr +/-- +Specification for single-constructor record type declarations. +Like `DatatypeBindingSpec` but the fields are given directly as `CommaSepBy Binding` +rather than through a `ConstructorList`; a single constructor named `T_mk` is +synthesized automatically. +-/ +structure RecordBindingSpec (argDecls : ArgDecls) where + /-- deBrujin index of the record type name -/ + nameIndex : DebruijnIndex argDecls.size + /-- deBrujin index of the field list (`CommaSepBy Binding`) -/ + fieldsIndex : DebruijnIndex argDecls.size + /-- Optional list of function templates (selectors, etc.) to expand -/ + functionTemplates : Array FunctionTemplate := #[] + deriving Repr + /-- Specification for declaring a single type variable. Creates a .tvar binding in the result context. @@ -954,6 +969,7 @@ inductive BindingSpec (argDecls : ArgDecls) where | type (_ : TypeBindingSpec argDecls) | scopedType (_ : TypeBindingSpec argDecls) -- Type added to global context | datatype (_ : DatatypeBindingSpec argDecls) +| record (_ : RecordBindingSpec argDecls) | tvar (_ : TvarBindingSpec argDecls) deriving Repr @@ -964,6 +980,7 @@ def nameIndex {argDecls} : BindingSpec argDecls → DebruijnIndex argDecls.size | .type v => v.nameIndex | .scopedType v => v.nameIndex | .datatype v => v.nameIndex +| .record v => v.nameIndex | .tvar v => v.nameIndex end BindingSpec @@ -1127,6 +1144,25 @@ def parseNewBindings (md : Metadata) (argDecls : ArgDecls) : Array (BindingSpec constructorsIndex := ⟨constructorsIndex, constructorsP⟩, functionTemplates } + | { dialect := _, name := "declareRecord" } => do + let args := attr.args + if args.size < 2 then + newBindingErr "declareRecord expects at least 2 arguments (name, fields)." + return none + let .catbvar nameIndex := args[0]! + | newBindingErr "declareRecord: invalid name index"; return none + let .catbvar fieldsIndex := args[1]! + | newBindingErr "declareRecord: invalid fields index"; return none + let .isTrue nameP := decideProp (nameIndex < argDecls.size) + | return panic! "Invalid name index" + let .isTrue fieldsP := decideProp (fieldsIndex < argDecls.size) + | return panic! "Invalid fields index" + let functionTemplates ← parseFunctionTemplates (args.extract 2 args.size) + some <$> .record <$> pure { + nameIndex := ⟨nameIndex, nameP⟩, + fieldsIndex := ⟨fieldsIndex, fieldsP⟩, + functionTemplates + } | q`StrataDDL.declareTVar => do let #[.catbvar nameIndex] := attr.args | newBindingErr "declareTVar expects 1 argument."; return none @@ -1758,6 +1794,9 @@ partial def resolveBindingIndices { argDecls : ArgDecls } (m : DialectMap) (src | a => panic! s!"Expected ident for type param {repr a}" foldOverArgAtLevel m addBinding #[] argDecls args b.typeParamsIndex.toLevel some <| .type params.toList none + | .record _ => + -- Records have no type params; constructor/selectors are handled in addRecordBindings. + some <| .type [] none | .tvar _ => -- tvar bindings are local only, not added to GlobalContext none @@ -1805,7 +1844,7 @@ private def getConstructorListPushAnnotation (opDecl : OpDecl) : Option (Nat × The accumulator is `Except String ...` because `foldOverArgBindingSpecs` fixes the fold's accumulator type; wrapping in `Except` lets us propagate errors through the fold without changing its generic signature. -/ -private def extractFieldsFromBindings (dialects : DialectMap) (arg : Arg) +def extractFieldsFromBindings (dialects : DialectMap) (arg : Arg) : Except String (Array (String × TypeExpr)) := -- We thread `Except` through the accumulator rather than changing -- `foldOverArgBindingSpecs`, which is used broadly with plain accumulators. @@ -2139,6 +2178,35 @@ FreeVarIndex values are consistent with this order. this adds entries for: `Option` (type), `None` (constructor), `Some` (constructor), `Option..isNone` (tester), `Option..isSome` (tester). -/ +private def addRecordBindings + (dialects : DialectMap) + (gctx : GlobalContext) + (src : SourceRange) + (dialectName : DialectName) + (preRegistered : Bool) + {argDecls : ArgDecls} + (b : RecordBindingSpec argDecls) + (args : Vector Arg argDecls.size) + : Except String GlobalContext := do + let recordName := + match args[b.nameIndex.toLevel] with + | .ident _ e => e + | a => panic! s!"Expected ident for record name {repr a}" + -- Step 1: Register the record type (no type parameters). + let k := GlobalKind.type [] none + let gctx ← gctx.defineChecked recordName k preRegistered + let recordIndex := gctx.findIndex? recordName |>.getD (gctx.vars.size - 1) + let recordType := mkDatatypeTypeRef src recordIndex #[] + -- Step 2: Extract fields from the CommaSepBy Binding argument and + -- synthesize a single constructor named `recordName ++ "_mk"`. + let fieldsArg := args[b.fieldsIndex.toLevel] + let fields ← extractFieldsFromBindings dialects fieldsArg + let ctorInfo : Array ConstructorInfo := #[{ name := recordName ++ "_mk", fields }] + -- Step 3: Expand function templates (field selectors etc.). + let (gctx, _) := expandFunctionTemplates dialectName src + recordName recordType ctorInfo b.functionTemplates gctx + return gctx + private def addDatatypeBindings (dialects : DialectMap) (gctx : GlobalContext) @@ -2190,7 +2258,7 @@ private def preRegisterType (dialects : DialectMap) (acc : Except String GlobalC {argDecls} (b : BindingSpec argDecls) (args : Vector Arg argDecls.size) : Except String GlobalContext := do let gctx ← acc match b with - | .datatype _ | .type _ => + | .datatype _ | .record _ | .type _ => let name := match args[b.nameIndex.toLevel] with | .ident _ e => e @@ -2212,6 +2280,8 @@ private def addBinding (dialects : DialectMap) (dialectName : DialectName) (preR match b with | .datatype datatypeSpec => addDatatypeBindings dialects gctx l dialectName preRegistered datatypeSpec args + | .record recordSpec => + addRecordBindings dialects gctx l dialectName preRegistered recordSpec args | _ => let name : Var := match args[b.nameIndex.toLevel] with diff --git a/Strata/DDM/Elab/Core.lean b/Strata/DDM/Elab/Core.lean index 1d7d39aa0d..3e18e69650 100644 --- a/Strata/DDM/Elab/Core.lean +++ b/Strata/DDM/Elab/Core.lean @@ -942,6 +942,33 @@ def evalBindingSpec | .error e => logError loc e pure <| .empty gctx + | .record b => + let nameInfo := args[b.nameIndex.toLevel].info + let (_, ident) ← + match nameInfo with + | .ofIdentInfo i => + pure (i.loc, i.val) + | _ => + logInternalError nameInfo.loc s!"Expected ident" + return tctx + assert! tctx.bindings.size = 0 + let gctx := tctx.globalContext + let gctx := gctx.ensureDefined ident (.type [] none) + let dialects := (← read).dialects + let fieldsArg := args[b.fieldsIndex.toLevel] + match extractFieldsFromBindings dialects fieldsArg.arg with + | .ok fields => + let recordIndex := gctx.findIndex? ident |>.getD (gctx.vars.size - 1) + let recordType := mkDatatypeTypeRef loc recordIndex #[] + let ctorInfo : Array ConstructorInfo := #[{ name := ident ++ "_mk", fields }] + let (gctx, errors) := gctx.expandFunctionTemplates + dialectName loc ident recordType ctorInfo + b.functionTemplates + errors.forM (logError loc) + pure <| .empty gctx + | .error e => + logError loc e + pure <| .empty gctx | .tvar b => let ident := evalBindingNameIndex args b.nameIndex pure <| tctx.push { ident, kind := .tvar loc ident } @@ -1666,7 +1693,29 @@ partial def elabExpr (tctx : TypingContext) (stx : Syntax) : ElabM Tree := do let einfo : ElabInfo := { loc := loc, inputCtx := tctx } let name := elabIdent stx[0] let some binding := tctx.lookupVar name - | logError loc s!"Unknown expr identifier {name}" + | -- Desugar dot notation: "base.field" → T..field(base) + -- A single dot (not "..") separates the variable from the field name. + let dotParts := name.splitOn ".." + let parts := name.splitOn "." + if parts.length == 2 && dotParts.length == 1 then + let baseName := parts[0]! + let fieldName := parts[1]! + if let some baseBinding := tctx.lookupVar baseName then + let typeExprOpt : Option TypeExpr := match baseBinding with + | .bvar _ (.expr tp) => some tp + | .fvar _ (.expr tp) => some tp + | _ => none + if let some (.fvar _ typeIdx _) := typeExprOpt then + if let some typeName := tctx.globalContext.nameOf? typeIdx then + let selectorName := typeName ++ ".." ++ fieldName + if let some selectorIdx := tctx.globalContext.findIndex? selectorName then + let baseExpr : Expr := match baseBinding with + | .bvar idx _ => .bvar loc idx + | .fvar idx _ => .fvar loc idx + let appExpr : Expr := .app loc (.fvar loc selectorIdx) (.expr baseExpr) + let info : ExprInfo := { toElabInfo := einfo, expr := appExpr } + return .node (.ofExprInfo info) #[] + logError loc s!"Unknown expr identifier {name}" return default match binding with | .bvar idx k => do diff --git a/Strata/DDM/Integration/Lean/ToExpr.lean b/Strata/DDM/Integration/Lean/ToExpr.lean index 2f505cc5ef..61dafa20ed 100644 --- a/Strata/DDM/Integration/Lean/ToExpr.lean +++ b/Strata/DDM/Integration/Lean/ToExpr.lean @@ -399,6 +399,17 @@ protected def toExpr {argDecls} (b : DatatypeBindingSpec argDecls) (argDeclsExpr end DatatypeBindingSpec +namespace RecordBindingSpec + +protected def toExpr {argDecls} (b : RecordBindingSpec argDecls) (argDeclsExpr : Lean.Expr) : Lean.Expr := + astExpr! mk + argDeclsExpr + (toExpr b.nameIndex) + (toExpr b.fieldsIndex) + (toExpr b.functionTemplates) + +end RecordBindingSpec + namespace TvarBindingSpec protected def toExpr {argDecls} (b : TvarBindingSpec argDecls) (argDeclsExpr : Lean.Expr) : Lean.Expr := @@ -423,6 +434,7 @@ private def toExpr {argDecls} (bi : BindingSpec argDecls) (argDeclsExpr : Lean.E | .type b => astExpr! type argDeclsExpr (b.toExpr argDeclsExpr) | .scopedType b => astExpr! scopedType argDeclsExpr (b.toExpr argDeclsExpr) | .datatype b => astExpr! datatype argDeclsExpr (b.toExpr argDeclsExpr) + | .record b => astExpr! record argDeclsExpr (b.toExpr argDeclsExpr) | .tvar b => astExpr! tvar argDeclsExpr (b.toExpr argDeclsExpr) end BindingSpec diff --git a/Strata/Languages/Boole/Grammar.lean b/Strata/Languages/Boole/Grammar.lean index 4b20ea8b5b..6755381a79 100644 --- a/Strata/Languages/Boole/Grammar.lean +++ b/Strata/Languages/Boole/Grammar.lean @@ -89,6 +89,15 @@ op for_down_to_by_statement (v : MonoBind, init : Expr, limit : Expr, @[scope(v)] body : Block) : Statement => "for " v " := " init " downto " limit step invs body; +// Record/struct type declaration: `type T := { f1: A, f2: B };` +// Desugars to a single-constructor datatype `T_mk(f1: A, f2: B)` with +// field selectors `T..f1(val)`, `T..f2(val)` etc. +@[declareRecord(name, fields, + perField([.datatype, .literal "..", .field], [.datatype], .fieldType), + perField([.datatype, .literal "..", .field, .literal "!"], [.datatype], .fieldType))] +op struct_decl (name : Ident, fields : CommaSepBy Binding) : Command => + "type " name " := " "{" fields "}" ";\n"; + category Program; op prog (commands : SpacePrefixSepBy Command) : Program => commands; diff --git a/Strata/Languages/Boole/Verify.lean b/Strata/Languages/Boole/Verify.lean index 30924563ed..8152c5103e 100644 --- a/Strata/Languages/Boole/Verify.lean +++ b/Strata/Languages/Boole/Verify.lean @@ -233,18 +233,6 @@ private def toCoreMonoBind (b : BooleDDM.MonoBind SourceRange) : TranslateM (Cor match b with | .mono_bind_mk _ ⟨_, n⟩ ty => return (mkIdent n, ← toCoreMonoType ty) -def toCoreTypedUn (m : SourceRange) (ty : Boole.Type) (op : String) (a : Core.Expression.Expr) : TranslateM Core.Expression.Expr := do - let .int _ := ty - | throwAt m s!"Unsupported typed operator type: {repr ty}" - let iop : Core.Expression.Expr := .op () ⟨s!"Int.{op}", ()⟩ none - return .app () iop a - -def toCoreTypedBin (m : SourceRange) (ty : Boole.Type) (op : String) (a b : Core.Expression.Expr) : TranslateM Core.Expression.Expr := do - let .int _ := ty - | throwAt m s!"Unsupported typed operator type: {repr ty}" - let iop : Core.Expression.Expr := .op () ⟨s!"Int.{op}", ()⟩ none - return mkCoreApp iop [a, b] - private def bvWidth (m : SourceRange) (ty : Boole.Type) : TranslateM Nat := match ty with | .bv1 _ => return 1 @@ -262,6 +250,20 @@ private def toCoreBvBin (m : SourceRange) (ty : Boole.Type) (op : String) (a b : let n ← bvWidth m ty return mkCoreApp (.op () ⟨s!"Bv{n}.{op}", ()⟩ none) [a, b] +def toCoreTypedUn (m : SourceRange) (ty : Boole.Type) (op : String) (a : Core.Expression.Expr) : TranslateM Core.Expression.Expr := do + match ty with + | .int _ => + let iop : Core.Expression.Expr := .op () ⟨s!"Int.{op}", ()⟩ none + return .app () iop a + | _ => toCoreBvUn m ty op a + +def toCoreTypedBin (m : SourceRange) (ty : Boole.Type) (op : String) (a b : Core.Expression.Expr) : TranslateM Core.Expression.Expr := do + match ty with + | .int _ => + let iop : Core.Expression.Expr := .op () ⟨s!"Int.{op}", ()⟩ none + return mkCoreApp iop [a, b] + | _ => toCoreBvBin m ty op a b + private def toCoreExtensionalEq (m : SourceRange) (ty : Boole.Type) @@ -373,9 +375,21 @@ def toCoreExpr (e : Boole.Expr) : TranslateM Core.Expression.Expr := do | .bvand m ty a b => toCoreBvBin m ty "And" (← toCoreExpr a) (← toCoreExpr b) | .bvor m ty a b => toCoreBvBin m ty "Or" (← toCoreExpr a) (← toCoreExpr b) | .bvxor m ty a b => toCoreBvBin m ty "Xor" (← toCoreExpr a) (← toCoreExpr b) - | .bvshl m ty a b => toCoreBvBin m ty "Shl" (← toCoreExpr a) (← toCoreExpr b) + | .bvshl m ty a b => + match ty with + | .int _ => do + -- Integer << n encoded as multiplication by 2^n; n must be a literal. + let n ← match b with + | .natToInt _ ⟨_, n⟩ => pure n + | _ => throwAt m "Integer << requires a constant (literal) shift amount" + toCoreTypedBin m ty "Mul" (← toCoreExpr a) (.intConst () (Int.ofNat (1 <<< n))) + | _ => toCoreBvBin m ty "Shl" (← toCoreExpr a) (← toCoreExpr b) | .bvushr m ty a b => toCoreBvBin m ty "UShr" (← toCoreExpr a) (← toCoreExpr b) | .bvsshr m ty a b => toCoreBvBin m ty "SShr" (← toCoreExpr a) (← toCoreExpr b) + | .bvult m ty a b => toCoreBvBin m ty "ULt" (← toCoreExpr a) (← toCoreExpr b) + | .bvule m ty a b => toCoreBvBin m ty "ULe" (← toCoreExpr a) (← toCoreExpr b) + | .bvugt m ty a b => toCoreBvBin m ty "UGt" (← toCoreExpr a) (← toCoreExpr b) + | .bvuge m ty a b => toCoreBvBin m ty "UGe" (← toCoreExpr a) (← toCoreExpr b) | .old _ _ a => return oldifyExpr (← get).currentInoutNames (← toCoreExpr a) | _ => throw (.fromMessage s!"Unsupported expression: {repr e}") @@ -747,6 +761,7 @@ private def registerCommandSymbols (cmd : BooleDDM.Command SourceRange) : List B -- Procedure names are referenced by call statements directly and are not Expr.fvar symbols. | .boole_procedure _ _ _ _ _ _ _ | .command_procedure _ _ _ _ _ _ => [] | .command_datatypes _ ⟨_, decls⟩ => decls.toList.map (fun _ => false) + | .struct_decl _ _ _ => [false] | .command_block _ _ => [] | .command_axiom _ _ _ => [] | .command_distinct _ _ _ => [] @@ -886,6 +901,20 @@ def toCoreDecls (cmd : BooleDDM.Command SourceRange) : TranslateM (List Core.Dec } .empty] | .command_datatypes _ ⟨_, decls⟩ => return [.type (.data (← decls.toList.mapM toCoreDatatypeDecl)) .empty] + | .struct_decl m ⟨_, tname⟩ ⟨_, fields⟩ => + -- Desugar `type T := { f1: A, f2: B }` to a single-constructor datatype. + -- DDM registration (type + selectors) is handled by @[declareRecord]. + let args ← fields.toList.mapM toCoreBinding + let ctorName := tname ++ "_mk" + let constr : Lambda.LConstr Unit := { + name := mkIdent ctorName + args := args + testerName := s!"{tname}..is{ctorName}" + } + return [.type (.data [{ name := tname + typeArgs := [] + constrs := [constr] + constrs_ne := by simp }]) .empty] /-- Render a `Boole.Program` to a format object using the provided `GlobalContext` and `DialectMap`. These should come from the originating `Strata.Program` (i.e. `env.globalContext` diff --git a/Strata/Languages/Core/DDMTransform/Grammar.lean b/Strata/Languages/Core/DDMTransform/Grammar.lean index 0374322193..9fbafaede1 100644 --- a/Strata/Languages/Core/DDMTransform/Grammar.lean +++ b/Strata/Languages/Core/DDMTransform/Grammar.lean @@ -39,6 +39,12 @@ constructors : Ident, testerTemplate : FunctionTemplate, accessorTemplate : FunctionTemplate, unsafeAccessorTemplate : FunctionTemplate); +// Declare metadata for single-constructor record types (field list variant). +// Unlike declareDatatype, the constructor is synthesized as `name ++ "_mk"`. +metadata declareRecord (name : Ident, fields : Ident, +accessorTemplate : FunctionTemplate, +unsafeAccessorTemplate : FunctionTemplate); + type bool; type int; type string; @@ -187,6 +193,10 @@ fn bvslt (tp : Type, a : tp, b : tp) : bool => @[prec(20), leftassoc] a " @[prec(20), leftassoc] a " <=s " b; 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 bvult (tp : Type, a : tp, b : tp) : bool => @[prec(20), leftassoc] a " @[prec(20), leftassoc] a " <=u " b; +fn bvugt (tp : Type, a : tp, b : tp) : bool => @[prec(20), leftassoc] a " >u " b; +fn bvuge (tp : Type, a : tp, b : tp) : bool => @[prec(20), leftassoc] a " >=u " 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 ")"; diff --git a/Strata/Languages/Core/DDMTransform/Translate.lean b/Strata/Languages/Core/DDMTransform/Translate.lean index aa088ca54f..727349860f 100644 --- a/Strata/Languages/Core/DDMTransform/Translate.lean +++ b/Strata/Languages/Core/DDMTransform/Translate.lean @@ -512,6 +512,10 @@ def translateFn (ty? : Option LMonoTy) (q : QualifiedIdent) : TransM Core.Expres | .some .bv1, q`Core.bvslt => return Core.bv1SLtOp | .some .bv1, q`Core.bvsge => return Core.bv1SGeOp | .some .bv1, q`Core.bvsgt => return Core.bv1SGtOp + | .some .bv1, q`Core.bvule => return Core.bv1ULeOp + | .some .bv1, q`Core.bvult => return Core.bv1ULtOp + | .some .bv1, q`Core.bvuge => return Core.bv1UGeOp + | .some .bv1, q`Core.bvugt => return Core.bv1UGtOp | .some .bv1, q`Core.neg_expr => return Core.bv1NegOp | .some .bv1, q`Core.add_expr => return Core.bv1AddOp | .some .bv1, q`Core.sub_expr => return Core.bv1SubOp @@ -542,6 +546,10 @@ def translateFn (ty? : Option LMonoTy) (q : QualifiedIdent) : TransM Core.Expres | .some .bv8, q`Core.bvslt => return Core.bv8SLtOp | .some .bv8, q`Core.bvsge => return Core.bv8SGeOp | .some .bv8, q`Core.bvsgt => return Core.bv8SGtOp + | .some .bv8, q`Core.bvule => return Core.bv8ULeOp + | .some .bv8, q`Core.bvult => return Core.bv8ULtOp + | .some .bv8, q`Core.bvuge => return Core.bv8UGeOp + | .some .bv8, q`Core.bvugt => return Core.bv8UGtOp | .some .bv8, q`Core.neg_expr => return Core.bv8NegOp | .some .bv8, q`Core.add_expr => return Core.bv8AddOp | .some .bv8, q`Core.sub_expr => return Core.bv8SubOp @@ -572,6 +580,10 @@ def translateFn (ty? : Option LMonoTy) (q : QualifiedIdent) : TransM Core.Expres | .some .bv16, q`Core.bvslt => return Core.bv16SLtOp | .some .bv16, q`Core.bvsge => return Core.bv16SGeOp | .some .bv16, q`Core.bvsgt => return Core.bv16SGtOp + | .some .bv16, q`Core.bvule => return Core.bv16ULeOp + | .some .bv16, q`Core.bvult => return Core.bv16ULtOp + | .some .bv16, q`Core.bvuge => return Core.bv16UGeOp + | .some .bv16, q`Core.bvugt => return Core.bv16UGtOp | .some .bv16, q`Core.neg_expr => return Core.bv16NegOp | .some .bv16, q`Core.add_expr => return Core.bv16AddOp | .some .bv16, q`Core.sub_expr => return Core.bv16SubOp @@ -602,6 +614,10 @@ def translateFn (ty? : Option LMonoTy) (q : QualifiedIdent) : TransM Core.Expres | .some .bv32, q`Core.bvslt => return Core.bv32SLtOp | .some .bv32, q`Core.bvsge => return Core.bv32SGeOp | .some .bv32, q`Core.bvsgt => return Core.bv32SGtOp + | .some .bv32, q`Core.bvule => return Core.bv32ULeOp + | .some .bv32, q`Core.bvult => return Core.bv32ULtOp + | .some .bv32, q`Core.bvuge => return Core.bv32UGeOp + | .some .bv32, q`Core.bvugt => return Core.bv32UGtOp | .some .bv32, q`Core.neg_expr => return Core.bv32NegOp | .some .bv32, q`Core.add_expr => return Core.bv32AddOp | .some .bv32, q`Core.sub_expr => return Core.bv32SubOp @@ -632,6 +648,10 @@ def translateFn (ty? : Option LMonoTy) (q : QualifiedIdent) : TransM Core.Expres | .some .bv64, q`Core.bvslt => return Core.bv64SLtOp | .some .bv64, q`Core.bvsge => return Core.bv64SGeOp | .some .bv64, q`Core.bvsgt => return Core.bv64SGtOp + | .some .bv64, q`Core.bvule => return Core.bv64ULeOp + | .some .bv64, q`Core.bvult => return Core.bv64ULtOp + | .some .bv64, q`Core.bvuge => return Core.bv64UGeOp + | .some .bv64, q`Core.bvugt => return Core.bv64UGtOp | .some .bv64, q`Core.neg_expr => return Core.bv64NegOp | .some .bv64, q`Core.add_expr => return Core.bv64AddOp | .some .bv64, q`Core.sub_expr => return Core.bv64SubOp @@ -1045,7 +1065,11 @@ partial def translateExpr (p : Program) (bindings : TransBindings) (arg : Arg) : | q`Core.bvsle | q`Core.bvslt | q`Core.bvsgt - | q`Core.bvsge => + | q`Core.bvsge + | q`Core.bvule + | q`Core.bvult + | q`Core.bvugt + | q`Core.bvuge => let ty ← translateLMonoTy bindings (dealiasTypeArg p tpa) if ¬ isArithTy ty then TransM.error s!"translateExpr unexpected type for {repr fni}: {repr args}" diff --git a/StrataTest/Languages/Boole/FeatureRequests/struct_field_access.lean b/StrataTest/Languages/Boole/FeatureRequests/struct_field_access.lean index b263203015..4c262d061d 100644 --- a/StrataTest/Languages/Boole/FeatureRequests/struct_field_access.lean +++ b/StrataTest/Languages/Boole/FeatureRequests/struct_field_access.lean @@ -9,57 +9,109 @@ import Strata.MetaVerifier open Strata /- -Near-upstream anchors: -- Source: dalek-lite `curve25519-dalek/src/specs/field_specs.rs` - `FieldElement51` is a 5-limb 255-bit field element: - pub struct FieldElement51 { pub(crate) limbs: [u64; 5] } - Every dalek spec function accesses struct fields directly: - pub open spec fn u64_5_bounded(limbs: [u64; 5], bit_limit: u64) -> bool { - forall|i: int| 0 <= i < 5 ==> limbs[i] < (1u64 << bit_limit) - } - pub open spec fn spec_add_fe51_limbs(a: &FieldElement51, b: &FieldElement51) - -> FieldElement51 { - FieldElement51 { limbs: [a.limbs[0] + b.limbs[0], ..., a.limbs[4] + b.limbs[4]] } - } - `edwards_specs.rs` uses `.X`, `.Y`, `.Z`, `.T` fields on `EdwardsPoint`. -- Gap: Boole has no record/struct type with named field access. Structs with - fields like `fe.limbs[i]` or `p.X` must be flattened into separate scalar - parameters or encoded as `Map int T`. There is no struct literal syntax and - no `.field` accessor in Boole expressions. -- Remaining gap: record/struct type declarations in Boole with named fields, - field accessor expressions (`p.field`), struct literal construction - (`T { f1: v1, f2: v2 }`), and quantification over fixed-size field arrays. +Near-upstream anchors from dalek-lite `curve25519-dalek/src/specs/field_specs.rs`: + pub struct FieldElement51 { pub(crate) limbs: [u64; 5] } + pub open spec fn u64_5_bounded(limbs: [u64; 5], bit_limit: u64) -> bool { + forall|i: int| 0 <= i < 5 ==> limbs[i] < (1u64 << bit_limit) + } + +The `[u64; 5]` array-typed field is modelled here with unrolled `bv64` limbs +(remaining gap: fixed-size array fields). The unsigned comparison ` -// fe.limb0 < bit_limit && fe.limb1 < bit_limit && -// fe.limb2 < bit_limit && fe.limb3 < bit_limit && fe.limb4 < bit_limit); -// -// procedure fe_add_seed(a: FieldElement51, b: FieldElement51) returns (r: FieldElement51) -// spec { -// requires fe_bounded(a, 2251799813685248); // 2^51 -// requires fe_bounded(b, 2251799813685248); -// ensures r.limb0 == a.limb0 + b.limb0; -// ensures r.limb1 == a.limb1 + b.limb1; -// ensures r.limb2 == a.limb2 + b.limb2; -// ensures r.limb3 == a.limb3 + b.limb3; -// ensures r.limb4 == a.limb4 + b.limb4; -// } -// { -// r := FieldElement51 { -// limb0: a.limb0 + b.limb0, -// limb1: a.limb1 + b.limb1, -// limb2: a.limb2 + b.limb2, -// limb3: a.limb3 + b.limb3, -// limb4: a.limb4 + b.limb4, -// }; -// }; +// Near dalek's FieldElement51 { limbs: [u64; 5] } — unrolled as bv64 limbs. +type FieldElement51 := { limb0: bv64, limb1: bv64, limb2: bv64, limb3: bv64, limb4: bv64 }; + +// Models u64_5_bounded with bit_limit=51: each limb below 2^51. +// Uses dot notation on the `fe` parameter (same desugaring as var-locals). +// Uses >` (UShr), `>>s` (SShr), `<<`, `~` lower to `Bv{N}.And/Or/Xor/UShr/SShr/Shl/Not` Core ops. - `bvWidth` helper extracts the bit-width from the Boole type and dispatches to the right-sized op. - Benchmark: [`bitvector_ops.lean`](../StrataTest/Languages/Boole/FeatureRequests/bitvector_ops.lean) (X25519 scalar clamping with `bv8` `&` and `|`). +- **Unsigned bitvector comparisons on `bvN` types** (`u`, `>=u`) + - `u`, `>=u` lower to `Bv{N}.ULt/ULe/UGt/UGe` Core ops via `toCoreBvBin`. + - Added `bvult/bvule/bvugt/bvuge` to Core DDM Grammar and Translate tables (all widths). + - Distinguishes unsigned comparison (matching Rust/Verus `u64 < x` semantics) from signed comparison `` in spec functions**: Native `Option` return type so fallible spec functions can be represented faithfully; currently encoded as `is_some` flag plus component functions. Every Vest parser returns `Option<(int, T)>`. ## Expressiveness requests @@ -98,6 +114,6 @@ These are the curated one-gap Boole seeds. | [`bitvector_ops.lean`](../StrataTest/Languages/Boole/FeatureRequests/bitvector_ops.lean) | Bitwise operators on `bvN` types | dalek-lite `scalar_specs.rs` | Implemented | | [`bitvector_proof_mode.lean`](../StrataTest/Languages/Boole/FeatureRequests/bitvector_proof_mode.lean) | `by (bit_vector)` proof mode | VeruSAGE-Bench Vest `leb128` | Active | | [`seq_slicing.lean`](../StrataTest/Languages/Boole/FeatureRequests/seq_slicing.lean) | Sequence slicing (`subrange`, `skip`, `take`, `drop_first`) | dalek-lite `scalar_specs.rs`, `core_specs.rs`; Vest `leb128`, `repetition` | Active | -| [`struct_field_access.lean`](../StrataTest/Languages/Boole/FeatureRequests/struct_field_access.lean) | Struct/record types with named field access | dalek-lite `field_specs.rs`, `edwards_specs.rs` | Active | +| [`struct_field_access.lean`](../StrataTest/Languages/Boole/FeatureRequests/struct_field_access.lean) | Struct/record types with named field access | dalek-lite `field_specs.rs`, `edwards_specs.rs` | Implemented (shorthand syntax + dot notation on var-locals and parameters + `bv64` fields + `` in spec functions; `matches` in `ensures`/`exists` | VeruSAGE-Bench Vest `SecureSpecCombinator`, `leb128` | Active |