feat(lean): specs for for-loops over signed ints

CHANGELOG.md

@@ -28,6 +28,7 @@ Changes to hax-lib:
  - Lean lib: For-loops for all unsigned integers (#1951)
  - Lean lib: Upgrade to Lean v4.29.0-rc1 (#1962)
  - Lean lib: Add support for Int128 and UInt128 while waiting for upstream in Lean (#1968)
+ - Lean lib: Add specs for for-loops over signed integers (#1988)
 
 Changes to the Lean backend:
  - Add `hax_zify` and `hax_construct_pure` tactics (#1888)

hax-lib/proof-libs/lean/Hax/core_models/epilogue/folds.lean

@@ -46,12 +46,30 @@ attribute [spec] rust_primitives.hax.folds.fold_range_return
 open Lean in
 set_option hygiene false in
 macro "declare_fold_specs" s:(&"signed" <|> &"unsigned") typeName:ident width:term : command => do
+
+  let signed ← match s.raw[0].getKind with
+  | `signed => pure true
+  | `unsigned => pure false
+  | _ => throw .unsupportedSyntax
+
   let tyDot (n : Name) := mkIdent (typeName.getId ++ n)
   let tySimp (n : Name) : TSyntax _ := .mk
     (Syntax.node .none ``Lean.Parser.Tactic.simpLemma #[mkNullNode, mkNullNode, tyDot n])
-  let tyRw (n : Name) : TSyntax `Lean.Parser.Tactic.rwRule := .mk
-    (Syntax.node .none ``Lean.Parser.Tactic.rwRule #[mkNullNode, tyDot n])
-  `(
+
+  let terminationMeasure ← if signed
+    then `(term| (e.toInt - s.toInt).toNat)
+    else `(term| (e - s))
+  let decreasingProof ← if signed then `(tacticSeq|
+    have : (s + 1).toInt = s.toInt + 1 := by grind
+    grind
+  ) else `(tacticSeq|
+    simp only [$(tySimp `sizeOf), Nat.add_lt_add_iff_right]
+    exact $(tyDot `sub_succ_lt_self) _ _ (by assumption)
+  )
+
+  let mut cmds := #[]
+
+  cmds := cmds.push $ ← `(
     /-- Implementation of Rust for-loops without early returns -/
     def $(tyDot `fold_range) {α : Type}
         (s e : $typeName)
@@ -63,11 +81,11 @@ macro "declare_fold_specs" s:(&"signed" <|> &"unsigned") typeName:ident width:te
         if s < e
         then fold_range (s + 1) e inv (← body init s) body pureInv
         else pure init
-    termination_by (e - s)
-    decreasing_by
-      simp only [$(tySimp `sizeOf), Nat.add_lt_add_iff_right]
-      exact $(tyDot `sub_succ_lt_self) _ _ (by assumption)
+    termination_by $terminationMeasure
+    decreasing_by $decreasingProof
+  )
 
+  cmds := cmds.push $ ← `(
     /-- Implementation of Rust for-loops with early returns -/
     def $(tyDot `fold_range_return) {α_acc α_ret : Type}
         (s e: $typeName)
@@ -87,16 +105,18 @@ macro "declare_fold_specs" s:(&"signed" <|> &"unsigned") typeName:ident width:te
         | .Continue res => fold_range_return (s + 1) e inv res body pureInv
       else
         pure (ControlFlow.Continue init)
-    termination_by (e - s)
-    decreasing_by
-      simp only [$(tySimp `sizeOf), Nat.add_lt_add_iff_right]
-      exact $(tyDot `sub_succ_lt_self) _ _ (by assumption)
+    termination_by $terminationMeasure
+    decreasing_by $decreasingProof
+  )
 
+  cmds := cmds.push $ ← `(
     @[spec]
     instance : @rust_primitives.hax.folds $typeName where
       fold_range := $(tyDot `fold_range)
       fold_range_return := $(tyDot `fold_range_return)
+  )
 
+  cmds := cmds.push $ ← `(
     /-- Specification of Rust for-loops without early returns (for bv_decide) -/
     @[specset bv]
     theorem $(mkIdent (s!"rust_primitives.hax.folds.fold_range_spec_bv_{typeName.getId}").toName) {α}
@@ -126,12 +146,42 @@ macro "declare_fold_specs" s:(&"signed" <|> &"unsigned") typeName:ident width:te
         mspec $(mkIdent (s!"rust_primitives.hax.folds.fold_range_spec_bv_{typeName.getId}").toName)
           <;> grind
       · grind
-    termination_by (e - s)
-    decreasing_by
-      simp only [$(tySimp `sizeOf), Nat.add_lt_add_iff_right]
-      exact $(tyDot `sub_succ_lt_self) _ _ (by assumption)
+    termination_by $terminationMeasure
+    decreasing_by $decreasingProof
+  )
 
-    /-- Specification of Rust for-loops without early returns (for grind) -/
+  cmds := cmds.push $ ← if signed then `(
+    /-- Specification of Rust for-loops on signed integers without early returns (for grind) -/
+    @[specset int]
+    theorem $(mkIdent (s!"rust_primitives.hax.folds.fold_range_spec_int_{typeName.getId}").toName) {α}
+        (s e : $typeName)
+        (inv : α -> $typeName -> RustM Prop)
+        (pureInv)
+        (init: α)
+        (body : α -> $typeName -> RustM α) :
+        s.toInt ≤ e.toInt →
+        pureInv.val init s →
+        (∀ (acc : α) (i : $typeName),
+          s.toInt ≤ i.toInt →
+          i.toInt < e.toInt →
+          pureInv.val acc i →
+          ⦃ ⌜ True ⌝ ⦄
+          (body acc i)
+          ⦃ ⇓ res => ⌜ pureInv.val res (i+1) ⌝ ⦄) →
+        ⦃ ⌜ True ⌝ ⦄
+        ($(tyDot `fold_range) s e inv init body pureInv)
+        ⦃ ⇓ r => ⌜ pureInv.val r e ⌝ ⦄ := by
+      intro h_le h_inv_s h_body
+      apply $(mkIdent (s!"rust_primitives.hax.folds.fold_range_spec_bv_{typeName.getId}").toName)
+      · exact $(tyDot `le_iff_toInt_le).mpr h_le
+      · exact h_inv_s
+      · intro acc i hi_ge hi_lt h_inv
+        apply h_body
+        · exact $(tyDot `le_iff_toInt_le).mp hi_ge
+        · exact $(tyDot `lt_iff_toInt_lt).mp hi_lt
+        · exact h_inv
+  ) else `(
+    /-- Specification of Rust for-loops on unsigned integers without early returns (for grind) -/
     @[specset int]
     theorem $(mkIdent (s!"rust_primitives.hax.folds.fold_range_spec_int_{typeName.getId}").toName) {α}
         (s e : $typeName)
@@ -152,14 +202,20 @@ macro "declare_fold_specs" s:(&"signed" <|> &"unsigned") typeName:ident width:te
         ($(tyDot `fold_range) s e inv init body pureInv)
         ⦃ ⇓ r => ⌜ pureInv.val r e ⌝ ⦄ := by
       apply $(mkIdent (s!"rust_primitives.hax.folds.fold_range_spec_bv_{typeName.getId}").toName)
-
   )
 
+  return ⟨mkNullNode cmds⟩
+
 declare_fold_specs unsigned UInt8 8
 declare_fold_specs unsigned UInt16 16
 declare_fold_specs unsigned UInt32 32
 declare_fold_specs unsigned UInt64 64
 declare_fold_specs unsigned USize64 64
 
+declare_fold_specs signed Int8 8
+declare_fold_specs signed Int16 16
+declare_fold_specs signed Int32 32
+declare_fold_specs signed Int64 64
+
 
 end Fold