diff --git a/.github/workflows/codeql.yml b/.github/workflows/codeql.yml index f50a1d1..a98ba16 100644 --- a/.github/workflows/codeql.yml +++ b/.github/workflows/codeql.yml @@ -30,7 +30,11 @@ jobs: fail-fast: false matrix: include: - - language: javascript-typescript + # Phronesis is Elixir/Erlang (BEAM) — not a CodeQL-supported source + # language, so `javascript-typescript` made `analyze` exit + # "no source files" on every run. `actions` scans the workflow YAML + # (always present), giving real SAST coverage. (Hypatia: SAST check.) + - language: actions build-mode: none steps: diff --git a/ECOSYSTEM.scm.bak b/ECOSYSTEM.scm.bak deleted file mode 100644 index 63a48e3..0000000 --- a/ECOSYSTEM.scm.bak +++ /dev/null @@ -1,20 +0,0 @@ -;; SPDX-License-Identifier: MPL-2.0 -;; SPDX-FileCopyrightText: 2025 Jonathan D.A. Jewell -;; ECOSYSTEM.scm — template-repo - -(ecosystem - (version "1.0.0") - (name "template-repo") - (type "project") - (purpose "Project in the hyperpolymath ecosystem") - - (position-in-ecosystem - "Part of hyperpolymath ecosystem. Follows RSR guidelines.") - - (related-projects - (project (name "rhodium-standard-repositories") - (url "https://github.com/hyperpolymath/rhodium-standard-repositories") - (relationship "standard"))) - - (what-this-is "Project in the hyperpolymath ecosystem") - (what-this-is-not "- NOT exempt from RSR compliance")) diff --git a/META.scm.bak b/META.scm.bak deleted file mode 100644 index 4b7b332..0000000 --- a/META.scm.bak +++ /dev/null @@ -1,24 +0,0 @@ -;; SPDX-License-Identifier: MPL-2.0 -;; SPDX-FileCopyrightText: 2025 Jonathan D.A. Jewell -;;; META.scm — template-repo - -(define-module (template-repo meta) - #:export (architecture-decisions development-practices design-rationale)) - -(define architecture-decisions - '((adr-001 - (title . "RSR Compliance") - (status . "accepted") - (date . "2025-12-15") - (context . "Project in the hyperpolymath ecosystem") - (decision . "Follow Rhodium Standard Repository guidelines") - (consequences . ("RSR Gold target" "SHA-pinned actions" "SPDX headers" "Multi-platform CI"))))) - -(define development-practices - '((code-style (languages . ("unknown")) (formatter . "auto-detect") (linter . "auto-detect")) - (security (sast . "CodeQL") (credentials . "env vars only")) - (testing (coverage-minimum . 70)) - (versioning (scheme . "SemVer 2.0.0")))) - -(define design-rationale - '((why-rsr "RSR ensures consistency, security, and maintainability."))) diff --git a/SPEC.core.scm.orig b/SPEC.core.scm.orig deleted file mode 100644 index 60c92b0..0000000 --- a/SPEC.core.scm.orig +++ /dev/null @@ -1,488 +0,0 @@ -;; SPDX-License-Identifier: MPL-2.0 -;; SPDX-FileCopyrightText: 2025 Phronesis Contributors -;; -;; SPEC.core.scm - Core Specification for Phronesis Rule Evaluation -;; -;; This file defines the formal semantics of rule evaluation and the -;; decision trace model in executable Guile Scheme. -;; -;; Per semantic anchor: "SPEC.core.scm defines rule evaluation + decision trace model" - -;;; ============================================================ -;;; SECTION 1: Core Type Definitions -;;; ============================================================ - -;; A Policy is a 5-tuple: (name, condition, action, priority, metadata) -(define-record-type - (make-policy name condition action priority metadata) - policy? - (name policy-name) - (condition policy-condition) - (action policy-action) - (priority policy-priority) - (metadata policy-metadata)) - -;; An Action is one of: -;; - (accept reason) -;; - (reject reason) -;; - (report message) -;; - (execute function args) -;; - (block actions...) -;; - (conditional cond then-action else-action) -(define-record-type - (make-action type payload) - action? - (type action-type) ; 'accept | 'reject | 'report | 'execute | 'block | 'conditional - (payload action-payload)) - -;; A TraceStep records a single evaluation step -(define-record-type - (make-trace-step type timestamp inputs result rationale) - trace-step? - (type trace-step-type) ; 'eval | 'match | 'vote | 'action | 'bind | 'error - (timestamp trace-step-timestamp) - (inputs trace-step-inputs) - (result trace-step-result) - (rationale trace-step-rationale)) - -;; A Trace is the complete audit trail of a decision -(define-record-type - (make-trace id started-at completed-at status steps decision metadata) - trace? - (id trace-id) - (started-at trace-started-at) - (completed-at trace-completed-at) - (status trace-status) ; 'pending | 'completed | 'failed - (steps trace-steps) ; list of trace-step - (decision trace-decision) ; (decision-type . reason) | #f - (metadata trace-metadata)) - -;; State represents the interpreter state -(define-record-type - (make-state policy-table consensus-log environment agents threshold) - state? - (policy-table state-policy-table) - (consensus-log state-consensus-log) - (environment state-environment) - (agents state-agents) - (threshold state-threshold)) - - -;;; ============================================================ -;;; SECTION 2: Operational Semantics - Evaluation Rules -;;; ============================================================ - -;; RULE 1: POLICY-MATCH -;; -;; Premise: -;; eval(condition, env) = true -;; policy = (name, condition, action, priority, metadata) -;; -;; Conclusion: -;; (state, policy, situation) --> (state', action-pending) -;; -;; The trace records: (match policy-name true "condition evaluated to true") - -(define (rule-policy-match state policy situation trace) - "Apply POLICY-MATCH rule: if condition is true, queue action." - (let* ((condition (policy-condition policy)) - (env (state-environment state)) - (eval-result (eval-condition condition env situation))) - (if (eq? eval-result #t) - (values state - (policy-action policy) - (trace-add-step trace 'match - `((policy . ,(policy-name policy))) - #t - "Policy condition evaluated to true")) - (values state - #f - (trace-add-step trace 'match - `((policy . ,(policy-name policy))) - #f - "Policy condition evaluated to false"))))) - - -;; RULE 2: ACTION-EXECUTE -;; -;; Premise: -;; action in pending-actions -;; consensus-approved(action, agents, threshold) = true -;; -;; Conclusion: -;; log' = log ++ [(action, votes, timestamp)] -;; execute(action) --> result -;; (state, action) --> (state', result) -;; -;; The trace records: (vote action votes approved "consensus achieved") -;; (action action-type result "action executed") - -(define (rule-action-execute state action agents threshold trace) - "Apply ACTION-EXECUTE rule: execute action if consensus approves." - (let* ((votes (collect-votes action agents)) - (approved (consensus-approved? votes agents threshold))) - (if approved - (let* ((trace (trace-add-step trace 'vote - `((action . ,action) (votes . ,votes)) - #t - (format #f "Consensus achieved: ~a/~a approved" - (count-approvals votes) (length agents)))) - (result (execute-action action state)) - (state (log-action state action votes 'approved)) - (trace (trace-add-step trace 'action - `((action . ,action)) - result - (format #f "Action executed: ~a" (action-type action))))) - (values state result trace)) - (let ((trace (trace-add-step trace 'vote - `((action . ,action) (votes . ,votes)) - #f - "Consensus not achieved"))) - (values state 'rejected trace))))) - - -;; RULE 3: COND-TRUE / COND-FALSE -;; -;; For conditional actions: -;; if eval(cond) = true then execute(then-action) -;; if eval(cond) = false then execute(else-action) or noop - -(define (rule-conditional state condition then-action else-action env trace) - "Apply COND-TRUE/COND-FALSE rule for conditional actions." - (let ((result (eval-expr condition env))) - (cond - ((eq? result #t) - (let ((trace (trace-add-step trace 'eval - `((conditional . "then")) - #t - "Conditional true, taking THEN branch"))) - (values then-action trace))) - ((and (eq? result #f) else-action) - (let ((trace (trace-add-step trace 'eval - `((conditional . "else")) - #f - "Conditional false, taking ELSE branch"))) - (values else-action trace))) - (else - (let ((trace (trace-add-step trace 'eval - `((conditional . "noop")) - #f - "Conditional false, no ELSE branch"))) - (values #f trace)))))) - - -;; RULE 4: MODULE-CALL -;; -;; Premise: -;; module M exports function F -;; eval(args) = values -;; -;; Conclusion: -;; M.F(values) --> result (atomically) - -(define (rule-module-call module-path args env trace) - "Apply MODULE-CALL rule: call module function atomically." - (let* ((arg-values (map (lambda (a) (eval-expr a env)) args)) - (result (call-module module-path arg-values)) - (trace (trace-add-step trace 'eval - `((module . ,module-path) (args . ,arg-values)) - result - (format #f "Module call: ~a" module-path)))) - (values result trace))) - - -;; RULE 5: CONSENSUS-VOTE -;; -;; consensus-approved(action, agents, threshold) = -;; (count(votes where vote = true) / |agents|) >= threshold - -(define (consensus-approved? votes agents threshold) - "Check if consensus threshold is met." - (let ((total (length agents)) - (approvals (count-approvals votes))) - (if (= total 0) - #t - (>= (/ approvals total) threshold)))) - -(define (count-approvals votes) - "Count the number of true votes." - (length (filter cdr votes))) - - -;;; ============================================================ -;;; SECTION 3: Decision Trace Model -;;; ============================================================ - -;; Invariant: Every decision MUST produce a trace. -;; The trace is an append-only log of all evaluation steps. - -(define (new-trace . metadata) - "Create a new trace with unique ID." - (make-trace - (generate-trace-id) ; unique identifier - (current-time) ; started-at - #f ; completed-at (not yet) - 'pending ; status - '() ; steps (empty) - #f ; decision (not yet) - (if (null? metadata) '() (car metadata)))) - -(define (trace-add-step trace step-type inputs result rationale) - "Append a step to the trace. Traces are immutable; returns new trace." - (let ((step (make-trace-step step-type (current-time) inputs result rationale))) - (make-trace - (trace-id trace) - (trace-started-at trace) - (trace-completed-at trace) - (trace-status trace) - (append (trace-steps trace) (list step)) ; append-only - (trace-decision trace) - (trace-metadata trace)))) - -(define (trace-complete trace decision) - "Mark trace as completed with final decision." - (make-trace - (trace-id trace) - (trace-started-at trace) - (current-time) ; completed-at = now - 'completed ; status - (trace-steps trace) - decision ; final decision - (trace-metadata trace))) - -(define (trace-fail trace reason) - "Mark trace as failed with error." - (make-trace - (trace-id trace) - (trace-started-at trace) - (current-time) - 'failed - (trace-steps trace) - (cons 'error reason) - (trace-metadata trace))) - - -;;; ============================================================ -;;; SECTION 4: Core Evaluation Functions -;;; ============================================================ - -(define (evaluate-policies policies situation state trace) - "Evaluate policies in priority order, returning first match. - - Invariant: trace is updated for EVERY policy evaluated. - Invariant: returns (state, decision, trace) tuple." - (if (null? policies) - (values state #f (trace-complete trace #f)) - (let* ((policy (car policies)) - (rest (cdr policies))) - (call-with-values - (lambda () (rule-policy-match state policy situation trace)) - (lambda (state action trace) - (if action - ;; Policy matched, execute action with consensus - (call-with-values - (lambda () (rule-action-execute state action - (state-agents state) - (state-threshold state) - trace)) - (lambda (state result trace) - (let ((decision (extract-decision action result))) - (values state decision (trace-complete trace decision))))) - ;; No match, try next policy - (evaluate-policies rest situation state trace))))))) - -(define (extract-decision action result) - "Extract decision from action execution result." - (case (action-type action) - ((accept) (cons 'accept (action-payload action))) - ((reject) (cons 'reject (action-payload action))) - (else #f))) - - -;;; ============================================================ -;;; SECTION 5: Termination Guarantee -;;; ============================================================ - -;; THEOREM: All Phronesis programs terminate. -;; -;; PROOF (by structural induction): -;; -;; Base cases: -;; - Literals evaluate immediately -;; - Variable lookup is O(1) in environment -;; - Module calls are atomic and finite -;; -;; Inductive cases: -;; - Binary/unary operations: terminate if operands terminate -;; - Comparisons: terminate if operands terminate -;; - Conditionals: finite branching, each branch terminates -;; - Blocks: finite sequence, each action terminates -;; - Policy evaluation: finite list, each policy checked once -;; -;; Key restrictions ensuring termination: -;; 1. No loops (while, for, recursion forbidden by grammar) -;; 2. No recursive function definitions -;; 3. Module calls cannot call back into Phronesis -;; 4. Policy list is finite and immutable during evaluation - -(define (termination-proof-sketch) - "Returns a structured proof of termination. - This is a documentation function, not executable proof." - '((theorem . "All Phronesis programs terminate") - (proof-method . "Structural induction on AST") - (base-cases - ((literals . "Constant time evaluation") - (variables . "Environment lookup is O(1)") - (module-calls . "Atomic and guaranteed finite"))) - (inductive-cases - ((expressions . "Terminate if subexpressions terminate") - (conditionals . "Finite branching, each branch terminates") - (blocks . "Finite sequence of terminating actions") - (policies . "Finite list, each evaluated once"))) - (restrictions - ((no-loops . "Grammar forbids while, for, recursion") - (no-recursion . "Functions cannot be defined") - (no-callbacks . "Modules cannot call back") - (finite-policies . "Policy list immutable during eval"))))) - - -;;; ============================================================ -;;; SECTION 6: Safety Properties -;;; ============================================================ - -;; PROPERTY 1: Trace Completeness -;; Every decision path produces a trace with all evaluation steps. - -(define (trace-complete? trace) - "Verify trace completeness: has steps and a final decision." - (and (not (null? (trace-steps trace))) - (or (eq? (trace-status trace) 'completed) - (eq? (trace-status trace) 'failed)))) - -;; PROPERTY 2: Consensus Safety -;; No action executes without consensus approval. - -(define (consensus-safe? state) - "Verify all logged actions have consensus approval." - (every (lambda (log-entry) - (eq? (assoc-ref log-entry 'result) 'approved)) - (filter (lambda (e) (eq? (assoc-ref e 'result) 'approved)) - (state-consensus-log state)))) - -;; PROPERTY 3: Audit Trail Integrity -;; The consensus log is append-only and immutable. - -(define (audit-trail-invariant old-log new-log) - "Verify new log is extension of old log (append-only)." - (let ((old-len (length old-log)) - (new-len (length new-log))) - (and (>= new-len old-len) - (equal? old-log (take new-log old-len))))) - - -;;; ============================================================ -;;; SECTION 7: Helper Functions (Implementation) -;;; ============================================================ - -(define (generate-trace-id) - "Generate a unique trace identifier." - (format #f "trace-~a" (random 1000000000))) - -(define (current-time) - "Get current timestamp." - (current-time-ns)) - -(define (current-time-ns) - "Get current time in nanoseconds (placeholder)." - 0) - -(define (eval-condition condition env situation) - "Evaluate a condition expression in the given environment." - ;; Placeholder - actual implementation in Elixir - #t) - -(define (eval-expr expr env) - "Evaluate an expression in the given environment." - ;; Placeholder - actual implementation in Elixir - expr) - -(define (collect-votes action agents) - "Collect votes from agents for an action." - ;; Placeholder - in production this is distributed - (map (lambda (a) (cons a #t)) agents)) - -(define (log-action state action votes result) - "Log an action to the consensus log." - (make-state - (state-policy-table state) - (append (state-consensus-log state) - (list `((action . ,action) - (votes . ,votes) - (result . ,result) - (timestamp . ,(current-time))))) - (state-environment state) - (state-agents state) - (state-threshold state))) - -(define (execute-action action state) - "Execute an action and return result." - ;; Placeholder - actual implementation in Elixir - 'executed) - -(define (call-module path args) - "Call a module function." - ;; Placeholder - actual implementation in Elixir - #t) - -(define (take lst n) - "Take first n elements of list." - (if (or (null? lst) (<= n 0)) - '() - (cons (car lst) (take (cdr lst) (- n 1))))) - -(define (every pred lst) - "Check if predicate holds for all elements." - (or (null? lst) - (and (pred (car lst)) - (every pred (cdr lst))))) - -(define (filter pred lst) - "Filter list by predicate." - (cond ((null? lst) '()) - ((pred (car lst)) (cons (car lst) (filter pred (cdr lst)))) - (else (filter pred (cdr lst))))) - -(define (assoc-ref alist key) - "Get value for key in association list." - (let ((pair (assoc key alist))) - (if pair (cdr pair) #f))) - - -;;; ============================================================ -;;; SECTION 8: Conformance Interface -;;; ============================================================ - -;; These functions define the interface that conforming implementations -;; must provide. - -(define (conformance-requirements) - "List of requirements for a conforming implementation." - '((must-implement - (parse "Parse source to AST") - (execute "Execute AST with state") - (trace "Produce decision trace for every execution") - (consensus "Implement consensus voting")) - (must-satisfy - (termination "All programs must terminate") - (trace-completeness "Every decision produces a trace") - (consensus-safety "No action without consensus") - (audit-integrity "Append-only consensus log")) - (may-implement - (optimization "Bytecode compilation, constant folding") - (distribution "Multi-node consensus via Raft/PBFT") - (persistence "Durable state storage")))) - - -;;; ============================================================ -;;; End of SPEC.core.scm -;;; ============================================================ diff --git a/academic/formal-verification/agda/Phronesis.agda b/academic/formal-verification/agda/Phronesis.agda index c832d95..c69a91e 100644 --- a/academic/formal-verification/agda/Phronesis.agda +++ b/academic/formal-verification/agda/Phronesis.agda @@ -35,20 +35,118 @@ data PhrType : Set where -- 2. Type Equality Decidability -- ═══════════════════════════════════════════════════════════════════════════ --- Decidable equality for types (needed for type checking) -_≟ᵗ_ : (τ₁ τ₂ : PhrType) → Dec (τ₁ ≡ τ₂) -TInt ≟ᵗ TInt = yes refl -TBool ≟ᵗ TBool = yes refl -TString ≟ᵗ TString = yes refl -TNull ≟ᵗ TNull = yes refl -TFloat ≟ᵗ TFloat = yes refl -TIP ≟ᵗ TIP = yes refl -TDateTime ≟ᵗ TDateTime = yes refl -TList τ₁ ≟ᵗ TList τ₂ with τ₁ ≟ᵗ τ₂ -... | yes refl = yes refl -... | no ¬p = no (λ { refl → ¬p refl }) --- ... other cases omitted for brevity -_ ≟ᵗ _ = no (λ ()) +-- Decidable equality for types — COMPLETE and SOUND. +-- +-- Decidability of type equality belongs to an extrinsic / gradual checking +-- layer. The intrinsic `Expr Γ τ` below does not consume it (types are static +-- indices there), but we provide a *total, sound* decision procedure in full +-- rather than the earlier incomplete stub whose catch-all `_ ≟ᵗ _ = no (λ ())` +-- was unsound (it claimed every pair of types unequal, incl. `TInt ≟ᵗ TInt`). +-- +-- The off-diagonal (distinct head constructors) must be enumerated: Agda +-- cannot refute `τ₁ ≡ τ₂` under wildcard patterns, so a single catch-all is +-- impossible here. Recursive cases (`TList`, `TRecord`) go via constructor +-- injectivity, structurally, mutually with the record-field-list decider `_≟ᶠ_`. +open import Relation.Nullary.Decidable using (map′) +open import Data.String using () renaming (_≟_ to _≟ˢ_) + +mutual + _≟ᵗ_ : (τ₁ τ₂ : PhrType) → Dec (τ₁ ≡ τ₂) + -- diagonal: nullary heads + TInt ≟ᵗ TInt = yes refl + TFloat ≟ᵗ TFloat = yes refl + TString ≟ᵗ TString = yes refl + TBool ≟ᵗ TBool = yes refl + TIP ≟ᵗ TIP = yes refl + TDateTime ≟ᵗ TDateTime = yes refl + TNull ≟ᵗ TNull = yes refl + -- diagonal: recursive heads, via constructor injectivity (structural) + TList σ ≟ᵗ TList ρ = map′ (cong TList) (λ { refl → refl }) (σ ≟ᵗ ρ) + TRecord fs ≟ᵗ TRecord gs = map′ (cong TRecord) (λ { refl → refl }) (fs ≟ᶠ gs) + -- off-diagonal: distinct head constructors are unequal + TInt ≟ᵗ TFloat = no λ() + TInt ≟ᵗ TString = no λ() + TInt ≟ᵗ TBool = no λ() + TInt ≟ᵗ TIP = no λ() + TInt ≟ᵗ TDateTime = no λ() + TInt ≟ᵗ TNull = no λ() + TInt ≟ᵗ TList _ = no λ() + TInt ≟ᵗ TRecord _ = no λ() + TFloat ≟ᵗ TInt = no λ() + TFloat ≟ᵗ TString = no λ() + TFloat ≟ᵗ TBool = no λ() + TFloat ≟ᵗ TIP = no λ() + TFloat ≟ᵗ TDateTime = no λ() + TFloat ≟ᵗ TNull = no λ() + TFloat ≟ᵗ TList _ = no λ() + TFloat ≟ᵗ TRecord _ = no λ() + TString ≟ᵗ TInt = no λ() + TString ≟ᵗ TFloat = no λ() + TString ≟ᵗ TBool = no λ() + TString ≟ᵗ TIP = no λ() + TString ≟ᵗ TDateTime = no λ() + TString ≟ᵗ TNull = no λ() + TString ≟ᵗ TList _ = no λ() + TString ≟ᵗ TRecord _ = no λ() + TBool ≟ᵗ TInt = no λ() + TBool ≟ᵗ TFloat = no λ() + TBool ≟ᵗ TString = no λ() + TBool ≟ᵗ TIP = no λ() + TBool ≟ᵗ TDateTime = no λ() + TBool ≟ᵗ TNull = no λ() + TBool ≟ᵗ TList _ = no λ() + TBool ≟ᵗ TRecord _ = no λ() + TIP ≟ᵗ TInt = no λ() + TIP ≟ᵗ TFloat = no λ() + TIP ≟ᵗ TString = no λ() + TIP ≟ᵗ TBool = no λ() + TIP ≟ᵗ TDateTime = no λ() + TIP ≟ᵗ TNull = no λ() + TIP ≟ᵗ TList _ = no λ() + TIP ≟ᵗ TRecord _ = no λ() + TDateTime ≟ᵗ TInt = no λ() + TDateTime ≟ᵗ TFloat = no λ() + TDateTime ≟ᵗ TString = no λ() + TDateTime ≟ᵗ TBool = no λ() + TDateTime ≟ᵗ TIP = no λ() + TDateTime ≟ᵗ TNull = no λ() + TDateTime ≟ᵗ TList _ = no λ() + TDateTime ≟ᵗ TRecord _ = no λ() + TNull ≟ᵗ TInt = no λ() + TNull ≟ᵗ TFloat = no λ() + TNull ≟ᵗ TString = no λ() + TNull ≟ᵗ TBool = no λ() + TNull ≟ᵗ TIP = no λ() + TNull ≟ᵗ TDateTime = no λ() + TNull ≟ᵗ TList _ = no λ() + TNull ≟ᵗ TRecord _ = no λ() + TList _ ≟ᵗ TInt = no λ() + TList _ ≟ᵗ TFloat = no λ() + TList _ ≟ᵗ TString = no λ() + TList _ ≟ᵗ TBool = no λ() + TList _ ≟ᵗ TIP = no λ() + TList _ ≟ᵗ TDateTime = no λ() + TList _ ≟ᵗ TNull = no λ() + TList _ ≟ᵗ TRecord _ = no λ() + TRecord _ ≟ᵗ TInt = no λ() + TRecord _ ≟ᵗ TFloat = no λ() + TRecord _ ≟ᵗ TString = no λ() + TRecord _ ≟ᵗ TBool = no λ() + TRecord _ ≟ᵗ TIP = no λ() + TRecord _ ≟ᵗ TDateTime = no λ() + TRecord _ ≟ᵗ TNull = no λ() + TRecord _ ≟ᵗ TList _ = no λ() + + -- Decidable equality on record field lists (mutual with _≟ᵗ_), structural. + _≟ᶠ_ : (fs gs : List (String × PhrType)) → Dec (fs ≡ gs) + [] ≟ᶠ [] = yes refl + [] ≟ᶠ (_ ∷ _) = no λ() + (_ ∷ _) ≟ᶠ [] = no λ() + ((x , σ) ∷ fs) ≟ᶠ ((y , ρ) ∷ gs) with x ≟ˢ y | σ ≟ᵗ ρ | fs ≟ᶠ gs + ... | yes refl | yes refl | yes refl = yes refl + ... | no x≢y | _ | _ = no λ { refl → x≢y refl } + ... | _ | no σ≢ρ | _ = no λ { refl → σ≢ρ refl } + ... | _ | _ | no fs≢gs = no λ { refl → fs≢gs refl } -- ═══════════════════════════════════════════════════════════════════════════ -- 3. Semantic Domain (Values indexed by Type) @@ -72,15 +170,19 @@ _ ≟ᵗ _ = no (λ ()) -- ═══════════════════════════════════════════════════════════════════════════ data Ctx : Set where - ∅ : Ctx - _,_ : Ctx → String × PhrType → Ctx + ∅ : Ctx + _,,_ : Ctx → String × PhrType → Ctx -infixl 5 _,_ +-- NOTE: context extension is `_,,_` (not `_,_`) to stay unambiguous from +-- Data.Product._,_ used for the (name × type) pair it stores. With a +-- single `_,_` in scope the mixfix parser cannot disambiguate +-- `Γ , (x , τ)` (the two operators have different fixities). +infixl 5 _,,_ -- Variable lookup (de Bruijn style would be cleaner, but using names for clarity) data _∋_∶_ : Ctx → String → PhrType → Set where - here : ∀ {Γ x τ} → (Γ , (x , τ)) ∋ x ∶ τ - there : ∀ {Γ x y τ τ'} → Γ ∋ x ∶ τ → (Γ , (y , τ')) ∋ x ∶ τ + here : ∀ {Γ x τ} → (Γ ,, (x , τ)) ∋ x ∶ τ + there : ∀ {Γ x y τ τ'} → Γ ∋ x ∶ τ → (Γ ,, (y , τ')) ∋ x ∶ τ -- ═══════════════════════════════════════════════════════════════════════════ -- 5. Intrinsically Typed Expressions @@ -130,7 +232,7 @@ infix 5 _==ᵉ_ _<ᵉ_ data Env : Ctx → Set where ε : Env ∅ - _▷_ : ∀ {Γ x τ} → Env Γ → ⟦ τ ⟧ → Env (Γ , (x , τ)) + _▷_ : ∀ {Γ x τ} → Env Γ → ⟦ τ ⟧ → Env (Γ ,, (x , τ)) infixl 5 _▷_ @@ -143,13 +245,13 @@ lookupEnv (there x) (ρ ▷ _) = lookupEnv x ρ -- 7. Denotational Semantics (Evaluation) -- ═══════════════════════════════════════════════════════════════════════════ -open import Data.Integer using (_+_; _-_; _*_; _≤ᵇ_) renaming (_+_ to _+ℤ_; _-_ to _-ℤ_; _*_ to _*ℤ_) +open import Data.Integer using (_≤ᵇ_) renaming (_+_ to _+ℤ_; _-_ to _-ℤ_; _*_ to _*ℤ_) -- Value equality (for comparison operators) -- Implemented via decidable equality per type, not postulated. -open import Data.Integer using (_≟_) renaming (_≟_ to _≟ℤ_) -open import Data.String using () renaming (_≟_ to _≟ˢ_) +open import Data.Integer using () renaming (_≟_ to _≟ℤ_) +-- (_≟ˢ_ for String is imported earlier, alongside _≟ᵗ_) open import Data.Nat using () renaming (_≟_ to _≟ⁿ_) open import Data.Bool using () renaming (_≟_ to _≟ᵇ_) @@ -198,7 +300,7 @@ mutual -- Integer less-than via the standard library ordering. _<ᵛ_ : ℤ → ℤ → Bool -a <ᵛ b = a ≤ᵇ b ∧ not (a ≡ᵛ b) +a <ᵛ b = (a ≤ᵇ b) ∧ not (_≡ᵛ_ {TInt} a b) where open import Data.Integer using (_≤ᵇ_) -- List membership via value equality. diff --git a/academic/formal-verification/agda/PhronesisEcho.agda b/academic/formal-verification/agda/PhronesisEcho.agda new file mode 100644 index 0000000..bead3a2 --- /dev/null +++ b/academic/formal-verification/agda/PhronesisEcho.agda @@ -0,0 +1,96 @@ +-- SPDX-License-Identifier: Apache-2.0 OR MIT +-- Copyright (c) 2026 Jonathan D.A. Jewell +-- +-- ===================================================================== +-- PhronesisEcho — echo-types integrated into Phronesis's semantics +-- ===================================================================== +-- +-- Phronesis is a provably-safe language for *agentic ethical reasoning*. +-- Its evaluator `eval : Env Γ → Expr Γ τ → ⟦ τ ⟧` is, like any decision +-- procedure, generally NON-INJECTIVE: many distinct situations (closed +-- expressions) collapse to the same verdict. That collapse is exactly the +-- information an auditor of an ethical decision needs back. +-- +-- hyperpolymath/echo-types provides the canonical, mechanised form of that +-- retained loss — the fiber `Echo f y := Σ A (λ x → f x ≡ y)`. Specialised +-- to the verdict map, `Echo verdict v` is the *provenance* of verdict `v`: +-- the proof-relevant record of which expressions justify it. A non-injective +-- verdict map has more than one provenance for a verdict, and (by the same +-- no-section argument echo-types makes elsewhere) the verdict alone cannot +-- recover which one fired. This module pins that correspondence so the +-- language's semantics and the echo-types formalisation share ONE notion of +-- structured loss. +-- +-- Flag stance: left at Agda's default discipline (matching Phronesis.agda), +-- importing the `--safe --without-K` `Echo`. Machine-checked against the real +-- echo-types library (registered as `echo-types`); see phronesis-formal.agda-lib. + +module PhronesisEcho where + +open import Echo using (Echo; echo-intro) +open import Phronesis + using ( PhrType; TBool; ∅; Expr; bool; _∧ᵉ_; Env; ε; eval ) + +open import Data.Bool using (Bool; true; false) +open import Data.Product using (Σ; _,_; _×_; proj₁; proj₂) +open import Relation.Binary.PropositionalEquality using (_≡_; _≢_; refl) + + +-- ===================================================================== +-- § 1. The verdict map: closed boolean evaluation as a classifier. +-- ===================================================================== +-- +-- A closed boolean Phronesis expression (a policy condition over the empty +-- context) evaluates to a Bool verdict. This is the lossy classifier whose +-- Echo carries the provenance. + +verdict : Expr ∅ TBool → Bool +verdict = eval ε + +-- The provenance of a verdict: which closed expressions justify it. +Provenance : Bool → Set +Provenance v = Echo verdict v + + +-- ===================================================================== +-- § 2. A verdict has many provenances (the loss is real and retained). +-- ===================================================================== +-- +-- Two genuinely different closed expressions both justify the verdict `true`; +-- their Echoes are distinct provenance witnesses over the same verdict. + +reason-a : Expr ∅ TBool +reason-a = bool true + +reason-b : Expr ∅ TBool +reason-b = bool true ∧ᵉ bool true + +-- Each is a provenance of `true` (echo-intro lands each in its own fiber, +-- because `verdict reason-a ≡ true` and `verdict reason-b ≡ true`). +provenance-a : Provenance true +provenance-a = echo-intro verdict reason-a + +provenance-b : Provenance true +provenance-b = echo-intro verdict reason-b + +-- The two justifications are distinct expressions (a literal vs a conjunction). +reasons-distinct : reason-a ≢ reason-b +reasons-distinct () + +-- HEADLINE: the verdict map is non-injective — the verdict `true` does NOT +-- determine its provenance. `Echo verdict true` is the object that retains, +-- and `proj₁` recovers, *which* expression justified the decision; the verdict +-- in `⟦ TBool ⟧ = Bool` has forgotten it. This is the type-level statement +-- that an ethical verdict is auditable only with its echo, not on its own. +verdict-forgets-provenance : + Σ (Expr ∅ TBool) (λ a → Σ (Expr ∅ TBool) (λ b → + (verdict a ≡ verdict b) × (a ≢ b))) +verdict-forgets-provenance = reason-a , reason-b , refl , reasons-distinct + +-- The Echo retains what the verdict drops: each provenance reproduces its +-- source expression under proj₁. +provenance-recovers-source-a : proj₁ provenance-a ≡ reason-a +provenance-recovers-source-a = refl + +provenance-recovers-source-b : proj₁ provenance-b ≡ reason-b +provenance-recovers-source-b = refl diff --git a/academic/formal-verification/agda/phronesis-formal.agda-lib b/academic/formal-verification/agda/phronesis-formal.agda-lib new file mode 100644 index 0000000..7008100 --- /dev/null +++ b/academic/formal-verification/agda/phronesis-formal.agda-lib @@ -0,0 +1,3 @@ +name: phronesis-formal +include: . +depend: standard-library echo-types