Journal of Formalized Mathematics
Volume 6, 1994
University of Bialystok
Copyright (c) 1994 Association of Mizar Users

### Relocatability

by
Yasushi Tanaka

MML identifier: RELOC
[ Mizar article, MML identifier index ]

```environ

vocabulary AMI_1, AMI_3, ARYTM_1, CAT_1, QC_LANG1, AMI_2, AMI_5, RELAT_1,
FUNCT_1, NAT_1, FINSET_1, ARYTM_3, FUNCT_4, BOOLE, CARD_3, PARTFUN1,
RELOC;
notation TARSKI, XBOOLE_0, SUBSET_1, XCMPLX_0, XREAL_0, CARD_3, INT_1, NAT_1,
RELAT_1, FUNCT_1, FUNCT_2, PARTFUN1, FUNCT_4, CQC_LANG, FINSET_1,
STRUCT_0, AMI_1, AMI_2, AMI_3, BINARITH, AMI_5;
constructors DOMAIN_1, BINARITH, AMI_5, MEMBERED, XBOOLE_0;
clusters AMI_1, AMI_3, AMI_5, FUNCT_1, RELSET_1, INT_1, FRAENKEL, XBOOLE_0,
MEMBERED, ZFMISC_1, NUMBERS, ORDINAL2;
requirements NUMERALS, SUBSET, BOOLE, ARITHM;

begin  :: Relocatability

reserve j, k, m for Nat;

definition
let loc be Instruction-Location of SCM , k be Nat;
func loc + k -> Instruction-Location of SCM means
:: RELOC:def 1

ex m being Nat st loc = il.m & it = il.(m+k);

func loc -' k -> Instruction-Location of SCM means
:: RELOC:def 2

ex m being Nat st loc = il.m & it = il.(m -' k);
end;

theorem :: RELOC:1
for loc being Instruction-Location of SCM ,k being Nat
holds loc + k -' k = loc;

theorem :: RELOC:2
for l1,l2 being Instruction-Location of SCM , k being Nat
holds
Start-At(l1 + k) = Start-At(l2 +k) iff Start-At l1 = Start-At l2;

theorem :: RELOC:3
for l1,l2 being Instruction-Location of SCM , k being Nat
st Start-At l1 = Start-At l2
holds
Start-At(l1 -' k) = Start-At(l2 -' k);

definition
let I be Instruction of SCM , k be Nat;
func IncAddr (I,k) -> Instruction of SCM equals
:: RELOC:def 3

goto (((@I) jump_address )@ +k) if InsCode I = 6,
if InsCode I = 7,
if InsCode I = 8
otherwise I;
end;

theorem :: RELOC:4
for k being Nat holds IncAddr(halt SCM,k) = halt SCM;

theorem :: RELOC:5
for k being Nat, a,b being Data-Location

theorem :: RELOC:6
for k being Nat, a,b being Data-Location

theorem :: RELOC:7
for k being Nat, a,b being Data-Location

theorem :: RELOC:8
for k being Nat, a,b being Data-Location

theorem :: RELOC:9
for k being Nat, a,b being Data-Location

theorem :: RELOC:10
for k being Nat,loc being Instruction-Location of SCM
holds IncAddr(goto loc,k) = goto (loc + k);

theorem :: RELOC:11
for k being Nat,loc being Instruction-Location of SCM,
a being Data-Location
holds IncAddr(a=0_goto loc,k) = a=0_goto (loc + k);

theorem :: RELOC:12
for k being Nat,loc being Instruction-Location of SCM,
a being Data-Location
holds IncAddr(a>0_goto loc,k) = a>0_goto (loc + k);

theorem :: RELOC:13
for I being Instruction of SCM, k being Nat
holds InsCode (IncAddr (I, k)) = InsCode I;

theorem :: RELOC:14
for II, I being Instruction of SCM,
k being 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;

definition
let p be programmed FinPartState of SCM , k be Nat;
func Shift ( p , k ) -> programmed FinPartState of SCM means
:: RELOC:def 4

dom it = { il.(m+k):il.m in dom p } &
for m st il.m in dom p holds it.il.(m+k) = p.il.m;
end;

theorem :: RELOC:15
for l being Instruction-Location of SCM , k being Nat,
p being programmed FinPartState of SCM st l in dom p
holds Shift(p,k).(l + k) = p.l;

theorem :: RELOC:16
for p being programmed FinPartState of SCM, k being Nat
holds dom Shift(p,k) =
{ il+k where il is Instruction-Location of SCM: il in dom p};

theorem :: RELOC:17
for p being programmed FinPartState of SCM, k being Nat
holds dom Shift(p,k) c= the Instruction-Locations of SCM;

definition
let p be programmed FinPartState of SCM, k be Nat;
func IncAddr ( p , k ) -> programmed FinPartState of SCM means
:: RELOC:def 5

dom it = dom p &
for m st il.m in dom p holds it.il.m = IncAddr(pi(p,il.m),k);
end;

theorem :: RELOC:18
for p being programmed FinPartState of SCM , k being Nat
for l being Instruction-Location of SCM st l in dom p

theorem :: RELOC:19
for i being Nat,
p being programmed FinPartState of SCM
holds

definition
let p be FinPartState of SCM , k be Nat;
func Relocated ( p, k ) -> FinPartState of SCM equals
:: RELOC:def 6

end;

theorem :: RELOC:20
for p being FinPartState of SCM

theorem :: RELOC:21
for p being FinPartState of SCM,k being Nat
holds DataPart(Relocated(p,k)) = DataPart(p);

theorem :: RELOC:22
for p being FinPartState of SCM,k being Nat

theorem :: RELOC:23
for p being FinPartState of SCM
holds dom ProgramPart(Relocated(p,k))
= { il.(j+k):il.j in dom ProgramPart(p) };

theorem :: RELOC:24
for p being FinPartState of SCM, k being Nat,
l being Instruction-Location of SCM
holds l in dom p iff l+k in dom Relocated(p,k);

theorem :: RELOC:25
for p being FinPartState of SCM , k being Nat
holds IC SCM in dom Relocated (p,k);

theorem :: RELOC:26
for p being FinPartState of SCM, k being Nat
holds IC Relocated (p,k) = (IC p) + k;

theorem :: RELOC:27
for p being FinPartState of SCM,
k being Nat,
loc being Instruction-Location of SCM,
I being Instruction of SCM
st loc in dom ProgramPart p & I = p.loc
holds IncAddr(I, k) = (Relocated (p, k)).(loc + k);

theorem :: RELOC:28
for p being FinPartState of SCM,k being Nat
holds Start-At (IC p + k) c= Relocated (p,k);

theorem :: RELOC:29
for s being data-only FinPartState of SCM,
p being FinPartState of SCM,
k being Nat st IC SCM in dom p
holds
Relocated((p +* s), k) = Relocated (p,k) +* s;

theorem :: RELOC:30
for k being Nat,
p being autonomic FinPartState of SCM ,
s1, s2 being State of SCM
st p c= s1 & Relocated (p,k) c= s2
holds p c= s1 +* s2|SCM-Data-Loc;

theorem :: RELOC:31
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);

theorem :: RELOC:32
for INS being Instruction of SCM,
s being State of SCM,
p being FinPartState of SCM,
i, j, k being Nat
st IC s = il.(j+k)
holds Exec(INS, s +* Start-At (IC s -' k))

begin :: Main theorems of Relocatability

theorem :: RELOC:33
for k being Nat
for p being autonomic FinPartState of SCM st IC SCM in dom p
for s being State of SCM st
p c= s
for i being Nat
holds (Computation (s +* Relocated (p,k))).i
= (Computation s).i +* Start-At (IC (Computation s ).i + k)
+* ProgramPart (Relocated (p,k));

theorem :: RELOC:34
for k being Nat,
p being autonomic FinPartState of SCM ,
s1, s2, s3 being State of SCM
st IC SCM in dom p & p c= s1 & Relocated (p,k) c= s2 &
s3 = s1 +* s2|SCM-Data-Loc
holds for i being 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))) &
(Computation s3).i|SCM-Data-Loc = (Computation s2).i|SCM-Data-Loc;

theorem :: RELOC:35
for p being autonomic FinPartState of SCM ,
k being Nat
st IC SCM in dom p
holds
p is halting iff Relocated (p,k) is halting;

theorem :: RELOC:36
for k being Nat
for p being autonomic FinPartState of SCM st IC SCM in dom p
for s being State of SCM st Relocated(p,k) c= s
holds
for i being 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));

theorem :: RELOC:37
for k being Nat
for p being FinPartState of SCM st IC SCM in dom p
for s being State of SCM st p c= s & Relocated(p,k) is autonomic
holds
for i being 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);

theorem :: RELOC:38
for p being FinPartState of SCM st IC SCM in dom p
for k being Nat
holds
p is autonomic iff Relocated (p,k) is autonomic;

theorem :: RELOC:39
for p being halting autonomic FinPartState of SCM st IC SCM in dom p
for k being Nat holds
DataPart(Result(p)) = DataPart(Result(Relocated(p,k)));

:: Relocatability

theorem :: RELOC:40
for F being PartFunc of FinPartSt SCM, FinPartSt SCM,
p being FinPartState of SCM st IC SCM in dom p & F is data-only
for k being Nat
holds
p computes F iff Relocated ( p,k) computes F;

```