:: Relocatability
:: by Yasushi Tanaka
::
:: Received June 16, 1994
:: Copyright (c) 1994 Association of Mizar Users

definition

canceled;
canceled;
let I be Instruction of SCM ;
let k be Element of NAT ;
func IncAddr I,k -> Instruction of SCM equals :Def3: :: RELOC:def 3
goto ((((@ I) jump_address ) @ ) + k) if InsCode I = 6
(((@ I) cond_address ) @ ) =0_goto ((((@ I) cjump_address ) @ ) + k) if InsCode I = 7
(((@ I) cond_address ) @ ) >0_goto ((((@ I) cjump_address ) @ ) + k) if InsCode I = 8
otherwise I;
correctness
coherence
( ( InsCode I = 6 implies goto ((((@ I) jump_address ) @ ) + k) is Instruction of SCM ) & ( InsCode I = 7 implies (((@ I) cond_address ) @ ) =0_goto ((((@ I) cjump_address ) @ ) + k) is Instruction of SCM ) & ( InsCode I = 8 implies (((@ I) cond_address ) @ ) >0_goto ((((@ I) cjump_address ) @ ) + k) is Instruction of SCM ) & ( not InsCode I = 6 & not InsCode I = 7 & not InsCode I = 8 implies I is Instruction of SCM ) );
consistency
for b₁ being Instruction of SCM holds
( ( InsCode I = 6 & InsCode I = 7 implies ( b₁ = goto ((((@ I) jump_address ) @ ) + k) iff b₁ = (((@ I) cond_address ) @ ) =0_goto ((((@ I) cjump_address ) @ ) + k) ) ) & ( InsCode I = 6 & InsCode I = 8 implies ( b₁ = goto ((((@ I) jump_address ) @ ) + k) iff b₁ = (((@ I) cond_address ) @ ) >0_goto ((((@ I) cjump_address ) @ ) + k) ) ) & ( InsCode I = 7 & InsCode I = 8 implies ( b₁ = (((@ I) cond_address ) @ ) =0_goto ((((@ I) cjump_address ) @ ) + k) iff b₁ = (((@ I) cond_address ) @ ) >0_goto ((((@ I) cjump_address ) @ ) + k) ) ) );
;

end;

:: deftheorem RELOC:def 1 :

canceled;

:: deftheorem RELOC:def 2 :

canceled;

:: deftheorem Def3 defines IncAddr RELOC:def 3 :

for I being Instruction of SCM
for k being Element of NAT holds
( ( InsCode I = 6 implies IncAddr I,k = goto ((((@ I) jump_address ) @ ) + k) ) & ( InsCode I = 7 implies IncAddr I,k = (((@ I) cond_address ) @ ) =0_goto ((((@ I) cjump_address ) @ ) + k) ) & ( InsCode I = 8 implies IncAddr I,k = (((@ I) cond_address ) @ ) >0_goto ((((@ I) cjump_address ) @ ) + k) ) & ( not InsCode I = 6 & not InsCode I = 7 & not InsCode I = 8 implies IncAddr I,k = I ) );

theorem :: RELOC:1

canceled;

theorem :: RELOC:2

canceled;

theorem :: RELOC:3

canceled;

theorem :: RELOC:4

for k being Element of NAT holds IncAddr (halt SCM ),k = halt SCM by Def3, AMI_5:37;

theorem Th5: :: RELOC:5

for k being Element of NAT
for a, b being Data-Location holds IncAddr (a := b),k = a := b

proof end;

theorem Th6: :: RELOC:6

for k being Element of NAT
for a, b being Data-Location holds IncAddr (AddTo a,b),k = AddTo a,b

proof end;

theorem Th7: :: RELOC:7

for k being Element of NAT
for a, b being Data-Location holds IncAddr (SubFrom a,b),k = SubFrom a,b

proof end;

theorem Th8: :: RELOC:8

for k being Element of NAT
for a, b being Data-Location holds IncAddr (MultBy a,b),k = MultBy a,b

proof end;

theorem Th9: :: RELOC:9

for k being Element of NAT
for a, b being Data-Location holds IncAddr (Divide a,b),k = Divide a,b

proof end;

theorem Th10: :: RELOC:10

for k being Element of NAT
for loc being Instruction-Location of SCM holds IncAddr (goto loc),k = goto (loc + k)

proof end;

theorem Th11: :: RELOC:11

for k being Element of NAT
for loc being Instruction-Location of SCM
for a being Data-Location holds IncAddr (a =0_goto loc),k = a =0_goto (loc + k)

proof end;

theorem Th12: :: RELOC:12

for k being Element of NAT
for loc being Instruction-Location of SCM
for a being Data-Location holds IncAddr (a >0_goto loc),k = a >0_goto (loc + k)

proof end;

theorem Th13: :: RELOC:13

for I being Instruction of SCM
for k being Element of NAT holds InsCode (IncAddr I,k) = InsCode I

proof end;

theorem Th14: :: RELOC:14

for II, I being Instruction of SCM
for k being Element of NAT st ( InsCode I = 0 or InsCode I = 1 or InsCode I = 2 or InsCode I = 3 or InsCode I = 4 or InsCode I = 5 ) & IncAddr II,k = I holds
II = I

proof end;

theorem :: RELOC:15

canceled;

theorem :: RELOC:16

canceled;

theorem :: RELOC:17

canceled;

definition

canceled;
let p be finite PartFunc of NAT ,the Instructions of SCM ;
let k be Element of NAT ;
func IncAddr p,k -> finite PartFunc of NAT ,the Instructions of SCM means :Def5: :: RELOC:def 5
( dom it = dom p & ( for m being Element of NAT st m in dom p holds
it . m = IncAddr (p /. m),k ) );
existence
ex b₁ being finite PartFunc of NAT ,the Instructions of SCM st
( dom b₁ = dom p & ( for m being Element of NAT st m in dom p holds
b₁ . m = IncAddr (p /. m),k ) )

proof end;

uniqueness
for b₁, b₂ being finite PartFunc of NAT ,the Instructions of SCM st dom b₁ = dom p & ( for m being Element of NAT st m in dom p holds
b₁ . m = IncAddr (p /. m),k ) & dom b₂ = dom p & ( for m being Element of NAT st m in dom p holds
b₂ . m = IncAddr (p /. m),k ) holds
b₁ = b₂

proof end;

end;

:: deftheorem RELOC:def 4 :

canceled;

:: deftheorem Def5 defines IncAddr RELOC:def 5 :

for p being finite PartFunc of NAT ,the Instructions of SCM
for k being Element of NAT
for b₃ being finite PartFunc of NAT ,the Instructions of SCM holds
( b₃ = IncAddr p,k iff ( dom b₃ = dom p & ( for m being Element of NAT st m in dom p holds
b₃ . m = IncAddr (p /. m),k ) ) );

theorem :: RELOC:18

for p being finite PartFunc of NAT ,the Instructions of SCM
for k, l being Element of NAT st l in dom p holds
(IncAddr p,k) . l = IncAddr (p /. l),k by Def5;

theorem Th19: :: RELOC:19

for i being Element of NAT
for p being finite PartFunc of NAT ,the Instructions of SCM holds Shift (IncAddr p,i),i = IncAddr (Shift p,i),i

proof end;

definition

let p be FinPartState of SCM ;
let k be Element of NAT ;
func Relocated p,k -> FinPartState of SCM equals :: RELOC:def 6
((Start-At ((IC p) + k)) +* [(IncAddr (Shift (ProgramPart p),k),k)]) +* (DataPart p);
correctness
coherence
((Start-At ((IC p) + k)) +* [(IncAddr (Shift (ProgramPart p),k),k)]) +* (DataPart p) is FinPartState of SCM ;
;

end;

:: deftheorem defines Relocated RELOC:def 6 :

for p being FinPartState of SCM
for k being Element of NAT holds Relocated p,k = ((Start-At ((IC p) + k)) +* [(IncAddr (Shift (ProgramPart p),k),k)]) +* (DataPart p);

theorem :: RELOC:20

canceled;

theorem Th21: :: RELOC:21

for p being FinPartState of SCM
for k being Element of NAT holds DataPart (Relocated p,k) = DataPart p

proof end;

theorem Th22: :: RELOC:22

for p being FinPartState of SCM
for k being Element of NAT holds ProgramPart (Relocated p,k) = IncAddr (Shift (ProgramPart p),k),k

proof end;

theorem Th23: :: RELOC:23

for k being Element of NAT
for p being FinPartState of SCM holds dom (ProgramPart (Relocated p,k)) = { (j + k) where j is Element of NAT : j in dom (ProgramPart p) }

proof end;

theorem Th24: :: RELOC:24

for p being FinPartState of SCM
for k being Element of NAT
for l being Instruction-Location of SCM holds
( l in dom p iff l + k in dom (Relocated p,k) )

proof end;

theorem Th25: :: RELOC:25

for p being FinPartState of SCM
for k being Element of NAT holds IC SCM in dom (Relocated p,k)

proof end;

theorem Th26: :: RELOC:26

for p being FinPartState of SCM
for k being Element of NAT holds IC (Relocated p,k) = (IC p) + k

proof end;

theorem Th27: :: RELOC:27

for p being FinPartState of SCM
for k, loc being Element of NAT
for I being Instruction of SCM st loc in dom (ProgramPart p) & I = p . loc holds
IncAddr I,k = (Relocated p,k) . (loc + k)

proof end;

theorem Th28: :: RELOC:28

for p being FinPartState of SCM
for k being Element of NAT holds Start-At ((IC p) + k) c= Relocated p,k

proof end;

theorem Th29: :: RELOC:29

for s being data-only FinPartState of SCM
for p being FinPartState of SCM
for k being Element of NAT st IC SCM in dom p holds
Relocated (p +* s),k = (Relocated p,k) +* s

proof end;

theorem Th30: :: RELOC:30

for k being Element of NAT
for p being autonomic FinPartState of SCM
for s1, s2 being State of SCM st p c= s1 & Relocated p,k c= s2 holds
p c= s1 +* (DataPart s2)

proof end;

theorem Th31: :: RELOC:31

for k being Element of NAT
for s being State of SCM holds Exec (IncAddr (CurInstr s),k),(s +* (Start-At ((IC s) + k))) = (Following s) +* (Start-At ((IC (Following s)) + k))

proof end;

theorem Th32: :: RELOC:32

for INS being Instruction of SCM
for s being State of SCM
for j, k being Element of NAT st IC s = j + k holds
Exec INS,(s +* (Start-At ((IC s) -' k))) = (Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k))

proof end;

theorem :: RELOC:33

for k being Element of NAT
for p being autonomic FinPartState of SCM st IC SCM in dom p holds
for s being State of SCM st p c= s holds
for i being Element of NAT holds Computation (s +* (Relocated p,k)),i = ((Computation s,i) +* (Start-At ((IC (Computation s,i)) + k))) +* (ProgramPart (Relocated p,k))

proof end;

Th34: for k being Element of NAT
for p being autonomic FinPartState of SCM
for s1, s2 being State of SCM st IC SCM in dom p & p c= s1 & Relocated p,k c= s2 holds
for i being Element of NAT holds
( (IC (Computation s1,i)) + k = IC (Computation s2,i) & IncAddr (CurInstr (Computation s1,i)),k = CurInstr (Computation s2,i) & (Computation s1,i) | (dom (DataPart p)) = (Computation s2,i) | (dom (DataPart (Relocated p,k))) & DataPart (Computation (s1 +* (DataPart s2)),i) = DataPart (Computation s2,i) )

proof end;

theorem :: RELOC:34

for k being Element of NAT
for p being autonomic FinPartState of SCM
for s1, s2 being State of SCM st IC SCM in dom p & p c= s1 & Relocated p,k c= s2 holds
for i being Element of NAT holds (IC (Computation s1,i)) + k = IC (Computation s2,i) by Th34;

theorem Th34B: :: RELOC:35

for k being Element of NAT
for p being autonomic FinPartState of SCM
for s1, s2 being State of SCM st IC SCM in dom p & p c= s1 & Relocated p,k c= s2 holds
for i being Element of NAT holds IncAddr (CurInstr (Computation s1,i)),k = CurInstr (Computation s2,i) by Th34;

theorem Th34C: :: RELOC:36

for k being Element of NAT
for p being autonomic FinPartState of SCM
for s1, s2 being State of SCM st IC SCM in dom p & p c= s1 & Relocated p,k c= s2 holds
for i being Element of NAT holds (Computation s1,i) | (dom (DataPart p)) = (Computation s2,i) | (dom (DataPart (Relocated p,k))) by Th34;

theorem :: RELOC:37

for k being Element of NAT
for p being autonomic FinPartState of SCM
for s1, s2, s3 being State of SCM st IC SCM in dom p & p c= s1 & Relocated p,k c= s2 & s3 = s1 +* (DataPart s2) holds
for i being Element of NAT holds DataPart (Computation s3,i) = DataPart (Computation s2,i) by Th34;

theorem Th35: :: RELOC:38

for p being autonomic FinPartState of SCM
for k being Element of NAT st IC SCM in dom p holds
( p is halting iff Relocated p,k is halting )

proof end;

theorem Th36: :: RELOC:39

for k being Element of NAT
for p being autonomic FinPartState of SCM st IC SCM in dom p holds
for s being State of SCM st Relocated p,k c= s holds
for i being Element of NAT holds Computation s,i = (((Computation (s +* p),i) +* (Start-At ((IC (Computation (s +* p),i)) + k))) +* (s | (dom (ProgramPart p)))) +* (ProgramPart (Relocated p,k))

proof end;

theorem Th37: :: RELOC:40

for k being Element of NAT
for p being FinPartState of SCM st IC SCM in dom p holds
for s being State of SCM st p c= s & Relocated p,k is autonomic holds
for i being Element of NAT holds Computation s,i = (((Computation (s +* (Relocated p,k)),i) +* (Start-At ((IC (Computation (s +* (Relocated p,k)),i)) -' k))) +* (s | (dom (ProgramPart (Relocated p,k))))) +* (ProgramPart p)

proof end;

theorem Th38: :: RELOC:41

for p being FinPartState of SCM st IC SCM in dom p holds
for k being Element of NAT holds
( p is autonomic iff Relocated p,k is autonomic )

proof end;

theorem Th39: :: RELOC:42

for p being autonomic halting FinPartState of SCM st IC SCM in dom p holds
for k being Element of NAT holds DataPart (Result p) = DataPart (Result (Relocated p,k))

proof end;

theorem :: RELOC:43

for F being PartFunc of FinPartSt SCM , FinPartSt SCM
for p being FinPartState of SCM st IC SCM in dom p & F is data-only holds
for k being Element of NAT holds
( p computes F iff Relocated p,k computes F )

proof end;