dataflow-policy

dataflow-policy checks a Prism dataflow project script against its declared memory and PII-encryption policies, and emits the project's canonical form. It is a Prism application: its behavior is authored once in LexLean (src/*.lex.tex) and PrismPM generates the verified browser application (GitHub Pages) and the command-line interface from that single model. No application behavior is written by hand outside the model.

Status

Development, version 0.1.0. The authoritative model is committed; the SDK binding, generated artifacts, CLI, and Pages deployment are not yet in place. The work is tracked in the dataflow-policy GitHub project and its milestones.

The model is LexLean language 1.2 notation, built with LexLean v0.4 and locked in lexlean.lock (lexlean/lock/2). Its product identifiers (dataflow-policy, the dataflow-policy/1 script header, and the repository and Pages URLs) are bound by the application model digest in System, which prismpm check reports and the model carries. The Lean project name and namespace (PrismCode in lexlean.toml, lakefile.toml and lake-manifest.json), the prism.arch label-word entries and the module titles bound to them ("Prism-code system model" and the like) are pinned by lexlean.lock and change only through a lexlean lock run. They are internal and are not product identifiers: prism-code names only the npm SDK package.

What it does

A request is UTF-8 text of at most 4096 bytes. The first line is the header dataflow-policy/1; each further non-empty line is one statement:

Statement	Meaning
node NAME KIND MEMORY	a node of kind input, operator, encrypt, or output with a memory requirement in bytes
edge SOURCE TARGET	a dataflow edge between two declared nodes
pii NAME	marks an input node as carrying personal data
policy memory LIMIT	no node may require more than LIMIT bytes
policy encrypt-pii	personal data must pass through an encrypt node before any output

The response is one of:

• status accepted followed by the canonical, sorted project;
• status rejected followed by every policy finding (finding memory ..., finding plaintext-pii ...) and the canonical project; or
• status error with the first failing line and its typed code (missing-header, unknown-command, wrong-arity, empty-field, unknown-kind, invalid-number, duplicate-node, unknown-node, self-edge, duplicate-edge, output-source, input-target, not-an-input, duplicate-pii, duplicate-policy, line-overflow) or request code (empty, too-large, invalid-utf8, too-many-lines), or response too-large when the report would exceed 16384 bytes.

The model proves, among other things, that a run is accepted only if the project is compliant (Engine.completedRunAcceptedOnlyIfCompliant) and that a failed run is never accepted (Engine.failedRunNeverAccepted).

Command line

The command-line interface is declared in the model, not written by hand. The application record in Specification uses the prismpm/text-application/3 profile (Foundation.View.Text.V3.Model), whose cli field holds the command, description, help sections, named examples and exit-code map. PrismPM generates the program from that record:

dataflow-policy check [FILE]    read the script from FILE, or from stdin when FILE
                           is omitted or `-`; print the report unchanged
dataflow-policy examples [NAME] list the examples, or print one example script
dataflow-policy --help
dataflow-policy --version       dataflow-policy 0.1.0, from cargoName and cargoVersion

A request over 4096 bytes is refused before dispatch (InputLimit, empty standard output). Exit codes come from the model: status accepted 0, status rejected 1, status error 2, usage error 64, input or output error 74.

--help prints the purpose, the statement reference (STATEMENTS), the report format (REPORT), the status texts (STATUS), the recovery text for every error and finding code (ERROR AND FINDING CODES), the example names and the exit-code table. The statement, status and code text is the text the page's workbench states in Workbench; CL-08 fails if the two differ. Two examples check as the page's example buttons do:

dataflow-policy examples accepted | dataflow-policy check
dataflow-policy examples rejected | dataflow-policy check; echo $?

Every failure of the command line is a typed diagnostic on standard error, dataflow-policy: <Failure>[: <detail>], with the exit code of its class. The vocabulary is the SDK's closed TextCliFailure set (PrismPM model/text-cli-diagnostics.toml); this repository registers a test for each failure a user can cause:

Failure	Cause	Exit	ID
UnknownFlag	an argument starting with - that is not --help, --version, - or --	64	CL-09
ExtraArgument	a second operand	64	CL-10
MissingCommand	no command	64	CL-11
UnknownCommand	a command other than check and examples	64	CL-12
UnknownExample	an example name the model does not declare	64	CL-13
InputMissing	the path does not exist	74	CL-14
InputOpen	the path cannot be opened	74	CL-15
InputType	the path is a directory or a symbolic link	74	CL-16
InputRead	reading failed after the request was opened	74	CL-17
OutputWrite	standard output is closed or full	74	CL-18
InputLimit	the request exceeds 4096 bytes	2	CL-03

The tests are crates/conformance/tests/cli/ (CL-01 to CL-18, scenarios in features/suites/cli.feature). They drive the program that prismpm build publishes at .prism/build/<id>/cli/bin/<host target>/dataflow-policy, or the program named by DATAFLOW_POLICY_CLI, and take every expectation from the model sources. They fail, rather than skip, when no program has been built.

Repository layout

Path	Owner
src/	authoritative LexLean model modules (System.lex.tex is the entrypoint)
language/prism.arch/	the architecture lexicon the model's glossary uses
lexlean.toml, lexlean.lock	LexLean project and its locked package closure
prismpm.toml	PrismPM project; generated output goes to .prism/
lakefile.toml, lean-toolchain, lake-manifest.json	Lean workspace bound by lexlean.lock
model/, features/suites/, CONFORMANCE.md	the repository's claim register (template contract)
crates/, xtask/, bootstrap/	repository gates inherited from the UOR template

Module	Content
Core	nodes, edges, policies, violations, canonical form
Interaction	script statements, parsing, admission of each statement
Compliance	memory and PII-propagation findings
Engine	line runner, certification, outcome rendering
Specification	request dispatch and the text application with its acceptance vectors
Workbench	proofs over the page guidance: statement forms, examples drawn from the acceptance vectors, status texts and recovery text for every error and finding code
Guide	the Text V3 workbench the page renders: purpose, statement reference, examples with expected reports, recovery for every code, status texts
Frame	the workbench frames: ui-check and ui-raw requests answered as closed JSON results around the unchanged text report
Foundation.View.Text.V1.Model	the text view contract
Production.Core, Production.BrowserSystem	system model types and manifest validation
System	the dataflow-policy system model and its GitHub Pages target
Architecture	the ISO/IEC/IEEE 42010 architecture description, checked against System
Design	the OPM (ISO/PAS 19450) process model and the UML component, sequence and state machine views of the architecture, each element checked against the architecture and system models
Foundation.Arch	the architecture and design-view vocabulary (copy of the PrismPM stdlib module at PrismPM#234)

Open in a codespace

The badge opens a codespace on the digest-pinned SDK image with Docker, Lean and Rust ready; nothing is installed on your machine. Its configuration is .devcontainer/codespaces/devcontainer.json, separate from the local .devcontainer/devcontainer.json, which is template policy bound by template.lock and stays as it is. The codespace shares the host's Docker daemon, so npx prism-code@0.2.0 check and build start the SDK image the codespace is already running on (no second download; measured with the devcontainer CLI on a CI runner). Not usable yet: the SDK image (14.8 GB on disk) does not fit the 32 GB disk of the machine types offered to this repository, so a codespace currently fails to start with no space left on device. To just try a verified Prism application with no SDK image, use the template's try page.

Toolchain

dataflow-policy is built with LexLean and the PrismPM SDK, used only through the digest-pinned SDK image in prismpm.lock. That lock and template.lock are written when the repository binds a public PrismPM SDK release; until then just vv and the bootstrap workflow cannot pass. See TEMPLATE-CONTRACT.md, AGENTS.md, and VERIFICATION.md.

Licensed under MIT or Apache-2.0.