Cairn Docs Claims Blog Packages

Claim ยท cairn_atproto 0.3.0

cairn_atproto^25 A write refused for its token was not applied

An assumption of cairn_atproto 0.3.0.

Id
cairn_atproto^25
Kind
assume
Reads as
assumed
Version
0.3.0

All of cairn_atproto 0.3.0's claims

What it says

A write the server answers 400 ExpiredToken was not applied, so the session's one resend after a refresh (cairn_atproto^12, ^13) writes it at most once. Checked against the fake PDS (cairn#251) and once against the real network (cairn#258).

Evidence

assumedStated, not proved. The proofs rely on it.
fuzzedNot shown yet: the trusted-base fuzzer's check atproto.expired-not-applied held. A CI step will publish it (#95).

Where it's defined

Declaration
CairnAtproto.ActClaims.expiredNotApplied
Module
CairnAtproto.ActClaims
Source
lean/CairnAtproto/ActClaims.lean:144 at v0.3.0
Statement hash
-

Ledger

cairn_atproto^25 is active in this version's claims.lock. An id never moves or changes meaning.