%
% implementation byte-writeable ram
% consisting of B 2^k x 8 banks
%

bw_ram[k:nat, B:posnat]: THEORY
BEGIN
  IMPORTING 
    bw_ram_types[k,B]

% data out put together from single bytes
  bw_ram_dout_impl(bytes : [bw_ram_bankt[k,B] -> bvec[8]]) : bw_ram_wordt[k,B] =
    LAMBDA (bit : below(8*B)) : 
      bytes(div(bit,8))(mod(bit,8));
                   
  bw_ram_dout(bw_ram:bw_ramt, address:bw_ram_addresst): bw_ram_wordt = 
    LET bytes = LAMBDA (bank:bw_ram_bankt) :
                  bw_ram(bank)(address) IN
      bw_ram_dout_impl(bytes);

% bw_ram_next_conf computes the new state of the ram given the inputs
  bw_ram_next_conf(bw_ram  : bw_ramt[k,B], 
                   address : bw_ram_addresst[k,B], 
                   din     : bw_ram_wordt[k,B], 
                   bank_we : bw_ram_bank_wet[k,B]): 
    [# next_conf : bw_ramt[k,B], dout : bw_ram_wordt[k,B] #] =
    LET ram   = LAMBDA (bank:bw_ram_bankt[k,B]):
                  ram_next_conf[k,8](bw_ram(bank), 
                                address, 
                                din^(8*bank+7,8*bank), 
                                bank_we(bank)),
        bytes = LAMBDA (bank:bw_ram_bankt[k,B]) :
                  ram(bank)`dout IN
    (#
      next_conf := LAMBDA (bank:bw_ram_bankt[k,B]) : 
                     ram(bank)`next_conf,
      dout      :=  bw_ram_dout_impl[k,B](bytes)
    #);

% bw_ram2p_next_conf computes the new state of the ram given the inputs (dual port)
  bw_ram2p_next_conf(bw_ram    : bw_ramt[k,B], 
                     radr,wadr : bw_ram_addresst[k,B], 
                     din       : bw_ram_wordt[k,B], 
                     bank_we   : bw_ram_bank_wet[k,B]): 
    [# next_conf : bw_ramt[k,B], dout : bw_ram_wordt[k,B] #] =
    LET ram   = LAMBDA (bank:bw_ram_bankt[k,B]):
                  ram2p_next_conf[k,8](bw_ram(bank), 
                                       radr, wadr,
                                       din^(8*bank+7,8*bank), 
                                       bank_we(bank)),
        bytes = LAMBDA (bank:bw_ram_bankt[k,B]) :
                  ram(bank)`dout IN
    (#
      next_conf := LAMBDA (bank:bw_ram_bankt[k,B]) : 
                     ram(bank)`next_conf,
      dout      :=  bw_ram_dout_impl[k,B](bytes)
    #);

  bw_ram_dout_correct : LEMMA
    FORALL (bw_ram  : bw_ramt,
            address : bw_ram_addresst,
            din     : bw_ram_wordt,
            bank_we : bw_ram_bank_wet):
      bw_ram_next_conf(bw_ram, address, din, bank_we)`dout =
        bw_ram_dout(bw_ram,address);

END bw_ram