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.
