docs: FS↔M anchors+mapping, release workflow, Rust WASM policy demo, tip link #87
There are no files selected for viewing
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,34 @@ | ||
| name: Release Artifacts | ||
|
|
||
| on: | ||
| push: | ||
| tags: | ||
| - 'v*' | ||
|
|
||
| permissions: | ||
| contents: write | ||
|
|
||
| jobs: | ||
| release: | ||
| runs-on: ubuntu-latest | ||
| steps: | ||
| - name: Checkout | ||
| uses: actions/checkout@v4 | ||
| with: | ||
| fetch-depth: 0 | ||
|
|
||
| - name: Prepare assets | ||
| run: | | ||
| mkdir -p dist | ||
| zip -r dist/schemas.zip schemas | ||
| zip -r dist/vectors.zip tests/vectors scripts/vectors | ||
| - name: Create GitHub Release | ||
| uses: softprops/action-gh-release@v2 | ||
| with: | ||
| files: | | ||
| dist/schemas.zip | ||
| dist/vectors.zip | ||
| env: | ||
| GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} | ||
|
|
||
|
||
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
|
|
@@ -67,3 +67,6 @@ fastlane/test_output | |
| !.vscode/tasks.json | ||
| !.vscode/launch.json | ||
| !.vscode/*.code-snippets | ||
|
|
||
| # Temp artifacts | ||
| tmp/ | ||
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -1,12 +1,143 @@ | ||
| --- | ||
| Author: J. Kirby Ross <[email protected]> (https://github.com/flyingrobots) | ||
| Created: 2025-10-27 | ||
| License: MIT | ||
| Scope: This document defines the minimal, requisite semantics and invariants that a Git-native ledger implementation must satisfy to be considered compliant. | ||
|
There was a problem hiding this comment. 🧹 Nitpick | 🔵 Trivial Minor: Add language specifiers to all fenced code blocks (MD040). Fenced blocks at lines 5, 20, 26, 32 lack language identifiers (e.g., -```
+```math
\mathcal{R} = (\mathcal{O}, \mathcal{R_{efs}})
-```
+```Repeat for all remaining code fences. Also applies to: 20-20, 26-26, 32-32 🧰 Tools🪛 markdownlint-cli2 (0.18.1)5-5: Fenced code blocks should have a language specified (MD040, fenced-code-language) 🤖 Prompt for AI Agents |
||
| Status: Draft | ||
| Summary: Defines the invariants, operations, and compliance requirements for a Git-native append-only ledger. | ||
| Version: 0.1.0 | ||
| --- | ||
|
|
||
| # **A Formal State-Transition Model for a Git-Native Verifiable Ledger** | ||
|
|
||
| ## Abstract | ||
|
|
||
| We present a formal state-transition model for a verifiable ledger kernel operating natively on a Git-based Directed Acyclic Graph (DAG). The model defines a ledger as a totally ordered sequence of entries, where each entry represents an atomic state transition. We formalize the system's core components: a pure state transition function $\mathcal{T}$, a constraint-based policy engine $\mathcal{P}$, and a cryptographic attestation mechanism $\mathcal{A}$. The central thesis of our model is the guarantee of **deterministic replayability**, where the ledger's final state is a pure function of its entry-set. This formalism provides a verifiable foundation for trusted, distributed systems, such as software supply chain attestation or decentralized registries. | ||
|
|
||
| --- | ||
|
|
||
| ## 1. Introduction | ||
|
|
||
| The Git object model, fundamentally a content-addressed Directed Acyclic Graph (DAG), provides a robust mechanism for tracking provenance. However, its inherent support for branching and non-linear histories complicates its use as a linear, append-only ledger. This paper introduces a formal model that superimposes a **totally ordered state machine** onto the Git DAG. We achieve this by constraining a specific Git reference (ref) to a fast-forward-only commit history, where each commit constitutes a **ledger entry** ($\mathcal{E}$). This model establishes the semantic bridge between low-level Git objects and high-level, verifiable ledger state transitions, enabling deterministic replay and cryptographic verification of the ledger's history and state. | ||
|
|
||
| --- | ||
|
|
||
| ## 2. Formal Model Definition | ||
|
|
||
| Let a Git repository be a tuple $\mathcal{R} = (\mathcal{O}, \mathcal{R_{efs}})$, where $\mathcal{O}$ is a content-addressed object store (a set of Git objects) and $\mathcal{R_{efs}}$ is a mapping from reference paths to commit identifiers (hashes). | ||
|
|
||
| We define a **Ledger Entry**, $\mathcal{E}$, as a commit object $C \in \mathcal{O}$ that adheres to a specific data schema (e.g., contains `/_ledger/entry.json` and associated attestations). | ||
|
|
||
| We define a Ledger, $\mathcal{L}$, as a tuple: | ||
|
|
||
| $$ | ||
| \mathcal{L} = (p, \mathbf{E}, \mathcal{A}, \mathcal{P}) | ||
| $$ | ||
|
|
||
| where: | ||
|
|
||
| - $p$ is the persistent reference path (e.g., `refs/heads/main-ledger`) in $\mathcal{R_{efs}}$. | ||
| - $\mathbf{E} = \langle \mathcal{E}_0, \mathcal{E}_1, \dots, \mathcal{E}_n \rangle$ is a **totally ordered sequence** of ledger entries. This ordering is strictly enforced by the commit ancestry relation under $p$, s.t. $\text{Parent}(\mathcal{E}_{i+1}) = \text{Hash}(\mathcal{E}_i)$. | ||
| - $\mathcal{A}$ is the set of all attestations, where each $\mathcal{A}_k \in \mathcal{A}$ is cryptographically bound to a specific entry $\mathcal{E}_i \in \mathbf{E}$. | ||
| - $\mathcal{P}$ is a set of policies applicable to $\mathcal{L}$. | ||
|
|
||
| The _head_ of the ledger $\mathcal{L}$ corresponds to the commit hash $\text{Hash}(\mathcal{E}_n)$, which is the value of $\mathcal{R_{efs}}[p]$. | ||
|
|
||
| --- | ||
|
|
||
| ## 3. The State Transition System | ||
|
|
||
| The ledger's semantics are defined by a deterministic state transition system. | ||
|
|
||
| Let $\mathcal{S}$ be the set of all possible ledger states. We define the initial state as the empty set: $\mathcal{S}_0 = \emptyset$. | ||
|
|
||
| We define a pure, deterministic state transition function $\mathcal{T}$: | ||
|
|
||
| $$ | ||
| \mathcal{T} : \mathcal{S} \times \mathcal{E} \to \mathcal{S} | ||
| $$ | ||
|
|
||
| Given a current state $\mathcal{S}_i$ (derived from entry $\mathcal{E}_i$), the subsequent state $\mathcal{S}_{i+1}$ is produced by applying the next entry $\mathcal{E}_{i+1}$: | ||
|
|
||
| $$ | ||
| \mathcal{S}_{i+1} = \mathcal{T}(\mathcal{S}_i, \mathcal{E}_{i+1}) | ||
| $$ | ||
|
|
||
| The function $\mathcal{T}$ must be **deterministic** and **pure**; it must produce an identical output state $\mathcal{S}_{i+1}$ given identical inputs $(\mathcal{S}_i, \mathcal{E}_{i+1})$, with no reliance on external I/O, network state, or stochastic processes. | ||
|
|
||
| ### 3.1. State Re-computation (Replay) | ||
|
|
||
| The complete state $\mathcal{S}_n$ of a ledger $\mathcal{L}$ with $n$ entries is the result of a functional fold (or reduction) over the entry sequence $\mathbf{E}$: | ||
|
|
||
| $$ | ||
| \mathcal{S}_n = \text{foldl}(\mathcal{T}, \mathcal{S}_0, \mathbf{E}) | ||
| $$ | ||
|
|
||
| Recursively, this is defined as: | ||
|
|
||
| - $\text{Replay}(\langle \rangle) = \mathcal{S}_0$ | ||
| - $\text{Replay}(\langle \mathcal{E}_0, \dots, \mathcal{E}_i \rangle) = \mathcal{T}(\text{Replay}(\langle \mathcal{E}_0, \dots, \mathcal{E}_{i-1} \rangle), \mathcal{E}_i)$ | ||
|
|
||
| This property is the foundation of the system's verifiability. | ||
|
|
||
| --- | ||
|
|
||
| ## 4. Transition Validity | ||
|
|
||
| Important: For a new entry $\mathcal{E}_{i+1}$ to be appended to the ledger at state $\mathcal{S}_i$, a global validity predicate $\mathcal{V}$ must evaluate to true. | ||
|
|
||
| $$ | ||
| \mathcal{V}(\mathcal{E}_{i+1}, \mathcal{E}_i, \mathcal{S}_i, \mathcal{P}) \to \{\text{true}, \text{false}\} | ||
| $$ | ||
|
|
||
| The predicate $\mathcal{V}$ is the logical conjunction of the following constraints: | ||
|
|
||
| 1. Ancestry Constraint: The entry must maintain the fast-forward chain. | ||
|
|
||
| $$ | ||
| \text{ParentHash}(\mathcal{E}_{i+1}) \equiv \text{Hash}(\mathcal{E}_i) | ||
| $$ | ||
|
|
||
| 2. Temporal Monotonicity: The entry's timestamp must be non-decreasing. | ||
|
|
||
| $$ | ||
| \text{Timestamp}(\mathcal{E}_{i+1}) \geq \text{Timestamp}(\mathcal{E}_i) | ||
| $$ | ||
|
|
||
| 3. Policy Adherence: The entry must satisfy all active policies $\mathcal{P}_k \in \mathcal{P}$, evaluated against the current state $\mathcal{S}_i$. (See §5). | ||
|
|
||
| $$ | ||
| \mathcal{P}_{\text{all}}(\mathcal{E}, \mathcal{S}) = \bigwedge_{k \in \mathcal{P}} \mathcal{P}_k(\mathcal{E}, \mathcal{S}) \equiv \text{true} | ||
| $$ | ||
|
|
||
| 4. Attestation Validity: All attestations $\mathcal{A}_k$ attached to $\mathcal{E}_{i+1}$ must be cryptographically valid. (See §6). | ||
|
|
||
| $$ | ||
| \forall \mathcal{A}_k:\; \mathcal{V}_{\text{attest}}\!\left(\mathcal{A}_k,\; \text{Hash}(\mathcal{E}_{i+1})\right) \equiv \text{true} | ||
| $$ | ||
|
|
||
| If $\mathcal{V}$ fails, the transition is rejected, and the entry $\mathcal{E}_{i+1}$ is not appended to the ledger $\mathcal{L}$. | ||
|
|
||
| --- | ||
|
|
||
| ### **5. Policy as a State Constraint** | ||
|
|
||
| A policy is a pure function (a predicate) that constrains valid transitions. | ||
|
|
||
| Policies are executed _before_ the state transition function $\mathcal{T}$ is applied. They are evaluated using the candidate entry ($\mathcal{E}_{i+1}$) and the previous state ($\mathcal{S}_i$). | ||
|
|
||
| Policies are composable, typically via logical conjunction: | ||
|
|
||
| $$ | ||
| \mathcal{P}_{\text{all}}(\mathcal{E}, \mathcal{S}) = \bigwedge_{k \in \mathcal{P}} \mathcal{P}_k(\mathcal{E}, \mathcal{S}) \equiv \text{true} | ||
| $$ | ||
|
|
||
| --- | ||
|
|
||
| ### **6. Attestation Model** | ||
|
|
||
| An attestation $\mathcal{A}$ provides a non-repudiable cryptographic binding between an external identity (signer) and a specific ledger entry $\mathcal{E}$. | ||
|
|
||
| Let $\mathcal{A}$ be a tuple $\mathcal{A} = (\text{signer\_id}, \sigma)$, where $\sigma$ is a digital signature. | ||
|
|
||
| The verification function $\mathcal{V}_{\text{attest}}$ (informally) checks that each attestation’s signature verifies against the entry hash with the signer’s public key. | ||
Oops, something went wrong.
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Uh oh!
There was an error while loading. Please reload this page.