%
% memory interface
% for a 2^a x (8*B) byte-writeable ram
%

memory_interface_lemmas[a : posnat, B : posnat]: THEORY

BEGIN

  IMPORTING 
    memory_interface_types_only[a,B];

% a byte selection function for the output
  byte(i:below(B), word:wordt[a,B]) : bytet[a,B] =
    word^(8*i+7,8*i);

  word_consists_of_bytes : LEMMA
    FORALL (word1,word2:wordt):
      word1=word2 IFF
      FORALL (b:below(B)):
       byte(b,word1)=byte(b,word2);

  address_bound : LEMMA
    FORALL (address:addresst):
      bv2nat(address)<2^a;

END memory_interface_lemmas