Tej Chajed authored 4 years ago and Robbert Krebbers committed 4 years ago

Implemented as an algebra for rules about `auth max_natUR` and a
logic-level wrapper for the auth element (a nat) and fragment (a
persistent lower-bound).

Fixes #327.

Tej Chajed authored 4 years ago and Robbert Krebbers committed 4 years ago

When running `iDestruct "H" as (?) "H"`, use the name of the binder in
"H". For example, if "H" has type `∃ y, Φ y`,  we now use `y` as the
name of the variable after freshening. Previously the name was always
the equivalent of running `fresh H`.

The implementation achieves this by forwarding the desired identifier
name through the `IntoExist` typeclass. Identifiers are serialized in
Gallina by using them as the name of a function of type `ident_name :=
unit -> unit`.

- all ascii notation is marked "only parsing" so this PR shouldn't
  change anything for anyone using only unicode notation.
- the algorithm for creating an ascii notation is pretty simple.
  - \ast -> *
  - \triangleright -> |>
  - \vee -> \/
  - \wedge -> /\
  - \forall -> forall
  - \exists -> exists
  - \ast -> **

Tej Chajed authored 5 years ago and Ralf Jung committed 5 years ago

Add array_copy_to (copy in-place to destination array) and array_clone
(copy to a freshly allocated array). The heap_lang spec and proof for
array_copy_to are inspired by
https://gitlab.mpi-sws.org/iris/lambda-rust/blob/3b4ae69fa3be1344245245bf05e5e80e790e064d/theories/lang/lib/memcpy.v.

Fixes #293.