Bump actions/checkout from 3 to 4 (#375)

Bumps [actions/checkout](https://github.com/actions/checkout) from 3 to 4.
- [Release notes](https://github.com/actions/checkout/releases)
- [Changelog](https://github.com/actions/checkout/blob/main/CHANGELOG.md)
- [Commits](actions/checkout@v3...v4)

---
updated-dependencies:
- dependency-name: actions/checkout
  dependency-type: direct:production
  update-type: version-update:semver-major
...

Signed-off-by: dependabot[bot] <[email protected]>
Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com>

sketch wp_read_RDH

deref: alias of load which does not keep changes to symbolic state

made while finding the memory being loaded, ie changes such as
splitting arrays and their corresponding lists and casting from
one separation logic predicate to another

List.upto needs to be pushed down, ie called again

on result of first simplification:

eg if len l1 = i
  (l1 ++ l2)[:i] --> l1[:i] --> l1

Actually makes insertion_sort work less well, because
it allows          ((_ ++ [|_|]) ++ _)[:_]
to be turned into  (_ ++ _ :: _)[:_]
and putting the discard boundary at a cons is not yet supported

use vm_compute instead of Ltac to check instruction bounds

`make bedrock2_install` now installs examples (#281)

We also have `bedrock2_install_{ex,noex}` targets now.

finish frame rule proof

Tag for Coq Workshop 2022 Superlinear Slowness presentation, LtacProf…

… output, optimized loop proof, no early subst

Tag for Coq Workshop 2022 Superlinear Slowness presentation, LtacProf…

… output, optimized loop proof, again

Tag for Coq Workshop 2022 Superlinear Slowness presentation, LtacProf…

… output, optimized loop proof