<commit_before>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).

# Version 0.9.7.0

## Module system

  * Friend modules (https://github.com/FStarLang/FStar/wiki/Friend-modules)

## Core typechecker

  * Revised typechecking of nested patterns and ascriptions on
    patterns, fixing unsoundnesses (issue #238, for example)

## Libraries

   * Two core axioms were discovered by <NAME> to be formulated
     in an unsound manner.

     FStar.FunctionalExtensionality has been reformulated to prevent
     equivalence proofs of a function on a given domain to be
     improperly extended to equivalence on a larger domain. The
     library was fixed to ensure that domain type used to prove the
     equivalence was recorded in the axiom. See
     examples/micro-benchmarks/Test.FunctionalExtensionality.fst for
     example uses.

     FStar.PropositionalExtensionality was found to be incompatible
     with the representation of `prop` as the type of all
     sub-singletons. `prop` has been reformulated as the type of all
     sub-types of `unit`.

     See issue #1542 for more discussion.

## Syntax

   * We now overload `&` to construct both dependent and non-dependent
     tuple types. `t1 & t2` is equivalent to `tuple2 t1 t2` whereas
     `x:t1 & t2` is `dtuple2 t1 (fun x -> t2)`. See
     examples/micro-benchmarks/TupleSyntax.fst. The main value
     proposition here is that in contrast to `*`, which clashes with
     the multiplication on integers, the `&` symbol can be used for
     tuples while reserving `*` for multiplication.

## Extraction

   * Cross-module inlining: Declarations in interfaces marked with the
     `inline_for_extraction` qualifier have their definitions inlined
     in client code. Currently guarded by the --cmi flag, this will
     soon be the default behavior.

## SMT Encoding

   * A soundness bug was fixed in the encoding of recursive functions
     to SMT. The flaw resulted from omitting typing guards in the
     axioms corresponding to the equational behavior of pure and ghost
     recursive functions. The fix makes reasoning about recursive
     functions with SMT slightly more demanding: if the typing of an
     application of a recursive functions requires some non-trivial
     proof, the SMT solver may require some assistance with that proof
     before it can unfold the definition of the recursive
     function. For an example of the kind of additional proof that may
     be needed, see this commit:
     936ce47f2479af52f3c3001bd87bed810dbf6e1f. We need to call lemmas
     to prove that the recursive function that appears in the
     inductive hypothesis is well-typed.


# Version 0.9.6.0

## Command line options

   F* reads .checked files by default unless the `--cache_off` option is provided.
   To write .checked files, provide `--cache_checked_modules`

   `--use_two_phase_tc true` is now the default. This improves type
   inference for implicit arguments and reduces our trust in type
   inference, since the result of type inference is type-checked
   again.

   `--use_extracted_interfaces` now takes a boolean string as an
   option, i.e., `--use_extracted_interfaces true` or<commit_msg>some more explanations in changes.md<commit_after>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).

# Version 0.9.7.0

## Module system

  * Friend modules (https://github.com/FStarLang/FStar/wiki/Friend-modules)

## Core typechecker

  * Revised typechecking of nested patterns and ascriptions on
    patterns, fixing unsoundnesses (issue #238, for example)

## Libraries

   * Two core axioms were discovered by <NAME> to be formulated
     in an unsound manner.

     FStar.FunctionalExtensionality has been reformulated to prevent
     equivalence proofs of a function on a given domain to be
     improperly extended to equivalence on a larger domain. The
     library was fixed to ensure that domain type used to prove the
     equivalence was recorded in the axiom. See
     examples/micro-benchmarks/Test.FunctionalExtensionality.fst for
     example uses.

     FStar.PropositionalExtensionality was found to be incompatible
     with the representation of `prop` as the type of all
     sub-singletons. `prop` has been reformulated as the type of all
     sub-types of `unit`.

     See issue #1542 for more discussion.

## Syntax

   * We now overload `&` to construct both dependent and non-dependent
     tuple types. `t1 & t2` is equivalent to `tuple2 t1 t2` whereas
     `x:t1 & t2` is `dtuple2 t1 (fun x -> t2)`. See
     examples/micro-benchmarks/TupleSyntax.fst. The main value
     proposition here is that in contrast to `*`, which clashes with
     the multiplication on integers, the `&` symbol can be used for
     tuples while reserving `*` for multiplication.

## Extraction

   * Cross-module inlining: Declarations in interfaces marked with the
     `inline_for_extraction` qualifier have their definitions inlined
     in client code. Currently guarded by the --cmi flag, this will
     soon be the default behavior. Also see:
     https://github.com/FStarLang/FStar/wiki/Cross-module-Inlining
     and https://github.com/FStarLang/FStar/tree/master/examples/extraction/cmi.

## SMT Encoding

   * A soundness bug was fixed in the encoding of recursive functions
     to SMT. The flaw resulted from omitting typing guards in the
     axioms corresponding to the equational behavior of pure and ghost
     recursive functions. The fix makes reasoning about recursive
     functions with SMT slightly more demanding: if the typing of an
     application of a recursive functions requires some non-trivial
     proof, the SMT solver may require some assistance with that proof
     before it can unfold the definition of the recursive
     function. For an example of the kind of additional proof that may
     be needed, see these commits:
     https://github.com/FStarLang/FStar/commit/936ce47f2479af52f3c3001bd87bed810dbf6e1f
     and https://github.com/project-everest/hacl-star/commit/2220ab81bbae735495a42ced6485665d9facdb0b.
     We need to call lemmas
     to prove that the recursive function that appears in the
     inductive hypothesis is well-typed
     (e.g. calling `wp_monotone` lemma for well-typedness of `wp_compute` in the second commit) .
     In some cases, it may also be possible to use the normalizer to
     do the unfolding:
     https://github.com/project-everest/hacl-star/commit/6e9175e607e591faa5b6a0d6052fc4a336f7bf41#diff-127ee9d47350eff0fa0d79847257d493R290.
     Another kind of change required hoisting some type declarations:
     https://github.com/FStarLang/FStar/commit/819ad64065f1e70aec3665f5df6b58a7d43cdce1
     to get around imprecision in the SMT encoding. This can be handled in F*
     with an additional SMT axiom on type constructors like `list`, but
     we only found a couple of instances of this. So, for now, we are going with the
     hoisting workaround.


# Version 0.9.6.0

## Command line options

   F* reads .checked files by default unless the `--cache_off` option is provided.
   To write .checked files, provide `--cache_checked_modules`

   `--use_two_phase_tc true` is now the default. This improves type
   inference for implicit arguments and reduces our trust in type
   inference, since the result of type inference is type-checked
   again.

   `--use_extracted_interfaces` now takes a boolean string as an
   option, i.e., `--use_extracted_interfaces true` or
{'fraction_non_alphanumeric': 0.05598386905467916, 'fraction_numerical': 0.02277309927647966, 'mean_word_length': 3.459016393442623, 'pattern_counts': {'":': 0, '<': 5, '<?xml version=': 0, '>': 7, 'https://': 8, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 4, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '7000077', 'n_tokens_mistral': 2459, 'n_tokens_neox': 2272, 'n_words': 1057}