Calculator

Calculator is the first reference PrismPM application. Its arithmetic, wire protocol, Hologram packaging, and user interface are authored once in src/Calculator.lex.tex. LexLean generates Lean; PrismPM verifies the model and produces the Rust crate, Core-Wasm guest, binary Hologram archive, portable View, and GitHub Pages projection. None of those application semantics are handwritten here.

The deployed application is https://uor-foundation.github.io/calculator-example/.

Verify from a clean checkout

Open the repository in its VS Code devcontainer, then run:

just vv

That one command:

1. proves this model and lock are byte-identical to PrismPM's canonical getting-started Calculator;
2. runs prismpm check, two deterministic builds, prismpm verify, and the complete application-acceptance gate;
3. compares every committed package, Holo, browser, and evidence artifact to the regenerated bytes;
4. builds, tests, and lints this consumer against the isolated registry-format prism-calculator and prism-stdlib release candidates;
5. reproduces the whole Prism build from a second absolute root; and
6. runs the generated GUI's modeled Playwright and WCAG 2.2 A/AA acceptance suite with pinned Chromium.

Dependency acquisition is confined to devcontainer setup. Verification is locked and offline.

The devcontainer runs just setup automatically. It can be repeated explicitly when a lockfile changes; just vv itself never fetches dependencies.

Use the generated Rust API

This repository is itself a consumer of the generated crate:

use prism_calculator::{calculate, Operation};

assert_eq!(calculate(Operation::Multiply, 6, 7), Ok(42));

The checked-in Cargo.toml requires exactly prism-calculator = "=0.1.0". Until the public Cargo publication step is complete, verification resolves the byte-final candidates from registry/; it never substitutes a path or Git dependency.

Artifact map

Path	Role
src/Calculator.lex.tex	authoritative application model, mirrored byte-for-byte from PrismPM
artifacts/Calculator.holo	strict binary Hologram v4 fat application (HOLO header)
artifacts/model.prism.json	canonical generated Prism model document
artifacts/application-acceptance.json	complete PrismPM application acceptance result
registry/*.crate	byte-final registry-format package candidates
public/	exact generated GitHub Pages production closure
RELEASE-CANDIDATE.json	cross-artifact identities and publication state
SHA256SUMS	committed artifact checksums

Do not edit generated artifacts. Change the canonical Calculator model in PrismPM, regenerate there, mirror the model and lock here, and update every derived byte in one reviewed change.

Local preview

Inside the devcontainer:

just serve

Then open http://127.0.0.1:4173. The server only serves the six attested files in public/; it supplies no calculation or presentation behavior.

Licenses

Licensed under either Apache License 2.0 or MIT, at your option.