Cairn Docs Claims Blog Packages

Claim ยท cairn 0.3.0

cairn^901 The Swift frame decoder agrees with Lean's

An assumption of cairn 0.3.0.

Id
cairn^901
Kind
assume
Reads as
assumed
Version
0.3.0

All of cairn 0.3.0's claims

What it says

For every byte buffer, the host's Frame(bytes:) accepts exactly when Lean's proved decodeFrame does, and then decodes the same frame.

Evidence

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

Where it's defined

Declaration
Cairn.Fuzz.Trusted.Claims.swiftFrameDecoder
Module
Cairn.Fuzz.Trusted.Claims
Source
lean/Cairn/Fuzz/Trusted/Claims.lean:16 at v0.3.0
Statement hash
-

Ledger

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