Skip to content

README.md

Latest commit

 

History

History
272 lines (209 loc) · 9.51 KB

README.md

File metadata and controls

272 lines (209 loc) · 9.51 KB

Sponsor

// SPDX-License-Identifier: MPL-2.0 // Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) j.d.a.jewell@open.ac.uk = Alloyiser Jonathan D.A. Jewell j.d.a.jewell@open.ac.uk :toc: left :icons: font :source-highlighter: rouge

== What Is Alloyiser?

Alloyiser takes API specifications (OpenAPI 3.x, GraphQL schemas, gRPC .proto files) and extracts their entity relationships into Alloy 6 formal models — then runs the https://alloytools.org[Alloy Analyzer] to find design bugs before any implementation code exists.

https://en.wikipedia.org/wiki/Alloy_(specification_language)[Alloy] is a lightweight formal modelling language created by Daniel Jackson at MIT. It uses relational logic and SAT solving to exhaustively search for counterexamples to declared invariants. If your API spec says "every order must have a customer" but there exists a reachable state where an orphaned order can appear, Alloy will find it and show you the concrete scenario.

Alloyiser makes this power accessible: you point it at your spec files, declare invariants in alloyiser.toml, and get a counterexample report — no Alloy expertise required.

Part of the https://github.com/hyperpolymath/iseriser[-iser family] of acceleration frameworks.

== Key Value

  • Find API design bugs before writing code — race conditions, impossible states, orphaned resources
  • Database schema verification — detect unreachable states and constraint violations
  • Protocol state machine validation — verify handshakes, transitions, and liveness properties
  • Microservice contract checking — prove that service A's expectations match service B's guarantees
  • CI/CD gate — fail a pull request if Alloy finds a counterexample in the spec

== Architecture

                       alloyiser pipeline
                       ==================

┌──────────────┐ ┌─────────────┐ ┌───────────────────┐ │ OpenAPI 3.x │ │ GraphQL │ │ gRPC .proto │ │ spec.yaml │ │ schema.gql │ │ service.proto │ └──────┬───────┘ └──────┬──────┘ └────────┬──────────┘ │ │ │ └───────────┬───────┘────────────────────┘ │ ▼ ┌───────────────────────┐ │ Spec Parser │ Rust: extract entities, fields, │ (src/core/) │ relationships, constraints └───────────┬───────────┘ │ ▼ ┌───────────────────────┐ │ Relation Extractor │ entities → Alloy signatures │ (src/bridges/) │ fields → Alloy relations └───────────┬───────────┘ constraints → Alloy facts │ ▼ ┌───────────────────────┐ │ Idris2 ABI │ Proves: model extraction │ (src/interface/abi/)│ preserves spec semantics └───────────┬───────────┘ │ ▼ ┌───────────────────────┐ │ Alloy Codegen │ Generates .als files with: │ (src/codegen/) │ sig, field, fact, pred, assert └───────────┬───────────┘ │ ▼ ┌───────────────────────┐ │ Alloy Analyzer │ SAT solving via Kodkod/SAT4J │ (alloy6.jar) │ bounded model checking └───────────┬───────────┘ │ ▼ ┌───────────────────────┐ │ Counterexample │ Human-readable violation report │ Report │ with concrete state instances └───────────────────────┘

== Alloy Concepts (Quick Reference)

Alloyiser generates these Alloy constructs from your API specs:

[cols="1,2,2"] |=== | Alloy Construct | What It Means | Extracted From

| sig (Signature) | An entity type — like a class or table | OpenAPI schema objects, GraphQL types, protobuf messages

| field | A relation between signatures | Object properties, field types, foreign keys

| fact | An invariant that must always hold | Required fields, uniqueness constraints, enum restrictions

| pred (Predicate) | A reusable named constraint | API operation pre/post conditions

| assert (Assertion) | A property to verify | User-declared invariants in alloyiser.toml

| check | Run SAT solver to find counterexamples to an assertion | Automatic: one check per assertion

| run | Generate a satisfying instance | Automatic: used to visualise valid states |===

== How It Works

=== 1. Create a manifest

[source,toml]

alloyiser.toml — point at your spec, declare what to verify

[workload] name = "pet-store-api" entry = "specs/petstore.yaml" strategy = "openapi"

[data] input-type = "OpenAPI3" output-type = "AlloyModel"

[invariants]

Declare properties your API should satisfy:

no-orphaned-pets = "all p: Pet | some p.owner" unique-pet-ids = "all disj p1, p2: Pet | p1.id != p2.id" valid-status = "all p: Pet | p.status in Available + Pending + Sold"

[options] scope = 5 # Check up to 5 instances of each entity alloy-jar = "lib/alloy6.jar" output-dir = "generated/alloy"

=== 2. Generate and check

[source,bash]

Initialise a new manifest in the current directory

alloyiser init

Validate the manifest

alloyiser validate -m alloyiser.toml

Generate Alloy models from the spec

alloyiser generate -m alloyiser.toml -o generated/alloy

Run the Alloy Analyzer (finds counterexamples)

alloyiser run -m alloyiser.toml

Show manifest summary

alloyiser info -m alloyiser.toml

=== 3. Read the report

Alloyiser produces a counterexample report showing concrete states that violate your invariants. For example:

VIOLATION: no-orphaned-pets Counterexample found (scope 5): Pet$0 = { id: 1, name: "Fido", status: Available, owner: none } Explanation: The OpenAPI spec allows creating a Pet without an owner field (owner is not in the required array). This violates the invariant that every Pet must have an owner. Fix: Add "owner" to the required fields in the Pet schema.

== Use Cases

Microservice contract verification:: Two services agree on a shared schema. Alloyiser checks that the producer's guarantees satisfy the consumer's expectations — catching mismatches before integration testing.

Database schema consistency:: Extract entity-relationship constraints from your migration files or ORM definitions. Verify referential integrity, cardinality constraints, and state machine transitions.

Protocol state machine validation:: Model a multi-step protocol (OAuth flow, payment processing, order lifecycle) as an Alloy state machine. Check liveness ("the order eventually reaches a terminal state") and safety ("a refund cannot exceed the original charge").

API evolution safety:: When adding fields or endpoints, regenerate the Alloy model and re-check. Alloyiser detects regressions: "adding optional field X breaks invariant Y."

== CLI Commands

[cols="1,2"] |=== | Command | Description

| alloyiser init | Create a new alloyiser.toml manifest in the current directory

| alloyiser validate | Parse and validate the manifest (checks structure, not semantics)

| alloyiser generate | Extract entities from the spec and generate .als Alloy model files

| alloyiser build | Compile generated artifacts (Alloy model + Zig FFI bridge)

| alloyiser run | Run the Alloy Analyzer against the generated models

| alloyiser info | Display a summary of the manifest configuration |===

== Building

[source,bash]

Build

cargo build --release

Test

cargo test

Full quality check (format + lint + test)

just quality

Pre-commit scan

just assail

Requires:

  • Rust (nightly, via asdf)
  • Alloy 6 JAR for analyzer integration (Phase 3+)
  • Idris2 for ABI proofs (Phase 5+)
  • Zig for FFI bridge (Phase 5+)

== Status

Pre-alpha (scaffold phase). The CLI skeleton, manifest parser, and project structure are in place. Code generation and Alloy Analyzer integration are pending — see link:ROADMAP.adoc[ROADMAP] for the implementation plan.

What exists today:

  • Rust CLI with init, validate, generate, build, run, info subcommands
  • TOML manifest parser and validator
  • Codegen stub (ready for Alloy .als generation)
  • Idris2 ABI type definitions (template — being specialised for Alloy model types)
  • Full RSR infrastructure: 17 CI/CD workflows, Containerfile, Justfile, governance docs

== License

SPDX-License-Identifier: MPL-2.0