proof/kernel_local · eukhe · Tangled

Coding agent with a memory of all things

eukhe proof kernel_local

21 files

at bend/stackfix

gildrb.com · kernel_local, launcher: the models' own terms are pinned (kernel_terms_exact, kernel_sweep_terms_exact, launcher_adoption_exact), so the laws that read them say what they claim · 2w ago

kernel_local: runs as compiled Bend (ffi_kernel_local, spec-speller entry laws); the Rust copy, its bridge and the law-covered tests go

kernel_answer_exact.bend

kernel_local: runs as compiled Bend (ffi_kernel_local, spec-speller entry laws); the Rust copy, its bridge and the law-covered tests go

kernel_download_only_on_install.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>

kernel_fetch_verified_before_use.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>

kernel_ffi_answers.bend

kernel_local: runs as compiled Bend (ffi_kernel_local, spec-speller entry laws); the Rust copy, its bridge and the law-covered tests go

kernel_ffi_example.bend

kernel_local: runs as compiled Bend (ffi_kernel_local, spec-speller entry laws); the Rust copy, its bridge and the law-covered tests go

kernel_ffi_malformed_exact.bend

kernel_local, launcher, fsmode: a malformed request gets exactly 'E <area>: malformed request' (laws *_ffi_malformed_exact): a blind adversary's bare 'E' passed the laws that read only the first char

kernel_ffi_malformed.bend

kernel_local: runs as compiled Bend (ffi_kernel_local, spec-speller entry laws); the Rust copy, its bridge and the law-covered tests go

kernel_install_fetches.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>

kernel_lock_attempt_leaves_none.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>

kernel_lock_judge.bend

kernel_local: runs as compiled Bend (ffi_kernel_local, spec-speller entry laws); the Rust copy, its bridge and the law-covered tests go

kernel_lock_sweep_keeps_live.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>

kernel_lock_sweep_removes_dead.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>

kernel_missing_names_install.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>

kernel_missing_spares_tools.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>

kernel_plan_exact.bend

kernel_local: runs as compiled Bend (ffi_kernel_local, spec-speller entry laws); the Rust copy, its bridge and the law-covered tests go

kernel_session_never_downloads.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>

kernel_setup_runs.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>

kernel_start_exact.bend

kernel_local: runs as compiled Bend (ffi_kernel_local, spec-speller entry laws); the Rust copy, its bridge and the law-covered tests go

kernel_sweep_terms_exact.bend

kernel_local, launcher: the models' own terms are pinned (kernel_terms_exact, kernel_sweep_terms_exact, launcher_adoption_exact), so the laws that read them say what they claim

kernel_terms_exact.bend

kernel_local, launcher: the models' own terms are pinned (kernel_terms_exact, kernel_sweep_terms_exact, launcher_adoption_exact), so the laws that read them say what they claim