Skip to content

Commit 654dd77

Browse files
hyperpolymathclaude
hyperpolymath
and
claude
committed
Grammar v0.5.0: Harvard Sentinel — runtime integrity verification
Section 21: Harvard Sentinel - sentinel_decl: @sentinel name = { grammar_hash, type_rules_hash, invariants } Lives in Data Language — total, pure, cannot be tampered without parse error - Sentinel-guarded agents: agent X @sentinel(name) { } Runtime verifies sentinel hashes before control block executes - Attested spawn: spawn attested Worker(...) Parent demands child's sentinel matches — chain of trust between agents - verify_integrity(sentinel) expression — @ToTal check, returns Bool - Cross-agent attestation protocol pattern for session types Invariant 6 (Integrity): sentinel is Data, protected by the grammar it monitors. Circular but productively so — like a TPM measurement chain. Threat model: humans can't attack (can't write 007 at scale). Compromised agents can't attack (sentinel catches them). Tampering with sentinel requires breaking grammar = parse error. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
1 parent c8cc182 commit 654dd77

1 file changed

Lines changed: 141 additions & 2 deletions

File tree

‎spec/grammar.ebnf‎

Lines changed: 141 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -2,7 +2,7 @@
22
(* Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) *)
33
(* *)
44
(* 007 Agent Meta-Language — Formal Grammar (EBNF) *)
5-
(* Version: 0.4.0-draft *)
5+
(* Version: 0.5.0-draft *)
66
(* Date: 2026-03-24 *)
77
(* *)
88
(* INVARIANT 1 (Harvard Architecture): *)
@@ -901,7 +901,138 @@ control_expr = (* ... existing alternatives ... *)
901901
(* The result is DATA (Harvard-separated, immutable). *)
902902
903903
(* ========================================================= *)
904-
(* END OF GRAMMAR — VERSION 0.4.0-draft *)
904+
(* 21. HARVARD SENTINEL — Runtime integrity verification *)
905+
(* ========================================================= *)
906+
(* The Harvard Architecture provides compile-time safety: *)
907+
(* parse errors catch syntactic violations, type errors catch *)
908+
(* type-level violations. But what if someone tampers with *)
909+
(* the grammar or type checker ITSELF? *)
910+
(* *)
911+
(* The sentinel is a Data-language construct that hashes the *)
912+
(* grammar rules and type judgements. Because it lives in *)
913+
(* Data, it is total, pure, and Harvard-protected — it *)
914+
(* cannot be tampered with without breaking the grammar, *)
915+
(* which is a parse error. *)
916+
(* *)
917+
(* Threat model: humans can't attack because they can't *)
918+
(* write 007 at scale. Compromised agents can't attack *)
919+
(* because the sentinel catches them. The only vector is *)
920+
(* compromising the sentinel itself, but the sentinel is *)
921+
(* Data, protected by the grammar it monitors. *)
922+
(* *)
923+
(* This is circular, but productively so — like a TPM whose *)
924+
(* measurement chain includes itself. *)
925+
926+
(* --------------------------------------------------------- *)
927+
(* 21.1 SENTINEL DECLARATION — integrity hash set *)
928+
(* --------------------------------------------------------- *)
929+
(* A sentinel is a @total data block containing hashes of *)
930+
(* grammar rules, type checker judgements, and invariants. *)
931+
(* It is evaluated at compile time (total = guaranteed to *)
932+
(* terminate) and stored as immutable Data. *)
933+
934+
sentinel_decl = "@sentinel" , ident , "=" ,
935+
"{" , sentinel_fields , "}" ;
936+
937+
sentinel_fields = sentinel_field , { "," , sentinel_field } , [ "," ] ;
938+
939+
sentinel_field = "grammar_hash" , ":" , sentinel_hash_call
940+
| "type_rules_hash" , ":" , sentinel_hash_call
941+
| "invariant" , ":" , sentinel_invariant_list
942+
| ident , ":" , data_expr ;
943+
944+
sentinel_hash_call = "hash_grammar" , "(" , ")"
945+
| "hash_type_rules" , "(" , ")"
946+
| "hash_invariant" , "(" , string_literal , ")" ;
947+
948+
sentinel_invariant_list = "[" , sentinel_hash_call ,
949+
{ "," , sentinel_hash_call } , [ "," ] , "]" ;
950+
951+
(* Example: *)
952+
(* @sentinel integrity = { *)
953+
(* grammar_hash: hash_grammar(), *)
954+
(* type_rules_hash: hash_type_rules(), *)
955+
(* invariant: [ *)
956+
(* hash_invariant("harvard_separation"), *)
957+
(* hash_invariant("hermeneutic_data_only"), *)
958+
(* hash_invariant("economic_boundary"), *)
959+
(* hash_invariant("kategoria_harvard") *)
960+
(* ] *)
961+
(* } *)
962+
963+
(* --------------------------------------------------------- *)
964+
(* 21.2 SENTINEL-GUARDED AGENTS *)
965+
(* --------------------------------------------------------- *)
966+
(* An agent may declare a sentinel guard. Before the agent's *)
967+
(* control block executes, the runtime verifies the sentinel *)
968+
(* hashes match the actual grammar and type rules. If ANY *)
969+
(* mismatch is detected, the agent REFUSES TO START. *)
970+
(* This is not a type error — it is a RUNTIME HALT. *)
971+
972+
agent_decl = "agent" , agent_name , [ "(" , agent_params , ")" ] ,
973+
[ "implements" , protocol_role_list ] ,
974+
[ "on" , "locale" , locale_expr ] ,
975+
[ "@sentinel" , "(" , ident , ")" ] ,
976+
"{" , agent_body , "}" ;
977+
978+
(* --------------------------------------------------------- *)
979+
(* 21.3 ATTESTED SPAWN — Chain of trust *)
980+
(* --------------------------------------------------------- *)
981+
(* When spawning with `attested`, the parent agent demands *)
982+
(* that the child's sentinel hash matches its own. If the *)
983+
(* child has been compiled with a different grammar or type *)
984+
(* checker (i.e., tampered), the spawn FAILS. *)
985+
(* *)
986+
(* This creates a chain of trust between agents. Every agent *)
987+
(* in the chain has verified integrity. A compromised agent *)
988+
(* cannot join the chain. *)
989+
990+
spawn_stmt = [ "linear" ] , "let" , ident , "=" ,
991+
"spawn" , [ "attested" ] , agent_name ,
992+
"(" , spawn_args , ")" ;
993+
994+
(* --------------------------------------------------------- *)
995+
(* 21.4 INTEGRITY VERIFICATION EXPRESSION *)
996+
(* --------------------------------------------------------- *)
997+
(* verify_integrity() is a @total Data function that checks *)
998+
(* a sentinel against the current runtime. Returns Bool. *)
999+
(* Because it is @total and Data, it cannot be suppressed, *)
1000+
(* cannot lie (deterministic), and cannot be tampered with *)
1001+
(* without breaking the grammar. *)
1002+
1003+
control_expr = (* ... existing alternatives ... *)
1004+
| "verify_integrity" , "(" , ident , ")" ;
1005+
1006+
(* verify_integrity(sentinel_name) → Bool *)
1007+
(* Returns true if all sentinel hashes match the runtime. *)
1008+
(* Returns false if ANY hash mismatches (tampered grammar, *)
1009+
(* modified type rules, broken invariants). *)
1010+
(* This is a Data expression despite appearing in Control — *)
1011+
(* it performs no side effects, only reads immutable state. *)
1012+
1013+
(* --------------------------------------------------------- *)
1014+
(* 21.5 CROSS-AGENT ATTESTATION PROTOCOL *)
1015+
(* --------------------------------------------------------- *)
1016+
(* Agents may exchange sentinel hashes as part of session *)
1017+
(* type protocols. This extends the chain of trust to *)
1018+
(* multi-agent choreographies. *)
1019+
1020+
(* Example protocol with attestation: *)
1021+
(* session protocol SecureReview { *)
1022+
(* Reviewer -> Author : Attest(sentinel_hash: String) *)
1023+
(* Author -> Reviewer : Attest(sentinel_hash: String) *)
1024+
(* branch by Reviewer { *)
1025+
(* | proceed given { hashes_match: true } -> { *)
1026+
(* Reviewer -> Author : Feedback(score: Int) *)
1027+
(* } *)
1028+
(* | abort given { hashes_match: false } -> { *)
1029+
(* Reviewer -> Author : Abort(reason: String) *)
1030+
(* } *)
1031+
(* } *)
1032+
(* } *)
1033+
1034+
(* ========================================================= *)
1035+
(* END OF GRAMMAR — VERSION 0.5.0-draft *)
9051036
(* ========================================================= *)
9061037
(* *)
9071038
(* INVARIANT 1 (Harvard): data_expr is a strict subset that *)
@@ -932,6 +1063,14 @@ control_expr = (* ... existing alternatives ... *)
9321063
(* separated — they contain only Data expressions, not *)
9331064
(* Control. The type system cannot inject side effects. *)
9341065
(* *)
1066+
(* *)
1067+
(* INVARIANT 6 (Integrity): The Harvard sentinel lives in *)
1068+
(* Data. It hashes the grammar and type rules. Because it is *)
1069+
(* Data, it is total, pure, and Harvard-protected. Tampering *)
1070+
(* with the sentinel requires breaking the grammar, which is *)
1071+
(* a parse error. Attested spawn creates chains of trust *)
1072+
(* between agents — a compromised agent cannot join the chain. *)
1073+
(* *)
9351074
(* FIVE FACETS (language family convergence): *)
9361075
(* 007 — computation as interpretation (hermeneutic) *)
9371076
(* Eclexia — computation as economics (shadow prices) *)

0 commit comments

Comments
 (0)