Yichus/Law
Builtin package (resource law.bosatsu).
This is the complete package source used by this build. The export
list names its public API; definitions below give the types and behavior.
New to the API? Start with Make a calculator or Build an API, then use this page to look up a definition.
package Yichus/Law
from Zafu/Control/IterState import (
foldl_List as iter_foldl_List,
done as iter_done,
continue as iter_continue,
value as iter_value,
)
# Universal claims about pure total functions. Existing `yichus law`
# checks Obligation values over seeded generated inputs: a bounded
# observation, never proof. FiniteObligation names an explicit finite
# domain for a separate exhaustive method; it does not change the sampled
# meaning of an ordinary Obligation.
#
# Spec-first, persona-first: the property suggester (`api_suggest_properties`)
# proposes Obligations as complete compilable units filled from the typed IR;
# a piece it cannot fill from facts arrives as a WitnessTodo — a typed named
# hole. Totality is why holes are a variant and not a `hole[a]` function: a
# total language cannot conjure an `a`, so an unfilled hole is a constructor
# the checker sees and reports as `inconclusive: hole not filled`, never as
# a pass.
export (
Domain(),
Law(),
WitnessSpec(),
Obligation(),
FiniteObligation(),
CommitObligation(),
Discharge(),
Obligations(),
FoldRun(),
Pair(),
Triple(),
FieldFact(),
TableFact(),
ParamFact(),
GuardFact(),
BindingFact(),
StructField(),
StructFact(),
ProgramFacts(),
Suggestion(),
Rule(),
RuleSet(),
Dismissed(),
default_rules,
guards_near,
first_bound_guard,
is_lower_rel,
is_upper_rel,
exists_List,
filter_List,
flat_map_List,
contains_String,
never_below,
never_above,
conserves,
inverse,
idempotent,
commutative,
associative,
order_independent,
permutes,
permute_by,
multiset_eq,
size_List,
)
# Everything type-specific about an input domain in one place: how to print
# it in a counterexample, how to generate it, how to shrink it.
# `gen = None` means "derive from the type" (ValueGen, seeded by the
# checker's portable splitmix64); `shrink = None` means the structural
# default. The catalog fills these in, so a user pasting a suggested law
# never constructs one by hand.
struct Domain[i](
name: String,
describe: i -> String,
gen: Option[Int -> i],
shrink: Option[i -> List[i]]
)
# A universal claim about a pure total function: `check` must hold for
# every input of the domain. Checked by seeded generation.
struct Law[i](name: String, domain: Domain[i], check: i -> Bool)
# Anti-vacuity. A law that holds because nothing ever happens is worse than
# no law: an enrollment fold that admits nobody satisfies "no seat count
# goes negative". Every Law needs a Witness some generated input satisfies,
# or its verdict is `inconclusive: vacuous`. WitnessTodo is the suggester's
# named hole: the check cannot be derived from the program's facts, and
# `why` says exactly what is missing. An Obligation carrying a WitnessTodo
# checks `inconclusive: hole not filled`.
enum WitnessSpec[i]:
Witness(name: String, check: i -> Bool)
WitnessTodo(name: String, why: String)
struct Obligation[i](law: Law[i], witnesses: List[WitnessSpec[i]])
# An explicit, complete domain for one obligation. The values are the entire
# claimed scope, not a seed or a sample. Repeated values do not enlarge it.
# First occurrence order is significant: it sets normalized value indices and
# the domain identity, so reordering the same values changes that identity.
# Keeping this wrapper separate preserves the sampled meaning of every
# existing Obligation and Domain declaration.
struct FiniteObligation[i](obligation: Obligation[i], values: List[i])
# --- Commit obligations ----------------------------------------------------
# The strategy ladder: what the engine may do at commit time depends on
# which obligations the checked laws discharge. The user never needs this
# table — `api_obligations` walks them down it one proposed property at a
# time. A Discharge NAMES the laws (by their Law.name) that stand as
# bounded evidence for an obligation; the engine checks those laws hold
# and fails closed on anything violated, inconclusive, or unnamed. The
# binding is a declaration: the evidence is the named laws' verdicts,
# and a licensed strategy is licensed by bounded evidence, never proof.
# The rungs, in licensing order:
# - DistinctKeyCommutativity: applying two operations with distinct keys
# commutes; licenses per-key independence (a larger effective
# interleaving bound).
# - PerOpMonotonicity: each operation moves its key's value
# monotonically; with commutativity, licenses escrow interval
# arithmetic and the single-write commit.
# - DeclaredLattice: a declared lattice (zero, combine, le) extends the
# same arithmetic past Int to sets, multisets, and max-registers.
# - NonMonotoneWitness: an explicitly declared non-monotone key
# property; licenses bounded witness search instead of the monotone
# ladder.
# Constructor order is a wire format: ObligationsExtractor decodes these
# by variant index (0-3). Append new rungs at the end; never reorder.
enum CommitObligation:
DistinctKeyCommutativity
PerOpMonotonicity
DeclaredLattice
NonMonotoneWitness
struct Discharge(obligation: CommitObligation, laws: List[String])
# The program's declared obligation evidence, discovered by binding type
# like Obligation. Several bindings per module are collected and all
# considered; one is the conventional shape.
struct Obligations(discharges: List[Discharge])
# The catalog's own input shape for "run a fold over some operations".
# `shuffle` seeds the permutation the order-independence law compares
# against, so ordering is generated rather than assumed.
struct FoldRun[s, o](initial: s, ops: List[o], shuffle: Int)
# Argument shapes for the binary/ternary catalog laws (a tuple-free
# vocabulary keeps generated snippets dependent only on this package).
struct Pair[a](fst: a, snd: a)
struct Triple[a](t1: a, t2: a, t3: a)
# --- Suggestion vocabulary -------------------------------------------------
# Facts are reified from the typed IR by the suggester (Scala builds them as
# JSON; the compiler's own ValueToJson bridge decodes them into these
# structs). A rule is an ordinary Bosatsu function over the facts; teams add
# their own RuleSet, which is what keeps the suggester open rather than an
# eighth closed checker.
struct FieldFact(name: String, kind: String)
# access_policy is the declared policy's exact name ("OwnerScoped" /
# "Public") or "undeclared" when no AccessRule names the resource;
# access_proven is the static access checker's verdict — the same
# analyzer api_access_check runs. Rules over these facts propose
# declarations and defer the proving to the checker: access is a static
# proof, never a bounded law.
#
# conformances names the handler bindings a declared Yichus/Spec
# Conformance already binds to a model of this table — rules over it
# propose drafts for the writers no model covers, and the conformance
# checker (api_conformance_check) decides whether code and model agree.
struct TableFact(
name: String,
package_name: String,
fields: List[FieldFact],
readers: List[String],
writers: List[String],
access_policy: String,
access_proven: Bool,
conformances: List[String]
)
struct ParamFact(
name: String,
type_name: String,
is_list: Bool,
element_type: String
)
# A comparison against an Int literal, recovered from the compiled IR's
# CompareLit/CompareInt nodes and normalized so the guarded value is on the
# left: relation is one of "eq", "ne", "lt", "lte", "gt", "gte". The
# relation is what lets a rule tell a floor guard from a ceiling guard.
struct GuardFact(literal: Int, relation: String)
# Rendering conventions (LawFacts.scala fills these; rules match on the
# strings): a param's type renders fully qualified for world types
# ("Yichus/Data::Db", "Yichus/Access::Principal") and other packages'
# types as "Pkg/Path::Name"; type_imports lists the same-package type
# names in the signature, bare. importable means the package exports the binding and
# every same-package type its signature names, so a generated standalone
# file can import it: rules whose snippet imports the binding fire only
# on importable bindings, since any other snippet would not compile.
struct BindingFact(
name: String,
package_name: String,
params: List[ParamFact],
result_type: String,
is_pure: Bool,
reads: List[String],
writes: List[String],
read_modify_writes: List[String],
guards: List[GuardFact],
calls: List[String],
type_imports: List[String],
declared_laws: List[String],
importable: Bool
)
# A struct a user package defines (one constructor), its fields in
# declaration order with each field's type rendered as for params and the
# bindings ("Pkg::name") that read the field: readers holds those whose
# compiled IR extracts it and every user binding that calls one of them,
# at any depth and across packages; direct_readers holds only the first
# kind.
# importable means a sibling package can import the type with its
# constructor (`export (Name())`), so a generated file can build and
# take apart its values.
struct StructField(name: String, kind: String, readers: List[String], direct_readers: List[String])
struct StructFact(
name: String,
package_name: String,
fields: List[StructField],
importable: Bool
)
struct ProgramFacts(bindings: List[BindingFact], tables: List[TableFact], structs: List[StructFact])
# unlocks names what acting on the suggestion enables, and its shape is
# a contract: a suggestion proposing an Obligation names its catalog law
# as `laws.<name>`; a suggestion proposing a declaration a static
# checker proves names the tool (`api_access_check`). Consumers route on
# this — the report's needed channel carries only `laws.*` suggestions
# as Obligation artifacts.
struct Suggestion(
template: String,
because: String,
unlocks: String,
snippet: String,
targets: List[String]
)
struct Rule(name: String, run: ProgramFacts -> List[Suggestion])
struct RuleSet(name: String, rules: List[Rule])
# A declined suggestion. The suggester drops any suggestion matching a
# discovered Dismissed binding and reports it under `dismissed` — never
# silently — so a declined suggestion stops firing instead of looping an
# agent forever. The reason is required: the next reader learns why.
# A grouped suggestion (several targets sharing one snippet, like the
# per-package access rules) is dismissed only when every target has its
# own Dismissed binding: declining one table never silences a sibling
# that still needs a policy.
struct Dismissed(template: String, target: String, reason: String)
# --- Int and list helpers --------------------------------------------------
def size_List[a](items: List[a]) -> Int:
items.foldl_List(0, (acc, _) -> add(acc, 1))
def at_least(value: Int, floor: Int) -> Bool:
match cmp_Int(value, floor):
case LT: False
case _: True
def at_most(value: Int, ceiling: Int) -> Bool:
match cmp_Int(value, ceiling):
case GT: False
case _: True
def all_Ints(values: List[Int], pred: Int -> Bool) -> Bool:
values.foldl_List(True, (acc, v) ->
match acc:
case False: False
case True: pred(v)
)
def rev_append[a](items: List[a], tail: List[a]) -> List[a]:
loop items:
case []: tail
case [head, *rest]: rev_append(rest, [head, *tail])
# Remove the first element equal (by `eq`) to `target`; None if absent.
def remove_first[a](items: List[a], target: a, eq: (a, a) -> Bool) -> Option[List[a]]:
recur items:
case []: None
case [head, *rest]:
match eq(head, target):
case True: Some(rest)
case False:
match remove_first(rest, target, eq):
case Some(pruned): Some([head, *pruned])
case None: None
# Equality of multisets under a caller-supplied element equality.
def multiset_eq[a](left: List[a], right: List[a], eq: (a, a) -> Bool) -> Bool:
loop left:
case []: right matches []
case [head, *rest]:
match remove_first(right, head, eq):
case Some(pruned): multiset_eq(rest, pruned, eq)
case None: False
# Internal carrier for pick_at: the element and the list without it.
struct Picked[a](item: a, rest: List[a])
# Element at `idx` plus the list without it; None when out of range.
def pick_at[a](items: List[a], idx: Int) -> Option[Picked[a]]:
match cmp_Int(idx, 0):
case LT: None
case _:
recur items:
case []: None
case [head, *rest]:
match cmp_Int(idx, 0):
case EQ: Some(Picked(head, rest))
case _:
match pick_at(rest, sub(idx, 1)):
case Some(Picked(picked, pruned)): Some(Picked(picked, [head, *pruned]))
case None: None
def permute_step[a](
fuel: List[a],
remaining: List[a],
count: Int,
code: Int,
acc: List[a]
) -> List[a]:
loop fuel:
case []: rev_append(acc, remaining)
case [_, *fs]:
match cmp_Int(count, 0):
case GT:
idx = mod_Int(code, count)
match pick_at(remaining, idx):
case Some(Picked(picked, pruned)):
permute_step(fs, pruned, sub(count, 1), div(code, count), [picked, *acc])
case None: rev_append(acc, remaining)
case _: rev_append(acc, remaining)
# Seed-indexed permutation of a list: the seed is read as a Lehmer code,
# so every permutation of the list is reachable from some seed (codes are
# taken mod n! implicitly, digit by digit). Deterministic, total, and the
# same on every runtime — the checker derives `shuffle` from its portable
# splitmix64 stream.
def permute_by[a](seed: Int, items: List[a]) -> List[a]:
n = size_List(items)
code = match cmp_Int(seed, 0):
case LT: sub(0, seed)
case _: seed
permute_step(items, items, n, code, [])
# --- The catalog -----------------------------------------------------------
# Named templates: a suggestion is a one-line instantiation, and each law's
# `name` is a plain sentence, so a verdict reads as a claim about the user's
# domain rather than about a combinator.
def never_below[i](name: String, d: Domain[i], values: i -> List[Int], floor: Int) -> Law[i]:
Law(name, d, x -> all_Ints(values(x), v -> at_least(v, floor)))
def never_above[i](name: String, d: Domain[i], values: i -> List[Int], ceiling: Int) -> Law[i]:
Law(name, d, x -> all_Ints(values(x), v -> at_most(v, ceiling)))
def conserves[i](name: String, d: Domain[i], before: i -> Int, after: i -> Int) -> Law[i]:
Law(name, d, x -> eq_Int(before(x), after(x)))
def inverse[i, s](
name: String,
d: Domain[i],
start: i -> s,
roundtrip: i -> s,
eq: (s, s) -> Bool
) -> Law[i]:
Law(name, d, x -> eq(start(x), roundtrip(x)))
def idempotent[i, s](
name: String,
d: Domain[i],
once: i -> s,
twice: i -> s,
eq: (s, s) -> Bool
) -> Law[i]:
Law(name, d, x -> eq(once(x), twice(x)))
def commutative[a, r](
name: String,
d: Domain[Pair[a]],
f: (a, a) -> r,
eq: (r, r) -> Bool
) -> Law[Pair[a]]:
def chk(p: Pair[a]) -> Bool:
Pair(x, y) = p
eq(f(x, y), f(y, x))
Law(name, d, chk)
def associative[a](
name: String,
d: Domain[Triple[a]],
f: (a, a) -> a,
eq: (a, a) -> Bool
) -> Law[Triple[a]]:
def chk(t: Triple[a]) -> Bool:
Triple(x, y, z) = t
eq(f(f(x, y), z), f(x, f(y, z)))
Law(name, d, chk)
# The output is a permutation of the input: catches the fold that silently
# drops or duplicates an item.
def permutes[i, a](
name: String,
d: Domain[i],
input: i -> List[a],
output: i -> List[a],
eq: (a, a) -> Bool
) -> Law[i]:
Law(name, d, x -> multiset_eq(input(x), output(x), eq))
# Running the fold over the ops and over a seed-indexed permutation of the
# ops gives equal results. Ordering is generated, not assumed.
def order_independent[s, o, r](
name: String,
fold: (s, List[o]) -> r,
eq: (r, r) -> Bool,
d: Domain[FoldRun[s, o]]
) -> Law[FoldRun[s, o]]:
def chk(run: FoldRun[s, o]) -> Bool:
FoldRun(initial, ops, shuffle) = run
eq(fold(initial, ops), fold(initial, permute_by(shuffle, ops)))
Law(name, d, chk)
# --- List and String helpers for rules -------------------------------------
def exists_List[a](items: List[a], pred: a -> Bool) -> Bool:
def step(acc: Bool, item: a) -> Bool:
match acc:
case True: True
case False: pred(item)
items.foldl_List(False, step)
def filter_List[a](items: List[a], pred: a -> Bool) -> List[a]:
def step(acc: List[a], item: a) -> List[a]:
match pred(item):
case True: [item, *acc]
case False: acc
rev_append(items.foldl_List([], step), [])
def flat_map_List[a, b](items: List[a], f: a -> List[b]) -> List[b]:
def step(acc: List[b], item: a) -> List[b]:
rev_append(f(item), acc)
rev_append(items.foldl_List([], step), [])
def contains_String(items: List[String], target: String) -> Bool:
exists_List(items, s -> eq_String(s, target))
# --- The default suggestion rules ------------------------------------------
#
# Rules run over ProgramFacts reified from the compiled IR. Every
# suggestion is a complete standalone Bosatsu file: package declaration,
# imports, and an Obligation whose unfillable pieces are NAMED HOLES — a
# stub projection returning [], a permissive eq returning True, a
# WitnessTodo. The holes are safe by construction: a hole can make the
# verdict inconclusive, never a false pass and never a false violation.
# A rule that cannot fill a piece from the facts emits a hole and says
# what is missing; a rule with nothing honest to say emits nothing.
def is_lower_rel(rel: String) -> Bool:
match eq_String(rel, "gt"):
case True: True
case False: eq_String(rel, "gte")
def is_upper_rel(rel: String) -> Bool:
match eq_String(rel, "lt"):
case True: True
case False: eq_String(rel, "lte")
# A type rendered from another package ("Other/Pkg::T") cannot be named
# by a generated standalone file; rules that would name one stay silent.
def is_qualified_type(s: String) -> Bool:
match partition_String(s, "::"):
case None: False
case Some(_): True
# The fold shape the fold rules fire on: two parameters, a state and a
# List of operations (either order), returning the state's own type —
# `(S, List[O]) -> S` is a fold of operations; `(List[a], a) -> Bool` or
# `(List[a], a) -> List[a]` is not. The binding must be importable, since
# every fold snippet imports it, and its state and operation types must be
# nameable there (no other package's types, which render "Pkg::T").
# state_first records the call spelling.
struct FoldShape(state: ParamFact, ops: ParamFact, state_first: Bool)
def fold_shape(b: BindingFact) -> Option[FoldShape]:
BindingFact(_, _, params, result_type, _, _, _, _, _, _, _, _, importable) = b
shape = match params:
case [p1, p2]:
ParamFact(_, _, list1, _) = p1
ParamFact(_, _, list2, _) = p2
match (list1, list2):
case (False, True): Some(FoldShape(p1, p2, True))
case (True, False): Some(FoldShape(p2, p1, False))
case _: None
case _: None
match shape:
case Some(FoldShape(ParamFact(_, state_type, _, _), ParamFact(_, _, _, elem_type), _)):
match (importable, is_qualified_type(state_type), is_qualified_type(elem_type), eq_String(state_type, result_type)):
case (True, False, False, True): shape
case _: None
case None: None
# Own guards first, in declaration order, then called bindings' guards in
# their order — first_bound_guard takes the first match, so ordering is
# part of the contract.
def guards_near(b: BindingFact, all_bindings: List[BindingFact]) -> List[GuardFact]:
BindingFact(_, _, _, _, _, _, _, _, own, calls, _, _, _) = b
called = all_bindings.flat_map_List(other -> (
BindingFact(oname, _, _, _, _, _, _, _, oguards, _, _, _, _) = other
match contains_String(calls, oname):
case True: oguards
case False: []
))
rev_append(rev_append(own, []), called)
# A fold snippet exports an Obligation over FoldRun[S, O]; S and O are
# exactly the signature's types, so the fold's package is exposed only
# when its own types appear there.
def fold_exposes(pkg: String, type_imports: List[String]) -> String:
match type_imports:
case []: "exposes Yichus/Law\n"
case _: concat_String(["exposes (", pkg, ", Yichus/Law)\n"])
def import_clause(pkg: String, binding_name: String, type_imports: List[String]) -> String:
extra = type_imports.foldl_List("", (acc, t) -> concat_String([acc, ", ", t]))
concat_String(["from ", pkg, " import (", binding_name, extra, ")\n"])
def fold_call(binding_name: String, shape: FoldShape) -> String:
FoldShape(_, _, state_first) = shape
match state_first:
case True: concat_String([binding_name, "(initial, ops)"])
case False: concat_String([binding_name, "(ops, initial)"])
def fold_run_type(shape: FoldShape) -> String:
FoldShape(state, ops, _) = shape
ParamFact(_, state_type, _, _) = state
ParamFact(_, _, _, elem_type) = ops
concat_String(["FoldRun[", state_type, ", ", elem_type, "]"])
# Shared skeleton for the floor and ceiling suggestions: a standalone
# file with a stub projection (values_hole) and a WitnessTodo, both named
# holes. The pasted file compiles and checks `inconclusive` until the
# holes are filled — never a false pass.
def bound_snippet(
b: BindingFact,
shape: FoldShape,
literal: Int,
catalog_fn: String,
phrase: String,
suffix: String
) -> String:
BindingFact(bname, pkg, _, _, _, _, _, _, _, _, type_imports, _, _) = b
run_type = fold_run_type(shape)
lit_str = int_to_String(literal)
concat_String([
"package ", pkg, "/Laws\n",
"\n",
"from Yichus/Law import (Domain, FoldRun, Obligation, WitnessTodo, ", catalog_fn, ")\n",
import_clause(pkg, bname, type_imports),
"\n",
"export (", bname, "_", suffix, ")\n",
"\n",
fold_exposes(pkg, type_imports),
"\n",
"# Suggested by the ", catalog_fn, " rule: a guard in or reachable from\n",
"# `", bname, "` compares an Int against ", lit_str, ". Two named holes:\n",
"# values_hole — project the Ints this law bounds from a completed run\n",
"# the WitnessTodo — prove a generated run actually exercised `", bname, "`\n",
"# The Domain's gen is a third hole when the type-driven default cannot\n",
"# build a ", run_type, ": if the verdict says 'not generable', replace\n",
"# the first None in the Domain with Some(seed -> ...)\n",
"def values_hole(run: ", run_type, ") -> List[Int]:\n",
" FoldRun(initial, ops, _) = run\n",
" _ = ", fold_call(bname, shape), "\n",
" []\n",
"\n",
"def describe_hole(_: ", run_type, ") -> String:\n",
" \"", bname, " run\"\n",
"\n",
bname, "_runs = Domain(\"", bname, " runs\", describe_hole, None, None)\n",
"\n",
bname, "_", suffix, " = Obligation(\n",
" ", catalog_fn, "(\"", bname, " results stay ", phrase, " ", lit_str, "\", ", bname, "_runs, values_hole, ", lit_str, "),\n",
" [WitnessTodo(\"the run is meaningful\", \"replace values_hole's [] with the projected values, then turn this into a Witness that some generated run exercises ", bname, "\")]\n",
")\n"
])
def first_bound_guard(
b: BindingFact,
all_bindings: List[BindingFact],
keep: String -> Bool
) -> Option[GuardFact]:
iter_value(iter_foldl_List(guards_near(b, all_bindings), None, (_, g) -> (
GuardFact(_, rel) = g
match keep(rel):
case True: iter_done(Some(g))
case False: iter_continue(None)
)))
def bound_rule_run(
facts: ProgramFacts,
keep: String -> Bool,
template: String,
catalog_fn: String,
phrase: String,
suffix: String
) -> List[Suggestion]:
ProgramFacts(bindings, _, _) = facts
def suggest(b: BindingFact) -> List[Suggestion]:
BindingFact(bname, _, _, _, _, _, _, _, _, _, _, declared, _) = b
match declared:
case [_, *_]: []
case []:
match fold_shape(b):
case None: []
case Some(shape):
match first_bound_guard(b, bindings, keep):
case None: []
case Some(GuardFact(lit, rel)):
because = concat_String([
"a guard in or reachable from `", bname,
"` compares an Int against the literal ", int_to_String(lit),
" (relation ", rel, "), and `", bname, "` folds a list of operations"
])
unlocks = concat_String(["laws.", catalog_fn])
[Suggestion(template, because, unlocks, bound_snippet(b, shape, lit, catalog_fn, phrase, suffix), [bname])]
bindings.flat_map_List(suggest)
def rule_numeric_floor(facts: ProgramFacts) -> List[Suggestion]:
bound_rule_run(facts, is_lower_rel, "numeric-floor", "never_below", "at or above", "floor")
def rule_numeric_ceiling(facts: ProgramFacts) -> List[Suggestion]:
bound_rule_run(facts, is_upper_rel, "numeric-ceiling", "never_above", "at or below", "ceiling")
def rule_fold_ordering(facts: ProgramFacts) -> List[Suggestion]:
ProgramFacts(bindings, _, _) = facts
def suggest(b: BindingFact) -> List[Suggestion]:
BindingFact(bname, pkg, _, result_type, is_pure, _, _, _, _, _, type_imports, declared, _) = b
match (is_pure, declared):
case (False, _): []
case (_, [_, *_]): []
case (True, []):
match fold_shape(b):
case None: []
case Some(shape):
run_type = fold_run_type(shape)
FoldShape(state, ops_param, _) = shape
ParamFact(_, state_type, _, _) = state
ParamFact(_, _, _, elem_type) = ops_param
_ = elem_type
because = concat_String([
"`", bname, "` folds a list of operations over a ", state_type,
"; whether the outcome depends on operation order is a property worth pinning either way"
])
snippet = concat_String([
"package ", pkg, "/Laws\n",
"\n",
"from Yichus/Law import (Domain, FoldRun, Obligation, WitnessTodo, order_independent)\n",
import_clause(pkg, bname, type_imports),
"\n",
"export (", bname, "_order)\n",
"\n",
fold_exposes(pkg, type_imports),
"\n",
"# Suggested by the fold-ordering rule. One named hole:\n",
"# eq_hole — real equality for ", result_type, "; it returns True so the\n",
"# stub can never report a false violation, and the WitnessTodo blocks\n",
"# any pass until it is filled.\n",
"# The Domain's gen is a second hole when the type-driven default cannot\n",
"# build a ", run_type, ": if the verdict says 'not generable', replace\n",
"# the first None in the Domain with Some(seed -> ...)\n",
"def fold_hole(initial: ", state_type, ", ops: List[", elem_type, "]) -> ", result_type, ":\n",
" ", fold_call(bname, shape), "\n",
"\n",
"def eq_hole(left: ", result_type, ", right: ", result_type, ") -> Bool:\n",
" _ = left\n",
" _ = right\n",
" True\n",
"\n",
"def describe_hole(_: ", run_type, ") -> String:\n",
" \"", bname, " run\"\n",
"\n",
bname, "_runs = Domain(\"", bname, " runs\", describe_hole, None, None)\n",
"\n",
bname, "_order = Obligation(\n",
" order_independent(\"", bname, " is order independent\", fold_hole, eq_hole, ", bname, "_runs),\n",
" [WitnessTodo(\"orders can differ\", \"fill eq_hole with real equality, then turn this into a Witness that some generated run has at least two operations\")]\n",
")\n"
])
[Suggestion("fold-ordering", because, "laws.order_independent", snippet, [bname])]
bindings.flat_map_List(suggest)
def rule_unbounded_numeric(facts: ProgramFacts) -> List[Suggestion]:
ProgramFacts(bindings, tables, _) = facts
# Silence is per package: a guard silences only its own package's
# tables, since the because-text claims no bound is checked in the
# module that owns the table — a guard elsewhere says nothing here.
def pkg_has_guard(pkg: String) -> Bool:
bindings.exists_List(b -> (
BindingFact(_, bpkg, _, _, _, _, _, _, guards, _, _, _, _) = b
match guards:
case []: False
case [_, *_]: eq_String(bpkg, pkg)
))
def suggest(t: TableFact) -> List[Suggestion]:
TableFact(tname, tpkg, fields, _, writers, _, _, _) = t
match (pkg_has_guard(tpkg), writers):
case (True, _): []
case (_, []): []
case (False, [_, *_]):
int_fields = fields.filter_List(f -> (
FieldFact(_, kind) = f
eq_String(kind, "Int")
))
def per_field(f: FieldFact) -> List[Suggestion]:
FieldFact(fname, _) = f
because = concat_String([
"`", tname, ".", fname, "` is an Int written by handlers, and no bound on any",
" Int is checked anywhere in this module — is that intended?"
])
snippet = concat_String([
"package ", tpkg, "/Laws\n",
"\n",
"from Yichus/Law import (Domain, Obligation, WitnessTodo, never_below)\n",
"\n",
"export (", fname, "_floor)\n",
"\n",
"exposes (Yichus/Law)\n",
"\n",
"# Suggested by the unbounded-numeric rule. Two named holes:\n",
"# floor_hole — the intended lower bound for ", tname, ".", fname, "\n",
"# the Domain — connect it to the real states this field takes\n",
"floor_hole = 0\n",
"\n",
"def field_values_hole(state: Int) -> List[Int]:\n",
" [state]\n",
"\n",
fname, "_domain = Domain(\"", tname, ".", fname, " values\", int_to_String, None, None)\n",
"\n",
fname, "_floor = Obligation(\n",
" never_below(\"", tname, ".", fname, " stays at or above the floor\", ", fname, "_domain, field_values_hole, floor_hole),\n",
" [WitnessTodo(\"a written value appears\", \"the Int domain is a placeholder; generate the real states ", tname, ".", fname, " takes\")]\n",
")\n"
])
[Suggestion("unbounded-numeric", because, "laws.never_below", snippet, [concat_String([tname, ".", fname])])]
int_fields.flat_map_List(per_field)
tables.flat_map_List(suggest)
# The access rules group per package: a suggestion's snippet is a whole
# standalone file named `{pkg}/Access` (or `{pkg}/AccessNotes`), so two
# tables sharing a package must share one snippet — two files declaring
# the same package could not both be pasted.
def table_pkg(t: TableFact) -> String:
TableFact(_, tpkg, _, _, _, _, _, _) = t
tpkg
def table_name(t: TableFact) -> String:
TableFact(tname, _, _, _, _, _, _, _) = t
tname
def table_policy(t: TableFact) -> String:
TableFact(_, _, _, _, _, policy, _, _) = t
policy
def distinct_pkgs(ts: List[TableFact]) -> List[String]:
def add(acc: List[String], t: TableFact) -> List[String]:
p = table_pkg(t)
match acc.exists_List(q -> eq_String(p, q)):
case True: acc
case False: [p, *acc]
reverse(ts.foldl_List([], add))
def join_String(sep: String, xs: List[String]) -> String:
match xs:
case []: ""
case [x, *rest]: concat_String([x, *rest.flat_map_List(r -> [sep, r])])
# A table handlers read or write with no declared access policy gets the
# paste-ready AccessSpec proposed. OwnerScoped is the safe starting
# point; api_access_check proves or refutes the declaration against the
# compiled IR — the rule proposes, the static checker decides. One
# suggestion per package: its AccessSpec covers every undeclared touched
# table there.
def rule_undeclared_access(facts: ProgramFacts) -> List[Suggestion]:
ProgramFacts(_, tables, _) = facts
def undeclared_touched(t: TableFact) -> Bool:
TableFact(_, _, _, readers, writers, policy, _, _) = t
touched = match (readers, writers):
case ([], []): False
case _: True
match (eq_String(policy, "undeclared"), touched):
case (True, True): True
case _: False
undeclared = tables.filter_List(undeclared_touched)
def per_pkg(pkg: String) -> List[Suggestion]:
names = undeclared.filter_List(t -> eq_String(table_pkg(t), pkg)).map_List(table_name)
match names:
case []: []
case [tname]:
because = concat_String([
"handlers touch `", tname,
"` and no AccessRule names it: who may read this data is undeclared, so nothing is proven about it"
])
snippet = concat_String([
"package ", pkg, "/Access\n",
"\n",
"from Yichus/Access import AccessRule, AccessSpec, OwnerScoped\n",
"\n",
"export (access_rules)\n",
"\n",
"exposes (Yichus/Access)\n",
"\n",
"# Suggested by the undeclared-access rule: handlers read or write\n",
"# \"", tname, "\" with no declared access policy. OwnerScoped is the\n",
"# safe starting point; api_access_check proves or refutes it against\n",
"# the compiled IR. Change to Public only if this data really is.\n",
"access_rules = AccessSpec([\n",
" AccessRule(\"", tname, "\", OwnerScoped),\n",
"])\n"
])
[Suggestion("undeclared-access", because, "api_access_check", snippet, [tname])]
case _:
listed = join_String(", ", names.map_List(n -> concat_String(["`", n, "`"])))
rule_lines = names.flat_map_List(n -> [" AccessRule(\"", n, "\", OwnerScoped),\n"])
because = concat_String([
"handlers touch ", listed,
" and no AccessRule names them: who may read this data is undeclared, so nothing is proven about it"
])
snippet = concat_String([
"package ", pkg, "/Access\n",
"\n",
"from Yichus/Access import AccessRule, AccessSpec, OwnerScoped\n",
"\n",
"export (access_rules)\n",
"\n",
"exposes (Yichus/Access)\n",
"\n",
"# Suggested by the undeclared-access rule: handlers read or write\n",
"# these tables with no declared access policy. OwnerScoped is the\n",
"# safe starting point; api_access_check proves or refutes it against\n",
"# the compiled IR. Change to Public only if this data really is.\n",
"access_rules = AccessSpec([\n",
*rule_lines,
"])\n"
])
[Suggestion("undeclared-access", because, "api_access_check", snippet, names)]
distinct_pkgs(undeclared).flat_map_List(per_pkg)
# A declared policy the static checker cannot prove is a finding, not a
# pass: the fix is in the code (key every operation on the table by
# Principal.user_id for OwnerScoped), never in weakening the declaration.
# The snippet is a note file — it compiles as pasted and records the
# finding, because the real change belongs in the handler. One note file
# per package, listing every unproven declaration there.
def rule_unproven_access(facts: ProgramFacts) -> List[Suggestion]:
ProgramFacts(_, tables, _) = facts
def declared_unproven(t: TableFact) -> Bool:
TableFact(_, _, _, _, _, policy, proven, _) = t
match (eq_String(policy, "undeclared"), proven):
case (False, False): True
case _: False
unproven = tables.filter_List(declared_unproven)
def per_pkg(pkg: String) -> List[Suggestion]:
in_pkg = unproven.filter_List(t -> eq_String(table_pkg(t), pkg))
match in_pkg:
case []: []
case [t]:
tname = table_name(t)
policy = table_policy(t)
because = concat_String([
"`", tname, "` declares ", policy,
" but api_access_check cannot prove it from the compiled IR — fix the code, never weaken the declaration"
])
snippet = concat_String([
"package ", pkg, "/AccessNotes\n",
"\n",
"# Suggested by the unproven-access rule: \"", tname, "\" declares\n",
"# ", policy, " but the static checker cannot prove it. Key every db\n",
"# operation on this table by Principal.user_id (for OwnerScoped),\n",
"# then run api_access_check for the precise failing operation.\n",
"# This note file records the finding; the fix belongs in the handler.\n"
])
[Suggestion("unproven-access", because, "api_access_check", snippet, [tname])]
case _:
names = in_pkg.map_List(table_name)
listed = join_String(", ", names.map_List(n -> concat_String(["`", n, "`"])))
table_lines = in_pkg.flat_map_List(t -> [
"# \"", table_name(t), "\" declares ", table_policy(t), "\n"
])
because = concat_String([
listed,
" declare access policies api_access_check cannot prove from the compiled IR — fix the code, never weaken the declarations"
])
snippet = concat_String([
"package ", pkg, "/AccessNotes\n",
"\n",
"# Suggested by the unproven-access rule: these tables declare\n",
"# policies the static checker cannot prove:\n",
*table_lines,
"# Key every db operation on them by Principal.user_id (for\n",
"# OwnerScoped), then run api_access_check for the precise failing\n",
"# operation. This note file records the findings; the fixes belong\n",
"# in the handlers.\n"
])
[Suggestion("unproven-access", because, "api_access_check", snippet, names)]
distinct_pkgs(unproven).flat_map_List(per_pkg)
# --- Conformance derivation ------------------------------------------------
# The engine knows the handler, the table, and the input from the typed
# IR; a first-cut model filled from those facts is a far better starting
# point than a blank Conformance — this is what lets a non-expert get a
# model at all. The draft models ROW COUNT: sound for a handler that
# appends one row per call, and immediately reported as a located
# divergence (with the exact input) by api_conformance_check for a
# handler that updates or deletes — the user edits the step, never the
# code to match a wrong model.
def table_conformances(t: TableFact) -> List[String]:
TableFact(_, _, _, _, _, _, _, confs) = t
confs
def find_binding(bindings: List[BindingFact], target: String) -> Option[BindingFact]:
iter_value(iter_foldl_List(bindings, None, (_, b) -> (
BindingFact(bname, _, _, _, _, _, _, _, _, _, _, _, _) = b
match eq_String(bname, target):
case True: iter_done(Some(b))
case False: iter_continue(None)
)))
def is_world_param(type_name: String) -> Bool:
match eq_String(type_name, "Yichus/Data::Db"):
case True: True
case False: eq_String(type_name, "Yichus/Access::Principal")
def table_writers(t: TableFact) -> List[String]:
TableFact(_, _, _, _, writers, _, _, _) = t
writers
def add_distinct(acc: List[String], x: String) -> List[String]:
match contains_String(acc, x):
case True: acc
case False: [x, *acc]
# The handler's one modelable input: its parameters minus the world the
# runtime injects (Db, Principal). Exactly one, in the same package's
# vocabulary — anything else is out of conformance v1's shape and the
# rule stays silent rather than proposing a draft that cannot compile.
def conformable_input(b: BindingFact) -> Option[ParamFact]:
BindingFact(_, _, params, _, _, _, _, _, _, _, _, _, _) = b
match params.filter_List(p -> (
ParamFact(_, tname, _, _) = p
match is_world_param(tname):
case True: False
case False: True
)):
case [one]:
ParamFact(_, tname, _, _) = one
match is_qualified_type(tname):
case True: None
case False: Some(one)
case _: None
struct ConformanceDraftee(handler_name: String, input_type: String, needs_type_import: Bool)
def draftee_of(bindings: List[BindingFact], confs: List[String], w: String) -> List[ConformanceDraftee]:
match contains_String(confs, w):
case True: []
case False:
match find_binding(bindings, w):
case None: []
case Some(b):
# The draft imports the handler: an unexported one would not compile.
BindingFact(_, _, _, _, _, _, _, _, _, _, type_imports, _, importable) = b
match (importable, conformable_input(b)):
case (True, Some(ParamFact(_, tname, _, _))):
[ConformanceDraftee(w, tname, contains_String(type_imports, tname))]
case _: []
def draft_member(t_name: String, d: ConformanceDraftee) -> String:
ConformanceDraftee(w, input_type, _) = d
concat_String([
"def ", w, "_show_input(_: ", input_type, ") -> String:\n",
" \"<input>\"\n",
"\n",
w, "_model = Conformance(\n",
" \"", w, " row count\",\n",
" \"", t_name, "\",\n",
" [],\n",
" 0,\n",
" int_to_String,\n",
" ", w, "_show_input,\n",
" count_rows,\n",
" eq_Int,\n",
" handler(\"", w, "\", ", w, "),\n",
" (n, _) -> add(n, 1)\n",
")\n"
])
def rule_unmodeled_conformance(facts: ProgramFacts) -> List[Suggestion]:
ProgramFacts(bindings, tables, _) = facts
def per_pkg(pkg: String) -> List[Suggestion]:
in_pkg = tables.filter_List(t -> eq_String(table_pkg(t), pkg))
draftees = in_pkg.flat_map_List(t -> (
confs = table_conformances(t)
table_writers(t).flat_map_List(w -> draftee_of(bindings, confs, w).map_List(d -> (t, d)))
))
match draftees:
case []: []
case _:
names = draftees.map_List(pair -> (
(_, d) = pair
ConformanceDraftee(w, _, _) = d
w
))
listed = join_String(", ", names.map_List(n -> concat_String(["`", n, "`"])))
needs_pkg = draftees.exists_List(pair -> (
(_, d) = pair
ConformanceDraftee(_, _, needs) = d
needs
))
type_import_names = reverse(draftees.flat_map_List(pair -> (
(_, d) = pair
ConformanceDraftee(_, tname, needs) = d
match needs:
case True: [tname]
case False: []
)).foldl_List([], add_distinct))
import_extra = type_import_names.foldl_List("", (acc, t) ->
concat_String([acc, ", ", t])
)
exposes_line = match needs_pkg:
case True: concat_String(["exposes (", pkg, ", Yichus/Spec)\n"])
case False: "exposes (Yichus/Spec)\n"
members = draftees.map_List(pair -> (
(t, d) = pair
draft_member(table_name(t), d)
))
because = concat_String([
listed,
" write tables no Conformance binds to a model: the checker cannot say whether the code matches any model of its effect"
])
snippet = concat_String([
"package ", pkg, "/Conformance\n",
"\n",
"from ", pkg, " import (", join_String(", ", names), import_extra, ")\n",
"from Yichus/Service import handler\n",
"from Yichus/Spec import Conformance\n",
"\n",
"export (", join_String(", ", names.map_List(n -> concat_String([n, "_model"]))), ")\n",
"\n",
exposes_line,
"\n",
"# Suggested by the unmodeled-conformance rule. First-cut model: ROW\n",
"# COUNT — init 0 over an empty seed, each call appends one row. For a\n",
"# handler that updates or deletes instead, api_conformance_check\n",
"# reports the divergence with the exact input; edit that model's step\n",
"# (the last argument) to the intended effect — never the code to\n",
"# match a wrong model. Replace each show_input hole with a real\n",
"# rendering so counterexamples read in your domain's terms.\n",
"\n",
"def count_rows[a](rows: List[a]) -> Int:\n",
" rows.foldl_List(0, (n, _) -> add(n, 1))\n",
"\n",
join_String("\n", members)
])
[Suggestion("unmodeled-conformance", because, "api_conformance_check", snippet, names)]
distinct_pkgs(tables).flat_map_List(per_pkg)
# --- Round trip: a value's own field fed back -------------------------
#
# A pure binding that takes a value and a String (or lists of each), where
# the value's struct carries String fields and the binding (directly or
# through any binding it calls) reads one of them, is a reader or checker
# of text the program also writes: an answer checker given a question and
# an answer, a parser given a record and its rendering. Other field types
# (an order and a quantity) are ordinary arguments, not a round trip.
# Feeding each value its own field back should be accepted: the inverse
# law between whatever produced the field and the binding that reads it.
# The rule matches types only: which field is "its own" and what
# "accepted" means are named holes.
struct OwnFields(read: List[String], unread: List[String])
# own: the field the snippet fills own_hole with (one the checker reads);
# others: the struct's remaining String fields, named in the snippet.
struct RoundTrip(value: StructFact, own: String, others: List[String], lists: Bool)
def struct_ref(st: StructFact, from_pkg: String) -> String:
StructFact(sname, spkg, _, _) = st
sname if eq_String(spkg, from_pkg) else concat_String([spkg, "::", sname])
# The struct's String fields, split by whether the binding reads them
# (a field's readers include every caller of a reader). The fields it
# extracts itself come first: a checker reads the field it checks against
# (an answer checker reads answer_text, not prompt), even when a helper it
# calls reads another.
def own_fields(st: StructFact, b: BindingFact) -> OwnFields:
StructFact(_, _, fields, _) = st
BindingFact(bname, pkg, _, _, _, _, _, _, _, _, _, _, _) = b
me = concat_String([pkg, "::", bname])
texts = fields.flat_map_List(f -> (
StructField(fname, fkind, readers, direct) = f
[(fname, contains_String(direct, me), contains_String(readers, me))] if eq_String(fkind, "String") else []
))
mine = texts.flat_map_List(t -> (
(fname, by_me, _) = t
[fname] if by_me else []
))
through_calls = texts.flat_map_List(t -> (
(fname, by_me, is_read) = t
match (by_me, is_read):
case (False, True): [fname]
case _: []
))
OwnFields(
[*mine, *through_calls],
texts.flat_map_List(t -> (
(fname, _, is_read) = t
[] if is_read else [fname]
))
)
# (value type, lists) when the parameters are a value and a String, or a
# List of values and a List[String].
def value_and_text(params: List[ParamFact]) -> Option[(String, Bool)]:
match params:
case [ParamFact(_, _, True, value_type), ParamFact(_, _, True, "String")]: Some((value_type, True))
case [ParamFact(_, value_type, False, _), ParamFact(_, "String", False, _)]: Some((value_type, False))
case _: None
# The snippet names the result type as rendered, so a result type from
# another package keeps the rule silent rather than proposing a file that
# cannot compile.
def round_trip_of(structs: List[StructFact], b: BindingFact) -> Option[RoundTrip]:
BindingFact(_, pkg, params, result_type, is_pure, _, _, _, _, _, _, declared, importable) = b
match (is_pure, importable, is_qualified_type(result_type), declared, value_and_text(params)):
case (True, True, False, [], Some((value_type, lists))):
value_struct = structs.filter_List(st -> (
StructFact(_, _, _, st_importable) = st
eq_String(struct_ref(st, pkg), value_type) if st_importable else False
))
match value_struct:
case [st, *_]:
match own_fields(st, b):
case OwnFields([own, *more], unread): Some(RoundTrip(st, own, [*more, *unread], lists))
case _: None
case []: None
case _: None
def field_pattern(fields: List[StructField], own: String, bind: String) -> String:
join_String(", ", fields.map_List(f -> (
StructField(fname, _, _, _) = f
bind if eq_String(fname, own) else "_"
)))
def rule_round_trip(facts: ProgramFacts) -> List[Suggestion]:
ProgramFacts(bindings, _, structs) = facts
def suggest(b: BindingFact) -> List[Suggestion]:
match round_trip_of(structs, b):
case None: []
case Some(RoundTrip(st, first_own, rest, lists)):
BindingFact(bname, pkg, _, result_type, _, _, _, _, _, _, type_imports, _, _) = b
StructFact(sname, spkg, fields, _) = st
own_type = "String"
same_pkg = eq_String(spkg, pkg)
struct_import = "" if same_pkg else concat_String(["from ", spkg, " import (", sname, ")\n"])
call = concat_String([bname, "([x], [own_hole(x)])"]) if lists else concat_String([bname, "(x, own_hole(x))"])
others = match rest:
case []: ""
case _: concat_String(["# (the other ", own_type, " fields of ", sname, ": ", join_String(", ", rest), ")\n"])
because = concat_String([
"`", bname, "` takes a ", sname, " and a ", own_type, ", and a ", sname,
" carries ", own_type, " fields of its own (", join_String(", ", [first_own, *rest]),
"): feeding a value its own field back is a round trip worth pinning"
])
snippet = concat_String([
"package ", pkg, "/Laws\n",
"\n",
"from Yichus/Law import (Domain, Obligation, WitnessTodo, inverse)\n",
import_clause(pkg, bname, type_imports),
struct_import,
"\n",
"export (", bname, "_round_trip)\n",
"\n",
"exposes (", spkg, ", Yichus/Law)\n",
"\n",
"# Suggested by the round-trip rule. Two named holes:\n",
"# own_hole — the field that is the value's own ", own_type, "; filled\n",
"# with one `", bname, "` or a binding it calls reads\n",
others,
"# accepted_hole — whether the result counts as accepted; it returns\n",
"# True so the stub can never report a false violation, and the\n",
"# WitnessTodo blocks any pass until it is filled.\n",
"# The Domain's gen is a third hole: the type-driven default builds\n",
"# arbitrary ", sname, " values, not ones the program produces. Replace\n",
"# the first None in the Domain with Some(seed -> ...) built by the\n",
"# program's own constructor of ", sname, " values.\n",
"def own_hole(x: ", sname, ") -> ", own_type, ":\n",
" ", sname, "(", field_pattern(fields, first_own, "own"), ") = x\n",
" own\n",
"\n",
"def accepted_hole(result: ", result_type, ") -> Bool:\n",
" _ = result\n",
" True\n",
"\n",
"def fed_back(x: ", sname, ") -> Bool:\n",
" accepted_hole(", call, ")\n",
"\n",
"def accepted(_: ", sname, ") -> Bool:\n",
" True\n",
"\n",
"def describe_hole(_: ", sname, ") -> String:\n",
" \"", sname, "\"\n",
"\n",
bname, "_values = Domain(\"", sname, " values\", describe_hole, None, None)\n",
"\n",
bname, "_round_trip = Obligation(\n",
" inverse(\"", bname, " accepts each ", sname, "'s own ", first_own, "\", ", bname, "_values, accepted, fed_back, eq_Bool),\n",
" [WitnessTodo(\"the value is one the program produces\", \"fill own_hole and accepted_hole, give the Domain a gen built by the program's own constructor, then turn this into a Witness that some generated value is accepted\")]\n",
")\n"
])
[Suggestion("round-trip", because, "laws.inverse", snippet, [bname])]
bindings.flat_map_List(suggest)
default_rules = RuleSet("yichus-default", [
Rule("numeric-floor", rule_numeric_floor),
Rule("numeric-ceiling", rule_numeric_ceiling),
Rule("fold-ordering", rule_fold_ordering),
Rule("round-trip", rule_round_trip),
Rule("unbounded-numeric", rule_unbounded_numeric),
Rule("undeclared-access", rule_undeclared_access),
Rule("unproven-access", rule_unproven_access),
Rule("unmodeled-conformance", rule_unmodeled_conformance),
])