Repository navigation
Pre proved auth - #762
Merged
Merged
Pre proved auth#762
Conversation
An app runs its kernel behind h5i_app_std::authz::guard (or guard_viewed) with a policy written in Rust, lists the function under [authz] in h5i-app.toml, and gets an authorization theorem with no hand-written Lean. - h5i-app-std: the guard, Transition/Policy/Disclose/View traits, and AuthzSpecs.lean, proven once for every kernel: committed writes are permitted (each in the state the earlier ones leave), disclosed rows are visible, read-only commands under guard_viewed are noninterfering with what the view hides, and ReadOnly.Sound follows. h5i_authz instantiates it for an app. - h5i app: extract copies AuthzSpecs and writes generated/Authz.lean; check gates <fn>.authorized; lint checks Kernel::transition runs the guarded function; the check record carries the coverage line. - examples/app/forum: Nyxis's bulletin board ported with no hand-written Lean, with buggy-handler denial tests and a PostgreSQL agreement test. - Docs: docs/app/AUTHZ.md, docs/design/design-authz.md, TRUST, NUMBERS, ROADMAP (A11), MANUAL. Apps without [authz] are unchanged; existing extractions are identical.
Review fixes for framework-proven authorization. - Policy gains a required `stored(s, d)`: a disclosed row counts only if it is in the state, exactly as disclosed, and visible there. Before, `visible` judged the reply's copy, so a handler could relabel a hidden draft as published and have it accepted. The theorems now state `Shown` (stored and visible) for every disclosed row. - `h5i_authz` proves `<fn>.kernel_apply_eq`, that the Transition instance's `kernel_apply` is the kernel's own `apply`, and refuses to generate anything otherwise; `h5i app check` requires it. - Lint matches whole identifiers, also requires the server's `Kernel::apply` to call the kernel's `apply`, and accepts the generated read-only proof only for guard_viewed kernels. - Forum: `stored` compares with the row under its key; new posts take the counter's next id and the counter moves only by one; a forged-row handler bug is now among the denied ones. Docs and numbers updated, including the quadratic cost of `stored` on long listings.
Fixes from an independent review of framework-proven authorization. - extract: Authz.lean gains a generated storage section (A4 for the app, no hand-written model): sql_fits, apply_write_enc, apply_enc and pg_stored prove the store commits what the kernel's apply computes. Table writes are read off the extracted sql_write with the regex crate; a misreading fails the build. The same text checks for board and booking. Before, the forum had no storage proof while the docs said writes were checked in the states the store commits. - check: builds the Authz module itself, so a stale Authz.olean cannot pass the gate; requires the storage theorems when generated; records the coverage line only after the gate passes; a comment no longer counts as a ReadOnly.Sound proof. - lint: every impl Kernel in crates' src/ (tests excluded) must be wired, so a wired decoy cannot cover an unwired impl; the generated read-only proof counts only if Kernel::read_only delegates. - h5i_authz: rejects a guarded function that alters its arguments (it ran Lean out of memory) and checks kernel_apply before adding anything. - web: required theorems include the storage theorems and read_only_sound. - Docs: AUTHZ, TRUST, ROADMAP, MANUAL, design doc, NUMBERS, forum README.
docs/MANUAL.md gained the [authz] section; PAGE_HISTORY records the new content hash and date, and the manual and sitemap are rebuilt (markdown 3.9, as pinned).
Fixes from a fourth independent review of framework-proven authorization. - lint reads the Rust with syn (new crates/h5i-app-cli/src/rust.rs): each crate's module tree from lib.rs, main.rs and src/bin, #[cfg(test)] items left out, any spelling or rename of the trait path, calls found in the syntax tree, unparsable files an error. The text scan cut each file at its first #[cfg(test)], so a test module above the real impl hid it (a bypass with [authz], and an unproven read_only passing without it). - With [authz], every impl Store must write with schema_store and load with schema_load (no hand-written ones) and keep the default load_for: a partial load would have the policy judge a partial state. - extract fails when it cannot generate the storage proof, unless `[authz] storage` names a hand-written theorem, which check requires; the coverage line shows which. - check records the theorems it required; the web view shows that list instead of recomputing it. A missing Authz target fails with a hint. - Docs: what pg_stored proves versus what lint checks, load_for, the storage option, the open schema hypotheses. Manual hash updated.
Five reviews kept finding ways past the syntactic lint that tied a hand-written server Kernel/Store to the proofs. Move the wiring out of the app instead: - h5i_app_core::Authz<T>: the one Kernel impl for Authz<_> (coherence); its transition is guard_viewed of T's instances, called by framework code, so what the engine runs is guarded whatever the handlers do. - h5i_app_std::authz_kernel!: writes guarded_transition (what Authz.lean proves) and impl AuthzKernel (the types Authz<T> uses; only the kernel crate may write it) from one list of types, so the two match by construction, plus `App`. - The schema mapping macro's `store` form generates the Store (default full-tenant load_for); it is its own Table tag. - Forum's server now writes no Kernel or Store. The only fact outside the proofs is that the engine is built from App and the generated store. - lint under [authz] only flags hand-written Kernel/Store/AuthzKernel impls (hygiene); rust.rs follows [lib]/[[bin]] paths, #[path], cfg'd modules, cfg(all(test, ...)) and rename chains as rustc does. - check requires read_only_sound, records required theorems before building, and restricts [authz] storage to a theorem in the kernel's namespace, printing it; extract writes Schema.lean before Authz.lean. - web lists the latest check's required theorems. Tried from the server: a second Kernel impl for App, an AuthzKernel impl and a policy swap are all rejected by the compiler (E0117).
Fixes from a sixth independent review. - The schema mapping macro named the kernel by relative paths ($krate::decode, $krate::sql_writes, ...). The macro expands in the server, so a server module named like the kernel could stand in for them under the generated Store. Every kernel path is now absolute (::$krate::...), with a test that fails on a relative one. - lint under [authz] requires the kernel to invoke authz_kernel! exactly once: a hand-written guarded_transition next to an App over another type would have the theorems about one instantiation and the engine running another. Documented as trusted kernel wiring, next to the server's engine line. - Docs and comments no longer suggest plain `guard` works under [authz] (Authz<T> runs guard_viewed; check requires read_only_sound). - examples/app/README.md: the forum is one row of the tutorial table.
Fixes from a seventh independent review. - `[authz] guarded` accepts only ["guarded_transition"], the function authz_kernel! writes: naming another function let the proofs be about a stricter policy while App ran the kernel's own. - New deps check (lint and check): every h5i_app_* dependency of the project's crates must be the package of that name and come from where h5i-app-core comes from, read from `cargo metadata`. A `package =` rename or a look-alike crate could supply an Authz<T> that skips the guard, with the Rust and the extracted Lean unchanged. - lint counts only `h5i_app_std::authz_kernel!` by that path. - The schema store form fails to compile without `writes` and a snapshot (its schema_store/schema_load would resolve to server functions), and extract refuses to generate a storage proof Schema.lean cannot support. - Docs agree on what stays trusted; dead code from the lint-based design removed.
From a final review scoped to honest but mistaken apps. - docs/app/AUTHZ.md opens with who the guarantee is for (the reader of the policy, not a check on the author) and the reviewed surface. The claim is narrowed: the code behind the guard may be wrong, as long as the server acts only through H5iApp with each request's Actor. The surface now includes how a request becomes a principal (the Authenticator / principal function, or_anonymous, assume_authenticated), ReplyCodec::scope, Write with apply_write, and Engine::migrate. A8 is stated as that condition; replays with a coarse scope and the missing stamp are listed. - lint under [authz] fails on .engine(), .snapshot() and .snapshot_for() outside tests (a route acting as another user, an unguarded export), and lists assume_authenticated, or_anonymous and .migrate() as reviewed-surface locations. - TRUST.md, ROADMAP A11, the design doc, the forum README and the h5i-app-http comment match. An engine handle that accepts only an authenticated Actor is left for a separate change.
…] check `extern crate <other> as h5i_app_core;` bound a framework name to another crate with Cargo's resolution unchanged, so the package check passed while `authz_kernel!` reached a stand-in `Authz<T>`. The framework check now rejects such aliases (including `self as …`) in every project crate. `check` gated theorem names and axioms, not statements, so a hand-edited generated Authz.lean, AuthzSpecs.lean or extracted kernel passed. For an [authz] project it now re-extracts and compares first; `prove` and xtask verify skip that when extraction was just done or checked.
… at the root A server with its own [workspace] resolved its own h5i_app_* dependencies, which the kernel's cargo metadata never showed. The framework check now reads the resolution of every crate under the project, and fails if one cannot be read. From inside a module, authz_kernel!'s App runs that module's guard while a hand-written guarded_transition at the crate root is the one proven. Lint now requires the macro at the top level of the crate root, not under cfg.
…t state docs/app's reference pages and docs/design's design notes covered the same ground in two places, and both had grown into long histories. Each part now has one file in docs/design that says how it works now, what it guarantees and its limits; histories, alternatives and superseded measurements stay in git. The set goes from about 67k words to 25k. docs/app/* become design-app*.md, design-authz.md merges into design-app-authz.md, and design-h5i-ir.md (code removed with the old engine) is dropped. Rewriting against the code fixed stale claims: the websec and browser docs described the removed engine, the console doc contradicted itself on message rendering, and match's exit codes and diff's flags were wrong. References across code, READMEs, skills, the site and llms.txt follow the new names; the manual is regenerated.
The engine moved to github.com/h5i-dev/h5i-browser on 2026-10-19; the docs said it was removed.
# Conflicts: # docs/build-content.py # docs/sitemap.xml
An [authz] project's check now re-extracts it to confirm proofs/generated/ is fresh, and the lean job had only Lean, so examples/app/forum failed. Install the pinned tools there as the extract job does, building xtask before Nix puts Charon's toolchain on PATH.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
No description provided.