Introduce ub variant for Result

backends/lean/Aeneas/Std/Array/Core.lean

@@ -37,6 +37,7 @@ def List.clone (clone : α → Result α) (l : List α) : Result ({ l' : List α
   match h :List.mapM clone l with
   | ok v => ok ⟨ v, by have := List.mapM_Result_length h; scalar_tac ⟩
   | fail e => fail e
+  | ub => ub
   | div => div
 
 @[step]

backends/lean/Aeneas/Std/Core/Ops.lean

@@ -77,6 +77,7 @@ def BuiltinFnMut (Inputs : Type u) (Outputs : Type v) : core.ops.function.FnMut
     match f x with
     | ok y => ok (y, f)
     | fail e => fail e
+    | ub => ub
     | div => div
 }
 

backends/lean/Aeneas/Std/Primitives.lean

@@ -63,6 +63,7 @@ open Error
 inductive Result (α : Type u) where
   | ok (v: α): Result α
   | fail (e: Error): Result α
+  | ub
   | div
 deriving Repr, BEq
 
@@ -82,12 +83,12 @@ instance Result_Nonempty (α : Type u) : Nonempty (Result α) :=
 def ok? {α: Type u} (r: Result α): Bool :=
   match r with
   | ok _ => true
-  | fail _ | div => false
+  | fail _ | ub | div => false
 
 def div? {α: Type u} (r: Result α): Bool :=
   match r with
   | div => true
-  | ok _ | fail _ => false
+  | ok _ | fail _ | ub => false
 
 def massert (b : Prop) [Decidable b] : Result Unit :=
   if b then ok () else fail assertionFailure
@@ -119,6 +120,7 @@ def bind {α : Type u} {β : Type v} (x: Result α) (f: α → Result β) : Resu
   match x with
   | ok v  => f v
   | fail v => fail v
+  | ub => ub
   | div => div
 
 -- Allows using Result in do-blocks
@@ -131,6 +133,7 @@ instance : Pure Result where
 
 @[simp] theorem bind_ok (x : α) (f : α → Result β) : bind (.ok x) f = f x := by simp [bind]
 @[simp] theorem bind_fail (x : Error) (f : α → Result β) : bind (.fail x) f = .fail x := by simp [bind]
+@[simp] theorem bind_ub (f : α → Result β) : bind .ub f = .ub := by simp [bind]
 @[simp] theorem bind_div (f : α → Result β) : bind .div f = .div := by simp [bind]
 
 @[simp] theorem bind_tc_ok (x : α) (f : α → Result β) :
@@ -139,6 +142,9 @@ instance : Pure Result where
 @[simp] theorem bind_tc_fail (x : Error) (f : α → Result β) :
   (do let y ← fail x; f y) = fail x := by simp [Bind.bind, bind]
 
+@[simp] theorem bind_tc_ub (f : α → Result β) :
+  (do let y ← ub; f y) = ub := by simp [Bind.bind, bind]
+
 @[simp] theorem bind_tc_div (f : α → Result β) :
   (do let y ← div; f y) = div := by simp [Bind.bind, bind]
 
@@ -178,6 +184,7 @@ noncomputable instance : MonoBind Result where
     · exact h _
     · exact FlatOrder.rel.refl
     · exact FlatOrder.rel.refl
+    . exact FlatOrder.rel.refl
 
 end Order
 
@@ -284,6 +291,7 @@ def loop {α : Type u} {β : Type v} (body : α → Result (ControlFlow α β))
     | ControlFlow.cont x => loop body x
     | ControlFlow.done x => ok x
   | fail e => fail e
+  | ub => ub
   | div => div
 partial_fixpoint
 

backends/lean/Aeneas/Std/Scalar/Ops/Mul.lean

@@ -43,7 +43,8 @@ theorem UScalar.mul_equiv {ty} (x y : UScalar ty) :
   match mul x y with
   | ok z => x.val * y.val ≤ UScalar.max ty ∧ (↑z : Nat) = ↑x * ↑y ∧ z.bv = x.bv * y.bv
   | fail _ => UScalar.max ty < x.val * y.val
-  | .div => False := by
+  | ub => False
+  | div => False := by
   simp only [mul]
   have := tryMk_eq ty (x.val * y.val)
   split <;> simp_all only [inBounds, true_and, not_lt, gt_iff_lt]
@@ -73,7 +74,8 @@ theorem IScalar.mul_equiv {ty} (x y : IScalar ty) :
   match mul x y with
   | ok z => IScalar.min ty ≤ x.val * y.val ∧ x.val * y.val ≤ IScalar.max ty ∧ z.val = x.val * y.val ∧ z.bv = x.bv * y.bv
   | fail _ => ¬(IScalar.min ty ≤ x.val * y.val ∧ x.val * y.val ≤ IScalar.max ty)
-  | .div => False := by
+  | ub => False
+  | div => False := by
   simp only [mul, not_and, not_le]
   have := tryMk_eq ty (x.val * y.val)
   split <;> simp_all only [inBounds, min, max, true_and, not_and, not_lt] <;>

backends/lean/Aeneas/Std/Slice.lean

@@ -1012,6 +1012,7 @@ def Slice.mapM  {α β} (f : α → Result β) (x : Slice α) : Result (Slice β
   match h : x.val.mapM f with
   | ok xs  => ok ⟨xs, List.mapM_Result_length h ▸ x.prop⟩
   | fail e => fail e
+  | ub => ub
   | div    => div
 
 @[step]
@@ -1047,6 +1048,7 @@ theorem Slice.mapM_spec {α β} {f : α → Result β} {s : Slice α} {post : Na
     exact hf
   case h_2 e heq => simp [hl'] at heq
   case h_3 heq => simp [hl'] at heq
+  case h_4 heq => simp [hl'] at heq
 
 -- ============================================================================
 -- Slice.fill — overwrite every element with a clone of `v`
@@ -1060,6 +1062,7 @@ def core.slice.Slice.fill {T : Type} (cloneInst : core.clone.Clone T)
   match h : s.val.mapM (fun _ => cloneInst.clone v) with
   | .ok val => .ok ⟨val, List.mapM_Result_length h ▸ s.property⟩
   | .fail e => .fail e
+  | .ub => .ub
   | .div => .div
 
 private theorem List.mapM_const_ok {T : Type} (l : List T)
@@ -1087,11 +1090,13 @@ theorem core.slice.Slice.fill.spec {T : Type} (cloneInst : core.clone.Clone T)
     | .ok v' =>
       congr 1; have := hclone; rw [hc] at this; simp [WP.wp_return] at this; exact this
     | .fail _ => exfalso; have := hclone; rw [hc] at this; simp at this
+    | .ub => exfalso; have := hclone; rw [hc] at this; simp at this
     | .div => exfalso; have := hclone; rw [hc] at this; simp at this
   have hmapM := List.mapM_const_ok s.val hcl
   split
   · rename_i val heq; rw [hmapM] at heq; cases heq; simp [spec_ok, Slice.length, List.length_replicate]
   · exfalso; simp_all
   · exfalso; simp_all
+  · exfalso; simp_all
 
 end Aeneas.Std

backends/lean/Aeneas/Std/Vec.lean

@@ -182,6 +182,7 @@ def Vec.index_mut_usize {α : Type u} (v: Vec α) (i: Usize) :
   | ok x =>
     ok (x, Vec.set v i)
   | fail e => fail e
+  | ub => ub
   | div => div
 
 @[step]
@@ -357,6 +358,7 @@ def alloc.vec.Vec.extend_from_slice {T : Type} (cloneInst : core.clone.Clone T)
     | ok s' =>
       ok ⟨ v.val ++ s'.val , by have := Slice.clone_length h'; scalar_tac ⟩
     | fail e => fail e
+    | ub => ub
     | div => div
   else fail .panic
 

backends/lean/Aeneas/Std/WP.lean

@@ -19,6 +19,7 @@ def theta (m:Result α) : Wp α :=
   match m with
   | ok x => wp_return x
   | fail _ => fun _ => False
+  | ub => fun _ => False
   | div => fun _ => False
 
 def spec {α} (x:Result α) (p:Post α) :=
@@ -28,6 +29,7 @@ def dspec {α} (x:Result α) (p:Post α) :=
   match x with
   | ok x => p x
   | fail _ => False
+  | ub => False
   | div => True
 
 theorem spec_dspec (α) (x : Result α) (p: Post α) : spec x p → dspec x p := by
@@ -61,6 +63,9 @@ theorem spec_ok (x : α) : spec (ok x) p ↔ p x := by simp [spec, theta, wp_ret
 @[simp, grind =, agrind =]
 theorem spec_fail (e : Error) : spec (fail e) p ↔ False := by simp [spec, theta]
 
+@[simp, grind =, agrind =]
+theorem spec_ub : spec ub p ↔ False := by simp [spec, theta]
+
 @[simp, grind =, agrind =]
 theorem spec_div : spec div p ↔ False := by simp [spec, theta]
 
@@ -77,6 +82,10 @@ theorem spec_ok_pair {α β} (a : α) (b : β) (f : α → β → Prop) :
 theorem spec_fail_pair (e : Error) (f : α → β → Prop) :
     spec (fail e) (uncurry f) ↔ False := by simp
 
+@[simp, grind =, agrind =]
+theorem spec_ub_pair (f : α → β → Prop) :
+    spec ub (uncurry f) ↔ False := by simp
+
 @[simp, grind =, agrind =]
 theorem spec_div_pair (f : α → β → Prop) :
     spec div (uncurry f) ↔ False := by simp
@@ -101,6 +110,8 @@ theorem spec_bind {α β} {k : α -> Result β} {Pₖ : Post β} {m : Result α}
     apply Hm
   · simp
     apply Hm
+  · simp
+    apply Hm
 
 /-- Small helper to currify functions -/
 def curry {α β γ} (f : α × β → γ) (x : α) : β → γ := fun y => f (x, y)
@@ -149,6 +160,8 @@ theorem spec_bind' {α β} {k : α -> Result β} {Pₖ : Post β} {m : Result α
     apply Hm
   · simp
     apply Hm
+  · simp
+    apply Hm
 
 /-- We use this lemma to decompose nested `uncurry'` predicates into a sequence of universal quantifiers. -/
 @[simp]
@@ -216,6 +229,8 @@ theorem dspec_bind' {α β} {k : α -> Result β} {Pₖ : Post β} {m : Result 
     apply Hm
   · simp
     apply Hm
+  · simp
+    apply Hm
 
 @[simp]
 def qimp_dspec_uncurry' {α₀ α₁ β} (P : α₀ → α₁ → Prop) (k : α₀ × α₁ → Result β) (Q : β → Prop) :
@@ -791,7 +806,7 @@ open Std.Do
 
 instance Result.instWP : WP Result.{u} (.except (ULift Error) (.except PUnit .pure)) where
   wp x := {
-    trans Q := match x with | .ok a => Q.1 a | .fail e => Q.2.1 (ULift.up e) | .div => Q.2.2.1 .unit
+    trans Q := match x with | .ok a => Q.1 a | .fail e => Q.2.1 (ULift.up e) | .ub => ⟨False⟩ | .div => Q.2.2.1 .unit
     conjunctiveRaw Q₁ Q₂ := by
       apply SPred.bientails.of_eq
       cases x <;> simp