Changeset 2119


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

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

Location:
src/ASM
Files:
3 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.
  • src/ASM/Fetch.ma

    r1961 r2119  
    1717  λpc: Word.
    1818    〈add … pc (bitvector_of_nat 16 1), lookup … pc pmem (zero …)〉.
     19
     20(*CSC: move elsewhere *)
     21axiom eq_bitvector_of_nat_to_eq:
     22 ∀n,n1,n2.
     23  n1 < 2^n → n2 < 2^n →
     24   bitvector_of_nat n n1 = bitvector_of_nat n n2 → n1=n2.
     25
     26discriminator Prod.
     27
     28definition load_code_memory0:
     29 ∀program: list Byte. Σres: BitVectorTrie Byte 16.
     30  let program_size ≝ |program| in
     31   program_size ≤ 2^16 →
     32    ∀pc. ∀pc_ok: pc < program_size.
     33     nth_safe ? pc program pc_ok = \snd (next res (bitvector_of_nat … pc))
     34
     35 λprogram. \snd
     36  (foldl_strong ?
     37   (λprefix.
     38     Σres: nat × (BitVectorTrie Byte 16).
     39      let 〈i,mem〉 ≝ res in
     40      i = |prefix| ∧
     41      (i ≤ 2^16 →
     42        ∀pc. ∀pc_ok: pc < |prefix|.
     43         nth_safe ? pc prefix pc_ok = \snd (next mem (bitvector_of_nat … pc))))
     44   program
     45   (λprefix,v,tl,prf,i_mem.
     46     let 〈i,mem〉 ≝ i_mem in
     47      〈S i,insert … (bitvector_of_nat … i) v mem〉)
     48  〈0,Stub Byte 16〉).
     49[3: cases (foldl_strong ? (λprefix.Σres.?) ???) * #i #mem * #H1 >H1 #H2 @H2
     50| % // #_ #pc #abs @⊥ @(absurd … abs (not_le_Sn_O …))
     51| cases i_mem in p; * #i' #mem' #H #EQ destruct(EQ) cases H -H #H1 #H2 %
     52  [ >length_append >H1 normalize //
     53  | #LE #pc #pc_ok
     54    cases (le_to_or_lt_eq … pc_ok)
     55    [2: #EQ_Spc >(?: pc = |prefix| + 0) in pc_ok;
     56      [2: >length_append in EQ_Spc; normalize #EQ @injective_S >EQ //]
     57      #pc_ok <nth_safe_prepend [2: //] whd in ⊢ (??%?);
     58      <H1 <plus_n_O whd in ⊢ (???%); //
     59    | >length_append <plus_n_Sm <plus_n_O #LT <shift_nth_prefix [2: /2/]
     60      >H2 [2: @(transitive_le … LE) //]
     61      cut (pc ≠ i) [ >H1 @lt_to_not_eq @lt_S_S_to_lt //] #NEQ
     62      whd in ⊢ (??%%); @sym_eq @lookup_insert_miss >eq_bv_false %
     63      #EQ @(absurd ?? NEQ) @(eq_bitvector_of_nat_to_eq … EQ) try assumption
     64      @(transitive_lt … LE) >H1 @lt_S_S_to_lt //]]
     65qed.
     66
     67definition load_code_memory: list Byte → BitVectorTrie Byte 16 ≝
     68 λprogram.load_code_memory0 program.
     69
     70lemma load_code_memory_ok:
     71 ∀program: list Byte.
     72  let program_size ≝ |program| in
     73   program_size ≤ 2^16 →
     74    ∀pc. ∀pc_ok: pc < program_size.
     75     nth_safe ? pc program pc_ok = \snd (next (load_code_memory program) (bitvector_of_nat … pc)).
     76whd in match load_code_memory; normalize nodelta #program @pi2
     77qed.
    1978
    2079lemma Prod_inv_rect_Type0:
  • src/ASM/Status.ma

    r2111 r2119  
    11041104qed.
    11051105
    1106 definition load_code_memory ≝
    1107  fold_left_i … (
    1108    λi, mem, v.
    1109      insert … (bitvector_of_nat … i) v mem) (Stub Byte 16).
    1110 
    1111 definition load ≝
    1112  λl,cm.
    1113  λstatus.
    1114    set_code_memory (BitVectorTrie Word 16) ? cm status (load_code_memory l).
    1115 
    11161106definition fetch_pseudo_instruction:
    11171107 ∀code_mem:list labelled_instruction. ∀pc:Word.
Note: See TracChangeset for help on using the changeset viewer.