proof/fsmode · eukhe · Tangled

Coding agent with a memory of all things

eukhe proof fsmode

20 files

at bend/all-shell

gildrb.com · fsmode: the model's own terms are pinned (fsmode_socket_dir_exact, fsmode_safe_exact, fsmode_modes_exact): a blind adversary's socket_dir that ignored the owner passed socket_dir_owned through its own Seen.safe · 2w ago

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

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

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

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

cwd_is_explicit.bend

proofs: files past 1,000 lines become folders by topic (proof/base/, proof/<area>/base/, proof/optchat/push_agrees_always/); P1 binders renamed

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

fsmode_ffi_answers.bend

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

fsmode_ffi_example.bend

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

fsmode_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

fsmode_ffi_malformed.bend

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

fsmode_modes_exact.bend

fsmode: the model's own terms are pinned (fsmode_socket_dir_exact, fsmode_safe_exact, fsmode_modes_exact): a blind adversary's socket_dir that ignored the owner passed socket_dir_owned through its own Seen.safe

fsmode_safe_exact.bend

fsmode: the model's own terms are pinned (fsmode_socket_dir_exact, fsmode_safe_exact, fsmode_modes_exact): a blind adversary's socket_dir that ignored the owner passed socket_dir_owned through its own Seen.safe

fsmode_socket_dir_exact.bend

fsmode: the model's own terms are pinned (fsmode_socket_dir_exact, fsmode_safe_exact, fsmode_modes_exact): a blind adversary's socket_dir that ignored the owner passed socket_dir_owned through its own Seen.safe

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

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

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

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

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

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

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