Review a forum API

1. One run, in sentences

The toolkit can run one handler of the program on rows you name and tell you, in sentences, what happened. The run below asks: can a stranger read a members-only thread? The thread t1 admits bob; carol is in no member list. The first line is the handler's answer; the paragraphs are the tool's account of it.

Verbatim from docs/forum-demo/outputs/step2-why-read_thread.txt, which scripts/forum-demo/replay.sh regenerates and a test holds this page to. Lines elided are marked ....

## read_thread as carol   (record: docs/forum-demo/records/read_thread-as-carol.json)
output: "Response(status: 403, body: \"{\"view\":\"forbidden\",\"rule\":\"members only\",\"message\":\"This thread is for its members only.\"}\")"
...
    This run evaluated the handler 'read_thread' (package Demo/Forum) with 'db' (the world's database), 'p' = Principal(user_id: "carol", roles: []) (provided) and 'req' = ReadThreadRequest("t1") (provided). It returned Response(status: 403, body: "{"view":"forbidden","rule":"members only","message":"This thread is for its members only."}").
...
    Proven for every input, by static dataflow (no run needed): 'db' may reach the result, so no run can rule its influence out; 'p' may reach the result, so no run can rule its influence out; 'req' may reach the result, so no run can rule its influence out.
...
    Observed on this run, not proven (bounded-observation (seed 7, one recorded handler run; 3 variations per aspect, each on a fresh world from the same seeded rows)): changing field 'user_id' of parameter 'p' across the seeded values never changed the result, which does not show independence; changing field 'roles' of parameter 'p' across the seeded values never changed the result, which does not show independence; changing parameter 'req' from ReadThreadRequest("t1") to ReadThreadRequest("moderators94") moved status from 403 to 404 (+1) and body from "{"view":"forbidden","rule":"members only","message":"This thread is for its members only."}" to "{"view":"not_found","what":"thread"}". Seeded and varied values are drawn from the seed, not from the domain: an integer may be negative or far outside any expected range. The run forced global values for 11 definitions: can_see, forbid, is_moderator, jobj, join_with, jstr, member_String, moderators_table, quote, roster_key, threads_table. Loading a function value does not establish that its body ran. Global values for 12 definitions this one can reach were not forced on this input: bool_literal, jarr, jarr_of_str, jbool, jint, jraw, not_found, posts_table, render_post, render_thread, render_visibility, respond (an absence on this input, not a fault; another input may force them).
...
    The world was seeded with 1 row in 'moderators', 1 row in 'posts' and 1 row in 'threads'. Seeded rows, as rendered: 'moderators': ["mona"]; 'posts': [Post(id: "p1", thread_id: "t1", author: "bob", body: "first", edited: False)]; 'threads': Thread(id: "t1", title: "private planning", author: "alice", visibility: Members, members: ["bob"], reply_cap: 2). Every read found its row. No table changed.
...

How to read it. The answer is a refusal (status 403) that names its rule, "members only", and says it to the person refused: "This thread is for its members only." The next paragraphs keep two kinds of fact apart, and the difference is the whole point:

• Proven for every input is established by reading the program, not by running it: static dataflow follows, through the compiled program, which inputs can flow into the result. The scope is the analyzer’s model of the compiled program. "May reach the result" means a structural path exists; it does not prove an actual dependency. A sampled run can show no change, but cannot establish independence for every input.
• Observed on this run, not proven is what a few varied runs showed: the tool changed one input at a time (three variations each, from seed 7) and reports what happened. "Never changed the result, which does not show independence" means: the tool tried three other names for the caller and got the same refusal, and it is telling you that this does not prove the caller's name is irrelevant. The run as bob, in the same output file, is the witness that it is relevant: he gets the thread.
• The world paragraph lists the rows the run started from, in the tool's own rendering, so the account can be checked against its starting point.

What it does not say. That members-only threads are private. One stranger was refused once. A sentence that would establish the rule for every stranger has to come from a "proven" paragraph or from the verifier's proofs (section 6 shows one); this run can refute a rule, never establish one.

2. The experiments on offer

Every run ends by proposing the experiments its own facts make worth running. None is run unasked. The run below is the reply cap: dave replies to a thread that already holds as many replies as its cap allows.

Verbatim from docs/forum-demo/outputs/step3-why-post_reply.txt, which scripts/forum-demo/replay.sh regenerates and a test holds this page to. Lines elided are marked ....

## post_reply as dave, thread full   (record: docs/forum-demo/records/post_reply-as-dave--thread-full.json)
output: "Response(status: 422, body: \"{\"view\":\"rejected\",\"issue_count\":1,\"issues\":[{\"field\":\"thread_id\",\"code\":\"thread_full\",\"hint\":\"the thread has reached its reply cap\"}]}\")"
...
proposals:
    p = a principal who owns no row -- the recorded run's principal is 'dave'; untried: the principal 'someone-else' with no roles, who appears in no seeded row, which tests whether the result depends on who asks
    every table empty -- the recorded run was seeded with rows in threads, posts, moderators; untried: an empty world, where every read misses
    table 'threads' empty -- the recorded run was seeded with rows in threads; untried: the same world with 'threads' empty, so a read of it misses while the other tables stand
    table 'posts' empty -- the recorded run was seeded with rows in posts; untried: the same world with 'posts' empty, so a read of it misses while the other tables stand
    table 'moderators' empty -- the recorded run was seeded with rows in moderators; untried: the same world with 'moderators' empty, so a read of it misses while the other tables stand
...

How to read it. The answer is a rejection (status 422) naming the field and the reason, "the thread has reached its reply cap". Each proposal has a name before the dashes and, after them, its grounds: what the recorded run had, then untried, the one change the proposal would make, ending with the question that change would answer ("which tests whether the result depends on who asks"). A proposal to change one input field also states its sound fact (proven for every input) and what was observed on this run. You order one by its name; you never write a request yourself. To choose, read the question at the end of each line and take the one whose question is yours: for the members-only rule, the proposal that changes the caller.

On the page. To run one: open the WebMCP workbench, press Open record in the Evaluate a definition section, and choose the run's record file (this run's is post_reply-as-dave--thread-full.json, saved from its raw view). The sentences appear under the output, and under them Proposed next lists these proposals, each with a Run button. Pressing one runs that experiment beside the run on screen and prints its output; the run on screen stays.

What it does not say. Whether any of them is the experiment that would settle the cap. None is: the run that would tell a working cap from a broken one is a thread one reply under it, which the same output file's first run is. The proposals come from the run's facts (a caller, the seeded tables), and a cap is a fact about a count the tool does not yet read. The page records this limit.

3. How the program is written: the conventions page

The conventions page lists, for each recurring shape in the program, the definitions written in that shape and how each is written, so a definition written differently from its neighbours is visible without being marked. A shape is what a definition takes and returns, with the parts that differ between neighbours left as a hole (_); the parts filled in are its fillers. A family is two or more definitions of one shape that agree on every filler but one. The block below is the family of the six request handlers.

Verbatim from docs/forum-demo/outputs/step1c-organize-conventions.txt, which scripts/forum-demo/replay.sh regenerates and a test holds this page to. Lines elided are marked ....

$ yichus organize conventions demos/service/forum.bosatsu
conventions  forum.bosatsu
families 18 (2+ bindings of one signature shape agreeing on every filler but one type, or but fillers that vary in lockstep)  concepts served 11
...
   (Db, Principal, _) -> IO[Response]  x6  forms: call 3, variant-match 3  concepts: EditPostRequest, GrantModeratorRequest, OpenThreadRequest, PutProfileRequest, ReadThreadRequest, ReplyRequest
      grant_moderator  call  builds from forbid, is_moderator, jarr_of_str, jraw, member_String, moderators_table, respond, roster_key  reads not measurable (newtype GrantModeratorRequest)
      open_thread  call  builds from jarr, jraw, parse_thread, reject, render_thread, respond, threads_table
      read_thread  call  builds from can_see, forbid, jarr, jint, jraw, moderators_table, not_found, posts_table, render_post, render_thread, respond, roster_key, threads_table  reads not measurable (newtype ReadThreadRequest)
      edit_post  variant-match  builds from can_edit, can_see, check_text, find_post, forbid, jarr, jint, jraw, moderators_table, not_found, posts_table, reject, render_post, render_thread, replace_post, respond, roster_key, threads_table  reads thread_id, post_id, body
      post_reply  variant-match  builds from can_see, check_text, forbid, has_room, jarr, jint, jraw, moderators_table, not_found, posts_table, reject, render_post, render_thread, respond, roster_key, threads_table  reads thread_id, body
      put_profile  variant-match  builds from check_text, jarr, jraw, profiles_table, reject, render_profile, respond  reads not measurable (newtype PutProfileRequest)
...
   handlers  declared 8  convergent 6  divergent 2  absent 0  not claimed 0
      family (Db, Principal, _) -> IO[Response]  forms: call 3, variant-match 3 (no single form: the declared members disagree among themselves)
      convergent  put_profile, grant_moderator, open_thread, read_thread, post_reply, edit_post
      divergent   get_profile  shape (Db, Principal) -> IO[Response]; the family's is (Db, Principal, _) -> IO[Response]
      divergent   list_threads  shape (Db, Principal) -> IO[Response]; the family's is (Db, Principal, _) -> IO[Response]
...

How to read it. The first lines count the families and the concepts served, the declared kinds of value that have a member in some family. The family line names the shape (three inputs: Db, the store the handler reads and writes, Principal, the caller, and a third differing per handler), counts the members (x6), counts their forms, the coarse way each body begins (call: it calls something; variant-match: it branches on which kind of value it was given; the other forms a program can have are listed in the lens guide), and names the concepts among its fillers. Each member line names the definitions it builds from (every definition of the program its body uses) and, where the tool could measure it, the fields it reads (reads thread_id, post_id, body). "Reads not measurable (newtype ...)" is a limit of the tool, not a fault of the handler: a newtype is a concept with one field, named so a bare number or string is not passed around unlabelled, and the wrapper compiles away, so the tool cannot see the read. The declared-families block is the agent's own claim, "these eight are the handlers", checked against what the page found: convergent members sit in the family as claimed; divergent ones do not, with the difference named (these two take two inputs, not three); absent would be a claimed name no definition has; not claimed would be a definition of the family's shape the claim leaves out.

What it does not say. Which way of writing a handler is right. Three are calls and three are matches; the page counts them and stops. A definition written unlike its neighbours may be right. The whole page is one text file; the lens guide defines every line of it.

4. Where to look first: the heuristic aid

For a reader who cannot judge from the conventions page, the aid names places to compare: a member whose reads lack a field that a neighbour in the same family reads. Every line of it says it is a heuristic.

Verbatim from docs/forum-demo/outputs/step1c-organize-aid.txt, which scripts/forum-demo/replay.sh regenerates and a test holds this page to. Lines elided are marked ....

$ yichus organize aid demos/service/forum.bosatsu
conventions-aid  forum.bosatsu
HEURISTIC AID: a program over the conventions page for a reader who cannot judge from the page.
...
families read 18  members read 46 (35 not compared: no reads line, or an accessor)  flags 0

heuristic: (none: no compared member lacks a field its own concept declares and a same-family neighbour reads)
...

How to read it. flags 0 means no compared member lacks a field a neighbour reads. It does not mean every member is right: 35 of 45 members were not compared at all, and the line says so. A member is not compared when it has no reads line, or when it is an accessor, a definition whose whole job is to hand back one field. A flag, when there is one, is a place to ask the writer a question.

5. What changed between the draft and the delivered program

The diff compares two versions of the program and lists what moved, channel by channel. Below, the agent's first draft of the routes against the delivered forum: three declarations were added (the agent's own claims about the program's shape), and three routes changed the permissions they declare.

Verbatim from docs/forum-demo/outputs/step1c-organize-diff.txt, which scripts/forum-demo/replay.sh regenerates and a test holds this page to. Lines elided are marked ....

$ yichus organize diff --before <routes draft> --after demos/service/forum.bosatsu
organization-diff  routes draft -> forum.bosatsu
bindings 56 -> 60 (+4)  plumbing 24 -> 24 (0)  dup mass 47 -> 37 (-10)  total mass 1994 -> 2261 (+267)
clone pairs 0 -> 0 (0)  bypasses 0 -> 0 (0)
...
bindings added:
   + forum_reading  Yichus/Organize::ReadingOrder
   + forum_shape  Yichus/Organize::FamilySpec
   + forum_tables  Yichus/Organize::FamilySpec
   + thread_request_issues  (req: OpenThreadRequest) -> List[Issue]
...
family joins:
   + forum_reading joined no family (a framework declaration: the conventions page lists it under framework artifacts, in no family)
   + forum_shape joined no family (a framework declaration: the conventions page lists it under framework artifacts, in no family)
   + forum_tables joined no family (a framework declaration: the conventions page lists it under framework artifacts, in no family)
   + thread_request_issues joined no family (2 other bindings share its shape (_) -> _[_], but it agrees with none of them on every filler but one: not a family)

family leaves:
   (none)

stack movement (kept bindings whose layer or used-above changed):
   ~ forum_api  moved up 1 (L6 -> L7)  used-above 0 (unchanged)
   ~ open_thread  moved up 1 (L5 -> L6)  used-above 1 (unchanged)
   ~ parse_thread  moved up 1 (L4 -> L5)  used-above 1 (unchanged)

framework artifacts:
   + forum_reading: Yichus/Organize::ReadingOrder
   + forum_shape: Yichus/Organize::FamilySpec
   + forum_tables: Yichus/Organize::FamilySpec
   ~ route /posts/reply -> post_reply  read moderators, create posts, read posts, write posts, read threads  (was: post_reply  read moderators, read posts, write posts, read threads)
   ~ route /threads -> list_threads  read moderators, query threads  (was: list_threads  read moderators, read threads)
   ~ route /threads/open -> open_thread  create threads, write threads  (was: open_thread  write threads)

declarations (Yichus/Organize: a change to a claim, apart from a change to the code):
   + forum_shape  FamilySpec 'handlers' (8 members)
   + forum_tables  FamilySpec 'tables' (4 members)
   + forum_reading  ReadingOrder (33 steps)
...

How to read it. The summary line counts, before and after: bindings (definitions); plumbing (definitions whose shape names no concept of the program: helpers for text and lists); dup mass (compiled pieces repeated inside definitions instead of shared) against total mass (the compiled size of the whole program; every mass is a count of pieces in the compiled program, not bytes); clone pairs (two definitions with the same body); and bypasses (a definition that exists and is used, written out again somewhere instead of called). None of these is a score; the lens guide defines each. "Bindings added" lists new definitions with their types. "Family joins" says, for each, whether it joined a family of the conventions page and, if not, why in the page's own terms; a framework artifact (or framework declaration) is a definition the platform reads rather than the program calls, such as the routes table, the access rules, or the agent's claims about the program's shape, and it never joins a family. "Stack movement" lists definitions whose place in the program's layering changed: a definition's layer is its height in the build order (layer 0 has no dependencies on other user definitions; each layer is built from the ones below), and used-above counts the definitions built from it; "moved up 1 (L6 -> L7)" says the definition now sits one layer higher. Under "framework artifacts", a ~ route line shows a route's permissions now and, in parentheses, before; a permission names a table and one of four actions: read one row, query the table's rows, write an existing row, create a new row under a fresh id. /threads/open now declares that it creates threads, which the verifier had found missing from the draft. "Declarations" lists the claims the agent added apart from the code.

What it does not say. Whether the change was the right one. The diff is a list of movements; the verifier's proof (the next section) is what says the delivered routes declare what their handlers do.

6. The proof a verdict can rest on

The verifier checks modeled database operations against declared owner-key and guard policies. Read each property’s status and assumptions; compilation alone does not establish access control. Below, its verdict over the delivered forum and one of its lines: every write post_reply makes to the posts table happens after the members-only check on the thread the post belongs to.

Verbatim from docs/forum-demo/outputs/step1c-verify.txt, which scripts/forum-demo/replay.sh regenerates and a test holds this page to. Lines elided are marked ....

$ yichus api verify demos/service/forum.bosatsu
proven False
compiles proven
...
access:posts proven
...
    Demo/Forum::post_reply db_write on "posts": dominated by can_see(Principal.user_id, row of threads), on the row it was applied to (key thread_id)
...

How to read it. proven False on the first line is the verdict over every check (compiles proven under it says the program type-checked, the floor every other check stands on); further down the same output, two checks about running several copies of the program at once are the ones that fail, and with one copy declared the verdict turns True and they drop to warnings (the builder page shows both runs whole). The access checks are all proven. The quoted line names the handler, the table, the kind of access, and the guard the write is dominated by, the tool's word for a check that every path to the write passes through, so the write cannot happen unless the check passed. This establishes the reported guard-dominance property in the compiled model. Establishing the members-only rule also requires the guard’s logic, its row relationship, and the runtime’s behavior to satisfy that rule.

What it does not say. That can_see is the right rule. The proof shows the write sits under it; whether "any member who can see the thread may reply" is the rule you asked for is yours to judge.

How to reach a verdict from these pages

• Before accepting a guarantee, check that the property actually expresses the rule you asked for, that it was established, and that its assumptions match the deployment. A heading or check name alone is insufficient.
• An "observed on this run" sentence can refute (a run that did what the rule forbids) but never establish. On its own it supports at most "cannot tell", plus an experiment ordered by name from the proposals or a report line demanded from the writer.
• For a seeded value outside the intended domain, check whether the program rejects it. A negative count or empty name can expose a real validation defect if the system accepts it.
• Cannot tell is a finding about the materials. Each question these pages could not answer names a page line, a sentence, or a proposal that should exist.

Where to go next

• Reading the organization lenses: every page the toolkit renders about a program, what each answers, and what it does not say.
• The forum walkthrough: the prompts the agent was given, step by step, and what the tools caught at each.
• Building with an agent: the same runs from the command line, for the person beside you who does read code.