Arrays with non-constant lengths - #1325

Draft

eponier wants to merge 29 commits into

mainfrom

array_unknown_size2

Commits on Mar 24, 2026

Remove useless import
eponier
committed
8e2ded3
change compiler (.v files)
eponier
committed
ee5fd2f
patch OCaml
eponier
committed
5634ab1
A few fixes, to recover the behavior of main
eponier
committed
f6b649b
Remove ALSub/Sub case
eponier
committed
482dd5c
Add some kind of templating
eponier
committed
0c54a2e
first example compiles
eponier
committed
616af1e
Greatly polishes templating
eponier
committed
a56fafe
add tests
eponier
committed
8af0673
new syntax
eponier
committed
064b174
Stricter typing of length vars
eponier
committed
fe10bfb
cleaner tests
eponier
committed
794ada1
hack for 0
eponier
committed
af99fb9
Fixes after rebase
eponier
committed
36bdbc3
new syntax with { }
eponier
committed
8f948d9
WIP: change to randombytes
eponier
committed
c7c4a75
WIP
eponier
committed
bfce2f2
polymorphic randombytes
eponier
committed
e2e12f5
array length is Z
eponier
committed
fd49027
Exit pprog
eponier
committed
9c3461b
More operators in type array_length
eponier
committed
131f74b
Better typechecking of syscalls
eponier
committed
cb6b36d
Inference of length args in the simple case
eponier
committed
cf28acb
Printing of length exprs uses printer of exprs
eponier
committed
f27eace
fix after rebase
eponier
committed
95c3164
Only one version of randombytes using bytes
eponier
committed
f4a4e9c
Better error when not the right number of args
eponier
committed
6d0e566
Fix env in pretyping
eponier
committed
207d4c1
fix after rebase
eponier
committed
987d5a5