[antonkov]

The headline theorems no longer trust 10 of the 37 routines that were hooked
(replaced by a trusted Lean contract). The proofs now execute their machine code
in the pinned libsignal-cli binary:

• musl libc (rustc 1.98.1's self-contained libc.a): memmove, bcmp (and the
  memcmp it tail-calls), strlen
• Rust standard library: memrchr, str::from_utf8, SystemTime::duration_since,
  <SystemTime as Add>::add
• non-cryptographic helpers in the crypto crates: subtle::black_box and the
  zeroizing Drop impls of x25519_dalek::SharedSecret and StaticSecret

27 hooked routines remain: the 23 low-level cryptographic primitives (whose
security the theorems assume), Rust's error-message formatting
(core::fmt::write, format_inner), and the two functions that write files and
standard output. CliHooks, which the binary theorems quantify over, now holds
only the abstract cryptographic primitives.

The headline theorem statements are unchanged; the trusted definitions they
refer to (the hook table, CliHooks, the ELF pin) are smaller. The pinned binary
changes because the newly verified routines are now linked and placed as
verified code: same libsignal v0.105.4 and rustc 1.98.1, linker script
third_party/libsignal/libsignal-session/cli-elf/stock/stock_c2.ld, SHA-256
50066cbd732256eb5f19f93d1d98800914336b7926225de3ebfa0bb37eca98ce
(was 2f20c836…).

The bug-injection mutants are rebuilt with the same link recipe and 27-hook
table, and their disproofs still go through. comparator passes on this tree;
comparator/README.md now explains how the challenge and solution are set up and
how to run the check locally.

GitOrigin-RevId: 84be1556f741f1f348de110f12d9883d70ba9980

[google-cla]

Thanks for your pull request! It looks like this may be your first contribution to a Google open source project. Before we can look at your pull request, you'll need to sign a Contributor License Agreement (CLA).

View this failed invocation of the CLA check for more information.

For the most up to date status, view the checks section at the bottom of the pull request.