From 770ed26952fd8b6de920669bb6564cf16ac7f6d4 Mon Sep 17 00:00:00 2001 From: Robert Allan James Date: Fri, 14 Aug 2026 14:43:55 -0400 Subject: [PATCH] proof/: add StarForth_ACL_Words.thy (acl_words.c coverage) Fills the gap the existing ACL_*.thy policy theories deliberately don't cover: the six plain field-accessor getters (ACL-MODE@, ACL-PINNED?, ACL-TTL@, ACL-ALLOW@, ACL-HEAT@, ACL-WORD-ID) and ACL-INIT-PRIMITIVES (dictionary-wide bulk reset of unpinned entries). The mutating words (ACL-PIN, ACL-MODE!, ACL-TTL!, ACL-ALLOW!, ACL-INHERIT) were already modelled word-for-word in ACL_Pin_Monotone.thy / ACL_Inherit_Clears_Pin.thy and are cross-referenced, not duplicated. ACL-INIT-PRIMITIVES models cleanly despite the C using a raw ->link linked-list walk: the abstract word_id-indexed dictionary expresses "for every entry" directly, without needing the pointer-chasing gap already flagged for TRAVERSE/FIND elsewhere. --- proof/ROOT | 1 + proof/StarForth_ACL_Words.thy | 177 ++++++++++++++++++++++++++++++++++ 2 files changed, 178 insertions(+) create mode 100644 proof/StarForth_ACL_Words.thy diff --git a/proof/ROOT b/proof/ROOT index 6583b69..d6ca4f9 100644 --- a/proof/ROOT +++ b/proof/ROOT @@ -37,3 +37,4 @@ session "StarForth" = "HOL-Library" + ACL_TTL_Bounded ACL_Emergency_Bypass ACL_No_Escalation + StarForth_ACL_Words diff --git a/proof/StarForth_ACL_Words.thy b/proof/StarForth_ACL_Words.thy new file mode 100644 index 0000000..7fff783 --- /dev/null +++ b/proof/StarForth_ACL_Words.thy @@ -0,0 +1,177 @@ +theory StarForth_ACL_Words + imports StarForth_Base ACL_Pin_Monotone ACL_Inherit_Clears_Pin +begin + +(* ========================================================================= + Mirrors: src/word_source/acl_words.c + Registers: ACL-MODE@ ACL-MODE! ACL-PINNED? ACL-TTL@ ACL-TTL! ACL-ALLOW@ + ACL-ALLOW! ACL-HEAT@ ACL-WORD-ID ACL-PIN ACL-INHERIT + ACL-INIT-PRIMITIVES + + ── Relationship to the existing ACL_*.thy files ──────────────────────── + The mutating half of this file is ALREADY modelled, word-for-word, by + the dedicated ACL policy theories -- not duplicated here, only + cross-referenced: + ACL-PIN -> ACL_Pin_Monotone.acl_pin (forth_acl_pin) + ACL-MODE! -> ACL_Pin_Monotone.acl_mode_store (forth_acl_mode_store) + ACL-TTL! -> ACL_Pin_Monotone.acl_ttl_store (forth_acl_ttl_store) + ACL-ALLOW! -> ACL_Pin_Monotone.acl_allow_store (forth_acl_allow_store) + ACL-INHERIT -> ACL_Inherit_Clears_Pin.acl_inherit_entry + (both forth_acl_inherit AND the direct-C-call + acl_inherit_entry() are the SAME function in the C -- + acl_words.c:265-277 is a thin stack-popping wrapper + around acl_words.c:314-321 -- so one theory covers both.) + + This file adds what those theories deliberately don't cover: the six + plain field-accessor GETTERS (ACL-MODE@, ACL-PINNED?, ACL-TTL@, + ACL-ALLOW@, ACL-HEAT@, ACL-WORD-ID) and ACL-INIT-PRIMITIVES (the + dictionary-wide bulk reset), neither of which any existing theory + states. + + ── XT-pop plumbing -- NOT MODELLED, same gap as CFA/`>BODY` ──────────── + Every one of these words' actual FORTH-level bodies starts by popping an + XT and casting it to `DictEntry*` (`pop_xt`, acl_words.c:51-66) -- the + identical "cast cell_t <-> DictEntry*" gap already named in + StarForth_Dictionary_Manipulation_Words.thy (`cfa_not_modelled` et al.): + the abstract dictionary is word_id-indexed with no raw-pointer + counterpart. Exactly like ACL_Pin_Monotone/ACL_Inherit_Clears_Pin + already do, the definitions below operate directly on a `dict_entry` + (or, for ACL-INIT-PRIMITIVES, the whole `vm_state`'s dictionary) -- + modelling "what the word does once it already has the entry", not the + stack-popping/pointer-cast step that gets it there. Stack-underflow + guards (`vm->dsp < 1` etc.) are likewise not modelled here for the same + reason: they guard the unmodelled pop, not any field transition. + ======================================================================== *) + +(* ── Field-accessor getters ( xt -- value ), modelled as dict_entry \ cell ── *) + +definition acl_mode_fetch :: "dict_entry \ cell" where + "acl_mode_fetch e = word_of_nat (de_acl_mode e)" + +definition acl_pinned_query :: "dict_entry \ cell" where + "acl_pinned_query e = to_forth_bool (de_acl_pinned e)" + +definition acl_ttl_fetch :: "dict_entry \ cell" where + "acl_ttl_fetch e = word_of_nat (de_acl_ttl e)" + +definition acl_allow_fetch :: "dict_entry \ cell" where + "acl_allow_fetch e = to_forth_bool (de_acl_allow e)" + +definition acl_heat_fetch :: "dict_entry \ cell" where + "acl_heat_fetch e = de_heat e" + +definition acl_word_id_fetch :: "dict_entry \ cell" where + "acl_word_id_fetch e = word_of_nat (de_word_id e)" + +(* ── Getter/setter roundtrips against the ACL_Pin_Monotone definitions ──── *) + +lemma pinned_query_true_iff_pinned: + "acl_pinned_query e = -1 \ de_acl_pinned e" + by (simp add: acl_pinned_query_def to_forth_bool_eq) + +lemma pinned_query_after_pin: + "acl_pinned_query (acl_pin e) = -1" + by (simp add: acl_pinned_query_def acl_pin_def) + +lemma mode_fetch_after_store_unpinned: + assumes "\ de_acl_pinned e" + shows "acl_mode_fetch (acl_mode_store m e) = word_of_nat m" + using assms by (simp add: acl_mode_fetch_def acl_mode_store_def) + +lemma mode_fetch_after_store_pinned_unchanged: + assumes "de_acl_pinned e" + shows "acl_mode_fetch (acl_mode_store m e) = acl_mode_fetch e" + using assms by (simp add: acl_mode_store_def) + +lemma ttl_fetch_after_store_unpinned: + assumes "\ de_acl_pinned e" + shows "acl_ttl_fetch (acl_ttl_store n e) = word_of_nat n" + using assms by (simp add: acl_ttl_fetch_def acl_ttl_store_def) + +lemma ttl_fetch_after_store_pinned_unchanged: + assumes "de_acl_pinned e" + shows "acl_ttl_fetch (acl_ttl_store n e) = acl_ttl_fetch e" + using assms by (simp add: acl_ttl_store_def) + +lemma allow_fetch_after_store_unpinned: + assumes "\ de_acl_pinned e" + shows "acl_allow_fetch (acl_allow_store flag e) = to_forth_bool flag" + using assms by (simp add: acl_allow_fetch_def acl_allow_store_def) + +lemma allow_fetch_after_store_pinned_unchanged: + assumes "de_acl_pinned e" + shows "acl_allow_fetch (acl_allow_store flag e) = acl_allow_fetch e" + using assms by (simp add: acl_allow_store_def) + +(* Getters touch no field -- trivially true by construction (they take a + dict_entry and return a cell, not a dict_entry), stated once for the + record so the "getters are read-only" property is an explicit lemma + rather than an unstated assumption. *) +lemma word_id_fetch_after_pin_unchanged: + "acl_word_id_fetch (acl_pin e) = acl_word_id_fetch e" + by (simp add: acl_word_id_fetch_def acl_pin_def) + +lemma heat_fetch_after_pin_unchanged: + "acl_heat_fetch (acl_pin e) = acl_heat_fetch e" + by (simp add: acl_heat_fetch_def acl_pin_def) + +(* ── ACL-INIT-PRIMITIVES ( -- ) : dictionary-wide bulk reset ─────────────── *) +(* C (forth_acl_init_primitives): walks vm->latest's ->link chain; for every + entry NOT pinned, sets acl_ttl=0, acl_allow=1, acl_mode=ACL_MODE_TTL. + Pinned entries are left untouched. No stack effect. + + The C walk is a raw linked-list traversal (gap already named elsewhere: + dictionary_manipulation_words.c's raw-pointer navigation). The abstract + `dictionary :: nat \ dict_entry option` model sidesteps that gap + entirely here -- unlike TRAVERSE/FIND/etc., which need the actual + pointer-chasing mechanics, ACL-INIT-PRIMITIVES only needs "for every + entry in the dictionary", which the word_id-indexed model expresses + directly and arguably MORE faithfully than reasoning about ->link + pointer arithmetic would. *) + +definition acl_init_reset :: "dict_entry \ dict_entry" where + "acl_init_reset e = + (if de_acl_pinned e then e + else e\de_acl_ttl := 0, de_acl_allow := True, de_acl_mode := ACL_MODE_TTL\)" + +definition forth_acl_init_primitives :: "vm_state \ vm_state" where + "forth_acl_init_primitives vm = + vm\dictionary := (\wid. map_option acl_init_reset (dictionary vm wid))\" + +lemma init_primitives_pinned_untouched: + assumes "dictionary vm wid = Some e" + assumes "de_acl_pinned e" + shows "dictionary (forth_acl_init_primitives vm) wid = Some e" + using assms by (simp add: forth_acl_init_primitives_def acl_init_reset_def) + +lemma init_primitives_unpinned_reset: + assumes "dictionary vm wid = Some e" + assumes "\ de_acl_pinned e" + shows "dictionary (forth_acl_init_primitives vm) wid = + Some (e\de_acl_ttl := 0, de_acl_allow := True, de_acl_mode := ACL_MODE_TTL\)" + using assms by (simp add: forth_acl_init_primitives_def acl_init_reset_def) + +lemma init_primitives_preserves_absence: + assumes "dictionary vm wid = None" + shows "dictionary (forth_acl_init_primitives vm) wid = None" + using assms by (simp add: forth_acl_init_primitives_def) + +lemma init_primitives_never_pins: + assumes "dictionary vm wid = Some e" + shows "de_acl_pinned e \ + (\e'. dictionary (forth_acl_init_primitives vm) wid = Some e' \ de_acl_pinned e')" + using assms by (auto simp: forth_acl_init_primitives_def acl_init_reset_def) + +lemma init_primitives_data_stack_unchanged: + "data_stack (forth_acl_init_primitives vm) = data_stack vm" + by (simp add: forth_acl_init_primitives_def) + +lemma init_primitives_never_errors: + "vm_error (forth_acl_init_primitives vm) = vm_error vm" + by (simp add: forth_acl_init_primitives_def) + +lemma init_primitives_preserves_latest: + "latest_id (forth_acl_init_primitives vm) = latest_id vm" + by (simp add: forth_acl_init_primitives_def) + +end