sky^35 The post you are reading stays still

What it says

When a refresh puts posts above the post at the top of the view (^34 keeps its key), or heights above it are corrected, the runtime moves the offset by exactly as much as that post moved, so it stays where it was on screen, unless the offset is clamped. At the very top too: the new posts land above the view, and N new posts (^33) offers them. Checked by the fuzzer at every step.

Evidence

proved	init	`Sky.anchor.init`
proved	step	`Sky.anchor.step`
proved	receive	`Sky.anchor.receive`
proved	reachable	`Sky.anchor.reachable`
proved	reachableAll	`Sky.anchor.reachableAll`
fuzzed	Not shown yet: the claim-driven fuzzer held it in every random sequence (docs/fuzz.md). A CI step will publish it (#95).
tested	Not shown yet: the running app matched the model at every step that exercised it (docs/conformance.md). A CI step will publish it (#95).

Where it's defined

Declaration: Sky.anchor
Module: Sky.Claims
Source: lean/Sky/Claims.lean:328 at v0.3.1
Machine: Sky.machine
Statement: Sky.anchor.holds
Statement hash: b09d72a09d49dd01

Ledger

sky^35 is active in this version's claims.lock, statement b09d72a09d49dd01. An id never moves or changes meaning.