qed.
*)
-(*
(* parametrizzazione dell'enunciato del teorema *)
(* dimostrazione senza svolgimento degli stati *)
-lemma dTest_HCS08_sReverse_aux ≝
+nlemma dTest_HCS08_sReverse_aux ≝
λt:memory_impl.λstring:list byte8.
(* 1) la stringa deve avere una lunghezza ∈ [0,3072] *)
(byte8_bounded_strlen string 〈〈x0,xC〉:〈x0,x0〉〉) ∧
qed.
*)
-definition sReverseCalc ≝
+ndefinition sReverseCalc ≝
λstring:list byte8.
match execute HCS08 MEM_TREE
(TickOK ? (dTest_HCS08_sReverse_status MEM_TREE 〈x0,x0〉 〈〈x0,xD〉:〈x4,xB〉〉 (byte8_strlen string) string))
| TickOK s ⇒ Some ? (set_mem_desc HCS08 MEM_TREE s (load_from_source_at MEM_TREE (get_mem_desc HCS08 MEM_TREE s) dTest_zeros 〈〈x0,xD〉:〈x0,x0〉〉))
].
-definition sReverseNoCalc ≝
+ndefinition sReverseNoCalc ≝
λstring:list byte8.
Some ? (set_pc_reg HCS08 MEM_TREE
(dTest_HCS08_sReverse_status MEM_TREE (fst ?? (shr_b8 (w16h (byte8_strlen string))))
(byte8_strlen string) (reverse_list ? string))
(mk_word16 (mk_byte8 x1 x9) (mk_byte8 x2 xB))).
-definition sReverseCalc32 ≝ sReverseCalc dTest_random_32.
-definition sReverseCalc64 ≝ sReverseCalc dTest_random_64.
-definition sReverseCalc128 ≝ sReverseCalc dTest_random_128.
-definition sReverseCalc256 ≝ sReverseCalc dTest_random_256.
-definition sReverseCalc512 ≝ sReverseCalc dTest_random_512.
-definition sReverseCalc1024 ≝ sReverseCalc dTest_random_1024.
-definition sReverseCalc2048 ≝ sReverseCalc dTest_random_2048.
-definition sReverseCalc3072 ≝ sReverseCalc dTest_random_3072.
-
-definition sReverseNoCalc32 ≝ sReverseNoCalc dTest_random_32.
-definition sReverseNoCalc64 ≝ sReverseNoCalc dTest_random_64.
-definition sReverseNoCalc128 ≝ sReverseNoCalc dTest_random_128.
-definition sReverseNoCalc256 ≝ sReverseNoCalc dTest_random_256.
-definition sReverseNoCalc512 ≝ sReverseNoCalc dTest_random_512.
-definition sReverseNoCalc1024 ≝ sReverseNoCalc dTest_random_1024.
-definition sReverseNoCalc2048 ≝ sReverseNoCalc dTest_random_2048.
-definition sReverseNoCalc3072 ≝ sReverseNoCalc dTest_random_3072.
+ndefinition sReverseCalc32 ≝ sReverseCalc dTest_random_32.
+ndefinition sReverseCalc64 ≝ sReverseCalc dTest_random_64.
+ndefinition sReverseCalc128 ≝ sReverseCalc dTest_random_128.
+ndefinition sReverseCalc256 ≝ sReverseCalc dTest_random_256.
+ndefinition sReverseCalc512 ≝ sReverseCalc dTest_random_512.
+ndefinition sReverseCalc1024 ≝ sReverseCalc dTest_random_1024.
+ndefinition sReverseCalc2048 ≝ sReverseCalc dTest_random_2048.
+ndefinition sReverseCalc3072 ≝ sReverseCalc dTest_random_3072.
+
+ndefinition sReverseNoCalc32 ≝ sReverseNoCalc dTest_random_32.
+ndefinition sReverseNoCalc64 ≝ sReverseNoCalc dTest_random_64.
+ndefinition sReverseNoCalc128 ≝ sReverseNoCalc dTest_random_128.
+ndefinition sReverseNoCalc256 ≝ sReverseNoCalc dTest_random_256.
+ndefinition sReverseNoCalc512 ≝ sReverseNoCalc dTest_random_512.
+ndefinition sReverseNoCalc1024 ≝ sReverseNoCalc dTest_random_1024.
+ndefinition sReverseNoCalc2048 ≝ sReverseNoCalc dTest_random_2048.
+ndefinition sReverseNoCalc3072 ≝ sReverseNoCalc dTest_random_3072.
(* *********************** *)
(* HCS08GB60 Counting Sort *)
(* *********************** *)
(* versione ridotta, in cui non si riazzerano gli elementi di counters *)
-definition dTest_HCS08_cSort_source : word16 → (list byte8) ≝
+ndefinition dTest_HCS08_cSort_source : word16 → (list byte8) ≝
λelems:word16.
let m ≝ HCS08 in source_to_byte8 m (
(* BEFORE: A=0x00 H:X=0x0F4C SP=0x0F4B PC=0x18C8 Z=true *)
).
(* creazione del processore+caricamento+impostazione registri *)
-definition dTest_HCS08_cSort_status ≝
+ndefinition dTest_HCS08_cSort_status ≝
λt:memory_impl.
λI_op:bool.
λA_op:byte8.
I_op.
(* parametrizzazione dell'enunciato del teorema parziale *)
-lemma dTest_HCS08_cSort_aux ≝
+nlemma dTest_HCS08_cSort_aux ≝
λt:memory_impl.λstring:list byte8.
(* 1) la stringa deve avere una lunghezza ∈ [0,3072] *)
(byte8_bounded_strlen string 〈〈x0,xC〉:〈x0,x0〉〉) ∧
qed.
*)
-definition cSortCalc ≝
+ndefinition cSortCalc ≝
λstring:list byte8.
match execute HCS08 MEM_TREE
(TickOK ? (dTest_HCS08_cSort_status MEM_TREE true 〈x0,x0〉 〈〈x0,xF〉:〈x4,xC〉〉 (byte8_strlen string) string))
| TickOK s ⇒ None ?
].
-definition cSortNoCalc ≝
+ndefinition cSortNoCalc ≝
λstring:list byte8.
Some ? (set_pc_reg HCS08 MEM_TREE
(dTest_HCS08_cSort_status MEM_TREE false 〈xF,xF〉 〈〈x0,x1〉:〈x0,x0〉〉 (byte8_strlen string) (byte8_list_ordering string))
(mk_word16 (mk_byte8 x1 x9) (mk_byte8 x3 xC))).
-definition cSortCalc32 ≝ cSortCalc dTest_random_32.
-definition cSortCalc64 ≝ cSortCalc dTest_random_64.
-definition cSortCalc128 ≝ cSortCalc dTest_random_128.
-definition cSortCalc256 ≝ cSortCalc dTest_random_256.
-definition cSortCalc512 ≝ cSortCalc dTest_random_512.
-definition cSortCalc1024 ≝ cSortCalc dTest_random_1024.
-definition cSortCalc2048 ≝ cSortCalc dTest_random_2048.
-definition cSortCalc3072 ≝ cSortCalc dTest_random_3072.
-
-definition cSortNoCalc32 ≝ cSortNoCalc dTest_random_32.
-definition cSortNoCalc64 ≝ cSortNoCalc dTest_random_64.
-definition cSortNoCalc128 ≝ cSortNoCalc dTest_random_128.
-definition cSortNoCalc256 ≝ cSortNoCalc dTest_random_256.
-definition cSortNoCalc512 ≝ cSortNoCalc dTest_random_512.
-definition cSortNoCalc1024 ≝ cSortNoCalc dTest_random_1024.
-definition cSortNoCalc2048 ≝ cSortNoCalc dTest_random_2048.
-definition cSortNoCalc3072 ≝ cSortNoCalc dTest_random_3072.
+ndefinition cSortCalc32 ≝ cSortCalc dTest_random_32.
+ndefinition cSortCalc64 ≝ cSortCalc dTest_random_64.
+ndefinition cSortCalc128 ≝ cSortCalc dTest_random_128.
+ndefinition cSortCalc256 ≝ cSortCalc dTest_random_256.
+ndefinition cSortCalc512 ≝ cSortCalc dTest_random_512.
+ndefinition cSortCalc1024 ≝ cSortCalc dTest_random_1024.
+ndefinition cSortCalc2048 ≝ cSortCalc dTest_random_2048.
+ndefinition cSortCalc3072 ≝ cSortCalc dTest_random_3072.
+
+ndefinition cSortNoCalc32 ≝ cSortNoCalc dTest_random_32.
+ndefinition cSortNoCalc64 ≝ cSortNoCalc dTest_random_64.
+ndefinition cSortNoCalc128 ≝ cSortNoCalc dTest_random_128.
+ndefinition cSortNoCalc256 ≝ cSortNoCalc dTest_random_256.
+ndefinition cSortNoCalc512 ≝ cSortNoCalc dTest_random_512.
+ndefinition cSortNoCalc1024 ≝ cSortNoCalc dTest_random_1024.
+ndefinition cSortNoCalc2048 ≝ cSortNoCalc dTest_random_2048.
+ndefinition cSortNoCalc3072 ≝ cSortNoCalc dTest_random_3072.
(* ********************** *)
(* HCS08GB60 numeri aurei *)
(* ********************** *)
(* versione ridotta, in cui non si riazzerano gli elementi di counters *)
-definition dTest_HCS08_gNum_source : word16 → (list byte8) ≝
+ndefinition dTest_HCS08_gNum_source : word16 → (list byte8) ≝
λelems:word16.
let m ≝ HCS08 in source_to_byte8 m (
(* BEFORE: A=0x00 HX=0x1A00 PC=0x18BE SP=0x016F Z=1 (I=1) *)
).
(* creazione del processore+caricamento+impostazione registri *)
-definition dTest_HCS08_gNum_status ≝
+ndefinition dTest_HCS08_gNum_status ≝
λt:memory_impl.
λI_op:bool.
λA_op:byte8.
I_op.
(* NUMERI AUREI: Somma divisori(x)=x, fino a 0xFFFF sono 6/28/496/8128 *)
-definition dTest_HCS08_gNum_aurei ≝
+ndefinition dTest_HCS08_gNum_aurei ≝
λnum:word16.match gt_w16 num 〈〈x1,xF〉:〈xC,x0〉〉 with
[ true ⇒ [ 〈x0,x0〉 ; 〈x0,x6〉 ; 〈x0,x0〉 ; 〈x1,xC〉 ; 〈x0,x1〉 ; 〈xF,x0〉 ; 〈x1,xF〉 ; 〈xC,x0〉 ]
| false ⇒ match gt_w16 num 〈〈x0,x1〉:〈xF,x0〉〉 with
; 〈x0,x0〉 ; 〈x0,x0〉 ; 〈x0,x0〉 ; 〈x0,x0〉 ; 〈x0,x0〉 ; 〈x0,x0〉 ; 〈x0,x0〉 ; 〈x0,x0〉 ].
(* esecuzione execute k*(n+2) *)
-let rec dTest_HCS08_gNum_execute1 (m:mcu_type) (t:memory_impl) (s:tick_result (any_status m t)) (n,ntot:nat) on n ≝
+nlet rec dTest_HCS08_gNum_execute1 (m:mcu_type) (t:memory_impl) (s:tick_result (any_status m t)) (n,ntot:nat) on n ≝
match s with
[ TickERR s' error ⇒ TickERR ? s' error
| TickSUSP s' susp ⇒ TickSUSP ? s' susp
].
(* esecuzione execute k*(n+1)*(n+2) *)
-let rec dTest_HCS08_gNum_execute2 (m:mcu_type) (t:memory_impl) (s:tick_result (any_status m t)) (n,ntot:nat) on n ≝
+nlet rec dTest_HCS08_gNum_execute2 (m:mcu_type) (t:memory_impl) (s:tick_result (any_status m t)) (n,ntot:nat) on n ≝
match s with
[ TickERR s' error ⇒ TickERR ? s' error
| TickSUSP s' susp ⇒ TickSUSP ? s' susp
].
(* esecuzione execute k*n*(n+1)*(n+2) *)
-let rec dTest_HCS08_gNum_execute3 (m:mcu_type) (t:memory_impl) (s:tick_result (any_status m t)) (n,ntot:nat) on n ≝
+nlet rec dTest_HCS08_gNum_execute3 (m:mcu_type) (t:memory_impl) (s:tick_result (any_status m t)) (n,ntot:nat) on n ≝
match s with
[ TickERR s' error ⇒ TickERR ? s' error
| TickSUSP s' susp ⇒ TickSUSP ? s' susp
].
(* esecuzione execute 80+11*n*(n+1)*(n+2) *)
-definition dTest_HCS08_gNum_execute4 ≝
+ndefinition dTest_HCS08_gNum_execute4 ≝
λm:mcu_type.λt:memory_impl.λs:tick_result (any_status m t).λntot:nat.
match s with
[ TickERR s' error ⇒ TickERR ? s' error
].
(* parametrizzazione dell'enunciato del teorema parziale *)
-lemma dTest_HCS08_gNum_aux ≝
+nlemma dTest_HCS08_gNum_aux ≝
λt:memory_impl.λnum:word16.
(* 2) match di esecuzione su tempo in forma di upperbound *)
match dTest_HCS08_gNum_execute4 HCS08 t
] =
Some ? (dTest_HCS08_gNum_status t false 〈x0,x0〉 num 〈〈x1,x9〉:〈x5,x1〉〉 〈〈x1,x8〉:〈xB,xE〉〉 num (dTest_HCS08_gNum_aurei num)).
-definition gNumCalc ≝
+ndefinition gNumCalc ≝
λnum:word16.
match dTest_HCS08_gNum_execute4 HCS08 MEM_TREE
(TickOK ? (dTest_HCS08_gNum_status MEM_TREE true 〈x0,x0〉 〈〈x1,xA〉:〈x0,x0〉〉 〈〈x1,x8〉:〈xB,xE〉〉 〈〈x1,x8〉:〈xB,xE〉〉 num dTest_zeros))
| TickOK s ⇒ None ?
].
-definition gNumNoCalc ≝
+ndefinition gNumNoCalc ≝
λnum:word16.
Some ? (dTest_HCS08_gNum_status MEM_TREE false 〈x0,x0〉 num 〈〈x1,x9〉:〈x5,x1〉〉 〈〈x1,x8〉:〈xB,xE〉〉 num (dTest_HCS08_gNum_aurei num)).
-definition gNumCalc1 ≝ gNumCalc 〈〈x0,x0〉:〈x0,x1〉〉.
-definition gNumCalc2 ≝ gNumCalc 〈〈x0,x0〉:〈x0,x2〉〉.
-definition gNumCalc5 ≝ gNumCalc 〈〈x0,x0〉:〈x0,x5〉〉.
-definition gNumCalc10 ≝ gNumCalc 〈〈x0,x0〉:〈x0,xA〉〉.
-definition gNumCalc20 ≝ gNumCalc 〈〈x0,x0〉:〈x1,x4〉〉.
-definition gNumCalc50 ≝ gNumCalc 〈〈x0,x0〉:〈x3,x2〉〉.
-definition gNumCalc100 ≝ gNumCalc 〈〈x0,x0〉:〈x6,x4〉〉.
-definition gNumCalc250 ≝ gNumCalc 〈〈x0,x0〉:〈xF,xA〉〉.
-definition gNumCalc500 ≝ gNumCalc 〈〈x0,x1〉:〈xF,x4〉〉.
-definition gNumCalc1000 ≝ gNumCalc 〈〈x0,x3〉:〈xE,x8〉〉.
-
-definition gNumNoCalc1 ≝ gNumNoCalc 〈〈x0,x0〉:〈x0,x1〉〉.
-definition gNumNoCalc2 ≝ gNumNoCalc 〈〈x0,x0〉:〈x0,x2〉〉.
-definition gNumNoCalc5 ≝ gNumNoCalc 〈〈x0,x0〉:〈x0,x5〉〉.
-definition gNumNoCalc10 ≝ gNumNoCalc 〈〈x0,x0〉:〈x0,xA〉〉.
-definition gNumNoCalc20 ≝ gNumNoCalc 〈〈x0,x0〉:〈x1,x4〉〉.
-definition gNumNoCalc50 ≝ gNumNoCalc 〈〈x0,x0〉:〈x3,x2〉〉.
-definition gNumNoCalc100 ≝ gNumNoCalc 〈〈x0,x0〉:〈x6,x4〉〉.
-definition gNumNoCalc250 ≝ gNumNoCalc 〈〈x0,x0〉:〈xF,xA〉〉.
-definition gNumNoCalc500 ≝ gNumNoCalc 〈〈x0,x1〉:〈xF,x4〉〉.
-definition gNumNoCalc1000 ≝ gNumNoCalc 〈〈x0,x3〉:〈xE,x8〉〉.
-*)
-
+ndefinition gNumCalc1 ≝ gNumCalc 〈〈x0,x0〉:〈x0,x1〉〉.
+ndefinition gNumCalc2 ≝ gNumCalc 〈〈x0,x0〉:〈x0,x2〉〉.
+ndefinition gNumCalc5 ≝ gNumCalc 〈〈x0,x0〉:〈x0,x5〉〉.
+ndefinition gNumCalc10 ≝ gNumCalc 〈〈x0,x0〉:〈x0,xA〉〉.
+ndefinition gNumCalc20 ≝ gNumCalc 〈〈x0,x0〉:〈x1,x4〉〉.
+ndefinition gNumCalc50 ≝ gNumCalc 〈〈x0,x0〉:〈x3,x2〉〉.
+ndefinition gNumCalc100 ≝ gNumCalc 〈〈x0,x0〉:〈x6,x4〉〉.
+ndefinition gNumCalc250 ≝ gNumCalc 〈〈x0,x0〉:〈xF,xA〉〉.
+ndefinition gNumCalc500 ≝ gNumCalc 〈〈x0,x1〉:〈xF,x4〉〉.
+ndefinition gNumCalc1000 ≝ gNumCalc 〈〈x0,x3〉:〈xE,x8〉〉.
+
+ndefinition gNumNoCalc1 ≝ gNumNoCalc 〈〈x0,x0〉:〈x0,x1〉〉.
+ndefinition gNumNoCalc2 ≝ gNumNoCalc 〈〈x0,x0〉:〈x0,x2〉〉.
+ndefinition gNumNoCalc5 ≝ gNumNoCalc 〈〈x0,x0〉:〈x0,x5〉〉.
+ndefinition gNumNoCalc10 ≝ gNumNoCalc 〈〈x0,x0〉:〈x0,xA〉〉.
+ndefinition gNumNoCalc20 ≝ gNumNoCalc 〈〈x0,x0〉:〈x1,x4〉〉.
+ndefinition gNumNoCalc50 ≝ gNumNoCalc 〈〈x0,x0〉:〈x3,x2〉〉.
+ndefinition gNumNoCalc100 ≝ gNumNoCalc 〈〈x0,x0〉:〈x6,x4〉〉.
+ndefinition gNumNoCalc250 ≝ gNumNoCalc 〈〈x0,x0〉:〈xF,xA〉〉.
+ndefinition gNumNoCalc500 ≝ gNumNoCalc 〈〈x0,x1〉:〈xF,x4〉〉.
+ndefinition gNumNoCalc1000 ≝ gNumNoCalc 〈〈x0,x3〉:〈xE,x8〉〉.
projects / helm.git / blobdiff