v1.2.1: protocol-squisher.net site

protocol-squisher.net Site

Five-tabbed static website for protocol-squisher.net, built with ddraig-ssg (Idris 2 dependently typed SSG):

Pages

• About — Project intro, five pillars, who it's for
• The Project — 13 analysers, architecture, formal guarantee, usage
• Technology — IR, constraints, transport classes, ECHIDNA/VeriSimDB
• Progress & Contact — Status, numbers, timeline, media/user contact
• Governance & Help — License, security, data handling, accessibility, FAQ

Features

• Tabbed navigation with active-tab CSS class highlighting
• Responsive layout (mobile + desktop + print)
• System font stack (no web font downloads)
• Build script auto-locates ddraig-ssg binary
• WCAG AA compliant contrast

ddraig-ssg Enhancements

• Multi-page site generation with build command
• SitePage type with slug and navOrder for tab ordering
• {{nav}}, {{slug}}, {{tags}}, {{body_class}} template placeholders
• File I/O via Idris 2's System.Directory.listDir
• Draft page skipping

DNS for protocol-squisher.net pending registration.

v1.2.0: SchemaAnalyzer Trait & Public Library API

What's New

Phase 4a/4b complete: protocol-squisher is now usable as a library dependency.

SchemaAnalyzer Trait (Phase 4a)

Universal trait defined in protocol-squisher-ir and implemented across all 13 analyzers:

use protocol_squisher::prelude::*;
use protocol_squisher::protobuf_analyzer::ProtobufAnalyzer;

let analyzer = ProtobufAnalyzer::new();
assert_eq!(analyzer.analyzer_name(), "protobuf");
let schema = analyzer.analyze_str(proto_source, "user")?;

Public Library API (Phase 4b)

All modules re-exported from the root crate:

• protocol_squisher::ir — Schema, Constraint, Field types, SchemaAnalyzer trait
• protocol_squisher::compat — Transport class scoring
• protocol_squisher::meta_analysis — Squishability patterns
• protocol_squisher::{avro,protobuf,thrift,...}_analyzer — All 13 analyzers
• protocol_squisher::all_analyzers() — Dynamic dispatch registry
• protocol_squisher::prelude — Convenience re-exports

Stats

• 937 tests, 0 failures (up from 921)
• 13 protocol analyzers, all implementing SchemaAnalyzer
• cargo audit: 0 vulnerabilities / 275 dependencies
• panic-attack: PASS verdict
• GitHub security: 0 alerts

Breaking Changes

None. This is a purely additive release.

v1.1.2: Roadmap + PanLL Five-Pillar Architecture

What's New

Roadmap rewrite with PanLL integration and five-pillar developer suite architecture.

Highlights

• ROADMAP.adoc completely rewritten with completed Phases 0-3 and new Phases 4-6
• Five-Pillar architecture identified: Languages, Databases, Protocols, Containers, Quality/Observability
• Phase 4 (Library Extraction): SchemaAnalyzer trait, public API, constraint evaluation, HTTP server
• Phase 5 (PanLL ProtocolModule): Three-pane mapping, Tauri integration, Protocol Playground
• Phase 6 (Convergence): stapeln ContainerModule, QualityModule, cross-pillar analysis
• v1.1.1 changelog with full documentation sync and security sweep results

Stats (unchanged from v1.1.1)

• 921 tests, 0 failures
• 13 protocol analyzers
• Formal proofs in 5 systems (Agda, Coq, Lean 4, Isabelle, Z3)
• panic-attack PASS verdict
• cargo audit: 0 vulnerabilities / 275 dependencies

Documentation Only

No code changes. This is a roadmap/documentation release.

v1.1.1 — Documentation Sync, Security Sweep, Formatting

What's Changed (since v1.0.0)

ECHIDNA Bridge Integration

• 30-backend cross-prover consensus (Coq, Z3, Lean4) with CLI integration
• Offline fallback — no running services required
• Trust levels (Level1–Level3) from cross-prover agreement

VeriSimDB Integration

• Analysis persistence with InMemoryStore fallback
• Historical reports and compatibility trend queries
• Feedback-o-Tron: suggestion generation from stored analysis records

Phase 3 Hardening

• Security Bridge (95%): Negotiation, audit logging, downgrade risk, cert expiry, TLS probing — 31 tests
• Enterprise (95%): Audit queries, governance reports, migration validation, VeriSimDB-backed registry
• Performance (100%): SIMD byte search, chunked streaming, hardware detection, lazy schemas
• Distributed (90%): Job queue, progress tracking, retry policies, stats, partition rebalancer

Formal Proofs (5 Systems)

• Agda: 8 theorems — OptimizationSoundness, ConcordeSafety, ContainerPropagation, WheelbarrowNecessity, CarriesInvariant
• Coq: ConcordeSafety, CarriesInvariant, ContainerPropagation
• Lean 4: concorde_safety, wheelbarrow_necessity
• Isabelle: WheelbarrowNecessity
• Z3/SMT: transport exhaustiveness, Concorde constraints, optimization soundness

13 Format Analyzers

Rust, Python, JSON Schema, Protobuf, Bebop, FlatBuffers, MessagePack, Avro, Cap'n Proto, Thrift, ReScript, GraphQL (new), TOML (new)

v1.1.1 Specifics

• All 34 Cargo.toml versions + 16 non-Cargo files synchronized to 1.1.x
• cargo fmt applied across all crates
• panic-attack full security sweep: 0 critical, verdict PASS
• cargo audit: 0 vulnerabilities / 275 dependencies

Metrics

• 921 tests passing, 0 failures
• 0 clippy warnings
• 0 vulnerabilities (cargo audit, 275 deps)
• 48 files updated in docs sync

Full Changelog

v1.0.0...v1.1.1

v1.0.0 — Universal Protocol Interoperability

Protocol Squisher v1.0.0

Universal protocol interoperability through automatic adapter synthesis.

The Invariant: If it compiles, it carries.

Highlights

• 11 protocol analyzers: Rust, Python, JSON Schema, Protobuf, Bebop, FlatBuffers, MessagePack, Avro, Cap'n Proto, Thrift, ReScript
• Canonical IR (ephapax): universal intermediate representation with Idris2 dependent type foundations
• Transport class scoring: automatic Concorde / Business / Economy / Wheelbarrow classification for any format pair
• JSON fallback: guaranteed Wheelbarrow-class transport — slow but unbreakable
• PyO3 code generation: automatic Rust ↔ Python binding generation
• Optimizer: Concorde-class adapter suggestions with zero-copy detection
• CLI tool: analyze-schema, check, optimize, generate, optimize-ai, diversity-report, synthesize
• 721 tests passing across all crates
• Formal verification: Concorde Safety and Container Propagation theorems fully proven in Agda; Concorde Safety cross-validated in Lean

Quick Start

cargo install --path crates/protocol-squisher-cli

protocol-squisher analyze-schema --protocol protobuf --input schema.proto
protocol-squisher check --rust src/lib.rs --python models.py
protocol-squisher generate --rust src/lib.rs --python models.py --output generated/

Known Limitations

• Formal proofs for Wheelbarrow Necessity (2 postulates) and Carries Invariant (1 hole) are partial — see proofs/README.adoc
• Coq, Isabelle, and Z3 proofs are planned but not started
• Security bridge, enterprise features, and distributed squishing are scaffolded but not production-ready
• SIMD acceleration is a stub only

See CHANGELOG.md for full details.