Lean: Fix termination checker (#1095)

rems-project · Mar 3, 2025 · af7e7cf · af7e7cf
1 parent cd20e9a
commit af7e7cf
Show file tree

Hide file tree

Showing 3 changed files with 25 additions and 12 deletions.
diff --git a/src/sail_lean_backend/Sail/Sail.lean b/src/sail_lean_backend/Sail/Sail.lean
@@ -508,20 +508,17 @@ instance : HOr (BitVec n) (BitVec m) (BitVec n) where
 instance : HXor (BitVec n) (BitVec m) (BitVec n) where
   hXor x y := x ^^^ y
 
-def Int.zpow (m n : Int) : Int := m ^ n.toNat
-
-infixl:65 " +i "   => Int.add
-infixl:65 " -i " => Int.sub
-infixr:80 " ^i "   => Int.pow
-infixl:70 " *i "   => Int.mul
-
-macro_rules | `($x +i $y)   => `(binop% Int.add $x $y)
-macro_rules | `($x -i $y)   => `(binop% Int.sub $x $y)
-macro_rules | `($x ^i $y)   => `(rightact% Int.zpow $x $y)
-macro_rules | `($x *i $y)   => `(binop% Int.mul $x $y)
+instance : HPow Int Int Int where
+  hPow x n := x ^ n.toNat
 
+infixl:65 " +i "   => fun (x y : Int) => x + y
+infixl:65 " -i "   => fun (x y : Int) => x - y
+infixl:65 " ^i "   => fun (x y : Int) => x ^ y
+infixl:65 " *i "   => fun (x y : Int) => x * y
 
 notation:50 x "≤b" y => decide (x ≤ y)
 notation:50 x "<b" y => decide (x < y)
 notation:50 x "≥b" y => decide (x ≥ y)
 notation:50 x ">b" y => decide (x > y)
+
+macro_rules | `(tactic| decreasing_trivial) => `(tactic| simp_all <;> omega)
diff --git a/test/lean/typquant.expected.lean b/test/lean/typquant.expected.lean
@@ -58,7 +58,7 @@ open option
 
 namespace Functions
 
-/-- Type quantifiers: k_ex737# : Bool, k_ex736# : Bool -/
+/-- Type quantifiers: k_ex761# : Bool, k_ex760# : Bool -/
 def neq_bool (x : Bool) (y : Bool) : Bool :=
   (Bool.not (BEq.beq x y))
 
@@ -189,6 +189,12 @@ def test_constr (app_0 : virtaddr) : (BitVec 32) :=
   let .virtaddr addr := app_0
   addr
 
+/-- Type quantifiers: n : Nat, n ≥ 0 -/
+def termination (n : Nat) : Int :=
+  if (BEq.beq n 0)
+  then 0
+  else (1 +i (termination (n -i 1)))
+
 def initialize_registers (_ : Unit) : Unit :=
   ()
 

diff --git a/test/lean/typquant.sail b/test/lean/typquant.sail
@@ -67,3 +67,13 @@ function hex_bits_signed2_backwards_matches(n, str) = true
  newtype virtaddr = virtaddr : bits(32)
 
 function test_constr (virtaddr(addr) : virtaddr) -> bits(32) = addr
+
+val termination : forall 'n, 'n >= 0. int('n) -> int
+
+function termination(n) = {
+  if n == 0 then {
+    0
+  } else {
+    1 + termination(n - 1)
+  }
+}