proof/auth_flight · eukhe · Tangled

Coding agent with a memory of all things

eukhe proof auth_flight

1 folder · 27 files

at bend/stackfix

gildrb.com · laws: flight_store_terms_exact (the store's accessors are its fields; a mutant Sto.fresh made flight_after_end_served vacuous) · 2w ago

life: supervise timeouts, revival veto and auth flight decisions run as compiled Bend (new entries timeouts 90, revive 91, auth_flight 92); the Rust copies and the timeouts/revival bridges go

proofs: no misc files: a claim that calls nothing is logic (proof/base/logic/), every other topic keeps its function name; comments cite laws/ and proof/

flight_after_end_served.bend

laws: one laws/<area>.bend per area, shared spec helpers in laws/base.bend, LAWS.bend imports only; fills re-aliased def <Area>.<law>

flight_after_end_stored.bend

laws: one laws/<area>.bend per area, shared spec helpers in laws/base.bend, LAWS.bend imports only; fills re-aliased def <Area>.<law>

flight_board_joins.bend

laws: one laws/<area>.bend per area, shared spec helpers in laws/base.bend, LAWS.bend imports only; fills re-aliased def <Area>.<law>

flight_board_leads.bend

laws: close the adversaries' gaps in revive, timeouts and auth_flight (the entries' freshness and values are the models', the refresh model's every step pinned)

flight_callers_get_its_outcome.bend

laws: one laws/<area>.bend per area, shared spec helpers in laws/base.bend, LAWS.bend imports only; fills re-aliased def <Area>.<law>

flight_ffi_answers.bend

life: supervise timeouts, revival veto and auth flight decisions run as compiled Bend (new entries timeouts 90, revive 91, auth_flight 92); the Rust copies and the timeouts/revival bridges go

flight_ffi_example.bend

life: supervise timeouts, revival veto and auth flight decisions run as compiled Bend (new entries timeouts 90, revive 91, auth_flight 92); the Rust copies and the timeouts/revival bridges go

flight_ffi_malformed_exact.bend

life: supervise timeouts, revival veto and auth flight decisions run as compiled Bend (new entries timeouts 90, revive 91, auth_flight 92); the Rust copies and the timeouts/revival bridges go

flight_ffi_reads.bend

life: supervise timeouts, revival veto and auth flight decisions run as compiled Bend (new entries timeouts 90, revive 91, auth_flight 92); the Rust copies and the timeouts/revival bridges go

flight_land_ends.bend

laws: close the adversaries' gaps in revive, timeouts and auth_flight (the entries' freshness and values are the models', the refresh model's every step pinned)

flight_landed_serves.bend

laws: one laws/<area>.bend per area, shared spec helpers in laws/base.bend, LAWS.bend imports only; fills re-aliased def <Area>.<law>

flight_new_example.bend

laws: close the adversaries' gaps in revive, timeouts and auth_flight (the entries' freshness and values are the models', the refresh model's every step pinned)

flight_next_check_is_model.bend

life: supervise timeouts, revival veto and auth flight decisions run as compiled Bend (new entries timeouts 90, revive 91, auth_flight 92); the Rust copies and the timeouts/revival bridges go

flight_next_fetch_is_model.bend

life: supervise timeouts, revival veto and auth flight decisions run as compiled Bend (new entries timeouts 90, revive 91, auth_flight 92); the Rust copies and the timeouts/revival bridges go

flight_next_load_is_model.bend

life: supervise timeouts, revival veto and auth flight decisions run as compiled Bend (new entries timeouts 90, revive 91, auth_flight 92); the Rust copies and the timeouts/revival bridges go

flight_next_store_is_model.bend

life: supervise timeouts, revival veto and auth flight decisions run as compiled Bend (new entries timeouts 90, revive 91, auth_flight 92); the Rust copies and the timeouts/revival bridges go

flight_one_fetch.bend

proofs: no misc files: a claim that calls nothing is logic (proof/base/logic/), every other topic keeps its function name; comments cite laws/ and proof/

flight_open_empty.bend

life: supervise timeouts, revival veto and auth flight decisions run as compiled Bend (new entries timeouts 90, revive 91, auth_flight 92); the Rust copies and the timeouts/revival bridges go

flight_open_refuses.bend

life: supervise timeouts, revival veto and auth flight decisions run as compiled Bend (new entries timeouts 90, revive 91, auth_flight 92); the Rust copies and the timeouts/revival bridges go

flight_step_answers.bend

life: supervise timeouts, revival veto and auth flight decisions run as compiled Bend (new entries timeouts 90, revive 91, auth_flight 92); the Rust copies and the timeouts/revival bridges go

flight_step_exact.bend

laws: close the adversaries' gaps in revive, timeouts and auth_flight (the entries' freshness and values are the models', the refresh model's every step pinned)

flight_step_example.bend

life: supervise timeouts, revival veto and auth flight decisions run as compiled Bend (new entries timeouts 90, revive 91, auth_flight 92); the Rust copies and the timeouts/revival bridges go

flight_step_malformed_exact.bend

life: supervise timeouts, revival veto and auth flight decisions run as compiled Bend (new entries timeouts 90, revive 91, auth_flight 92); the Rust copies and the timeouts/revival bridges go

flight_step_reads.bend

life: supervise timeouts, revival veto and auth flight decisions run as compiled Bend (new entries timeouts 90, revive 91, auth_flight 92); the Rust copies and the timeouts/revival bridges go

flight_store_terms_exact.bend

laws: flight_store_terms_exact (the store's accessors are its fields; a mutant Sto.fresh made flight_after_end_served vacuous)

flight_terms_exact.bend

laws: close the adversaries' gaps in revive, timeouts and auth_flight (the entries' freshness and values are the models', the refresh model's every step pinned)