Proof: Copy By Load Example

In this example, we show how we can copy 3 values using LOAD instructions.

More precisely, we prove that

Let's prove the following theorem:

if the following are true:

the PC at time 0 = 0
instruction #0 is load dst=7 addr=6 imm=0
instruction #1 is load dst=8 addr=6 imm=1
instruction #2 is load dst=9 addr=6 imm=2
value of cell 3 at time 0 = 13
value of cell 4 at time 0 = 11
value of cell 5 at time 0 = 20
value of cell 6 at time 0 = 3

then value of cell 8 at time 3 = 11

Try out this example in the simulator:

Instructions

Memory Cells

Program Counter	Time
0	0

LW Computer Simulator

Notice how addr remains the same, and the imm is increased.

Instruction #0 copies cell #3 to cell #7. The source is the value stored in cell #6 (3) plus the imm (0).

Instruction #1 copies cell #4 to cell #8. The source is the value stored in cell #6 (3) plus the imm (1).

Instruction #2 copies cell #5 to cell #9. The source is the value stored in cell #6 (3) plus the imm (2).

To make claims about value of the cell #8 at time 3, we start at time 0, then make claims about the state at time 1, and use them to make claims about time 2, and so on.

Proof:

View as a tree | View dependent proofs | Try proving it

Given

1	the PC at time 0 = 0
2	instruction #0 is `load dst=7 addr=6 imm=0`
3	instruction #1 is `load dst=8 addr=6 imm=1`
4	instruction #2 is `load dst=9 addr=6 imm=2`
5	value of cell 3 at time 0 = 13
6	value of cell 4 at time 0 = 11
7	value of cell 5 at time 0 = 20
8	value of cell 6 at time 0 = 3

Proof Table

Comments

Please log in to add comments

#	Claim	Reason
1	value of cell 7 at time 1 = 13	if instruction #0 is `load dst=7 addr=6 imm=0` and the PC at time 0 = 0 and value of cell 6 at time 0 = 3 and value of cell 3 at time 0 = 13, then value of cell 7 at time 1 = 13 (Load 0)
2	the PC at time 1 = 1	if instruction #0 is `load dst=7 addr=6 imm=0` and the PC at time 0 = 0, then the PC at time 1 = 1 (Pc 0)
3	value of cell 3 at time 1 = 13	if instruction #0 is `load dst=7 addr=6 imm=0` and the PC at time 0 = 0 and value of cell 3 at time 0 = 13, then value of cell 3 at time 1 = 13 (Byte 3 Stays the Same 0)
4	value of cell 4 at time 1 = 11	if instruction #0 is `load dst=7 addr=6 imm=0` and the PC at time 0 = 0 and value of cell 4 at time 0 = 11, then value of cell 4 at time 1 = 11 (Byte 4 Stays the Same 0)
5	value of cell 5 at time 1 = 20	if instruction #0 is `load dst=7 addr=6 imm=0` and the PC at time 0 = 0 and value of cell 5 at time 0 = 20, then value of cell 5 at time 1 = 20 (Byte 5 Stays the Same 0)
6	value of cell 6 at time 1 = 3	if instruction #0 is `load dst=7 addr=6 imm=0` and the PC at time 0 = 0 and value of cell 6 at time 0 = 3, then value of cell 6 at time 1 = 3 (Byte 6 Stays the Same 0)
7	value of cell 8 at time 2 = 11	if instruction #1 is `load dst=8 addr=6 imm=1` and the PC at time 1 = 1 and value of cell 6 at time 1 = 3 and value of cell 4 at time 1 = 11, then value of cell 8 at time 2 = 11 (Load 1)
8	the PC at time 2 = 2	if instruction #1 is `load dst=8 addr=6 imm=1` and the PC at time 1 = 1, then the PC at time 2 = 2 (Pc 1)
9	value of cell 3 at time 2 = 13	if instruction #1 is `load dst=8 addr=6 imm=1` and the PC at time 1 = 1 and value of cell 3 at time 1 = 13, then value of cell 3 at time 2 = 13 (Byte 3 Stays the Same 1)
10	value of cell 4 at time 2 = 11	if instruction #1 is `load dst=8 addr=6 imm=1` and the PC at time 1 = 1 and value of cell 4 at time 1 = 11, then value of cell 4 at time 2 = 11 (Byte 4 Stays the Same 1)
11	value of cell 5 at time 2 = 20	if instruction #1 is `load dst=8 addr=6 imm=1` and the PC at time 1 = 1 and value of cell 5 at time 1 = 20, then value of cell 5 at time 2 = 20 (Byte 5 Stays the Same 1)
12	value of cell 6 at time 2 = 3	if instruction #1 is `load dst=8 addr=6 imm=1` and the PC at time 1 = 1 and value of cell 6 at time 1 = 3, then value of cell 6 at time 2 = 3 (Byte 6 Stays the Same 1)
13	value of cell 7 at time 2 = 13	if instruction #1 is `load dst=8 addr=6 imm=1` and the PC at time 1 = 1 and value of cell 7 at time 1 = 13, then value of cell 7 at time 2 = 13 (Byte 7 Stays the Same 1)
14	value of cell 9 at time 3 = 20	if instruction #2 is `load dst=9 addr=6 imm=2` and the PC at time 2 = 2 and value of cell 6 at time 2 = 3 and value of cell 5 at time 2 = 20, then value of cell 9 at time 3 = 20 (Load 2)
15	the PC at time 3 = 3	if instruction #2 is `load dst=9 addr=6 imm=2` and the PC at time 2 = 2, then the PC at time 3 = 3 (Pc 2)
16	value of cell 3 at time 3 = 13	if instruction #2 is `load dst=9 addr=6 imm=2` and the PC at time 2 = 2 and value of cell 3 at time 2 = 13, then value of cell 3 at time 3 = 13 (Byte 3 Stays the Same 2)
17	value of cell 4 at time 3 = 11	if instruction #2 is `load dst=9 addr=6 imm=2` and the PC at time 2 = 2 and value of cell 4 at time 2 = 11, then value of cell 4 at time 3 = 11 (Byte 4 Stays the Same 2)
18	value of cell 5 at time 3 = 20	if instruction #2 is `load dst=9 addr=6 imm=2` and the PC at time 2 = 2 and value of cell 5 at time 2 = 20, then value of cell 5 at time 3 = 20 (Byte 5 Stays the Same 2)
19	value of cell 6 at time 3 = 3	if instruction #2 is `load dst=9 addr=6 imm=2` and the PC at time 2 = 2 and value of cell 6 at time 2 = 3, then value of cell 6 at time 3 = 3 (Byte 6 Stays the Same 2)
20	value of cell 7 at time 3 = 13	if instruction #2 is `load dst=9 addr=6 imm=2` and the PC at time 2 = 2 and value of cell 7 at time 2 = 13, then value of cell 7 at time 3 = 13 (Byte 7 Stays the Same 2)
21	value of cell 8 at time 3 = 11	if instruction #2 is `load dst=9 addr=6 imm=2` and the PC at time 2 = 2 and value of cell 8 at time 2 = 11, then value of cell 8 at time 3 = 11 (Byte 8 Stays the Same 2)