Cairn Docs Claims Blog Packages

Claim ยท sky 0.3.1

sky^28 The password reaches one request

An invariant of sky 0.3.1.

Id
sky^28
Kind
invariant
Reads as
proved
Version
0.3.1

All of sky 0.3.1's claims

What it says

Every step but Sign in (the button, or Enter in the password field) has the same effects whatever the password field holds. Sign in's effects are the same too, for any password of the same length, once the redacted request's contents are blanked; with Sign in enabled its only request is createSession, carrying the password and marked redact, and the field is empty after. So the password is sent in exactly one request, and never shown by a tool (Cairn redacts it in dumps and logs; the fuzzer plants text in the field and checks).

Evidence

provedinitSky.passwordOnce.init
provedstepSky.passwordOnce.step
provedreceiveSky.passwordOnce.receive
provedreachableSky.passwordOnce.reachable
provedreachableAllSky.passwordOnce.reachableAll
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).

Where it's defined

Declaration
Sky.passwordOnce
Module
Sky.Claims
Source
lean/Sky/Claims.lean:287 at v0.3.1
Machine
Sky.machine
Statement
Sky.passwordOnce.holds
Statement hash
4d4fc01d47440f3b

Ledger

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