Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
28 changes: 9 additions & 19 deletions CHANGELOG.adoc
Original file line number Diff line number Diff line change
@@ -1,30 +1,20 @@
// SPDX-License-Identifier: CC-BY-SA-4.0
// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath)
= Changelog: typedqliser
:toc:
== Changelog

All notable changes to typedqliser will be documented in this file.

This format is based on https://keepachangelog.com/en/1.1.0/[Keep a Changelog],
and this project adheres to https://semver.org/spec/v2.0.0.html[Semantic Versioning].
The format is based on https://keepachangelog.com/en/1.1.0/[Keep a
Changelog], and this project adheres to
https://semver.org/spec/v2.0.0.html[Semantic Versioning].

== [0.1.0] - 2026-03-21
=== [0.1.0] - 2026-03-20

=== Phase 1 — RSR Compliance Sweep
==== Added

=== Added
* Phase 1 complete — scaffold, CLI, manifest parser, codegen stubs, ABI types
* RSR compliance sweep — STATE.a2ml, contractiles, Justfile updated
* Bespoke contractile constraints for Query language type safety and formal verification domain
* Project-specific Justfile recipes

== [0.0.1] - 2026-03-20

=== Added
* Initial project scaffold from rsr-template-repo
* CLI with subcommands (init, validate, generate, build, run, info)
* Manifest parser (`typedqliser.toml`)
* Codegen engine (stubs — target-language-specific implementation pending)
* Manifest parser (`+typedqliser.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)
Expand Down
18 changes: 0 additions & 18 deletions CHANGELOG.md

This file was deleted.

24 changes: 24 additions & 0 deletions CODE_OF_CONDUCT.adoc
Original file line number Diff line number Diff line change
@@ -0,0 +1,24 @@
== Contributor Covenant Code of Conduct

=== Our Pledge

We pledge to make participation a harassment-free experience for
everyone.

=== Our Standards

*Positive behavior:* * Using welcoming language * Being respectful of
differing viewpoints * Accepting constructive criticism * Focusing on
what is best for the community

*Unacceptable behavior:* * Harassment, trolling, or personal attacks *
Publishing private information without permission

=== Enforcement

Report issues to the maintainers. All complaints will be reviewed.

=== Attribution

Adapted from https://www.contributor-covenant.org/[Contributor Covenant]
v2.1.
27 changes: 0 additions & 27 deletions CODE_OF_CONDUCT.md

This file was deleted.

71 changes: 71 additions & 0 deletions CONTRIBUTING.adoc
Original file line number Diff line number Diff line change
@@ -0,0 +1,71 @@
== Contributing

Thank you for your interest in contributing! We follow a "`Dual-Track`"
architecture where human-readable documentation lives in the root and
machine-readable policies live in `+.machine_readable/+`.

=== How to Contribute

We welcome contributions in many forms:

* *Code:* Improving the core stack or extensions
* *Documentation:* Enhancing docs or AI manifests
* *Testing:* Adding property-based tests or formal proofs
* *Bug reports:* Filing clear, reproducible issues

=== Getting Started

[arabic]
. *Read the AI Manifest:* Start with `+0-AI-MANIFEST.a2ml+` (if present)
to understand the repository structure.
. *Environment:* Use `+nix develop+` or `+direnv allow+` to set up your
tools.
. *Task Runner:* Use `+just+` to see available commands
(`+just --list+`).

=== Development Workflow

==== Branch Naming

....
docs/short-description # Documentation
test/what-added # Test additions
feat/short-description # New features
fix/issue-number-description # Bug fixes
refactor/what-changed # Code improvements
security/what-fixed # Security fixes
....

==== Commit Messages

We follow https://www.conventionalcommits.org/[Conventional Commits]:

....
<type>(<scope>): <description>

[optional body]

[optional footer]
....

Types: `+feat+`, `+fix+`, `+docs+`, `+test+`, `+refactor+`, `+ci+`,
`+chore+`, `+security+`

=== Reporting Bugs

Before reporting: 1. Search existing issues 2. Check if it’s already
fixed in `+main+`

When reporting, include: - Clear, descriptive title - Environment
details (OS, versions, toolchain) - Steps to reproduce - Expected vs
actual behaviour

=== Code of Conduct

All contributors are expected to adhere to our
link:CODE_OF_CONDUCT.md[Code of Conduct].

=== License

By contributing, you agree that your contributions will be licensed
under the same license as the project (see LICENSE).
66 changes: 0 additions & 66 deletions CONTRIBUTING.md

This file was deleted.

52 changes: 52 additions & 0 deletions PROOF-NEEDS.adoc
Original file line number Diff line number Diff line change
@@ -0,0 +1,52 @@
== PROOF-NEEDS.md

=== Current State

* *LOC*: ~6,000
* *Languages*: Rust, Idris2, Zig
* *Existing ABI proofs*: `+src/interface/abi/*.idr+` (template-level)
* *Dangerous patterns*: None detected

=== What Needs Proving

==== Code Generation (src/codegen/)

* Generates typed query code from schemas
* Prove: generated code is well-typed with respect to the input schema
* Prove: generated queries are equivalent to the schema specification

==== Plugin System (src/plugins/)

* `+sql.rs+` — SQL code generation
* `+wasm.rs+` — WASM code generation
* Prove: SQL generation produces valid SQL that matches the typed query
semantics
* Prove: WASM generation preserves query semantics

==== ABI Module (src/abi/)

* Rust ABI module — should have Idris2-backed contracts for type-safe
FFI

==== Manifest Validation (src/manifest/)

* Schema manifest parsing and validation
* Prove: manifest parsing is total and produces valid configurations

=== Recommended Prover

* *Idris2* for ABI contracts and codegen correctness specifications
* *Lean4* alternative for SQL equivalence proofs

=== Priority

*MEDIUM* — Code generator correctness is important but downstream of
VCL-total and TypeLL. Focus proofs on SQL generation first as it
directly affects data integrity.

=== Template ABI Cleanup (2026-03-29)

Template ABI removed – was creating false impression of formal
verification. The removed files (Types.idr, Layout.idr, Foreign.idr)
contained only RSR template scaffolding with unresolved
\{\{PROJECT}}/\{\{AUTHOR}} placeholders and no domain-specific proofs.
44 changes: 0 additions & 44 deletions PROOF-NEEDS.md

This file was deleted.

21 changes: 12 additions & 9 deletions SECURITY.md → SECURITY.adoc
Original file line number Diff line number Diff line change
@@ -1,21 +1,24 @@
# Security Policy
== Security Policy

## Supported Versions
=== Supported Versions

| Version | Supported |
|---------|-----------|
| 0.1.x | ✅ |
[cols=",",options="header",]
|===
|Version |Supported
|0.1.x |✅
|===

## Reporting a Vulnerability
=== Reporting a Vulnerability

Please report security vulnerabilities to: j.d.a.jewell@open.ac.uk

Do NOT open a public issue for security vulnerabilities.

## Response Time
=== Response Time

We aim to respond within 48 hours and provide a fix within 7 days for critical issues.
We aim to respond within 48 hours and provide a fix within 7 days for
critical issues.

## Scope
=== Scope

This policy covers the typedqliser CLI tool and its generated artifacts.
Loading
Loading