Skip to content

Latest commit

 

History

History
66 lines (48 loc) · 2.65 KB

CHANGES.md

File metadata and controls

66 lines (48 loc) · 2.65 KB

master

Guidelines for the changelog:

  • There should be an entry, however brief, for each user-facing change to F*.
  • Entries should include a link to a PR if at all possible, which can provide rationale and a detailed technical explanation.
  • Each section lists PRs in ascending numerical order, then entries without a PR in roughly chronological order.
  • Changes that break existing code should explain how to update the code, possibly with details in the PR or links to sample fixes (for example, changes to F*'s test suite).

Standard library

  • commit FStar@f73f295e The specifications for the machine integer libraries (Int64.fst, UInt64.fst, etc) now forbid several forms of undefined behavior in C.

    The signed arithmetic add_underspec, sub_underspec, and mul_underspec functions have been removed.

    Shifts have a precondition that the shift is less than the bitwidth.

    Existing code may need additional preconditions to verify (for example, see a fix to HACL*). Code that relied on undefined behavior is unsafe, but it can be extracted using assume or admit.

C Extraction

  • PR #1176 inline_for_extraction on a type annotation now unfolds it at extraction time. This can help to reveal first-order code for C extraction; see FStarLang/kremlin #51.

Command line options

  • --hint_stats and --check_hints are gone b50c88930e3f2655704696902693941525f6cf9f. The former was rarely used. The latter may be restored, but the code was too messy to retain, given that the feature is also not much used.

  • --hint_info and --print_z3_statistics are deprecated. They are subsumed by --query_stats.

Error reporting

  • The error reports from SMT query failures have been substantially reworked. At least a diagnostic (i.e., an "Info" message) is issued for each SMT query failure together with a reason provided by the SMT solver. To see that diagnostic message, you at least need to have '--debug yes'. Additionally, localized assertion failures will be printed as errors. If no localized errors could be recovered (e.g., because of a solver timeout) then the dreaded "Unknown assertion failed" error is reported.

  • --query_stats now reports a reason for a hint failure as well as localized errors for sub-proofs that failed to replay. This is should provide a faster workflow than using --detail_hint_replay (which still exists)