Skip to content

Commit 31a2f85

Browse files
hyperpolymathclaude
hyperpolymath
and
claude
committed
feat: merge Progressive.idr, Containerfile, flake.nix from ochrance-framework
Consolidates valuable content before archiving the framework repo. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
1 parent 649b4d4 commit 31a2f85

4 files changed

Lines changed: 293 additions & 0 deletions

File tree

‎.devcontainer/Containerfile‎

Lines changed: 32 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,32 @@
1+
# SPDX-License-Identifier: PMPL-1.0-or-later
2+
# Copyright (c) {{CURRENT_YEAR}} {{AUTHOR}} (hyperpolymath) <{{AUTHOR_EMAIL}}>
3+
#
4+
# Dev Container image for {{PROJECT_NAME}}
5+
# Base: Chainguard Wolfi (minimal, supply-chain-secure)
6+
# Build: podman build -t {{PROJECT_NAME}}-dev -f .devcontainer/Containerfile .
7+
8+
FROM cgr.dev/chainguard/wolfi-base:latest
9+
10+
# Install common development tools
11+
RUN apk update && apk add --no-cache \
12+
bash \
13+
curl \
14+
git \
15+
openssh-client \
16+
ca-certificates \
17+
build-base \
18+
posix-libc-utils \
19+
shadow \
20+
&& rm -rf /var/cache/apk/*
21+
22+
# Create non-root dev user (matches devcontainer.json remoteUser)
23+
RUN groupadd -g 1000 nonroot || true \
24+
&& useradd -m -u 1000 -g 1000 -s /bin/bash nonroot || true
25+
26+
# Set workspace directory
27+
WORKDIR /workspaces/{{PROJECT_NAME}}
28+
29+
# Default shell
30+
ENV SHELL=/bin/bash
31+
32+
USER nonroot

‎Containerfile‎

Lines changed: 41 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,41 @@
1+
# SPDX-License-Identifier: PMPL-1.0-or-later
2+
# Copyright (c) {{CURRENT_YEAR}} {{AUTHOR}} (hyperpolymath) <{{AUTHOR_EMAIL}}>
3+
#
4+
# Containerfile for {{PROJECT_NAME}}
5+
# Build: podman build -t {{project}}:latest -f Containerfile .
6+
# Run: podman run --rm -it {{project}}:latest
7+
# Seal: selur seal {{project}}:latest
8+
9+
# --- Build stage ---
10+
FROM cgr.dev/chainguard/wolfi-base:latest AS build
11+
12+
# TODO: Install build dependencies for your stack
13+
# Examples:
14+
# RUN apk add --no-cache rust cargo # Rust
15+
# RUN apk add --no-cache elixir erlang # Elixir
16+
# RUN apk add --no-cache zig # Zig
17+
18+
WORKDIR /build
19+
COPY . .
20+
21+
# TODO: Replace with your build command
22+
# Examples:
23+
# RUN cargo build --release
24+
# RUN mix deps.get && MIX_ENV=prod mix release
25+
# RUN zig build -Doptimize=ReleaseSafe
26+
27+
# --- Runtime stage ---
28+
FROM cgr.dev/chainguard/static:latest
29+
30+
# Copy built artifact from build stage
31+
# TODO: Replace with your binary/artifact path
32+
# Examples:
33+
# COPY --from=build /build/target/release/{{project}} /usr/local/bin/
34+
# COPY --from=build /build/_build/prod/rel/{{project}} /app/
35+
# COPY --from=build /build/zig-out/bin/{{project}} /usr/local/bin/
36+
37+
# Non-root user (chainguard images default to nonroot)
38+
USER nonroot
39+
40+
# TODO: Replace with your entrypoint
41+
# ENTRYPOINT ["/usr/local/bin/{{project}}"]

‎flake.nix‎

Lines changed: 170 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,170 @@
1+
# SPDX-License-Identifier: PMPL-1.0-or-later
2+
# Copyright (c) {{CURRENT_YEAR}} {{AUTHOR}} (hyperpolymath) <{{AUTHOR_EMAIL}}>
3+
#
4+
# Nix flake for {{PROJECT_NAME}}
5+
#
6+
# NOTE: guix.scm is the PRIMARY development environment. This flake is provided
7+
# as a FALLBACK for contributors who use Nix instead of Guix. The .envrc checks
8+
# for Guix first, then falls back to Nix.
9+
#
10+
# Usage:
11+
# nix develop # Enter development shell
12+
# nix build # Build the project
13+
# nix flake check # Run checks
14+
# nix flake show # Show flake outputs
15+
#
16+
# With direnv (.envrc already configured):
17+
# direnv allow # Auto-enters shell on cd
18+
#
19+
# TODO: Replace {{PROJECT_NAME}} and {{PROJECT_DESCRIPTION}} with actual values.
20+
21+
{
22+
description = "{{PROJECT_NAME}} — RSR-compliant project";
23+
24+
inputs = {
25+
nixpkgs.url = "github:NixOS/nixpkgs/nixpkgs-unstable";
26+
flake-utils.url = "github:numtide/flake-utils";
27+
};
28+
29+
outputs = { self, nixpkgs, flake-utils }:
30+
flake-utils.lib.eachSystem [ "x86_64-linux" "aarch64-linux" ] (system:
31+
let
32+
pkgs = import nixpkgs { inherit system; };
33+
34+
# Common development tools present in every RSR project.
35+
commonTools = with pkgs; [
36+
git
37+
just
38+
nickel
39+
curl
40+
bash
41+
coreutils
42+
];
43+
44+
# ---------------------------------------------------------------
45+
# Language-specific packages: uncomment the stacks you need.
46+
# ---------------------------------------------------------------
47+
#
48+
# Rust:
49+
# rustc cargo clippy rustfmt rust-analyzer
50+
#
51+
# Elixir:
52+
# elixir erlang
53+
#
54+
# Gleam:
55+
# gleam erlang
56+
#
57+
# Zig:
58+
# zig zls
59+
#
60+
# Haskell:
61+
# ghc cabal-install haskell-language-server
62+
#
63+
# Idris2:
64+
# idris2
65+
#
66+
# OCaml:
67+
# ocaml dune_3 ocaml-lsp
68+
#
69+
# ReScript (via Deno):
70+
# deno
71+
#
72+
# Julia:
73+
# julia
74+
#
75+
# Ada/SPARK:
76+
# gnat gprbuild
77+
#
78+
# ---------------------------------------------------------------
79+
languageTools = with pkgs; [
80+
# TODO: Uncomment or add packages for your stack.
81+
# Example for a Rust project:
82+
# rustc
83+
# cargo
84+
# clippy
85+
# rustfmt
86+
# rust-analyzer
87+
];
88+
89+
in
90+
{
91+
# ---------------------------------------------------------------
92+
# Development shell — `nix develop`
93+
# ---------------------------------------------------------------
94+
devShells.default = pkgs.mkShell {
95+
name = "{{PROJECT_NAME}}-dev";
96+
97+
buildInputs = commonTools ++ languageTools;
98+
99+
# Environment variables available inside the shell.
100+
env = {
101+
PROJECT_NAME = "{{PROJECT_NAME}}";
102+
RSR_TIER = "infrastructure";
103+
};
104+
105+
shellHook = ''
106+
echo ""
107+
echo " {{PROJECT_NAME}} — development shell"
108+
echo " Nix: $(nix --version 2>/dev/null || echo 'unknown')"
109+
echo " Just: $(just --version 2>/dev/null || echo 'not found')"
110+
echo ""
111+
echo " Run 'just' to see available recipes."
112+
echo ""
113+
114+
# Source .envrc manually when direnv is not managing the shell.
115+
# This keeps project env vars (PROJECT_NAME, DATABASE_URL, etc.)
116+
# consistent whether you enter via 'nix develop' or 'direnv allow'.
117+
if [ -z "''${DIRENV_IN_ENVRC:-}" ] && [ -f .envrc ]; then
118+
# Only source the non-nix parts to avoid recursion.
119+
export PROJECT_NAME="{{PROJECT_NAME}}"
120+
export RSR_TIER="infrastructure"
121+
if [ -f .env ]; then
122+
set -a
123+
. .env
124+
set +a
125+
fi
126+
fi
127+
'';
128+
};
129+
130+
# ---------------------------------------------------------------
131+
# Package — `nix build`
132+
# ---------------------------------------------------------------
133+
packages.default = pkgs.stdenv.mkDerivation {
134+
pname = "{{PROJECT_NAME}}";
135+
version = "0.1.0";
136+
137+
src = self;
138+
139+
# TODO: Replace with real build instructions.
140+
# Examples:
141+
#
142+
# Rust (use rustPlatform.buildRustPackage instead of stdenv):
143+
# packages.default = pkgs.rustPlatform.buildRustPackage { ... };
144+
#
145+
# Elixir (use mixRelease):
146+
# packages.default = pkgs.beamPackages.mixRelease { ... };
147+
#
148+
# Zig:
149+
# buildPhase = "zig build -Doptimize=ReleaseSafe";
150+
151+
buildPhase = ''
152+
echo "TODO: Add build commands for {{PROJECT_NAME}}"
153+
'';
154+
155+
installPhase = ''
156+
mkdir -p $out/share/doc
157+
cp README.adoc $out/share/doc/ 2>/dev/null || true
158+
'';
159+
160+
meta = with pkgs.lib; {
161+
description = "{{PROJECT_DESCRIPTION}}";
162+
homepage = "https://github.com/hyperpolymath/{{PROJECT_NAME}}";
163+
license = licenses.mpl20; # PMPL-1.0-or-later extends MPL-2.0
164+
maintainers = [];
165+
platforms = [ "x86_64-linux" "aarch64-linux" ];
166+
};
167+
};
168+
}
169+
);
170+
}

‎ochrance-core/Ochrance/Framework/Progressive.idr‎

Lines changed: 50 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,50 @@
1+
-- SPDX-License-Identifier: PMPL-1.0-or-later
2+
-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
3+
4+
||| Ochrance.Framework.Progressive — Verification Assurance Tiers.
5+
|||
6+
||| This module implements the "Progressive Assurance" model, allowing the
7+
||| framework to scale its strictness based on the operational context.
8+
||| It defines the relationship between different verification modes
9+
||| and provides type-level evidence of security thresholds.
10+
11+
module Ochrance.Framework.Progressive
12+
13+
%default total
14+
15+
--------------------------------------------------------------------------------
16+
-- Verification Modes
17+
--------------------------------------------------------------------------------
18+
19+
||| MODES: Representing the three tiers of system assurance.
20+
||| - **Lax**: Structural sanity checks only.
21+
||| - **Checked**: Full cryptographic hash verification.
22+
||| - **Attested**: Formal proof of domain invariants.
23+
public export
24+
data VerificationMode = Lax | Checked | Attested
25+
26+
||| ORDERING: Defines the relationship Lax < Checked < Attested.
27+
public export
28+
Ord VerificationMode where
29+
compare Lax Lax = EQ
30+
compare Lax _ = LT
31+
compare Checked Attested = LT
32+
-- ... [Remaining cases]
33+
34+
--------------------------------------------------------------------------------
35+
-- Proof Witnesses
36+
--------------------------------------------------------------------------------
37+
38+
||| THRESHOLD PROOF: A dependent type that serves as evidence that a
39+
||| specific `mode` is at least as strict as a required `threshold`.
40+
public export
41+
data SatisfiesMinimum : (threshold : VerificationMode) -> (mode : VerificationMode) -> Type where
42+
||| WITNESS: Proves that the target mode meets or exceeds the threshold.
43+
MeetsThreshold : {0 t, m : VerificationMode}
44+
-> (prf : atLeast t m = True)
45+
-> SatisfiesMinimum t m
46+
47+
||| AUTO-PROOFS: Common threshold satisfied cases.
48+
public export
49+
attestedSatisfiesLax : SatisfiesMinimum Lax Attested
50+
attestedSatisfiesLax = MeetsThreshold Refl

0 commit comments

Comments
 (0)