Write cryptographic claims about time, place, and media. Hardware level is part of the type system. Compiles directly to Solidity.
program := proof_decl*
proof_decl := proof Session(string) { stmt* }
stmt := at_stmt
| captures_stmt
| attested_stmt
| requires_stmt
at_stmt := at time_claim from source
| at place_claim from source
time_claim := Time(unix_ms ± tol ms)
place_claim := Place(lat°N|S, lon°E|W ± tol m)
captures := captures Video(hash:"…") signed Device("…")
attested := attested Score(n) by Chip("…") [level Ln]
requires := requires L0|L1|L2|L3
| Claim | Infers | Notes |
|---|---|---|
Time ±>100ms | L0 | System clock OK |
Time ±≤100ms | L1 | GPS-disciplined recommended |
Time ±≤1ms | L2 | Requires CSAC atomic clock |
Place ±≥20m | L0 | Standard GPS |
Place ±5–20m | L1 | Chip-attested GPS |
Place ±<5m | L2 | RTK GPS required |
Device("ha-chip-*") | L1 | Hardware key detected |
attested … level L2 | L2 | Raises inferred level |