Ignore:
Timestamp:
Jun 27, 2012, 12:09:25 PM (8 years ago)
Author:
sacerdot
Message:

load_code_memory moved to Fetch.ma and proved correct w.r.t. next
(fetching) using Russell

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r2115 r2119  
    616616qed.
    617617
    618 definition load_code_memory_aux ≝
    619  fold_left_i_aux … (
    620    λi, mem, v.
    621      insert … (bitvector_of_nat … i) v mem) (Stub Byte 16).
    622 
    623618lemma vsplit_zero:
    624619  ∀A,m.
     
    10601055    ].
    10611056
    1062 (* This is a trivial consequence of fetch_assembly_pseudo + the proof that the
    1063    function that load the code in memory is correct. The latter is based
    1064    on missing properties from the standard library on the BitVectorTrie
    1065    data structrure.
    1066    
    1067    Wrong at the moment, requires Jaap's precondition to ensure that the program
    1068    does not overflow when put into code memory (i.e. shorter than 2^16 bytes).
    1069 *)
    1070 
    1071 lemma load_code_memory_ok:
    1072  ∀program.
    1073  let program_size ≝ |program| in
    1074   program_size ≤ 2^16 →
    1075    ∀pc. ∀pc_ok: pc < program_size.
    1076     nth_safe ? pc program pc_ok = \snd (next (load_code_memory program) (bitvector_of_nat … pc)).
    1077  #program elim program
    1078  [ #_ #pc #abs normalize in abs; @⊥ /2/
    1079  | #hd #tl #IH #size_ok *
    1080    [ #pc_ok whd in ⊢ (??%?); whd in match (load_code_memory ?);
    1081      whd in match next; normalize nodelta
    1082    | #pc' #pc_ok' whd in ⊢ (??%?);  whd in match (load_code_memory ?);
    1083      whd in match next; normalize nodelta
    1084    ]
    1085  cases daemon (*CSC: complete! *)
    1086 qed.
    1087 (*NO! Prima dimostrare tipo Russell di assembly in Assembly.ma
    1088 Poi dimostrare che per ogni i, se fetcho l'i-esimo bit di program
    1089 e' come fetchare l'i-esimo bit dalla memoria.
    1090 Concludere assembly_ok come semplice corollario.
    1091 *)
     1057(* This is a trivial consequence of fetch_assembly_pseudo + load_code_memory_ok. *)     
    10921058lemma assembly_ok:
    10931059  ∀program.
Note: See TracChangeset for help on using the changeset viewer.