From 3cb8024a09f1156dcd9dd3ecfff5e12b55e249f7 Mon Sep 17 00:00:00 2001 From: Claude Date: Thu, 18 Jun 2026 12:43:21 +0000 Subject: [PATCH] docs: de-dup README/CHANGELOG per RSR standard (keep .adoc; port sponsor badge) Brings this repo in line with the family-wide doc de-dup that landed across the -iser repos during base camp but was missed here (this repo was squash-merged before the cleanup). - Remove stale README.md (README.adoc is canonical), porting the GitHub sponsor badge into README.adoc. - Remove duplicate CHANGELOG.md (CHANGELOG.adoc is canonical). Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_01Mbq6yKF9RhFai6EQ7WqKhQ --- CHANGELOG.md | 18 ---- README.adoc | 2 + README.md | 272 --------------------------------------------------- 3 files changed, 2 insertions(+), 290 deletions(-) delete mode 100644 CHANGELOG.md delete mode 100644 README.md diff --git a/CHANGELOG.md b/CHANGELOG.md deleted file mode 100644 index 745f742..0000000 --- a/CHANGELOG.md +++ /dev/null @@ -1,18 +0,0 @@ -# Changelog - -All notable changes to alloyiser will be documented in this file. - -The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.1.0/), -and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0.html). - -## [0.1.0] - 2026-03-20 - -### Added -- Initial project scaffold from rsr-template-repo -- CLI with subcommands (init, validate, generate, build, run, info) -- Manifest parser (`alloyiser.toml`) -- Codegen engine (stubs — target-language-specific implementation pending) -- ABI module (Idris2 proof type definitions) -- Library API for programmatic use -- Full RSR template (17 CI workflows, governance docs, bot directives) -- README.adoc with architecture overview and value proposition diff --git a/README.adoc b/README.adoc index 389f3eb..a131a73 100644 --- a/README.adoc +++ b/README.adoc @@ -6,6 +6,8 @@ Jonathan D.A. Jewell :icons: font :source-highlighter: rouge +image:https://img.shields.io/badge/Sponsor-%E2%9D%A4-pink?logo=github[Sponsor,link=https://github.com/sponsors/hyperpolymath] + == What Is Alloyiser? Alloyiser takes **API specifications** (OpenAPI 3.x, GraphQL schemas, gRPC `.proto` files) diff --git a/README.md b/README.md deleted file mode 100644 index 2b57c11..0000000 --- a/README.md +++ /dev/null @@ -1,272 +0,0 @@ -[![Sponsor](https://img.shields.io/badge/Sponsor-%E2%9D%A4-pink?logo=github)](https://github.com/sponsors/hyperpolymath) - -// SPDX-License-Identifier: MPL-2.0 -// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) -= Alloyiser -Jonathan D.A. Jewell -: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