It requires some changes to the source code to generate better F* code.
In particular, we work around some issues around the use of question-marks until they are resolved in hax (see https://github.com/hacspec/hax/issues/15)
It also requires some hand-edits to the generated F*, to add let rec for recursive functions, and to add a trait implementation for mutable Bytes
Type of change
[ ] Bug fix
[X] New feature
[ ] Breaking change
[ ] Documentation
[ ] Automation
Motivation and Context
This is part of the formal verification of Bertie.
Changes
Checklist
[X] I have linked an issue to this PR
[X] I have described the changes
[ ] I have read and understood the code of conduct, contribution guidelines, and contributor license agreement
[ ] I have added tests for all changes
[ ] I have tested that all tests pass locally and all checks pass
This PR addresses issue #86.
It requires some changes to the source code to generate better F* code. In particular, we work around some issues around the use of question-marks until they are resolved in hax (see https://github.com/hacspec/hax/issues/15)
It also requires some hand-edits to the generated F*, to add
let recfor recursive functions, and to add a trait implementation for mutableBytesType of change
Motivation and Context
This is part of the formal verification of Bertie.
Changes
Checklist
Fixes #