ZF* Roadmap
Please propose upgrades/improvements to ZF* (including upgrades to ZFS-Tools and Zulib) in this issue.
ZF*
-
Add syntax support for match! ... with ...
as in F# 4.5 -
Upgrade FSharp.Compatibility.OCaml
to0.1.14
-
Add support for 256-bit machine integers -
Change resolution of FStar.*
syntax sugar toZen.*
-
Make let!
/if!
/match!
desugar to whicheverletBang
/ifBang
/matchBang
is in scope -
Add functionality to extract .fsi
files from.fst
and.fsti
. -
Review extraction of machine integers -
Asset/ContractID/Hash/PubKey etc. literals
Zulib
-
Migrate to FAKE 5
for builds -
Deterministic builds -
Create modules for machine integer conversions, eg. Zen.Conversions.UInt64
-
Remove EX
case from definition ofFStar.Pervasives.result
-
Add functions for hashing single elements to Zen.Hash
, eg.ofHash
,ofAsset
,ofString
,ofByteArray
, etc. -
Place bounds on the codomain length of all to_string
functions, or use z3str to reason about them -
Define list functions like sum
,any
, etc. recursively, instead of using folds that are harder to reason about -
Add functions to hash locks to Zen.Hash.Sha3 -
Extend list module -
Add bitwise operations to machine integer modules, eg. lshift
,rshift
,logand
, etc. -
Switch to 256-bit arithmetic by default, add FStar.Int256
andFStar.UInt256
modules -
Create 'prelude' module, which includes Zen.Cost, Zen.Types, etc. -
Create 'bounded' modules for lists, arrays. These would contain functions that are defined on lists/arrays with length less than some maxLength
, eg.module Zen.List.Bounded val map(#a #b: Type): maxLength: nat -> f:(a -> b) -> ls:list a{ length ls <= maxLength} -> list b `cost` (maxLength * 2 + 2)
-
Improve facilities for handling polarities -
Create a module for Bloom Filters -
Add iterators for collections (set, dictionary, array, etc.) which converts them to lists (for the dictionary - a list of pairs).
ZFS-Tools
-
Do not elaborate Ghost
andGTot
annotated functions, in the same way thatLemma
is not elaborated -
Do not elaborate lists of constants -
Better error messages on elaborator error -
Reserve letBang
,ifBang
, andmatchBang
identifiers in elaborator -
Write script to generate 'Contract Templates' from contracts, and generate contracts from templates
Zebra
-
Accept z3rlimit as a decimal with SI suffix, eg zebra --z3rlimit 3.5M
would be equivalent tozebra --z3rlimit 3500000
-
Switches should not be cumulative, but should instead have behaviour dependent on other switches. eg. v
switch should verify the elaborated output if used in combination with thee
switch. -
Add verbose switch -
Add support for pass-through arguments to ZF*
Edited by A L Manning