Cairn Docs Claims Blog Packages

Claim ยท sky 0.3.1

sky^32 A post

A move of sky 0.3.1, in The feed.

Id
sky^32
Kind
move
Reads as
proved
Place
The feed ^14
Version
0.3.1

All of sky 0.3.1's claims

What you do

Press a post (or Return on it); or scroll it into view.

What you see

Pressed, the post opens on bsky.app. In view, its avatar and images load (grey until they do, the same size after), and loads for posts far from it are cancelled.

Evidence

provedsound pressSky.postRowMove.press.sound
provedsound appearSky.postRowMove.appear.sound
fuzzedNot shown yet: the claim-driven fuzzer held it in every random sequence (docs/fuzz.md). A CI step will publish it (#95).
testedNot shown yet: the running app matched the model at every step that exercised it (docs/conformance.md). A CI step will publish it (#95).
seenNot shown yet: a screenshot of the app shows it. A CI step will publish it (#95).

Where it's defined

Declaration
Sky.postRowMove
Module
Sky.Claims
Source
lean/Sky/Claims.lean:172 at v0.3.1
Statement
Sky.postRowMove.enabled Sky.postRowMove.press.post Sky.postRowMove.appear.post
Statement hash
8d80101d7f518614

Ledger

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