proof/doc_commit · eukhe · Tangled

Coding agent with a memory of all things

eukhe proof doc_commit

1 folder · 30 files

at bend/stackfix

gildrb.com · proof: the wire lemmas that dash_access and gateway_answer borrowed from doc_commit move to proof/base · 2w ago

proof: the wire lemmas that dash_access and gateway_answer borrowed from doc_commit move to proof/base

docs: the writer's choices run as the compiled core (new entry doc_commit id 103)

commit_answer_is_reply.bend

docs: the writer's choices run as the compiled core (new entry doc_commit id 103)

commit_answer_spec.bend

docs: the writer's choices run as the compiled core (new entry doc_commit id 103)

commit_check_is_conflict.bend

docs: the writer's choices run as the compiled core (new entry doc_commit id 103)

commit_check_spec.bend

docs: the writer's choices run as the compiled core (new entry doc_commit id 103)

commit_choices_example.bend

docs: the writer's choices run as the compiled core (new entry doc_commit id 103)

commit_entry_answers.bend

proof: the wire lemmas that dash_access and gateway_answer borrowed from doc_commit move to proof/base

commit_entry_exact.bend

proof: the wire lemmas that dash_access and gateway_answer borrowed from doc_commit move to proof/base

commit_entry_example.bend

docs: the writer's choices run as the compiled core (new entry doc_commit id 103)

commit_entry_reads.bend

proof: the wire lemmas that dash_access and gateway_answer borrowed from doc_commit move to proof/base

commit_entry_refuses.bend

proof: the wire lemmas that dash_access and gateway_answer borrowed from doc_commit move to proof/base

commit_gate_spec.bend

docs: the writer's choices run as the compiled core (new entry doc_commit id 103)

commit_outcome_is_publish.bend

docs: the writer's choices run as the compiled core (new entry doc_commit id 103)

commit_outcome_spec.bend

docs: the writer's choices run as the compiled core (new entry doc_commit id 103)

commit_prefix_spec.bend

docs: the writer's choices run as the compiled core (new entry doc_commit id 103)

commit_seen_spec.bend

docs: the writer's choices run as the compiled core (new entry doc_commit id 103)

commit_sweep_is_model.bend

docs: the writer's choices run as the compiled core (new entry doc_commit id 103)

commit_sweep_spec.bend

docs: the writer's choices run as the compiled core (new entry doc_commit id 103)

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

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

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

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

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

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

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

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

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

write_saw_spec.bend

docs: the writer's choices run as the compiled core (new entry doc_commit id 103)

write_unseen_spec.bend

docs: the writer's choices run as the compiled core (new entry doc_commit id 103)

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