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.

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

Bdep #603

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

Bdep #603

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
277 commits
Select commit Hold shift + click to select a range
308aab1
nix
strub Dec 12, 2023
c31a5e4
lospec: automated formatting
strub Dec 12, 2023
7fb4bc8
lospec: failwith -> TypingError
strub Dec 12, 2023
9ef1dc2
lospec: kill warnings
strub Dec 12, 2023
277cc28
lospec: formatting
strub Dec 12, 2023
9b51d23
refactoring
strub Dec 12, 2023
806998c
lospec: ast
strub Dec 12, 2023
971b279
Change typing to return AST (In progress, map not done)
Gustavo2622 Dec 12, 2023
4f5ed12
Type AST should be done
Gustavo2622 Dec 13, 2023
7782bc4
Typing AST *should* be done
Gustavo2622 Dec 13, 2023
3c4d22f
Updated docs
Gustavo2622 Dec 13, 2023
82f0cce
Fixed issues with spec, added more mult variants and differentiated a…
Gustavo2622 Dec 13, 2023
d444d78
lospec: circuits
strub Dec 14, 2023
75cf839
lospec: fuzzer
strub Dec 15, 2023
c5fddee
lospec: compiles on all arch
strub Dec 15, 2023
629278f
lospec: remove warnings
strub Dec 15, 2023
fa77ddf
lospec: improve hash-consing
strub Dec 15, 2023
d295a03
nix
strub Dec 15, 2023
cd369bd
remove bck
strub Dec 15, 2023
2c53d48
Merge remote-tracking branch 'origin/main' into bdep
strub Dec 15, 2023
19e0367
WIP: Bit dependency generator from AST
Gustavo2622 Dec 19, 2023
7a1302c
Fixed add dependency and added mult
Gustavo2622 Dec 19, 2023
d5a9816
WIP: Push commit for bitdependency generator from AST
Gustavo2622 Dec 19, 2023
2da55f4
Added bitdep temp var propagation and map dependency generation
Gustavo2622 Dec 20, 2023
1fb4d8b
WIP: Bitdep Gen from AST - Fixed slice and other things for bitdep
Gustavo2622 Dec 20, 2023
9f71846
bitdep gen now works on examples/spec.txt
Gustavo2622 Dec 23, 2023
e0f6e76
Fixed map bit dep offsets
Gustavo2622 Dec 23, 2023
bcc6bed
Fixed shift semantics in bitdep
Gustavo2622 Dec 23, 2023
e720652
rework spec languages + AVX2 runtime
strub Jan 8, 2024
ba9f44f
fix
strub Jan 8, 2024
94808be
circuits: code refactoring
strub Jan 8, 2024
8bfc103
progress on circuit generation from specs
strub Jan 8, 2024
801f5ee
lospec: circuit generation
strub Jan 9, 2024
9109c98
lospec: CLI
strub Jan 9, 2024
a1ea92a
build
strub Jan 9, 2024
2afe1e6
lospec: factor out AST
strub Jan 9, 2024
e0a819e
lospec: positions in ptree
strub Jan 9, 2024
aeb16ee
lospec: localized typing errors
strub Jan 9, 2024
666e569
lospec: display source on error
strub Jan 9, 2024
fc6bb8b
typo
strub Jan 10, 2024
17912f1
drop AVX512
strub Jan 10, 2024
25c36da
lospec: all VP instructions of Kyber`s sampling
strub Jan 10, 2024
bf0cb8f
lospec: vpermq
strub Jan 10, 2024
1819d2f
lospec: example
strub Jan 11, 2024
670355c
TEMP: idassign
strub Jan 12, 2024
525c5e0
Merge branch 'rewrite-in-stmt-assign-2' into bdep
strub Jan 12, 2024
aa212e0
Added functions to bitdep
Gustavo2622 Jan 17, 2024
25a11ce
Bit dependency for new AST, untested
Gustavo2622 Jan 20, 2024
c6a59eb
Changed deps datastructure, fixed bugs in dep generation, added circu…
Gustavo2622 Jan 22, 2024
9446f1b
Fixed bugs in dependency generator
Gustavo2622 Jan 23, 2024
9003cc3
fixed more bugs
Gustavo2622 Jan 24, 2024
f3e09c0
evaluator first commit with Zarith
Gustavo2622 Jan 29, 2024
e0fdcfb
Added temp function context to evaluator
Gustavo2622 Jan 31, 2024
07f1b27
Added first version of AST BW evaluator (untested)
Gustavo2622 Feb 1, 2024
ee14d4e
Fixed evaluator bugs and added hardcoded evaluation to lospecs_test
Gustavo2622 Feb 2, 2024
1ec4ad3
Fixed concat bug on eval
Gustavo2622 Feb 2, 2024
71dc6b9
Refactored ERepeat in bitdep
Gustavo2622 Feb 2, 2024
d860ca3
Testing evaluator and fixing bugs
Gustavo2622 Feb 5, 2024
ae3022c
Fixed smul bugs
Gustavo2622 Feb 5, 2024
b8bdd4e
Finished testing basic ops
Gustavo2622 Feb 5, 2024
dbaddbd
Fully tested evaluator
Gustavo2622 Feb 6, 2024
9888e59
.
strub Feb 12, 2024
62fa6c8
Added stuff to ecBDep
Gustavo2622 Feb 12, 2024
21a3941
.
strub Feb 12, 2024
04c4183
Tentative 1st step
Gustavo2622 Feb 12, 2024
ca124ab
Added dep printing for generated circuits
Gustavo2622 Feb 14, 2024
e614964
Step one: Semi-tested version
Gustavo2622 Feb 15, 2024
3f58808
Tentative step 2
Gustavo2622 Feb 15, 2024
1706c3d
refactoring
strub Feb 27, 2024
549530a
aig equiv
strub Feb 27, 2024
39ebe72
Env doesnt update from rhs, inputs are parsed from EC
Gustavo2622 Feb 27, 2024
6851152
Added block equivalence checking
Gustavo2622 Feb 27, 2024
695565a
Added automatic processing based on return variables
Gustavo2622 Feb 27, 2024
f478ae8
Output
Gustavo2622 Mar 1, 2024
84757c2
.
strub Mar 1, 2024
7b4144b
Bruteforce testing
Gustavo2622 Mar 1, 2024
84717a8
Work plan 4/03
Gustavo2622 Mar 4, 2024
9a47583
First working example for circ from op for JWord.W16
Gustavo2622 Mar 6, 2024
1d34cdd
Polycompress circuit generation from op (lightly tested)
Gustavo2622 Mar 6, 2024
33cc560
Changed op
Gustavo2622 Mar 6, 2024
c86ac4e
First polycompress circuit working
Gustavo2622 Mar 7, 2024
5c9e395
Fixed bruteforce, added bitwuzla equivalence checking
Gustavo2622 Mar 8, 2024
d748e56
Cleanup
Gustavo2622 Mar 9, 2024
2be5f36
.
strub Mar 13, 2024
eaa369c
New example working
Gustavo2622 Mar 13, 2024
64886d2
Unhardcoded length
Gustavo2622 Mar 13, 2024
5752194
Fixed bug in bzequiv
Gustavo2622 Jun 18, 2024
ac814dc
Added high level API to name registers with strings
Gustavo2622 Jun 18, 2024
95c25e0
Added circuit input naming
Gustavo2622 Jun 18, 2024
5f017a6
Refactoring circuit functions into HLAig
Gustavo2622 Jun 19, 2024
c7bca79
Added bitstring and circuit env registering and operator precondition…
Gustavo2622 Jun 20, 2024
2ed8751
WIP: bdep tactic
Gustavo2622 Jun 21, 2024
35e1a2f
WIP: fixing types in bdep
Gustavo2622 Jun 24, 2024
7984f6f
WIP: Adding typesafe API for f_app
Gustavo2622 Jun 24, 2024
81254ce
WIP: converted pre and post in bdep to typesafe API
Gustavo2622 Jun 25, 2024
fb95a9f
WIP: Renamed p_lmap to p_map
Gustavo2622 Jun 25, 2024
02022bb
Improved CFold
Gustavo2622 Jun 25, 2024
a30e08d
WIP: Array explosion + new tactic
Gustavo2622 Jun 27, 2024
6035798
WIP: Fixed array get/set detection
Gustavo2622 Jun 29, 2024
69bb49e
WIP: (intermediate commit before refactoring HLAig)
Gustavo2622 Jul 2, 2024
2ae8d2a
WIP: Cleaner circuit implementation, working demo
Gustavo2622 Jul 2, 2024
411d4e3
WIP: If test working
Gustavo2622 Jul 3, 2024
3892e07
WIP: Proc translation: Barrett reduction (semi) working example
Gustavo2622 Jul 3, 2024
d700402
Merge remote-tracking branch 'origin/main' into bdep
strub Jul 4, 2024
5544931
CFold cleanup, Array tactic moved, SMT circ equiv modularized
Gustavo2622 Jul 4, 2024
66c5957
Fixed urem and added unit tests for urem and smod
Gustavo2622 Jul 4, 2024
e1fd3a7
Fixed bug in smod, barrett example now working
Gustavo2622 Jul 5, 2024
7bb2a7e
Original mapreduce working for polycompress
Gustavo2622 Jul 8, 2024
c4cf1b6
Optimizations for circuit gen and circuit auto tactics for normal and…
Gustavo2622 Jul 10, 2024
d38e008
WIP: bchange tactic (needs testing)
Gustavo2622 Jul 15, 2024
272ac2c
WIP: debug print for circ_equiv
Gustavo2622 Jul 24, 2024
4501c0f
mend
Gustavo2622 Jul 24, 2024
b1f221e
blash
Gustavo2622 Jul 24, 2024
b07ca8c
WIP: fixed naming bug (temporarily)
Gustavo2622 Jul 24, 2024
a3bdaf1
WIP: temp fix for circ equiv naming
Gustavo2622 Jul 24, 2024
2c5d8b4
WIP: Adding registering of QF_ABV bindings for EC ops
Gustavo2622 Jul 25, 2024
ee76855
Added QFABV bvadd bindings
Gustavo2622 Jul 25, 2024
6456d19
WIP: theory cloning for binding assurances
Gustavo2622 Jul 25, 2024
e7ad132
Bitstring certification and fixes for mapreduce postcondition WIP
Gustavo2622 Jul 31, 2024
9b9659a
WIP readded cloning
Gustavo2622 Aug 1, 2024
7d015af
WIP: Adding qfabv operator certification
Gustavo2622 Aug 2, 2024
6424651
Fixed postcondition for bdep mapreduce, improved parser spec for tactic
Gustavo2622 Aug 9, 2024
254162c
WIP: Rewrote circuit to match new abstraction, added (WIP) arrays
Gustavo2622 Aug 20, 2024
c53c62d
WIP: restoring mapreduce
Gustavo2622 Aug 21, 2024
5152364
Merge remote-tracking branch 'origin/main' into bdep
strub Aug 22, 2024
e9e2421
WIP: Added bsarray registering
Gustavo2622 Aug 22, 2024
90d2a74
Merge remote-tracking branch 'refs/remotes/origin/bdep' into bdep
Gustavo2622 Aug 22, 2024
41ce9ce
WIP: mapreduce for arrays, simple example working
Gustavo2622 Aug 22, 2024
5884f7d
WIP: Added array to_list registering and slicing operators
Gustavo2622 Aug 22, 2024
54ed6a0
deps
strub Aug 23, 2024
4830b25
deps
strub Aug 23, 2024
792f9b6
make "bind" a keyword again
strub Aug 23, 2024
ae4f398
EcCiruit: basic mli
strub Aug 23, 2024
5cb570b
remove examples that depend on JWord
strub Aug 23, 2024
84bba71
WIP: Added QFABV theory file
Gustavo2622 Aug 24, 2024
f836a2f
Merge remote-tracking branch 'refs/remotes/origin/bdep' into bdep
Gustavo2622 Aug 24, 2024
adae7b1
WIP: csubq with arrays
Gustavo2622 Aug 24, 2024
95694c6
WIP: propagate original precondition
Gustavo2622 Aug 25, 2024
b7e48bc
WIP: Zero extension and size checking for equivalence
Gustavo2622 Aug 27, 2024
d10110e
WIP: Added framing for bdep conseq
Gustavo2622 Aug 28, 2024
638f6ed
WIP: fixed bdep SMT bug
Gustavo2622 Aug 28, 2024
cde22bf
UNTESTED WIP: circuit based mapreduce equivalence
Gustavo2622 Sep 25, 2024
766df43
WIP: circuit based mapreduce equivalence
Gustavo2622 Sep 25, 2024
9a0957c
WIP: circuits for program equiv
Gustavo2622 Sep 26, 2024
b52a0f6
Fix for prhl proc rewrite
Gustavo2622 Sep 27, 2024
ee0abdc
Removed confusing error messages
Gustavo2622 Sep 27, 2024
2f6fa91
Added arithmetic right shift circuit for JWord
Gustavo2622 Sep 27, 2024
767a54d
WIP: asliceget/asliceset
Gustavo2622 Sep 27, 2024
4e03368
WIP: Added optional permutation to BDep
Gustavo2622 Oct 1, 2024
9db4f49
Fixed postcondition generation for permutation bdep
Gustavo2622 Oct 3, 2024
ab9f016
Merge remote-tracking branch 'origin/main' into bdep
strub Oct 4, 2024
df1a4d0
new ops for circuits
mbbarbosa-lectures Oct 7, 2024
222781c
Added precondition for bdepeq
Gustavo2622 Oct 7, 2024
f91208a
Multiple outputs for bdepeq
Gustavo2622 Oct 7, 2024
8ae8a6b
Added correct precond for lane pcond variant of bdepeq
Gustavo2622 Oct 7, 2024
3153548
Fixed pre condition generation in bdepeq
Gustavo2622 Oct 7, 2024
fc489e6
refactor binding of bitstrings
strub Oct 8, 2024
8c89fe4
nits
strub Oct 8, 2024
7859201
nits
strub Oct 8, 2024
3d746f0
binding arrays
strub Oct 8, 2024
a14de80
bind bv operators
strub Oct 8, 2024
3d70ac6
kill all warnings in EcEnv
strub Oct 8, 2024
798dba3
binding circuits - check op type
strub Oct 8, 2024
cb74176
Added bindings file
Gustavo2622 Oct 8, 2024
4ace7ae
fix imports of circuit related objects
strub Oct 9, 2024
ab5826b
progressing on sections
strub Oct 9, 2024
8311f76
done with sections
strub Oct 9, 2024
f1a8456
cloning, cleaning
strub Oct 9, 2024
7883d93
cleanup
strub Oct 9, 2024
34cff98
refactoring
strub Oct 10, 2024
70470f7
cleanup of lospec lib
strub Oct 10, 2024
e1d06a2
Merge remote-tracking branch 'origin/main' into bdep
strub Oct 10, 2024
35be0d9
nits
strub Oct 10, 2024
6fef389
nits
strub Oct 10, 2024
00f4bb3
nits
strub Oct 10, 2024
51098a1
nits
strub Oct 10, 2024
5e227dd
Added comments describing functions in src/ecCircuits.ml
Gustavo2622 Oct 10, 2024
4411b4c
reverse map
strub Oct 10, 2024
9b02e43
heterogeneous bv operators
strub Oct 11, 2024
32ec52c
binding of operators with arrays
strub Oct 11, 2024
636d2dd
refactoring (parser, variable lookup)
strub Oct 11, 2024
de2d1f0
no more strings
strub Oct 11, 2024
a2c40ce
fix compilation + remove dead code
strub Oct 11, 2024
2f9931e
refactor list functions
strub Oct 11, 2024
7bb7b5a
WIP, Untested: Removed most of hardcoded circuit gen, missing int con…
Gustavo2622 Oct 13, 2024
d0bbe5f
toint/ofint
strub Oct 14, 2024
37a6f2c
comparison operators
strub Oct 14, 2024
6ed4b84
complete reverse map
strub Oct 14, 2024
ced9610
Removed hardcoding in circuit gen, WIP actually finish the bindings
Gustavo2622 Oct 14, 2024
fa48002
Alias sub-expressions in statements
strub Oct 14, 2024
3dfd600
`proc rewrite` now supports the `/=` rule
strub Oct 15, 2024
a63d4a1
proc rewrite /= fix
strub Oct 15, 2024
07e0c4f
WIP, not working (yet): adding singed bvoperators and extract
Gustavo2622 Oct 15, 2024
ad4035a
WIP: added translation for sdiv, srem
Gustavo2622 Oct 15, 2024
8daa9a4
Int argument for extract
Gustavo2622 Oct 16, 2024
52cc5b6
The tactic `swap` now takes generalized code position.
strub Oct 16, 2024
c092139
nits
strub Oct 16, 2024
c4741f6
Added integer expression simplification in ecCircuits
Gustavo2622 Oct 16, 2024
b49967c
Theory for extract
Gustavo2622 Oct 16, 2024
1637f86
Concat op
Gustavo2622 Oct 16, 2024
e13839b
Added to_sint + signed theories (missing div and rem) and fixed conca…
Gustavo2622 Oct 16, 2024
3ec97e8
Updated bindings.ec
Gustavo2622 Oct 16, 2024
03c8825
nits
strub Oct 16, 2024
5a64534
Fixed control flow
Gustavo2622 Oct 16, 2024
7bd2843
nits
strub Oct 16, 2024
90b82f8
nits
strub Oct 16, 2024
b5959fc
nits
strub Oct 17, 2024
76e9779
Added support for true and false
Gustavo2622 Oct 18, 2024
e9fe694
Merge remote-tracking branch 'refs/remotes/origin/bdep' into bdep
Gustavo2622 Oct 18, 2024
1e842eb
Fixed bug in of_list
Gustavo2622 Oct 18, 2024
3f02c62
nits
strub Oct 18, 2024
89ed6f0
nits
strub Oct 18, 2024
15380f9
bugfixes
Gustavo2622 Oct 18, 2024
cf61fd7
Merge remote-tracking branch 'refs/remotes/origin/bdep' into bdep
Gustavo2622 Oct 18, 2024
49b46c9
nits
strub Oct 19, 2024
f392aa4
(Temporarily?) removed support for uninitialized program vars
Gustavo2622 Oct 20, 2024
558e3cd
Added map and init bvoperators
Gustavo2622 Oct 21, 2024
d1649fe
Added array inits
Gustavo2622 Oct 24, 2024
809b4b2
Added VPMULL
Gustavo2622 Oct 24, 2024
9b36d13
Sliceget/sliceset
Gustavo2622 Oct 24, 2024
470879c
Added Fapp support for fapply_safe
Gustavo2622 Oct 25, 2024
cd1b3be
WIP: not reducing bound ops
Gustavo2622 Oct 25, 2024
78784a9
Circuit generation working
Gustavo2622 Oct 25, 2024
b80e9be
Array get optimizations
Gustavo2622 Oct 26, 2024
095446a
some more bindings
mbbarbosa-lectures Oct 27, 2024
463ccc1
More optimizations
Gustavo2622 Oct 26, 2024
d101552
Merge remote-tracking branch 'refs/remotes/origin/bdep' into bdep
Gustavo2622 Oct 28, 2024
c6c4442
Array set optimization + status print changes
Gustavo2622 Oct 28, 2024
c6a5f34
fixed instruction semantics
mbbarbosa-lectures Oct 28, 2024
b5428e9
fixing AVXé
strub Oct 28, 2024
e7c90dc
Minor change to VPSLLV
Gustavo2622 Oct 28, 2024
3d05b4b
fixing left shifts
strub Oct 28, 2024
5245bc5
Fixed test for smod
Gustavo2622 Oct 28, 2024
3e2497c
circuits
strub Oct 28, 2024
26b8b76
Fixed smod tests and added ARMv7 spec
Gustavo2622 Oct 29, 2024
5ca3379
Tuple support + arm UMULHI_32
Gustavo2622 Oct 29, 2024
fb968b8
Tuple assignment uniformity
Gustavo2622 Oct 29, 2024
35ee4ae
lexer: do not lex decimal numbers when the parser won't accept them
strub Oct 29, 2024
13ce46c
unroll for: constant-propagate the counter
strub Oct 29, 2024
58d5777
fix "unroll for" failure (InvalidCPos)
strub Oct 30, 2024
637bc52
Fix deep code positions parsing
strub Oct 30, 2024
3ec3fa0
Clearer error messages on equiv failure
Gustavo2622 Oct 30, 2024
f48a08a
QFABV theory fixes
Gustavo2622 Nov 1, 2024
0afaec3
Semantic workaround for sliceget
Gustavo2622 Nov 3, 2024
ea2ac8c
Semantic workaround for sliceset
Gustavo2622 Nov 3, 2024
df30081
fixed typo
mbbarbosa-lectures Nov 4, 2024
17df76b
typo
mbbarbosa-lectures Nov 4, 2024
6993201
path for slice inits
mbbarbosa-lectures Nov 4, 2024
068e5e1
small tweak
mbbarbosa-lectures Nov 4, 2024
af5f720
Bitstring get
Gustavo2622 Nov 5, 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
2 changes: 1 addition & 1 deletion config/tests.config
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@ exclude = theories/prelude

[test-examples]
okdirs = !examples
exclude = examples/MEE-CBC examples/old examples/old/list-ddh !examples/incomplete examples/to-port
exclude = examples/MEE-CBC examples/exclude examples/old examples/old/list-ddh !examples/incomplete examples/to-port

[test-mee-cbc]
okdirs = examples/MEE-CBC
Expand Down
7 changes: 6 additions & 1 deletion dune
Original file line number Diff line number Diff line change
@@ -1,4 +1,9 @@
(dirs src theories examples scripts)
(env
(dev (flags -rectypes -warn-error -a+31 -w +28+33-9-23-32-58-67-69))
(release (flags -rectypes -warn-error -a+31 -w +28+33-9-23-32-58-67-69)
(ocamlopt_flags -O3 -unbox-closures)))

(dirs src libs theories examples scripts)

(install
(section (site (easycrypt commands)))
Expand Down
15 changes: 11 additions & 4 deletions dune-project
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
(lang dune 3.6)
(using menhir 2.0)
(lang dune 3.13)
(using menhir 3.0)
(using dune_site 0.1)

(wrapped_executables false)
Expand All @@ -10,17 +10,24 @@

(package
(name easycrypt)
(sites (lib theories) (libexec commands))
(sites (lib theories) (lib specs) (libexec commands))
(depends
(ocaml (>= 4.08.0))
(batteries (>= 3))
bitwuzla
(camlp-streams (>= 5))
camlzip
(dune (>= 3.6))
cmdliner
dune
dune-build-info
dune-site
hex
iter
(ocaml-inifiles (>= 1.2))
(pcre (>= 7))
ppx_deriving
ppx_deriving_yojson
(progress (>= 0.2))
(why3 (and (>= 1.7.0) (< 1.8)))
yojson
(zarith (>= 1.10))
Expand Down
9 changes: 8 additions & 1 deletion easycrypt.opam
Original file line number Diff line number Diff line change
Expand Up @@ -2,13 +2,20 @@
depends: [
"ocaml" {>= "4.08.0"}
"batteries" {>= "3"}
"bitwuzla"
"camlp-streams" {>= "5"}
"camlzip"
"dune" {>= "3.6" & >= "3.6"}
"cmdliner"
"dune" {>= "3.13"}
"dune-build-info"
"dune-site"
"hex"
"iter"
"ocaml-inifiles" {>= "1.2"}
"pcre" {>= "7"}
"ppx_deriving"
"ppx_deriving_yojson"
"progress" {>= "0.2"}
"why3" {>= "1.7.0" & < "1.8"}
"yojson"
"zarith" {>= "1.10"}
Expand Down
6 changes: 4 additions & 2 deletions easycrypt.project
Original file line number Diff line number Diff line change
@@ -1,4 +1,6 @@
[general]
provers = [email protected]
provers = [email protected]
provers = [email protected]
provers = [email protected]
provers = [email protected]

rdirs = Jasmin:jasmin/eclib
Loading