Cairn Docs Claims Blog Packages

Claim ยท yap 0.1.0

yap^318 Each clip is typed at most once

An invariant of yap 0.1.0.

Id
yap^318
Kind
invariant
Reads as
proved
Version
0.1.0

All of yap 0.1.0's claims

What it says

However replies arrive (late, twice, out of order, or never), and whatever else the host reports, no clip's transcript has been typed twice: the app's log of typed clips counts each at most once (`TypedInv`, `step_rel`).

Evidence

provedinitYap.typedOnce.init
provedstepYap.typedOnce.step
provedreceiveYap.typedOnce.receive
provedreachableYap.typedOnce.reachable
provedreachableAllYap.typedOnce.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
Yap.typedOnce
Module
Yap
Source
lean/Yap.lean:339 at v0.1.0
Machine
Yap.machine
Statement
Yap.typedOnce.holds
Statement hash
6f62fbcbeb412b23

Ledger

yap^318 is active in this version's claims.lock, statement 6f62fbcbeb412b23. An id never moves or changes meaning.