index
:
vericert
debug/unhashed
dev-michalis
dev/asplos
dev/div
dev/divider
dev/full-nix-build
dev/mac-op
dev/michalis
dev/scheduling
dev/value
exp/inl-cse-const
master
stable
Vericert is a formally verified high-level synthesis tool.
about
summary
refs
log
tree
commit
diff
stats
log msg
author
committer
range
path:
root
/
src
/
hls
/
Predicate.v
Commit message (
Expand
)
Author
Age
Files
Lines
*
Split proof up into more files
Yann Herklotz
2023-05-09
1
-0
/
+6
*
Finish forward and backward proofs for predicated proof
Yann Herklotz
2023-05-05
1
-8
/
+0
*
Try and prove equivalence of predicated things
Yann Herklotz
2023-05-05
1
-0
/
+8
*
Continue proofs about Abstr.v
Yann Herklotz
2023-05-04
1
-31
/
+18
*
Add structural equality for predicates
Yann Herklotz
2023-05-02
1
-0
/
+29
*
Update Sat.v names
Yann Herklotz
2023-04-28
1
-63
/
+63
*
Change nat to positive in Sat proof
Yann Herklotz
2023-04-27
1
-18
/
+17
*
Finish sem_update_instr finally
Yann Herklotz
2023-02-12
1
-0
/
+52
*
Change evaluation of predicates and remove forest_evaluable
Yann Herklotz
2023-02-11
1
-0
/
+50
*
Add proof using to ifconversionproof
Yann Herklotz
2022-09-29
1
-1
/
+1
*
Add global monad notation using Instances
Yann Herklotz
2022-09-26
1
-1
/
+1
*
Work on implementing abstract predicates
Yann Herklotz
2022-07-19
1
-140
/
+193
*
Rearrange definitions and create IfConversion template
Yann Herklotz
2022-06-06
1
-0
/
+12
*
Fix many more lemmas
Yann Herklotz
2022-06-05
1
-0
/
+9
*
Work on CondElim proof
Yann Herklotz
2022-06-03
1
-3
/
+3
*
Abstract useful function into Predicate.v
Yann Herklotz
2022-05-31
1
-0
/
+7
*
Improve simplification of predicates
Yann Herklotz
2021-11-14
1
-2
/
+10
*
Add the tseytin transformation instead
Yann Herklotz
2021-11-14
1
-210
/
+359
*
Improve simplification of predicates
Yann Herklotz
2021-11-13
1
-57
/
+80
*
Add simplify operation and simplify IfConversion
Yann Herklotz
2021-11-11
1
-0
/
+58
*
Add intermediate step in proof of sem pres
Yann Herklotz
2021-10-27
1
-0
/
+26
*
Work more on equivalence of SAT
Yann Herklotz
2021-10-26
1
-0
/
+15
*
Add type-class proofs to Predicate.v
Yann Herklotz
2021-10-24
1
-4
/
+207
*
Add work towards decidability of SAT solver
Yann Herklotz
2021-10-21
1
-0
/
+201