chore: simplify a proof in mvcgen test cases and remove duplicate (#12547)
This commit is contained in:
Sebastian Graf
GitHub
parent
e7aa785822
commit
6cf1c4a1be
2 changed files with 12 additions and 161 deletions
|
|
@ -533,149 +533,6 @@ example (p : Nat → Prop) [DecidablePred p] (n : Nat) :
|
|||
|
||||
end Automated
|
||||
|
||||
namespace Aeneas
|
||||
|
||||
inductive Error where
|
||||
| assertionFailure: Error
|
||||
| integerOverflow: Error
|
||||
| divisionByZero: Error
|
||||
| arrayOutOfBounds: Error
|
||||
| maximumSizeExceeded: Error
|
||||
| panic: Error
|
||||
| undef: Error
|
||||
|
||||
open Error
|
||||
|
||||
inductive Result (α : Type u) where
|
||||
| ok (v: α): Result α
|
||||
| fail (e: Error): Result α
|
||||
| div
|
||||
|
||||
instance : Monad Result where
|
||||
pure x := .ok x
|
||||
bind x f := match x with
|
||||
| .ok v => f v
|
||||
| .fail e => .fail e
|
||||
| .div => .div
|
||||
|
||||
instance : LawfulMonad Result :=
|
||||
LawfulMonad.mk' _
|
||||
(by dsimp only [Functor.map]; grind)
|
||||
(by dsimp only [bind]; grind)
|
||||
(by dsimp only [bind]; grind)
|
||||
|
||||
abbrev _root_.Std.Do.PredTrans.pushResult (x : Result α) : PredTrans (.except Error .pure) α :=
|
||||
match x with
|
||||
| .ok v => PredTrans.pure v
|
||||
| .fail e => PredTrans.throw e
|
||||
| .div => PredTrans.const ⌜False⌝
|
||||
|
||||
@[simp]
|
||||
theorem Result.apply_pushResult_pure {α} {a : α} {Q : PostCond α (.except Error .pure)} :
|
||||
(PredTrans.pushResult (pure a)).apply Q = Q.1 a := by rfl
|
||||
|
||||
@[simp]
|
||||
theorem Result.apply_pushResult_bind {α β} {x : Result α} {f : α → Result β} {Q : PostCond β (.except Error .pure)} :
|
||||
(PredTrans.pushResult (do let a ← x; f a)).apply Q =
|
||||
(PredTrans.pushResult x).apply (fun a => (PredTrans.pushResult (f a)).apply Q, Q.2) := by
|
||||
simp only [PredTrans.pushResult, bind]
|
||||
grind
|
||||
|
||||
instance Result.instWP : WP Result (.except Error .pure) where
|
||||
wp := PredTrans.pushResult
|
||||
|
||||
instance Result.instWPMonad : WPMonad Result (.except Error .pure) where
|
||||
wp_pure _ := by ext Q; simp [wp]
|
||||
wp_bind x f := by ext Q; simp [wp]
|
||||
|
||||
theorem Result.of_wp {α} {x : Result α} (P : Result α → Prop) :
|
||||
(⊢ₛ wp⟦x⟧ post⟨fun a => ⌜P (.ok a)⌝, fun e => ⌜P (.fail e)⌝⟩) → P x := by
|
||||
intro hspec
|
||||
match x with
|
||||
| .ok a => simpa [wp] using hspec
|
||||
| .fail e => simpa [wp] using hspec
|
||||
| .div => simp [wp] at hspec
|
||||
|
||||
/-- Kinds of unsigned integers -/
|
||||
inductive UScalarTy where
|
||||
| Usize
|
||||
| U8
|
||||
| U16
|
||||
| U32
|
||||
| U64
|
||||
| U128
|
||||
|
||||
def UScalarTy.numBits (ty : UScalarTy) : Nat :=
|
||||
match ty with
|
||||
| Usize => System.Platform.numBits
|
||||
| U8 => 8
|
||||
| U16 => 16
|
||||
| U32 => 32
|
||||
| U64 => 64
|
||||
| U128 => 128
|
||||
|
||||
/-- Signed integer -/
|
||||
structure UScalar (ty : UScalarTy) where
|
||||
/- The internal representation is a bit-vector -/
|
||||
bv : BitVec ty.numBits
|
||||
deriving Repr, BEq, DecidableEq
|
||||
|
||||
def UScalar.val {ty} (x : UScalar ty) : Nat := x.bv.toNat
|
||||
|
||||
def UScalar.ofNatCore {ty : UScalarTy} (x : Nat) (_ : x < 2^ty.numBits) : UScalar ty :=
|
||||
{ bv := BitVec.ofNat _ x }
|
||||
|
||||
instance (ty : UScalarTy) : CoeOut (UScalar ty) Nat where
|
||||
coe := λ v => v.val
|
||||
|
||||
def UScalar.tryMk (ty : UScalarTy) (x : Nat) : Result (UScalar ty) :=
|
||||
sorry
|
||||
|
||||
def UScalar.add {ty : UScalarTy} (x y : UScalar ty) : Result (UScalar ty) :=
|
||||
UScalar.tryMk ty (x.val + y.val)
|
||||
|
||||
instance {ty} : HAdd (UScalar ty) (UScalar ty) (Result (UScalar ty)) where
|
||||
hAdd x y := UScalar.add x y
|
||||
|
||||
@[irreducible]
|
||||
def UScalar.max (ty : UScalarTy) : Nat := 2^ty.numBits-1
|
||||
|
||||
theorem UScalar.add_spec {ty} {x y : UScalar ty}
|
||||
(hmax : ↑x + ↑y ≤ UScalar.max ty) :
|
||||
∃ z, x + y = Result.ok z ∧ (↑z : Nat) = ↑x + ↑y := sorry
|
||||
|
||||
abbrev U32 := UScalar .U32
|
||||
abbrev U32.max : Nat := UScalar.max .U32
|
||||
|
||||
theorem U32.add_spec {x y : U32} (hmax : x.val + y.val ≤ U32.max) :
|
||||
∃ z, x + y = Result.ok z ∧ (↑z : Nat) = ↑x + ↑y :=
|
||||
UScalar.add_spec sorry -- (by scalar_tac)
|
||||
|
||||
abbrev PCond (α : Type) := PostCond α (PostShape.except Error PostShape.pure)
|
||||
|
||||
@[spec]
|
||||
theorem U32.add_spec' {x y : U32} {Q : PCond U32} (hmax : ↑x + ↑y ≤ U32.max):
|
||||
⦃Q.1 (UScalar.ofNatCore (↑x + ↑y) sorry)⦄ (x + y) ⦃Q⦄ := by
|
||||
mintro h
|
||||
have ⟨z, ⟨hxy, hz⟩⟩ := U32.add_spec hmax
|
||||
simp [hxy, hz.symm, wp]
|
||||
sorry -- show Q.1 z ↔ Q.1 (ofNatCore z.val ⋯)
|
||||
|
||||
@[simp]
|
||||
theorem UScalar.ofNatCore_val_eq : (ofNatCore x h).val = x := sorry
|
||||
|
||||
def mul2_add1 (x : U32) : Result U32 :=
|
||||
do
|
||||
let i ← x + x
|
||||
i + (UScalar.ofNatCore 1 sorry : U32)
|
||||
|
||||
theorem mul2_add1_spec' (x : U32) (h : 2 * x.val + 1 ≤ U32.max)
|
||||
: ⦃Q.1 (UScalar.ofNatCore (2 * ↑x + (1 : Nat)) sorry)⦄ (mul2_add1 x) ⦃Q⦄ := by
|
||||
mvcgen [mul2_add1]
|
||||
all_goals simp_all +arith; try omega
|
||||
|
||||
end Aeneas
|
||||
|
||||
namespace VSTTE2010
|
||||
|
||||
namespace MaxAndSum
|
||||
|
|
|
|||
|
|
@ -214,29 +214,23 @@ instance : LawfulMonad Result :=
|
|||
(by dsimp only [bind]; grind)
|
||||
(by dsimp only [bind]; grind)
|
||||
|
||||
abbrev _root_.Std.Do.PredTrans.pushResult (x : Result α) : PredTrans (.except Error .pure) α :=
|
||||
match x with
|
||||
| .ok v => PredTrans.pure v
|
||||
| .fail e => PredTrans.throw e
|
||||
| .div => PredTrans.const ⌜False⌝
|
||||
instance Result.instWP : WP Result (.except Error .pure) where
|
||||
wp
|
||||
| .ok v => PredTrans.pure v
|
||||
| .fail e => PredTrans.throw e
|
||||
| .div => PredTrans.const ⌜False⌝
|
||||
|
||||
@[simp]
|
||||
theorem Result.apply_pushResult_pure {α} {a : α} {Q : PostCond α (.except Error .pure)} :
|
||||
(PredTrans.pushResult (pure a)).apply Q = Q.1 a := by rfl
|
||||
theorem Result.apply_wp_pure {α} {a : α} {Q : PostCond α (.except Error .pure)} :
|
||||
wp⟦pure (f := Result) a⟧ Q = Q.1 a := by rfl
|
||||
|
||||
@[simp]
|
||||
theorem Result.apply_pushResult_bind {α β} {x : Result α} {f : α → Result β} {Q : PostCond β (.except Error .pure)} :
|
||||
(PredTrans.pushResult (do let a ← x; f a)).apply Q =
|
||||
(PredTrans.pushResult x).apply (fun a => (PredTrans.pushResult (f a)).apply Q, Q.2) := by
|
||||
simp only [PredTrans.pushResult, bind]
|
||||
theorem Result.apply_wp_bind {α β} {x : Result α} {f : α → Result β} {Q : PostCond β (.except Error .pure)} :
|
||||
wp⟦do let a ← x; f a⟧ Q = wp⟦x⟧ (fun a => wp⟦f a⟧ Q, Q.2) := by
|
||||
simp only [wp, bind]
|
||||
grind
|
||||
|
||||
instance Result.instWP : WP Result (.except Error .pure) where
|
||||
wp := PredTrans.pushResult
|
||||
|
||||
instance Result.instWPMonad : WPMonad Result (.except Error .pure) where
|
||||
wp_pure _ := by ext Q; simp [wp]
|
||||
wp_bind x f := by ext Q; simp [wp]
|
||||
wp_pure _ := by ext Q : 1; apply Result.apply_wp_pure
|
||||
wp_bind x f := by ext Q : 1; apply Result.apply_wp_bind
|
||||
|
||||
theorem Result.of_wp {α} {x : Result α} (P : Result α → Prop) :
|
||||
(⊢ₛ wp⟦x⟧ post⟨fun a => ⌜P (.ok a)⌝, fun e => ⌜P (.fail e)⌝⟩) → P x := by
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue