§15: Android's post-quantum ratchet is verified cross-engine #8

Merged
paulhitt merged 1 commits from 4-android-v3-verified into main 2026-08-31 17:56:02 +00:00
paulhitt commented 2026-08-31 17:13:36 +00:00 (Migrated from gitlab.com)

The run the was waiting on has happened.

was now
§13 PQ ratchet, Android built, not yet cross-engine verified cross-engine
§14 sealed sender, Android wired, run not recorded engine verified, not wired end to end

What backs the

Thirteen assertions drive a v3 session between the Kotlin and web engines in both
directions. The load-bearing one is the web engine opening Kotlin-s reply:
sending it required decapsulating with the prekey seed, adopting the peer-s
pqdh, and encapsulating a fresh key — and doing those three in the wrong order
(§13.2) derives a different root key with no error anywhere.

That run is also what found the shipped code was wrong, and the table now
says so. The engine was attaching a ratchet step to any peer publishing a PQ
prekey — which every v2 device does — so a build with it would have broken every
conversation with the released 0.6 client. Sixteen Kotlin unit tests did not
catch it and could not: both sides of a self-test share the author-s reading.
That is the argument for this table-s whole discipline, so it belongs here rather
than only in a commit message.

Cross-engine here is Kotlin against the web engine, which is normative.
Kotlin against Swift directly still has not been run, and the cell says so.

Why §14 does not move

Its engine half is now verified cross-engine — six assertions, both
directions, including a seal addressed elsewhere that must not open. What is
unproven is the column-s actual claim, wired end to end.

LiveSealedSenderTest looks like that evidence and is not:

tests="2" skipped="0" failures="0"

on a run that did nothing. It returns early when FN_LIVE_FLEET is unset, and
JUnit records the early return as passed. A test that no-ops into green is
worse than an absent one — and this table is exactly where it would have been
believed.

The run the was waiting on has happened. | | was | now | |---|---|---| | §13 PQ ratchet, Android | built, not yet cross-engine | **verified cross-engine** | | §14 sealed sender, Android | wired, run not recorded | engine verified, **not** wired end to end | ### What backs the Thirteen assertions drive a v3 session between the Kotlin and web engines in both directions. The load-bearing one is **the web engine opening Kotlin-s reply**: sending it required decapsulating with the prekey seed, adopting the peer-s `pqdh`, and encapsulating a fresh key — and doing those three in the wrong order (§13.2) derives a different root key with no error anywhere. **That run is also what found the shipped code was wrong**, and the table now says so. The engine was attaching a ratchet step to any peer publishing a PQ prekey — which every v2 device does — so a build with it would have broken every conversation with the released 0.6 client. Sixteen Kotlin unit tests did not catch it and *could not*: both sides of a self-test share the author-s reading. That is the argument for this table-s whole discipline, so it belongs here rather than only in a commit message. Cross-engine here is Kotlin against the **web** engine, which is normative. Kotlin against Swift directly still has not been run, and the cell says so. ### Why §14 does not move Its engine half **is** now verified cross-engine — six assertions, both directions, including a seal addressed elsewhere that must not open. What is unproven is the column-s actual claim, *wired end to end*. `LiveSealedSenderTest` looks like that evidence and is not: ``` tests="2" skipped="0" failures="0" ``` on a run that did nothing. It returns early when `FN_LIVE_FLEET` is unset, and JUnit records the early return as **passed**. A test that no-ops into green is worse than an absent one — and this table is exactly where it would have been believed.
paulhitt commented 2026-08-31 17:13:40 +00:00 (Migrated from gitlab.com)

mentioned in merge request flamenet-relay!7

mentioned in merge request flamenet-relay!7
paulhitt (Migrated from gitlab.com) merged commit 40688024ae into main 2026-08-31 17:56:02 +00:00
paulhitt commented 2026-08-31 17:56:03 +00:00 (Migrated from gitlab.com)

mentioned in commit 40688024ae

mentioned in commit 40688024ae0fb032d4587c0476ad48559895347e
paulhitt commented 2026-09-09 18:59:49 +00:00 (Migrated from gitlab.com)

changed the description

changed the description
Sign in to join this conversation.