init z3 integration

GRAMMAR.bnf

@@ -34,6 +34,7 @@ top_level_declaration ::=
     | log_declaration
     | import_declaration
     | error_declaration
+    | ghost_declaration
 
 # ==========================================
 # IMPORT DECLARATIONS
@@ -56,6 +57,8 @@ contract_member ::=
     | struct_declaration
     | enum_declaration
     | error_declaration
+    | ghost_declaration
+    | contract_invariant
 
 # ==========================================
 # FUNCTION DECLARATIONS
@@ -136,6 +139,16 @@ indexed_modifier ::= "indexed"
 
 error_declaration ::= "error" identifier ("(" parameter_list? ")")? ";"
 
+# ==========================================
+# FORMAL VERIFICATION DECLARATIONS
+# ==========================================
+
+# Ghost declarations (specification-only code)
+ghost_declaration ::= "ghost" (variable_declaration | function_declaration | block)
+
+# Contract invariants (class invariants)
+contract_invariant ::= "invariant" identifier "(" expression ")" ";"
+
 # ==========================================
 # TYPE SYSTEM
 # ==========================================
@@ -203,6 +216,7 @@ statement ::=
     | lock_statement
     | unlock_statement
     | try_statement
+    | assert_statement
     | block
 
 # REVISED: LHS of assignment now restricted to a valid 'lvalue'.
@@ -229,10 +243,13 @@ expression_statement ::= expression ";"
 
 if_statement ::= "if" "(" expression ")" statement ("else" statement)?
 
-while_statement ::= "while" "(" expression ")" statement
+# Formal verification: Loop invariants
+while_statement ::= "while" "(" expression ")" invariant_clause* statement
 
 # NOTE: This is a foreach-style loop, e.g., for (my_map) |key, value| { ... }
-for_statement ::= "for" "(" expression ")" "|" identifier ("," identifier)? "|" statement
+for_statement ::= "for" "(" expression ")" "|" identifier ("," identifier)? "|" invariant_clause* statement
+
+invariant_clause ::= "invariant" "(" expression ")"
 
 return_statement ::= "return" expression? ";"
 
@@ -246,6 +263,9 @@ lock_statement ::= "@" "lock" "(" expression ")" ";"
 
 unlock_statement ::= "@" "unlock" "(" expression ")" ";"
 
+# Formal verification: Assertions
+assert_statement ::= "assert" "(" expression ("," string_literal)? ")" ";"
+
 try_statement ::= "try" expression ("catch" ("|" identifier "|")? block)?
 
 block ::= "{" statement* "}"

GRAMMAR.ebnf

@@ -16,7 +16,8 @@ TopLevelDeclaration =
   | EnumDeclaration
   | LogDeclaration
   | ImportDeclaration
-  | ErrorDeclaration ;
+  | ErrorDeclaration
+  | GhostDeclaration ;
 
 # ==========================================
 # IMPORT DECLARATIONS
@@ -38,7 +39,9 @@ ContractMember =
   | LogDeclaration
   | StructDeclaration
   | EnumDeclaration
-  | ErrorDeclaration ;
+  | ErrorDeclaration
+  | GhostDeclaration
+  | ContractInvariant ;
 
 # ==========================================
 # FUNCTION DECLARATIONS
@@ -104,6 +107,16 @@ LogParameter = [ "indexed" ] Identifier ":" Type ;
 
 ErrorDeclaration = "error" Identifier [ "(" [ ParameterList ] ")" ] ";" ;
 
+# ==========================================
+# FORMAL VERIFICATION DECLARATIONS
+# ==========================================
+
+# Ghost declarations (specification-only code)
+GhostDeclaration = "ghost" ( VariableDeclaration | FunctionDeclaration | Block ) ;
+
+# Contract invariants (class invariants)
+ContractInvariant = "invariant" Identifier "(" Expression ")" ";" ;
+
 # ==========================================
 # TYPE SYSTEM
 # ==========================================
@@ -162,6 +175,7 @@ Statement =
   | LockStatement
   | UnlockStatement
   | TryStatement
+  | AssertStatement
   | Block ;
 
 AssignmentStatement         = LValue "="  Expression ";" ;
@@ -177,10 +191,11 @@ MoveStatement        = "move" Expression "from" Expression "to" Expression ";" ;
 ExpressionStatement  = Expression ";" ;
 
 IfStatement    = "if"    "(" Expression ")" Statement [ "else" Statement ] ;
-WhileStatement = "while" "(" Expression ")" Statement ;
 
-# foreach-style loop: for (iterable) |item[, index]| statement
-ForStatement = "for" "(" Expression ")" "|" Identifier [ "," Identifier ] "|" Statement ;
+# Formal verification: Loop invariants
+WhileStatement = "while" "(" Expression ")" { InvariantClause } Statement ;
+ForStatement = "for" "(" Expression ")" "|" Identifier [ "," Identifier ] "|" { InvariantClause } Statement ;
+InvariantClause = "invariant" "(" Expression ")" ;
 
 ReturnStatement   = "return" [ Expression ] ";" ;
 BreakStatement    = "break"  [ ":" Identifier [ Expression ] ] ";" ;
@@ -190,6 +205,9 @@ LogStatement    = "log" Identifier "(" [ ExpressionList ] ")" ";" ;
 LockStatement   = "@" "lock"   "(" Expression ")" ";" ;
 UnlockStatement = "@" "unlock" "(" Expression ")" ";" ;
 
+# Formal verification: Assertions
+AssertStatement = "assert" "(" Expression [ "," StringLiteral ] ")" ";" ;
+
 TryStatement = "try" Expression [ "catch" [ "|" Identifier "|" ] Block ] ;
 
 Block        = "{" { Statement } "}" ;
@@ -263,6 +281,10 @@ ComptimeExpression = "comptime" Block ;
 CastExpression     = "@" "cast" "(" Type "," Expression ")" ;
 ErrorExpression    = "error" "." Identifier ;
 
+# Formal verification: Quantified expressions
+QuantifiedExpression = Quantifier Identifier ":" Type [ "where" Expression ] "=>" Expression ;
+Quantifier = "forall" | "exists" ;
+
 AnonymousStructLiteral = "." "{" [ AnonymousStructLiteralFieldList ] "}" ;
 AnonymousStructLiteralFieldList = AnonymousStructLiteralField { "," AnonymousStructLiteralField } [ "," ] ;
 AnonymousStructLiteralField = "." Identifier "=" Expression ;