Skip to content
Draft
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
396 commits
Select commit Hold shift + click to select a range
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
3cb9a99
Added xor and Rots (rots untested)
Gustavo2622 Nov 6, 2024
ea90494
Added type unfolding in binding search
Gustavo2622 Nov 6, 2024
fb482ee
Type unfolding fixes and pre/post generation for input/output array t…
Gustavo2622 Nov 6, 2024
700d348
Rol/ror fixes
Gustavo2622 Nov 6, 2024
fa09b2f
Added VPSHUFD_{128, 256}
Gustavo2622 Nov 7, 2024
12ff397
Fixed is_witness bug (when passing a non Fop)
Gustavo2622 Nov 7, 2024
12135bb
Fixes
Gustavo2622 Nov 7, 2024
2620add
popcount
strub Nov 8, 2024
2ad7572
Merge remote-tracking branch 'origin/main' into bdep
strub Nov 8, 2024
815618e
nits + remove dead code
strub Nov 8, 2024
1c46e9f
New tactic
Gustavo2622 Nov 8, 2024
7e8ba1f
nits (cfold)
strub Nov 8, 2024
604612d
.
strub Nov 8, 2024
5b2894f
Fine control over instr_equiv
Gustavo2622 Nov 8, 2024
4bc4724
unroll for*
strub Nov 8, 2024
ab80e38
.
strub Nov 8, 2024
c88b506
Instr equiv handle case when only one side set
Gustavo2622 Nov 8, 2024
adf51e2
Proc circuit gen after subst + simpl for bdep_form
Gustavo2622 Nov 8, 2024
0431c41
One more simplification for good measure
Gustavo2622 Nov 8, 2024
e77957b
.
strub Nov 9, 2024
6a103f7
Fixed bdepeq syntax
Gustavo2622 Nov 11, 2024
5136e09
Added option to bdepeq
Gustavo2622 Nov 11, 2024
bba1772
Comparison op theory fix
Gustavo2622 Nov 11, 2024
7debea1
Mapreduce split fix
Gustavo2622 Nov 11, 2024
9cadcda
Timing instrumentation for bdepeq
Gustavo2622 Nov 11, 2024
c27de22
BDep precondition generation unsoundness fix
Gustavo2622 Nov 11, 2024
0040117
More economic precondition for bdepeq
Gustavo2622 Nov 11, 2024
a07a54c
EXPERIMENTAL: bdep star (= bdep eval) tactic
Gustavo2622 Nov 11, 2024
dba99ce
Bdep star working : )
Gustavo2622 Nov 11, 2024
42f5bb9
Fixed edge case for of_bigsint
Gustavo2622 Nov 11, 2024
f91bdff
kill warnings
strub Nov 12, 2024
e65bcbd
Lane function + pcond generation fix (when op is bound directly)
Gustavo2622 Nov 12, 2024
d60ad58
Sign and better of_int for bdep_eval
Gustavo2622 Nov 12, 2024
f103e7a
remove assert
strub Nov 12, 2024
6f6839c
Precondition generation for bdep eval fix
Gustavo2622 Nov 12, 2024
34207a3
nits
strub Nov 12, 2024
250d601
Bdep input renaming fix
Gustavo2622 Nov 12, 2024
366f20d
Perm for bdep fixed
Gustavo2622 Nov 12, 2024
f987e09
nits
strub Nov 12, 2024
ff5663a
Inputs reversed for bdep
Gustavo2622 Nov 12, 2024
1aa5293
WIP
strub Nov 12, 2024
0d11e15
Actually reversed inputs this time
Gustavo2622 Nov 12, 2024
cd6555f
nits
strub Nov 12, 2024
c353c79
nits
strub Nov 13, 2024
fd267e3
stdlib
strub Nov 13, 2024
5b36f6f
nits
strub Nov 14, 2024
ff24051
specs
strub Nov 14, 2024
1d04ab9
qfabv
strub Nov 14, 2024
fa56c97
First pass on ecCircuits error handling
Gustavo2622 Nov 22, 2024
552bed8
First pass on ecPhlBDep error handling
Gustavo2622 Nov 24, 2024
7a8fddd
First refactor pass for ecPhlBDep
Gustavo2622 Nov 26, 2024
298c6d0
Second pass EcCircuits cleanup - Compute to zint and tuple refactoring
Gustavo2622 Nov 27, 2024
33c63f7
Bugfixes for BDep
Gustavo2622 Nov 29, 2024
39310b5
lazyly converting shifts to the correct type
mbbarbosa-lectures Nov 30, 2024
f865113
WIP: Better abstraction for ecCircuits
Gustavo2622 Dec 2, 2024
1038c8b
Second pass on ecCircuits abstraction
Gustavo2622 Dec 4, 2024
f50bd3a
Removed out.txt
Gustavo2622 Dec 12, 2024
a068502
WIP: Refactoring bdep, NOT COMPILING
Gustavo2622 Feb 3, 2025
ccefe93
WIP: Added more functionality
Gustavo2622 Feb 10, 2025
792d69f
WIP: Added baseop translations
Gustavo2622 Feb 11, 2025
cb2b11a
WIP: Added circ lambda implementations and further refactoring
Gustavo2622 Feb 12, 2025
64d8cd8
WIP: Added operator translations, next step: add operator translation…
Gustavo2622 Feb 13, 2025
475fcad
WIP: Added init translations and other stuff
Gustavo2622 Feb 14, 2025
8fcada5
WIP: Circ equivs refactored
Gustavo2622 Feb 17, 2025
2f76fb1
WIP: Mapreduce and dependency analysis implemented for refactoring
Gustavo2622 Feb 19, 2025
6dba1ed
WIP: Nearing the finish line
Gustavo2622 Feb 21, 2025
aee7b85
WIP: Finished refactoring, now testing
Gustavo2622 Feb 21, 2025
c97ce62
Fixed renaming bug
Gustavo2622 Feb 26, 2025
d102591
Misc fixes
Gustavo2622 Feb 26, 2025
4d70021
Compress working
Gustavo2622 Feb 26, 2025
405c471
Added test and small example working
Gustavo2622 Mar 12, 2025
53e0c35
f_loo generating circuit
Gustavo2622 Mar 13, 2025
7f6830e
Separation of concerns: Reg representation moved fully to backend
Gustavo2622 Mar 17, 2025
0688e81
Fixed VPSRA bindings, needs to be checked
Gustavo2622 Mar 18, 2025
3addec7
Better printing and sliceget fixes
Gustavo2622 Mar 18, 2025
141589d
Merged with origin/main
Gustavo2622 Mar 19, 2025
8288b26
Mapreduce paper simple examples
Gustavo2622 Mar 20, 2025
8565990
Added bdep solve + example
Gustavo2622 Mar 20, 2025
b5ed75f
Added context to bdep solve
Gustavo2622 Mar 20, 2025
33a6f93
Fixed circ_sat SMT input printing, fixed context for bdep solve
Gustavo2622 Mar 20, 2025
66efdd7
Filter example working
Gustavo2622 Mar 24, 2025
7ec289f
WIP: bdep slice (hack)
Gustavo2622 Mar 31, 2025
c9717f9
Generalized input alignment for bdep
Gustavo2622 Apr 2, 2025
753431d
Support for uninitialized inputs and proper checking for their presen…
Gustavo2622 Jul 25, 2025
d456013
Witness caching fix and uninit input check fix
Gustavo2622 Aug 5, 2025
01f21ac
Implemented slicing
Gustavo2622 Aug 8, 2025
cfc2e33
TEST: circuit rol index sixe fix
Gustavo2622 Aug 12, 2025
46886fd
Fixed smod and ror bugs, added rot test to Lospecs
Gustavo2622 Aug 13, 2025
9f22ece
Added input alignment check for bdep mapreduce
Gustavo2622 Aug 13, 2025
7205ffd
checking circuits
mbbarbosa Aug 16, 2025
433cbb4
WIP: Debugging tobytes
Gustavo2622 Aug 19, 2025
4abc833
fixed specs
mbbarbosa Aug 19, 2025
b5811d7
Added short-circuit for tuple assignments
Gustavo2622 Aug 19, 2025
ba65243
Added extra debug info when throwing uninitialized inputs error
Gustavo2622 Aug 19, 2025
91ac411
Added boolean not translation for circuits
Gustavo2622 Aug 26, 2025
1643573
First pass on printing for circuit code
Gustavo2622 Aug 26, 2025
e9a86ad
EcLowCircuits refactor + correctly cache circuits + mapreduce permuta…
Gustavo2622 Aug 29, 2025
bcd9c12
Generalized circuit decomposition
Gustavo2622 Sep 2, 2025
9813823
Better cache propagation and error message on failed binding size lookup
Gustavo2622 Sep 8, 2025
be7b2c6
Simplifying forms before computing
Gustavo2622 Sep 8, 2025
85f35ce
Restoring dependency error messages
Gustavo2622 Sep 8, 2025
f433cb0
(Hopefully) better error messages
Gustavo2622 Sep 8, 2025
6313f89
Removed catchable from tc_error
Gustavo2622 Sep 8, 2025
7a9c4d0
Lospecs cleanup
Gustavo2622 Sep 9, 2025
cf546c4
Properly restoring error messages for dependency check fail
Gustavo2622 Sep 9, 2025
83954bb
WIP: abstract bindings
Gustavo2622 Sep 10, 2025
53b87f7
Changed reduction in EcScope bindings processing
Gustavo2622 Sep 10, 2025
7760ba8
TEST
Gustavo2622 Sep 10, 2025
87fb2b7
Revert prev
Gustavo2622 Sep 10, 2025
a4efacf
Fixed opp binding
Gustavo2622 Sep 10, 2025
58c0795
Transitioned reg type to node arrav (vs node list as before)
Gustavo2622 Sep 11, 2025
63888bc
Flake commit (TEMP)
Gustavo2622 Sep 12, 2025
7d32b60
Merge remote-tracking branch 'origin/main' into bdep_ecCircuitsRefactor
Gustavo2622 Sep 12, 2025
ae9418d
WIP: test commit for merge
Gustavo2622 Sep 12, 2025
57a2e2b
Remove asserts pass
Gustavo2622 Sep 17, 2025
2aedd5d
Some cleanup on bdep
Gustavo2622 Sep 22, 2025
4da72a2
cleanup
strub Sep 26, 2025
6effb11
Merge remote-tracking branch 'origin/main' into bdep_ecCircuitsRefactor
strub Sep 26, 2025
6f04c3e
cleanup
strub Sep 26, 2025
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 3rdparty src etc 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 3rdparty src etc libs theories examples scripts)

(install
(section (site (easycrypt commands)))
Expand Down
3 changes: 2 additions & 1 deletion dune-project
Original file line number Diff line number Diff line change
Expand Up @@ -13,7 +13,8 @@
(sites (lib theories) (libexec commands) (lib config))
(depends
(ocaml (>= 4.08.0))
(batteries (>= 3))
(batteries (>= 3.9))
bitwuzla
(camlp-streams (>= 5))
camlzip
dune
Expand Down
3 changes: 2 additions & 1 deletion easycrypt.opam
Original file line number Diff line number Diff line change
@@ -1,7 +1,8 @@
# This file is generated by dune, edit dune-project instead
depends: [
"ocaml" {>= "4.08.0"}
"batteries" {>= "3"}
"batteries" {>= "3.9"}
"bitwuzla"
"camlp-streams" {>= "5"}
"camlzip"
"dune" {>= "3.13"}
Expand Down
Loading
Loading