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