Changeset 2702


Ignore:
Timestamp:
Feb 22, 2013, 3:27:16 PM (6 years ago)
Author:
sacerdot
Message:
  1. proof closed in ASM/UtilBranch
  2. more passes integrated in the compiler.ma
  3. some work on commenting out broken proofs in linearise.ma
Location:
src
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/UtilBranch.ma

    r1946 r2702  
    2424    >inductive_hypothesis
    2525    >inductive_hypothesis
    26     [1:
    27       change with (
    28         ? + (2 * buffer + 1) * ?) in ⊢ (??%?);
    29       change with (
    30         ? + buffer * (2 * 2^n')) in ⊢ (???%);
    31       cases daemon
    32     ]
    33   ]
    34   cases daemon
     26    [1: change with (? + (2 * buffer + 1) * ?) in ⊢ (??%?);
     27        >associative_plus in ⊢ (???%); @eq_f >commutative_plus
     28        whd in ⊢ (??%?); @eq_f2 // >commutative_times in ⊢ (???(??%));
     29        <associative_times //
     30    | <plus_n_O normalize <plus_n_O @eq_f <associative_times
     31      <commutative_times in ⊢ (???%); <associative_times //
    3532qed.
    3633
  • src/compiler.ma

    r2700 r2702  
    4444definition costlabel_map ≝ BitVectorTrie costlabel 16.
    4545
    46 axiom assembler : pseudo_assembly_program → res (object_code × costlabel_map).
    47 
    48 (* Only sloow include "ASM/Policy.ma".
    49 *)include "ASM/PolicyStep.ma". include "arithmetics/nat.ma". axiom jump_expansion': ∀program:preamble × (Σl:list labelled_instruction.S (|l|) < 2^16 ∧ is_well_labelled_p l).
     46include "ASM/Policy.ma".
     47(* Equivalent to the inclusion of ASM/Policy.ma, waiting for that slow
     48   file to compile
     49  include "ASM/PolicyStep.ma".
     50  axiom jump_expansion': ∀program:preamble × (Σl:list labelled_instruction.lt (S (|l|)) 2^16 ∧ is_well_labelled_p l).
    5051 option (Σsigma_policy:(Word → Word) × (Word → bool).
    5152   let 〈sigma,policy〉≝ sigma_policy in
    52    sigma_policy_specification 〈\fst program,\snd program〉 sigma policy).
     53   sigma_policy_specification 〈\fst program,\snd program〉 sigma policy). *)
    5354
    5455definition assembler : pseudo_assembly_program → res (object_code × costlabel_map) ≝
     
    5859  let p' ≝ 〈preamble, list_instr〉 in
    5960  ! sigma_pol ← opt_to_res ? (msg Jump_expansion_failed) (jump_expansion' p');
    60   let sigma ≝ λppc. \fst (sigma_pol ppc) in
    61   let pol ≝ λppc. \snd (sigma_pol ppc) in
     61  let sigma ≝ λppc. \fst sigma_pol ppc in
     62  let pol ≝ λppc. \snd sigma_pol ppc in
    6263  OK ? (assembly p sigma pol).
    6364cases daemon
     
    9293  return 〈p, ❬p', k'❭〉.
    9394  cases daemon
    94   qed.
     95qed.
  • src/joint/linearise.ma

    r2570 r2702  
    256256    cases s in H3; [3: *]
    257257    [ * ] normalize nodelta
    258     [1,3: [#f #args #dest |#s'] #nxt * #EQnth_opt #H %{EQnth_opt}
     258    [2,4: [#f #args #dest |#s'] #nxt * #EQnth_opt #H %{EQnth_opt}
    259259      inversion (lookup … visited nxt) in H; [2: #n'] #EQlookup
    260260      normalize nodelta *
     
    264264        whd in ⊢ (?%→?); >EQlookup *
    265265      ]
    266     | #a #ltrue #lfalse * [2: #H %2{H} ] * #H1 #H2 %1 %{H1}
     266    |3: #a #ltrue #lfalse * [2: #H %2{H} ] * #H1 #H2 %1 %{H1}
    267267      inversion (lookup … visited lfalse) in H2;
    268268      [ #ABS * #H' lapply (All_nth … H … H')
     
    270270      | #n' #_ normalize nodelta #EQ >EQ %
    271271      ]
    272     | #s #H @H
     272    | #s #H (*CSC XXXXXXXXXXXXXXXXXXXX @H *)
    273273    ]
    274274  ]
     
    327327  #P whd in match add_req_gen;
    328328  cases statement [ * [#f #args #dest|  #a #ltrue | #s ] #nxt | #s | * ]
    329 [2,4: normalize nodelta #H #_ @(H I) ]
    330   normalize nodelta inversion (nxt ∈ visited') #EQ normalize nodelta
    331   #H1 #H2 [1,3: @(H2 … (refl …)) >EQ % |*: @H1 % * ]
     329 [2,4: normalize nodelta #l #H1 #H2 lapply (H2 … (refl …)) -H2
     330      cases (l ∈ add …) in H1; normalize nodelta #H1 #H2 try @H2 try @H1 try %
     331      //
     332 |3,5: normalize nodelta [#_] #H #_ @H %
     333 | normalize nodelta in dest nxt ⊢ %; inversion (args ∈ add …) #EQ
     334   normalize nodelta [ @nxt | @dest ] >EQ try % ]
     335|14: skip
     336] cases daemon (*CSC: XXXXXXXXX
    332337|3: elim H #pre ** #H1 #H2 #_
    333338  #i >mem_set_union
     
    336341    #next #_ #next_vis #H >(mem_set_singl_to_eq … H) %2 assumption
    337342  | >mem_set_union
    338     #H elim (orb_Prop_true … H) -H
     343    #H elim (orb_Prop_true … H) -H (*CSC XXXXXXXXXX
    339344    [ #i_expl %1 @Exists_append_l
    340345      lapply i_expl whd in match translated_statement;
     
    361366        #i_vis %2 >mem_set_add @orb_Prop_r assumption
    362367      ]
    363     ]
     368    ]*) cases daemon
    364369  ]
    365370|4,5,6: change with reverse in match rev;
     
    418423        lapply (in_map_domain … visited vis_hd)
    419424        >H3 normalize nodelta //
    420       | %{statement}
     425      | %{statement}  (*CSC XXXXXXX
    421426        %
    422427        [ @lookup_eq_safe
     
    438443            |*: %%
    439444            ]
    440           ]
     445          ]*) cases daemon
    441446        ]
    442447      ]
    443448    | #NEQ #n_i >(lookup_add_miss … visited … NEQ)
     449      cases daemon (*CSC XXXX
    444450      #Hlookup elim (generated_prf1 … Hlookup)
    445451      #G1 * #s * #G2 #G3
     
    481487          ]
    482488        ]
    483       ]
     489      ] *)
    484490    ]
    485491  | #i whd in match visited';
     
    509515  @add_req_gen_prf [ #_ | #s #next #_ #_ ] normalize >gen_length_prf %
    510516|
    511 ]
     517]*)
    512518qed.
    513519
     
    644650               (stmt_at … c n = Some ? (sequential … s' it) ∧ sigma nxt = Some ? (S n)) ∨
    645651               (stmt_at … c n = Some ? (FCOND … I a ltrue nxt))
     652             | CALL _ _ _ ⇒
     653               (stmt_at … c n = Some ? (sequential … s' it)) ∧
     654                  ((sigma nxt = Some ? (S n)) ∨
     655                   (stmt_at … c (S n) = Some ? (GOTO … nxt)))               
     656             | COST_LABEL _ ⇒
     657               (stmt_at … c n = Some ? (sequential … s' it)) ∧
     658                  ((sigma nxt = Some ? (S n)) ∨
     659                   (stmt_at … c (S n) = Some ? (GOTO … nxt)))               
    646660             ]
    647661           | final s' ⇒
     
    829843  〈«mk_joint_internal_function (mk_lin_params p) globals
    830844   (joint_if_luniverse ?? f_sig) (joint_if_runiverse ?? f_sig)
    831    (joint_if_result ?? f_sig) (joint_if_params ?? f_sig) (joint_if_locals ?? f_sig)
    832    (joint_if_stacksize ?? f_sig) code entry entry (* exit is dummy! *), ?»,
     845   (joint_if_result ?? f_sig) (joint_if_params ?? f_sig)
     846   (joint_if_stacksize ?? f_sig) code entry, ?»,
    833847   sigma〉.
    834848normalize nodelta
Note: See TracChangeset for help on using the changeset viewer.