Cairn Docs Claims Blog Packages

Claim ยท cairn 0.3.0

cairn^902 Lean decodes what the Swift event encoder writes

An assumption of cairn 0.3.0.

Id
cairn^902
Kind
assume
Reads as
assumed
Version
0.3.0

All of cairn 0.3.0's claims

What it says

For every batch of events, Lean's proved decodeEvents decodes the host's encodeEvents bytes to the same events, and Lean's encoder gives back the same bytes.

Evidence

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

Where it's defined

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

Ledger

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