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 \<Rightarrow> cell ── *)

definition acl_mode_fetch :: "dict_entry \<Rightarrow> cell" where
  "acl_mode_fetch e = word_of_nat (de_acl_mode e)"

definition acl_pinned_query :: "dict_entry \<Rightarrow> cell" where
  "acl_pinned_query e = to_forth_bool (de_acl_pinned e)"

definition acl_ttl_fetch :: "dict_entry \<Rightarrow> cell" where
  "acl_ttl_fetch e = word_of_nat (de_acl_ttl e)"

definition acl_allow_fetch :: "dict_entry \<Rightarrow> cell" where
  "acl_allow_fetch e = to_forth_bool (de_acl_allow e)"

definition acl_heat_fetch :: "dict_entry \<Rightarrow> cell" where
  "acl_heat_fetch e = de_heat e"

definition acl_word_id_fetch :: "dict_entry \<Rightarrow> 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 \<longleftrightarrow> 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 "\<not> 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 "\<not> 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 "\<not> 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 \<Rightarrow> 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 \<Rightarrow> dict_entry" where
  "acl_init_reset e =
     (if de_acl_pinned e then e
      else e\<lparr>de_acl_ttl := 0, de_acl_allow := True, de_acl_mode := ACL_MODE_TTL\<rparr>)"

definition forth_acl_init_primitives :: "vm_state \<Rightarrow> vm_state" where
  "forth_acl_init_primitives vm =
     vm\<lparr>dictionary := (\<lambda>wid. map_option acl_init_reset (dictionary vm wid))\<rparr>"

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 "\<not> de_acl_pinned e"
  shows "dictionary (forth_acl_init_primitives vm) wid =
           Some (e\<lparr>de_acl_ttl := 0, de_acl_allow := True, de_acl_mode := ACL_MODE_TTL\<rparr>)"
  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 \<longleftrightarrow>
         (\<exists>e'. dictionary (forth_acl_init_primitives vm) wid = Some e' \<and> 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
