bitbitjump-maude: 8337131f88fb6dc98f3bd6957be3f760b7b4e3dc

     1: --- A pure implementation of BitBitJump, a "One
     2: --- Instruction Set Computer". A BBJ machine has an
     3: --- array of bits as memory (here we use bit shifting
     4: --- on a Natural number), a word length (here we use 8)
     5: --- and a program counter (which we'll call N).
     6: --- The key is that the memory is interpreted as both
     7: --- an array of bits and an array of words at different
     8: --- points in the instruction.
     9: --- The instruction is "bitbitjump", which is applied
    10: --- over and over. The algorithm is simple:
    11: ---  * Read the Nth and (N+1)th words from memory; call
    12: ---    their values X and Y.
    13: ---  * Read the Xth bit from memory; call its value Z.
    14: ---  * Set the value of the Yth bit in memory to Z.
    15: ---  * Read the (N+2)th word from memory; call its value
    16: ---  * N.
    17: --- This implementation is "pure" because it cannot do
    18: --- I/O, and it matches the original sematics of
    19: --- BitBitJump.
    20: mod BITBITJUMP is
    21: 	protecting NAT .
    22: 	protecting BOOL .
    23: 
    24: 	vars A B C Mem PC : Nat .
    25: 	var M : Machine .
    26: 
    27: 	sort Machine .
    28: 	op mac : Nat Nat -> Machine [ctor] .
    29: 
    30: 	--- Clears the bits less significant than or equal to the address
    31: 	op _above_ : Nat Nat -> Nat .
    32: 	eq (A) above (B) = (A >> B) << B .
    33: 
    34: 	--- Clears the bits more significant than or equal to the address
    35: 	op _below_ : Nat Nat -> Nat .
    36: 	eq A below 0 = 0 .
    37: 	eq A below B = A rem (1 << B) .
    38: 
    39: 	--- Read a bit from the given address
    40: 	op _[_] : Nat Nat -> Nat .
    41: 	eq A[0] = A rem 2 .
    42: 	eq A[s(B)] = (A >> 1)[B] .
    43: 
    44: 	--- Read an address from the given address
    45: 	op _{_} : Nat Nat -> Nat .
    46: 	eq A{0} = A rem 256 .
    47: 	eq A{s(B)} = (A >> 8){B} .
    48: 
    49: 	op _[_:=_] : Nat Nat Nat -> Nat .
    50: 	eq A[B := C] = ((A >> (B + 1)) << (B + 1)) + (C << B) + (A rem (1 << B)) .
    51: 
    52: 	--- Pure ByteByteJump only has one instruction.
    53: 	--- We read addresses from PC and PC+1, and copy the
    54: 	--- bit at the former to the latter. We then set PC
    55: 	--- to the address at PC+2
    56: 	op bitbit : Machine -> Machine .
    57: 	eq bitbit(mac(Mem, PC)) = mac(Mem[Mem{PC + 1} := Mem[Mem{PC}]], PC) .
    58: 	op jump : Machine -> Machine .
    59: 	eq jump(mac(Mem, PC)) = mac(Mem, Mem{PC + 2}) .
    60: 	op step : Machine Nat -> Machine .
    61: 	eq step(M, 0) = M .
    62: 	ceq step(mac(A, B), s(C)) = mac(A, B) if jump(bitbit(mac(A, B))) == mac(A, B) .
    63: 	ceq step(mac(A, B), s(C)) = step(jump(bitbit(mac(A, B))), C) if jump(bitbit(mac(A, B))) =/= mac(A, B) .
    64: 
    65: endm