Source files

planarian @ a924e09 · Spec v4.6 · snapshot main · all versions

Which invariants and obligations live in each file.

`crates/exec/src/kani.rs`

Obligation	Kind	Line	Invariants
`exec::approval_tokens_expire_after_their_lifetime`	Kani harness	14	I8
`exec::residue_security_is_never_intended`	Kani harness	94	I13
`exec::residue_crashes_are_faults`	Kani harness	105	I13
`exec::residue_is_inferred_only_where_allowed`	Kani harness	116	I13

`crates/policy/src/lib.rs`

Obligation	Kind	Line	Invariants
`policy::decide`	verified fn	869	I5
`policy::may_approve`	verified fn	923	I19
`policy::may_grant`	verified fn	942	I19
`policy::is_administrator`	verified fn	1014	I17

`crates/policy/src/proofs.rs`

Obligation	Kind	Line	Invariants
`policy::i5_autonomy_never_touches_reject`	proof fn	73	I5
`policy::i11_non_routine_session_asks`	proof fn	95	I11
`policy::i11_session_only_raises`	proof fn	118	I11
`policy::global_floors`	proof fn	129	I21
`policy::own_session_is_per_session`	proof fn	143	I21
`policy::i16_below_floor_needs_administrator`	proof fn	161	I16
`policy::administrator_class_only_on_ask_first`	proof fn	170	I16
`policy::security_override_held_for_administrator`	proof fn	179	I22
`policy::security_restart_runs_alone_only_to_restore`	proof fn	196	I22
`policy::i19_no_self_approval`	proof fn	215	I19
`policy::agents_and_unattributed_are_refused`	proof fn	227	I22
`policy::i10_canonical_probe_changes_ask`	proof fn	237	I10
`policy::unauthorized_is_refused_first`	proof fn	246	I5
`policy::core_is_never_a_target`	proof fn	255	I5
`policy::only_administrators_resolve`	proof fn	266	I22
`policy::users_cannot_change_generations`	proof fn	276	I22
`policy::i14_facts_caller_is_not_authority`	proof fn	290	I14
`policy::i17_administrators_never_empty`	proof fn	327	I17

`crates/txn/src/chain.rs`

Obligation	Kind	Line	Invariants
`txn::follows`	verified fn	97	I18
`txn::verify`	verified fn	120	I18
`txn::next_link`	verified fn	168	I18
`txn::appending_keeps_the_chain`	proof fn	182	I18
`txn::an_edited_record_breaks_the_chain`	proof fn	214	I18

`crates/txn/src/kani.rs`

Obligation	Kind	Line	Invariants
`txn::recovery_table_follows_the_state_machine`	Kani harness	185	I12
`txn::watchdog_takes_over_only_when_it_should`	Kani harness	199	I12
`txn::takeover_fences_out_the_previous_owner`	Kani harness	225	I15
`txn::override_swap_never_overwrites_a_third_party`	Kani harness	261	I23

`crates/txn/src/ledger.rs`

Obligation	Kind	Line	Invariants
`txn::compatible_exec`	verified fn	460	I6
`txn::well_formed`	verified fn	534	I6
`txn::validate`	verified fn	607	I6, I15
`txn::apply`	verified fn	915	I6, I12
`txn::add_interlock`	verified fn	934	I12
`txn::i6_one_generation_active`	proof fn	1235	I6

`crates/txn/src/machine.rs`

Obligation	Kind	Line	Invariants
`txn::step_allowed`	verified fn	61	I12
`txn::i12_steps_terminate`	proof fn	130	I12
`txn::i12_terminal_always_reachable`	proof fn	141	I12
`txn::terminal_is_final`	proof fn	151	I12
`txn::refusal_only_before_mutation`	proof fn	161	I12
`txn::runtime_never_reverts`	proof fn	171	I23
`txn::only_generations_publish`	proof fn	182	I6
`txn::boot_only_never_activates`	proof fn	194	I6
`txn::generations_commit_after_promotion`	proof fn	206	I23