Check that the code is wired as the graph plans

[yogthos]

A review of writ from the agent's side, where a spec is the plan and the check confirms the code follows it, found ways wrong code or a weaker-than-it-looks spec got through (writ-sg8).

Fixed:

• a spec helper named like a target fn was silently replaced by the target's, so a law judged the code with the code; a sort that rotates its input had sorted proved. That is now an error naming the helper to rename
• graph edges only bounded the code: a signal stuck on green kept every edge. Each target of an edge is now also a law that some value takes the step
• two states of one plain type couldn't be told apart, so :unsorted -> :sorted over (List Nat) checked only the type. That fails now; the fix is a refinement, and the edge into it becomes the law. An edge mixing a plain target with refined ones fails too
• a public fn with no ann passed unchecked; it fails now, and a passing report lists signed public fns no graph, machine or flow names

New:

• flow states the path data takes through a fn, (flow handle [s] [s normalize respond :result]), checked by following values through its lowered source (lambdas, fns passed by name, loops). It catches code that calls every layer but hands one the raw input
• calls takes {:through [..] :not [..]}, checked on the transitive graph and reported with the path
• calls and flow accept a fn of another namespace, so an effect shell's wiring can be stated; the shortener spec now pins shortener.server/app to core/handle through the store. The shell is read, never loaded
• edges can place the state with _ ([insert Nat _]) and take a state out of a tuple with first/second/last
• spec/plan prints the spec as a plan to confirm before code exists; mermaid draws a graph

Prover side: edge laws are written as the target's predicate of the call, so they're proved like the spec's own laws. "Never throws" is only provable symbolically, which recursion defeats, so for recursive fns the landing is proved and the report says totality was tested. A law that says the same as a proved one is proved by it when no proof from the code turns up.

Many demo specs used the two-plain-states graph, several claiming insert into any list is sorted; they now use a Sorted refinement, and some law counts in tests grew with the new edge laws.

writ tests: 392 pass. Examples: all pass; shortener takes 390s against 399s on main.