autosetup: add curated summaries for OZ Arrays, EIP-712 hashing, camelCase extSload

[jar-ben]

These library functions use inline assembly (raw mload / keccak) that the
points-to analysis can't scalarize, so autosetup-generated setups that reach them
hit PTA failures and downstream blow-ups. Curated, human-reviewed CVL summaries
give sound, reusable replacements — the same mechanism as the existing
OZ_SafeERC20 / OZ_Math entries.

Changes

• OZ_Arrays.spec (new) + registry oz_arrays_unsafeMemoryAccess: models Arrays.unsafeMemoryAccess as arr[pos] for the uint256[]/bytes32[]/address[] overloads.
• EIP712.spec (new) + registry eip712_hashTypedData: deterministic, injective uninterpreted function for solady _hashTypedData / OZ _hashTypedDataV4; injectivity via a single-quantifier left-inverse ghost.
• extload.template.spec + registry extload names: add camelCase extSload/extSloads alongside the existing lowercase extsload/exttload.

Validation

Both new CVL forms were run through certoraRun.py against a real protocol scene (via-IR off): they typecheck and attach (the Arrays.unsafeMemoryAccess and _hashTypedData PTA warnings clear). function_summaries.json parses; no AutoProver-local test asserts a registry entry-count, and the OZ-Math summary tests still pass.

Dependencies & follow-ups

• Stacked on the via_ir PR (jaroslav/autosetup-no-inherit-via-ir). The curated internal summaries only attach with viaIR off, so that PR must land first.