Documentation

CatCryptCore.Core.Location

Memory Locations #

This file defines memory locations for stateful computations.

source
structure CatCrypt.Core.Location :
Type 1

Location identifier with type information. Note: We fix ty at Type (universe 0) to avoid universe polymorphism issues that would otherwise require complex universe unification in invariant proofs. This is sufficient for cryptographic applications where location types are typically finite types like Bool, Fin n, BitVec n, etc.

Instances For
    source
    @[reducible, inline]
    abbrev CatCrypt.Core.LocSet :
    Type

    A set of locations

    Equations
    Instances For
      source
      @[implicit_reducible]
      noncomputable instance CatCrypt.Core.Location.instDecidableEq :
      DecidableEq Location

      We consider two locations equal if they have the same id. Note: This is a weaker notion that ignores type equality, which is appropriate for our heap model where location ids are unique.

      Equations