Commit d6c96f96 authored by Robbert Krebbers's avatar Robbert Krebbers

More about normalization in README.

parent 9acbe81f
Pipeline #20373 failed with stage
......@@ -80,6 +80,21 @@ Actris tactics are as follows:
put `H : c ↣ prot1` and `H : c ↣ prot2` back into the contexts of the two
respectively goals.
The above tactics implicitly perform normalization of the protocol `prot` in
the hypothesis `H : c ↣ prot`. For example, `wp_send` also works if there is a
with protocol the `iProto_dual ((<?> y1 .. yn, MSG v; {{ P }}; END) <++> prot)`.
Concretely, the normalization performs the following actions:
- It re-associates appends (`<++>`), and removes left-identities (`END`) of it.
- It moves appends (`<++>`) into sends (`<!>`), receives (`<?>`), selections
(`<+>`) and branches (`<&>`).
- It distributed duals (`iProto_dual`) over append (`<++>`).
- It unfolds `prot1` into `prot2` if there is an instance of the type class
`ProtoUnfold prot1 prot2`. When defining a recursive protocol, it is
useful to define a `ProtoUnfold` instance to obtain automatic unfolding
of the recursive protocol. For example, see `sort_protocol_br_unfold` in
[theories/examples/sort_br_del.v](theories/examples/sort_br_del.v).
[HeapLang]: https://gitlab.mpi-sws.org/iris/iris/blob/master/HeapLang.md
[ProofMode]: https://gitlab.mpi-sws.org/iris/iris/blob/master/ProofMode.md
[ActrisProofMode]: theories/channel/proofmode.v
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment