The README makes claims. This file backs them up with code paths, caveats, and honest gaps.
Provides typed, contract-validated configuration that enforces language policy, security policy, and infrastructure standards at build time.
How it works: augmented/lib/rsr.ncl defines Nickel contracts that are evaluated at nickel
export time — which runs during just build and just test. The AllowedLanguage contract
uses std.contract.from_predicate to check that a declared language string appears in the
hardcoded RSR allowlist (rescript, rust, gleam, elixir, deno, bash, javascript, nickel, guile,
julia, ocaml, haskell, ada, idris2, zig, v). Any value outside this list causes Nickel to fail
with a contract violation at build time, before the configuration is ever deployed.
augmented/lib/security.ncl adds analogous contracts for SPDX identifiers, HTTPS-only URL
enforcement, and no-MD5/no-SHA1 checks. The prelude (augmented/lib/prelude.ncl) re-exports all
modules so a consumer writes let aug = import "./lib/prelude.ncl" in { lang | aug.rsr.AllowedLanguage }.
Honest caveat: Nickel contracts run at nickel export time. They do NOT run at Elixir/Rust
compilation time, and they do NOT block git commit unless the project’s Justfile or CI workflow
explicitly runs nickel export as a gate. A project that never calls just build can silently
bypass all contracts.
The
augmented/lib/proven-bridge.nclmodule connects nickel-augmentation to the proven formally verified safety library. It re-exports key contracts that are backed by Idris2 dependent-type proofs via Zig FFI.
How it works: augmented/lib/proven-bridge.ncl attempts to import contract definitions from
the proven sibling repository. The has_proven field reports true or false depending on
whether the sibling path resolves. When it resolves, contracts such as SafePath, SafeEmail,
SafeUrl, SafeCrypto, SafeVersion, SafeString, and SafeMath carry Idris2-proven
correctness guarantees: their predicates are derived from formally verified Zig FFI functions
rather than ad-hoc string matching. When the bridge is unavailable, has_proven is false and
callers should fall back to the unverified contracts in augmented/lib/security.ncl.
Honest caveat: The proven bridge is a conditional integration. Its strength depends on the
proven repo being co-located and at the expected path. The Idris2 proofs and Zig FFI layer live
in proven, not here; this repo only imports them. If proven is not present, the bridge
degrades silently (no error, just has_proven = false).
| Repo | How nickel-augmentation is used | Status |
|---|---|---|
|
|
Active |
|
Nickel config files validated against rsr.ncl and security.ncl contracts |
Active |
|
RSR metadata config validated via augmented contracts in CI |
Active |
|
Project metadata Nickel config uses prelude contracts |
Active |
|
nickel-augmentation is the canonical source of RSR Nickel contracts for the ecosystem |
Active |
|
Hypatia’s neurosymbolic rules reference nickel-augmentation’s contract structure for validation |
Active |
|
|
Active |
| Path | What’s There |
|---|---|
|
Top-level re-export: |
|
RSR core contracts: |
|
Security contracts: SPDX identifier validation, HTTPS-only URLs, hash algorithm policy (no MD5/SHA1) |
|
CI/CD contracts: workflow presence validation, SHA-pinned action checks, permissions contracts |
|
Infrastructure contracts: container base image policy (Chainguard), Podman/not-Docker checks |
|
Bridge to |
|
Fallback proven contracts (used when |
|
Usage examples: annotated Nickel configs demonstrating each contract module |
|
Per-module documentation and the "augmentation boundary" specification |
|
Rust CLI source: walks |
|
Compiled |
|
K9 contractile templates (Kennel/Yard/Hunt) and must/trust/dust/lust policy files |
|
Typecheck + export validation tests run by |
|
Recipes: |
|
Architecture map: library, reporter, contractiles relationship and completion dashboard |
|
RSR-standard CI: CodeQL, Hypatia, Scorecard, quality, mirror workflows |
Open an issue or reach out to Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>.