Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

defined and proved bbT #51

Draft
wants to merge 60 commits into
base: main
Choose a base branch
from
Draft

defined and proved bbT #51

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
60 commits
Select commit Hold shift + click to select a range
27c897a
defined and proved bbT
mhk119 Jan 24, 2023
43f82ac
fixed proof
mhk119 Jan 24, 2023
2f8d6a3
ult proved!
mhk119 Feb 26, 2023
368110f
unsigned lt, bit_add
mhk119 Mar 27, 2023
839c612
more progress on bitadd
mhk119 Mar 27, 2023
8be8a55
Merge remote-tracking branch 'upstream/main' into bitvec
mhk119 Mar 27, 2023
26bb6a4
toBooltoNat
mhk119 Apr 13, 2023
1df32a2
tobool_tonat
mhk119 Apr 20, 2023
c609eda
updates
mhk119 Apr 27, 2023
89f670f
bitwise_neg proved
mhk119 May 1, 2023
806520b
Merge remote-tracking branch 'upstream/main' into bitvec
mhk119 May 4, 2023
aecb1b1
bitneg done half of bitmul
mhk119 May 5, 2023
4759943
multiplication!!!
mhk119 May 13, 2023
0f6806c
extract, equality and concat
mhk119 May 18, 2023
0110cb5
resolved sorries in concat
mhk119 May 18, 2023
4c094db
signedext
mhk119 May 26, 2023
25e3aaa
all done!
mhk119 May 28, 2023
bd5b08b
shortened ult and addition
mhk119 Jun 5, 2023
4622e98
neg
mhk119 Jun 8, 2023
301eb18
new file for PR
mhk119 Jun 11, 2023
eb0f81f
fixed docstring text wrapping
mhk119 Jun 11, 2023
4aae913
append_assoc
mhk119 Jun 12, 2023
cdbc22a
deleted a file
mhk119 Jun 12, 2023
6535beb
append_assoc
mhk119 Jun 12, 2023
4358f63
extract_append
mhk119 Jun 15, 2023
e8a2dae
cast_heq
mhk119 Jun 15, 2023
8931496
rw rules
mhk119 Jun 18, 2023
b2654be
reformatted bit_neg
mhk119 Jun 19, 2023
64950d8
PROVED DIVISION!!!!
mhk119 Jun 24, 2023
2e15c79
finally imported Bitwise into BitVec
mhk119 Jun 25, 2023
e585f2a
proved bv_concat_extract_1
mhk119 Jun 25, 2023
3788572
reorganized things in BitVec
mhk119 Jun 29, 2023
ed845e2
some comments
mhk119 Jun 29, 2023
1ba9ff2
changed some names
mhk119 Jun 29, 2023
36ca628
cleaned up the sorries
mhk119 Jun 29, 2023
e71cde2
fixed naming
mhk119 Jun 29, 2023
52e74d9
trying the new def on toNat
mhk119 Jul 7, 2023
54801fe
changed toNat
mhk119 Jul 8, 2023
77c750e
delete old version
mhk119 Jul 8, 2023
ce7c28a
simplifications due to better toNat
mhk119 Jul 8, 2023
a56364e
redefined other operators in terms of toNat
mhk119 Jul 9, 2023
9001321
migrated mul to toNat
mhk119 Jul 9, 2023
87e3abe
slt, rotate_eliminate
mhk119 Jul 23, 2023
2abd372
rotate_left and rotate_right rw rules
mhk119 Aug 6, 2023
ba51835
merging stuff
mhk119 Aug 19, 2023
5fb2bbc
tactic finished
mhk119 Aug 24, 2023
41149f8
lint
mhk119 Aug 24, 2023
9c75998
changes
mhk119 Aug 27, 2023
c58f28b
sdiv
mhk119 Aug 28, 2023
a7472ca
sdiv
mhk119 Sep 3, 2023
c291585
new updates. rewrite rules, ext theorems
mhk119 Oct 19, 2023
11ba8ff
new changes to rewrite rules
mhk119 Nov 6, 2023
60851e2
new changes; redefine to match std
mhk119 Nov 17, 2023
1f8dfc9
defns changed to match std
mhk119 Nov 20, 2023
4c99c1f
fixed bug in tactic
mhk119 Nov 28, 2023
a6923f1
updates
mhk119 Nov 28, 2023
1042301
bug fix
mhk119 Nov 29, 2023
b9d860f
some changes
mhk119 Jan 16, 2024
dd06f6e
extra files
mhk119 Jan 16, 2024
8ae53c0
shorten proof
mhk119 Jun 3, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
51 changes: 25 additions & 26 deletions Smt/BitVec.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,15 +7,14 @@ Authors: Wojciech Nawrocki

import Lean
import Smt.Translator
import Smt.Data.BitVec

namespace Smt.BitVec

open Lean Expr
open Translator Term

@[smtTranslator] def replaceType : Translator
| e@(app (const ``BitVec _) n) => do
| e@(app (const `BitVec _) n) => do
let n ← Meta.whnf n
let some n ← Meta.evalNat n |>.run
| throwError "bitvector type{indentD e}\nhas variable width"
Expand All @@ -29,64 +28,64 @@ def mkLit (w : Nat) (n : Nat) : Term :=

@[smtTranslator] def replaceEq : Translator
-- TODO: we should really just support beq/bne across all types uniformly
| app (app (const ``BEq.beq _) (app (const ``BitVec _) _)) _ => return symbolT "="
| app (app (app (app (const ``bne _) (app (const ``BitVec _) _)) _) e) e' =>
| app (app (const ``BEq.beq _) (app (const `BitVec _) _)) _ => return symbolT "="
| app (app (app (app (const ``bne _) (app (const `BitVec _) _)) _) e) e' =>
return appT (symbolT "not") (mkApp2 (symbolT "=") (← applyTranslators! e) (← applyTranslators! e'))
| _ => return none

@[smtTranslator] def replaceFun : Translator
| e@(app (const ``BitVec.zero _) w) => do
| e@(app (const `BitVec.zero _) w) => do
let w ← reduceWidth w e
if w == 0 then throwError "cannot emit bitvector literal{indentD e}\nof bitwidth 0"
return mkLit w 0
| e@(app (app (const ``BitVec.ofNat _) w) n) => do
| e@(app (app (const `BitVec.ofNat _) w) n) => do
let w ← reduceWidth w e
let n ← reduceLit n e
if w == 0 then throwError "cannot emit bitvector literal{indentD e}\nof bitwidth 0"
return mkLit w n
| app (const ``BitVec.add _) _ => return symbolT "bvadd"
| app (const ``BitVec.sub _) _ => return symbolT "bvsub"
| app (const ``BitVec.mul _) _ => return symbolT "bvmul"
| app (const ``BitVec.mod _) _ => return symbolT "bvurem"
| app (const ``BitVec.div _) _ => return symbolT "bvudiv"
| app (const ``BitVec.lt _) _ => return symbolT "bvult"
| app (const ``BitVec.le _) _ => return symbolT "bvule"
| app (const ``BitVec.complement _) _ => return symbolT "bvnot"
| app (const ``BitVec.and _) _ => return symbolT "bvand"
| app (const ``BitVec.or _) _ => return symbolT "bvor"
| app (const ``BitVec.xor _) _ => return symbolT "bvxor"
| e@(app (app (app (const ``BitVec.shiftLeft _) w) x) n) => do
| app (const `BitVec.add _) _ => return symbolT "bvadd"
| app (const `BitVec.sub _) _ => return symbolT "bvsub"
| app (const `BitVec.mul _) _ => return symbolT "bvmul"
| app (const `BitVec.mod _) _ => return symbolT "bvurem"
| app (const `BitVec.div _) _ => return symbolT "bvudiv"
| app (const `BitVec.lt _) _ => return symbolT "bvult"
| app (const `BitVec.le _) _ => return symbolT "bvule"
| app (const `BitVec.complement _) _ => return symbolT "bvnot"
| app (const `BitVec.and _) _ => return symbolT "bvand"
| app (const `BitVec.or _) _ => return symbolT "bvor"
| app (const `BitVec.xor _) _ => return symbolT "bvxor"
| e@(app (app (app (const `BitVec.shiftLeft _) w) x) n) => do
let w ← reduceWidth w e
let n ← reduceLit n e
if w == 0 then throwError "cannot emit bitvector literal{indentD e}\nof bitwidth 0"
return mkApp2 (symbolT "bvshl") (← applyTranslators! x) (mkLit w n)
| e@(app (app (app (const ``BitVec.shiftRight _) w) x) n) => do
| e@(app (app (app (const `BitVec.shiftRight _) w) x) n) => do
let w ← reduceWidth w e
let n ← reduceLit n e
if w == 0 then throwError "cannot emit bitvector literal{indentD e}\nof bitwidth 0"
return mkApp2 (symbolT "bvlshr") (← applyTranslators! x) (mkLit w n)
| e@(app (app (app (const ``BitVec.rotateLeft _) _) x) n) => do
| e@(app (app (app (const `BitVec.rotateLeft _) _) x) n) => do
let n ← reduceLit n e
return appT
(mkApp2 (symbolT "_") (symbolT "rotate_left") (literalT (toString n)))
(← applyTranslators! x)
| e@(app (app (app (const ``BitVec.rotateRight _) _) x) n) => do
| e@(app (app (app (const `BitVec.rotateRight _) _) x) n) => do
let n ← reduceLit n e
return appT
(mkApp2 (symbolT "_") (symbolT "rotate_right") (literalT (toString n)))
(← applyTranslators! x)
| app (app (const ``BitVec.append _) _) _ => return symbolT "concat"
| e@(app (app (app (const ``BitVec.extract _) _) i) j) => do
| app (app (const `BitVec.append _) _) _ => return symbolT "concat"
| e@(app (app (app (const `BitVec.extract _) _) i) j) => do
let i ← reduceLit i e
let j ← reduceLit j e
return mkApp3 (symbolT "_") (symbolT "extract") (literalT (toString i)) (literalT (toString j))
| e@(app (app (const ``BitVec.repeat_ _) _) i) => do
| e@(app (app (const `BitVec.repeat_ _) _) i) => do
let i ← reduceLit i e
return mkApp2 (symbolT "_") (symbolT "repeat") (literalT (toString i))
| e@(app (app (const ``BitVec.zeroExtend _) _) i) => do
| e@(app (app (const `BitVec.zeroExtend _) _) i) => do
let i ← reduceLit i e
return mkApp2 (symbolT "_") (symbolT "zero_extend") (literalT (toString i))
| e@(app (app (const ``BitVec.signExtend _) _) i) => do
| e@(app (app (const `BitVec.signExtend _) _) i) => do
let i ← reduceLit i e
return mkApp2 (symbolT "_") (symbolT "sign_extend") (literalT (toString i))
| _ => return none
Expand Down
Loading