Changeset 2443


Ignore:
Timestamp:
Nov 8, 2012, 2:27:54 PM (7 years ago)
Author:
tranquil
Message:

changed joint's stack pointer and internal stack

Location:
src
Files:
13 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/ERTLToLTL.ma

    r2286 r2443  
    130130  ; A ← RegisterSPH
    131131  ; A ← A .Sub. zero_byte
    132   ; RegisterSPL ← A
     132  ; RegisterSPH ← A
    133133  ].
    134134
     
    141141  ; A ← RegisterSPH
    142142  ; A ← A .Addc. zero_byte
    143   ; RegisterSPL ← A
     143  ; RegisterSPH ← A
    144144  ].
    145145
  • src/LIN/LINToASM.ma

    r2286 r2443  
    2222    ]. @I qed.
    2323
    24 (* TODO:
    25   this should translate back end immediates (which rely on beval) to ASM
    26   byte immediates. How should it work? surely needs arguments for instantiation
    27   of blocks. If it's too much a fuss, we can go back to byte immediates in the
    28   back end. *)
    29 definition asm_byte_of_beval : beval → Byte ≝
    30   λb.match b with
    31     [ BVByte b ⇒ b
    32     | BVundef ⇒ (* any will do *) zero_byte
    33     | BVnonzero ⇒ (* any will do *) maximum 7 @@ [[ true ]]
    34     | BVnull _ ⇒ zero_byte (* is it correct? *)
    35     | BVptr b p o ⇒ ?
    36     ].
    37   cases daemon qed.
    38 
    39 definition arg_address : hdw_argument → [[ acc_a ; direct ; registr ; data ]] ≝
    40   λa.match a with
    41   [ Reg r ⇒ register_address r
    42   | Imm bv ⇒ DATA (asm_byte_of_beval bv)
    43   ].
    44   cases a #x [2: normalize //] normalize nodelta
    45   elim (register_address ?) #rslt @is_in_subvector_is_in_supervector @I
    46 qed.
    47 
    48 let rec association (i: ident) (l: list (ident × nat))
    49                     on l: member i (eq_identifier ?) (map ? ? (fst ? ?) l) → nat ≝
    50   match l return λl. member i (eq_identifier ?) (map ? ? (fst ? ?) l) → nat with
    51   [ nil ⇒ λabsd. ?
     24let rec association A B (eq_A : A → A → bool) (a : A) (l: list (A × B))
     25                    on l: member A eq_A a (map ? ? (fst ? ?) l) → B ≝
     26  match l return λl. member A eq_A a (map ? ? (fst ? ?) l) → B with
     27  [ nil ⇒ Ⓧ
    5228  | cons hd tl ⇒
    53     λprf: member i (eq_identifier ?) (map ? ? (fst ? ?) (cons ? hd tl)).
    54       (match eq_identifier ? (\fst hd) i return λb. eq_identifier ? (\fst hd) i = b → nat with
    55       [ true ⇒ λeq_prf. \snd hd
    56       | false ⇒ λeq_prf. association i tl ?
    57       ]) (refl ? (eq_identifier ? (\fst hd) i))
    58   ].
    59   [ cases absd
    60   | cases prf
    61     [ > eq_prf
    62       # H
    63       cases H
     29    λprf.
     30    If eq_A a (\fst hd) then \snd hd else with eq_prf do
     31      association … eq_A a tl ?
     32  ].
     33  elim (orb_Prop_true … prf)
     34    [ > eq_prf *
    6435    | # H
    6536      assumption
    6637    ]
     38qed.
     39
     40definition association_ident ≝ association ident nat (eq_identifier ?).
     41definition association_block ≝ association block Word eq_block.
     42
     43definition asm_cst_well_def :
     44  list (block × Word) → beval → bool ≝
     45λglobals,bv.match bv with
     46[ BVptr b _ _ ⇒ member ? eq_block b (map ?? \fst globals)
     47| _ ⇒ true
     48].
     49
     50definition vector_cast :
     51∀A,n,m.A → Vector A n → Vector A m ≝
     52λA,n,m,dflt,v.
     53If leb n m then with prf do
     54  replicate … (m - n) dflt @@ v ⌈Vector ?? ↦ ?⌉
     55else with prf do
     56  \snd (vsplit … (v ⌈Vector ?? ↦ Vector ? (n - m + m)⌉)).
     57lapply prf @(leb_elim n)
     58[2,3: #_ * #abs elim (abs I) ]
     59#H #_ >commutative_plus_faster @eq_f [@sym_eq] @(minus_to_plus … (refl …))
     60[ assumption ]
     61@(transitive_le … (not_le_to_lt … H)) %2 %1
     62qed.
     63
     64definition asm_byte_of_beval :
     65  ∀globals,bv.asm_cst_well_def globals bv → Byte ≝
     66  λglobals,bv.match bv return λbv.asm_cst_well_def globals bv → Byte with
     67    [ BVByte b ⇒ λ_.b
     68    | BVundef ⇒ λ_.(* any will do *) zero_byte
     69    | BVnonzero ⇒ λ_.(* any will do *) maximum 7 @@ [[ true ]]
     70    | BVnull _ ⇒ λ_.zero_byte (* is it correct? *)
     71    | BVptr b p o ⇒ λprf.
     72      let b_inst ≝ vector_cast … (S p) zero_byte (rvsplit … 2 8 (association_block … prf)) in
     73      let 〈inst, ignore〉 ≝ op2_bytes Add … false b_inst o in
     74      head' … inst
     75    ].
     76
     77definition asm_arg_well_def :
     78  list (block × Word) → hdw_argument → bool ≝
     79λglobals,a.match a with
     80[ Imm bv ⇒ asm_cst_well_def globals bv
     81| _ ⇒ true
     82].
     83
     84definition arg_address : ∀globals,arg.asm_arg_well_def globals arg →
     85  [[ acc_a ; direct ; registr ; data ]] ≝
     86  λglobals,a.
     87  match a
     88  return λa.asm_arg_well_def globals a → [[ acc_a ; direct ; registr ; data ]]
     89  with
     90  [ Reg r ⇒ λ_.register_address r
     91  | Imm bv ⇒ λprf.DATA (asm_byte_of_beval … prf)
     92  ].
     93  [ elim (register_address ?) #rslt @is_in_subvector_is_in_supervector @I
     94  | @I
    6795  ]
    6896qed.
    6997
    7098definition lin_statement ≝ λg.labelled_obj LabelTag (joint_statement LIN g).
     99
     100definition asm_stmt_well_def :
     101  list (block × Word) → ∀old_globals.joint_statement LIN old_globals → bool ≝
     102  λblocks,old_globals,stmt.
     103  match stmt with
     104  [ sequential instr _ ⇒
     105    match instr with
     106    [ step_seq instr' ⇒
     107      match instr' with
     108      [ OP2 _ _ _ arg ⇒ asm_arg_well_def blocks arg
     109      | MOVE regs ⇒
     110        match regs with
     111        [ int_to_reg _ bv ⇒ asm_cst_well_def blocks bv
     112        | int_to_acc _ bv ⇒ asm_cst_well_def blocks bv
     113        | _ ⇒ true
     114        ]
     115      | _ ⇒ true
     116      ]
     117    | _ ⇒ true
     118    ]
     119  | _ ⇒ true
     120  ].
    71121 
    72122definition statement_labels ≝
     
    137187definition translate_statements ≝
    138188  λglobals: list (ident × nat).
     189  λblocks: list (block × Word).
    139190  λglobals_old: list ident.
    140   λprf: ∀i: ident. member i (eq_identifier ?) globals_old → member i (eq_identifier ?) (map ? ? (fst ? ?) globals).
     191  λprf: ∀i: ident. member ? (eq_identifier ?) i globals_old → member ? (eq_identifier ?) i (map ? ? (fst ? ?) globals).
    141192  λstatement: joint_statement LIN globals_old.
    142   match statement with
    143   [ final instr ⇒
     193  match statement return λstmt.asm_stmt_well_def blocks ? stmt → ? with
     194  [ final instr ⇒ λ_.
    144195    match instr with
    145196    [ GOTO lbl ⇒ Jmp (toASM_ident ? lbl)
     
    148199    ]
    149200  | sequential instr _ ⇒
    150       match instr with
     201      match instr return λinstr.asm_stmt_well_def blocks ? (sequential ?? instr ?) → ? with
    151202      [ step_seq instr' ⇒
    152         match instr' with
    153         [ extension_seq ext ⇒
     203        match instr' return λinstr'.asm_stmt_well_def ?? (sequential ?? (step_seq ?? instr') ?) → ? with
     204        [ extension_seq ext ⇒ λ_.
    154205          match ext with
    155206          [ SAVE_CARRY ⇒
     
    158209            Instruction (MOV ? (inl ?? (inr ?? 〈CARRY, asm_other_bit〉)))
    159210          ]
    160         | COMMENT comment ⇒ Comment comment
    161         | COST_LABEL lbl ⇒ Cost lbl
    162         | POP _ ⇒ Instruction (POP ? accumulator_address)
    163         | PUSH _ ⇒ Instruction (PUSH ? accumulator_address)
    164         | CLEAR_CARRY ⇒ Instruction (CLR ? CARRY)
    165         | CALL_ID f _ _ ⇒ Call (toASM_ident ? f)
    166         | extension_call abs ⇒ match abs in void with [ ]
    167         | OPACCS accs _ _ _ _ ⇒
     211        | COMMENT comment ⇒ λ_.Comment comment
     212        | COST_LABEL lbl ⇒ λ_.Cost lbl
     213        | POP _ ⇒ λ_.Instruction (POP ? accumulator_address)
     214        | PUSH _ ⇒ λ_.Instruction (PUSH ? accumulator_address)
     215        | CLEAR_CARRY ⇒ λ_.Instruction (CLR ? CARRY)
     216        | CALL_ID f _ _ ⇒ λ_.Call (toASM_ident ? f)
     217        | extension_call abs ⇒ λ_.match abs in void with [ ]
     218        | OPACCS accs _ _ _ _ ⇒ λ_.
    168219          match accs with
    169220          [ Mul ⇒ Instruction (MUL ? ACC_A ACC_B)
    170221          | DivuModu ⇒ Instruction (DIV ? ACC_A ACC_B)
    171222          ]
    172         | OP1 op1 _ _ ⇒
     223        | OP1 op1 _ _ ⇒ λ_.
    173224          match op1 with
    174225          [ Cmpl ⇒ Instruction (CPL ? ACC_A)
     
    176227          | Rl ⇒ Instruction (RL ? ACC_A)
    177228          ]
    178         | OP2 op2 _ _ reg ⇒
     229        | OP2 op2 _ _ reg ⇒ λprf'.?
     230          | _ ⇒ ?] | _ ⇒ ? ]].[12: whd in prf : (?%);
     231
    179232          match op2 with
    180233          [ Add ⇒
    181             let reg' ≝ arg_address reg in
     234            let reg' ≝ arg_address … prf' in
    182235            match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
    183236                                                           direct;
     
    195248            ] (subaddressing_modein … reg')
    196249          | Addc ⇒
    197             let reg' ≝ arg_address reg in
     250            let reg' ≝ arg_address … prf' in
    198251            match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
    199252                                                           direct;
     
    211264            ] (subaddressing_modein … reg')
    212265          | Sub ⇒
    213             let reg' ≝ arg_address reg in
     266            let reg' ≝ arg_address … prf' in
    214267            match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
    215268                                                           direct;
     
    227280            ] (subaddressing_modein … reg')
    228281          | And ⇒
    229             let reg' ≝ arg_address reg in
     282            let reg' ≝ arg_address … prf' in
    230283            match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
    231284                                                           direct;
     
    243296            ] (subaddressing_modein … reg')
    244297          | Or ⇒
    245             let reg' ≝ arg_address reg in
     298            let reg' ≝ arg_address … prf' in
    246299            match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
    247300                                                           direct;
     
    258311            ] (subaddressing_modein … reg')
    259312          | Xor ⇒
    260             let reg' ≝ arg_address reg in
     313            let reg' ≝ arg_address … prf' in
    261314            match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
    262315                                                           direct;
     
    273326            ] (subaddressing_modein … reg')
    274327          ]
    275         | LOAD _ _ _ ⇒ Instruction (MOVX ? (inl ? ? 〈ACC_A, EXT_INDIRECT_DPTR〉))
    276         | STORE _ _ _ ⇒ Instruction (MOVX ? (inr ? ? 〈EXT_INDIRECT_DPTR, ACC_A〉))
    277         | ADDRESS addr proof _ _ ⇒
    278           let look ≝ association addr globals (prf ? proof) in
     328        | LOAD _ _ _ ⇒ λ_.Instruction (MOVX ? (inl ? ? 〈ACC_A, EXT_INDIRECT_DPTR〉))
     329        | STORE _ _ _ ⇒ λ_.Instruction (MOVX ? (inr ? ? 〈EXT_INDIRECT_DPTR, ACC_A〉))
     330        | ADDRESS addr proof _ _ ⇒ λ_.
     331          let look ≝ association_ident addr globals (prf ? proof) in
    279332            Instruction (MOV ? (inl ? ? (inl ? ? (inr ? ? (〈DPTR, (data16_of_int look)〉)))))
    280         | SET_CARRY ⇒
     333        | SET_CARRY ⇒ λ_.
    281334          Instruction (SETB ? CARRY)
    282335        | MOVE regs ⇒
    283           match regs with
    284           [ to_acc _ reg ⇒
     336          match regs return λregs.asm_stmt_well_def ?? (sequential ?? (step_seq ?? (MOVE regs)) ?) → ? with
     337          [ to_acc _ reg ⇒ λ_.
    285338             let reg' ≝ register_address reg in
    286339               match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
     
    295348               | _ ⇒ λother: False. ⊥
    296349               ] (subaddressing_modein … reg')
    297           | from_acc reg _ ⇒
     350          | from_acc reg _ ⇒ λ_.
    298351             let reg' ≝ register_address reg in
    299352               match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
     
    308361               | _ ⇒ λother: False. ⊥
    309362               ] (subaddressing_modein … reg')
    310           | int_to_reg reg bv ⇒
    311             let b ≝ asm_byte_of_beval bv in
     363          | int_to_reg reg bv ⇒ λprf'.
     364            let b ≝ asm_byte_of_beval … prf' in
    312365            let reg' ≝ register_address reg in
    313366              match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
     
    322375              | _ ⇒ λother: False. ⊥
    323376              ] (subaddressing_modein … reg')
    324           | int_to_acc _ bv ⇒
    325             let b ≝ asm_byte_of_beval bv in
     377          | int_to_acc _ bv ⇒ λprf'.
     378            let b ≝ asm_byte_of_beval … prf' in
    326379            Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, DATA b〉))))))
    327380          ]
    328381        ]
    329       | COND _ lbl ⇒
     382      | COND _ lbl ⇒ λ_.
    330383        (* dpm: this should be handled in translate_code! *)
    331384        Instruction (JNZ ? (toASM_ident ? lbl))
    332385      ]
    333386    ].
    334   try assumption
    335   try @ I
     387  try @I
     388  assumption
    336389qed.
    337390
  • src/LIN/joint_LTL_LIN_semantics.ma

    r2286 r2443  
    2727 (* empty_framesT ≝ *) it
    2828 (* regsT ≝ *) hw_register_env
    29  (* empty_regsT ≝ *) init_hw_register_env.
     29 (* empty_regsT ≝ *) init_hw_register_env
     30 (* load_sp ≝ *) hwreg_retrieve_sp
     31 (* store_sp ≝ *) hwreg_store_sp.
    3032
    3133(*CSC: XXXX, for external functions only*)
     
    3739
    3840definition LTL_LIN_semantics ≝
    39   λF.mk_more_sem_unserialized_params LTL_LIN F
     41  λF.mk_sem_unserialized_params LTL_LIN F
    4042  (* st_pars            ≝ *) LTL_LIN_state
    4143  (* acca_store_        ≝ *) (λ_.hw_reg_store RegisterA)
  • src/LIN/semantics.ma

    r2286 r2443  
    33
    44definition LIN_semantics : sem_params ≝
    5   make_sem_lin_params LIN (LTL_LIN_semantics ?).
     5  make_sem_lin_params LIN LTL_LIN_semantics.
  • src/LTL/semantics.ma

    r2286 r2443  
    33
    44definition LTL_semantics : sem_params ≝
    5   make_sem_graph_params LTL (LTL_LIN_semantics ?).
     5  make_sem_graph_params LTL LTL_LIN_semantics.
  • src/common/ByteValues.ma

    r2435 r2443  
    103103axiom NotATwoBytesPointer: String.
    104104
    105 (* Fails if the address is not representable as a pair *)
    106 definition beval_pair_of_pointer: pointer → res (beval × beval) ≝
    107  λp. OK … (list_to_pair … (bevals_of_pointer p) (refl …)).
     105(* Should fail if the address is not representable as a pair
     106   As we only have 16 bit addresses atm, it never fails *)
     107definition beval_pair_of_pointer: pointer → (* res *) (beval × beval) ≝
     108 λp.list_to_pair … (bevals_of_pointer p) (refl …).
    108109(*
    109110 λp. match p with [ mk_pointer pty pbl pok poff ⇒
  • src/joint/SemanticUtils.ma

    r2422 r2443  
    66record hw_register_env : Type[0] ≝
    77  { reg_env : BitVectorTrie beval 6
    8   ; carry_bit : bebit
    98  ; other_bit : bebit
    109  }.
    1110
    1211definition empty_hw_register_env: hw_register_env ≝
    13   mk_hw_register_env (Stub …) BBundef BBundef.
     12  mk_hw_register_env (Stub …) BBundef.
    1413
    1514include alias "ASM/BitVectorTrie.ma".
     
    2019definition hwreg_store: Register → beval → hw_register_env → hw_register_env ≝
    2120 λr,v,env.mk_hw_register_env (insert … (bitvector_of_register r) v (reg_env env))
    22   (carry_bit env) (other_bit env).
    23 
    24 definition hwreg_set_carry : bebit → hw_register_env → hw_register_env ≝
    25 λv,env.mk_hw_register_env (reg_env env) v (other_bit env).
     21  (other_bit env).
    2622
    2723definition hwreg_set_other : bebit → hw_register_env → hw_register_env ≝
    28 λv,env.mk_hw_register_env (reg_env env) (carry_bit env) v.
    29 
     24λv,env.mk_hw_register_env (reg_env env) v.
     25
     26definition hwreg_retrieve_sp : hw_register_env → res xpointer ≝
     27λenv.
     28let spl ≝ hwreg_retrieve env RegisterSPL in
     29let sph ≝ hwreg_retrieve env RegisterSPH in
     30! ptr ← pointer_of_address 〈spl, sph〉 ;
     31match ptype ptr return λx.ptype ptr = x → res xpointer with
     32[ XData ⇒ λprf.return «ptr, prf»
     33| _ ⇒ λ_.Error … [MSG BadPointer]
     34] (refl …).
     35
     36definition hwreg_store_sp : hw_register_env → xpointer → hw_register_env ≝
     37λenv,sp.
     38let 〈spl, sph〉 ≝ beval_pair_of_pointer sp in
     39hwreg_store RegisterSPH sph (hwreg_store RegisterSPL spl env).
    3040
    3141(*** Store/retrieve on pseudo-registers ***)
    3242include alias "common/Identifiers.ma".
    3343
     44record reg_sp : Type[0] ≝
     45{ reg_sp_env :> identifier_map RegisterTag beval
     46; stackp : xpointer
     47}.
     48
    3449axiom BadRegister : String.
    3550
     
    3954 λlocals,reg. opt_to_res … [MSG BadRegister; CTX ? reg] (lookup … locals reg).
    4055
     56definition reg_sp_store ≝ λreg,v,locals.
     57! locals' ← reg_store reg v (reg_sp_env locals) ;
     58return mk_reg_sp locals' (stackp locals).
     59
     60definition reg_sp_retrieve ≝ λlocals.reg_retrieve locals.
     61
    4162(*** Store/retrieve on hardware registers ***)
    4263
    4364definition init_hw_register_env: xpointer → hw_register_env ≝
    44  λsp.
    45   let 〈dpl,dph〉 ≝
    46     match beval_pair_of_pointer sp return λx.beval_pair_of_pointer sp = x → ? with
    47     [ OK p ⇒ λ_.p
    48     | _ ⇒ λprf.⊥
    49     ] (refl …) in
    50   let env ≝ hwreg_store RegisterDPH dph empty_hw_register_env in
    51    hwreg_store RegisterDPL dpl env.
    52 @hide_prf
    53 normalize in prf; destruct(prf)
    54 qed.
     65 λsp.hwreg_store_sp empty_hw_register_env sp.
    5566
    5667(******************************** GRAPHS **************************************)
     
    150161
    151162definition make_sem_graph_params :
    152   ∀pars : graph_params.
    153   ∀g_pars : more_sem_unserialized_params pars (joint_closed_internal_function pars).
     163  ∀pars : unserialized_params.
     164  ∀g_pars : ∀F.sem_unserialized_params pars F.
    154165  sem_params ≝
    155   λpars,g_pars.
     166  λpars,spars.
     167  let g_pars ≝ mk_graph_params pars in
    156168  mk_sem_params
    157     pars
     169    g_pars
    158170    (mk_more_sem_params
    159       pars
    160171      g_pars
     172      (spars ?)
    161173      graph_offset_of_label
    162174      graph_label_of_offset
     
    187199  λo.nat_of_bitvector ? (offv o).
    188200
    189 
    190201definition make_sem_lin_params :
    191   ∀pars : lin_params.
    192   ∀g_pars : more_sem_unserialized_params pars (joint_closed_internal_function pars).
     202  ∀pars : unserialized_params.
     203  (∀F.sem_unserialized_params pars F) →
    193204  sem_params ≝
    194   λpars,g_pars.
     205  λpars,spars.
     206  let lin_pars ≝ mk_lin_params pars in
    195207  mk_sem_params
    196     pars
     208    lin_pars
    197209    (mk_more_sem_params
    198       pars
    199       g_pars
     210      lin_pars
     211      (spars ?)
    200212      lin_offset_of_nat
    201213      lin_nat_of_offset
  • src/joint/Traces.ma

    r2442 r2443  
    77 ; exit: cpointer
    88 ; ev_genv: genv sparams globals
    9  ; io_env : state sparams → ∀o:io_out.res (io_in o)
     9(* ; io_env : state sparams → ∀o:io_out.res (io_in o) *)
    1010 }.
    1111 
     
    1313 { prog_spars : sem_params
    1414 ; prog : joint_program prog_spars
    15  ; prog_io : state prog_spars → ∀o.res (io_in o)
     15(* ; prog_io : state prog_spars → ∀o.res (io_in o) *)
    1616 }.
    1717
     
    2828  «ptr, refl …»
    2929  (mk_genv_gen ?? (globalenv_noinit ? p) ?)
    30   (prog_io pars).
     30 (* (prog_io pars) *).
    3131(* TODO or TOBEFOUND *)
    3232cases daemon
     
    4949  let dummy_pc ≝ mk_pointer (mk_block Code (-1)) (mk_offset (bv_zero …)) in
    5050  let spp : xpointer ≝ mk_pointer spb (mk_offset (bitvector_of_Z ? external_ram_size)) in
    51   let ispp : xpointer ≝ mk_pointer ispb (mk_offset (bitvector_of_nat ? 47)) in
     51(*  let ispp : xpointer ≝ mk_pointer ispb (mk_offset (bitvector_of_nat ? 47)) in *)
    5252  let main ≝ prog_main … p in
    53   let st0 ≝ mk_state pars (empty_framesT …) spp ispp (BBbit false) (empty_regsT … spp) m in
     53  let st0 ≝ mk_state pars (empty_framesT …) empty_is (BBbit false) (empty_regsT … spp) m in
     54  let st0' ≝ set_sp … spp st0 in
    5455  (* use exit sem_globals as ra and call_dest_for_main as dest *)
    55   ! st0' ← save_frame ?? sem_globals (exit sem_globals) (call_dest_for_main … pars) st0 ;
    56   let st_pc0 ≝ mk_state_pc ? st0' dummy_pc in
     56  ! st0'' ← save_frame ?? sem_globals (exit sem_globals) (call_dest_for_main … pars) st0 ;
     57  let st_pc0 ≝ mk_state_pc ? st0'' dummy_pc in
    5758  ! main_block ← opt_to_res … [MSG MissingSymbol; CTX ? main] (find_symbol … ge main) ;
    5859  ! main_fd ← opt_to_res ? [MSG BadPointer] (find_funct_ptr … ge main_block) ;
     
    6364  ].
    6465  [ %
    65   | cases ispb
    66   | cases spb
    67   ] normalize //
     66  | cases spb normalize //
     67  ]
    6868qed.
    6969
     
    114114qed.
    115115
     116(*
    116117let rec io_evaluate O I X (env : ∀o.res (I o)) (c : IO O I X) on c : res X ≝
    117118  match c with
     
    122123  | Wrong e ⇒ Error … e
    123124  ].
     125*)
    124126
    125127definition cost_label_of_stmt :
     
    145147   (* as_status ≝ *) (state_pc p)
    146148   (* as_execute ≝ *)
    147     (λs1,s2.io_evaluate … (io_env p s1) (eval_state … p (ev_genv p) s1) = return s2)
     149    (λs1,s2.(* io_evaluate … (io_env p s1) *) (eval_state … p (ev_genv p) s1) = return s2)
    148150   (* as_pc ≝ *) cpointerDeq
    149151   (* as_pc_of ≝ *) (pc …)
     
    151153    (λs.
    152154      match (
    153         ! 〈fn, stmt〉 ← fetch_statement ? p … (ev_genv p) (pc … s) ;
     155        ! 〈fn, stmt〉 ← fetch_statement ? p … (ev_genv p) (pc … s) : IO ???;
    154156        match stmt with
    155157        [ sequential stp nxt ⇒
    156           ! 〈flow, s'〉  ← io_evaluate … (io_env p s) (eval_step … (ev_genv p) fn s stp) ;
     158          ! 〈flow, s'〉  ← (* io_evaluate … (io_env p s) *) (eval_step … (ev_genv p) fn s stp) ;
    157159          return step_flow_classifier … flow
    158160        | final stp ⇒
    159           ! flow ← io_evaluate … (io_env p s) (eval_fin_step_pc … (ev_genv p) fn s stp) ;
     161          ! flow ← (* io_evaluate … (io_env p s) *) (eval_fin_step_pc … (ev_genv p) fn s stp) ;
    160162          return fin_step_flow_classifier … flow
    161163        ]) with
    162       [ OK c ⇒ c
    163       | Error _ ⇒ cl_other
     164      [ Value c ⇒ c
     165      | _ ⇒ cl_other
    164166      ])
    165167   (* as_label_of_pc ≝ *)
     
    175177      succ_pc p p (pc … s1) nxt = return pc … s2)
    176178   (* as_final ≝ *) (λs.is_final (globals ?) p (ev_genv p) (exit p) s ≠ None ?)
    177    (* as_call_ident_≝ *) ?. cases daemon (* TODO *) qed.
     179   (* as_call_ident_≝ *)
     180   (λst.?). cases daemon (* TODO *) qed.
  • src/joint/TranslateUtils.ma

    r2286 r2443  
    22include "joint/blocks.ma".
    33include "utilities/hide.ma".
     4include "utilities/deqsets.ma".
    45
    56(* general type of functions generating fresh things *)
     
    6465    add_graph … mid (final … (\snd b)) def
    6566  ].
     67
     68(* ignoring register allocation for now *)
     69
     70definition luniverse_ok : ∀p : graph_params.∀g.joint_internal_function p g → Prop ≝
     71λp,g,def.fresh_map_for_univ … (joint_if_code … def) (joint_if_luniverse … def).
     72
     73lemma present_to_memb : ∀tag,A,l,m.present tag A m l → bool_to_Prop (l∈m).
     74#tag #A * #l * #m whd in ⊢ (%→?%);
     75elim (lookup tag ???)
     76[ * #ABS elim (ABS ?) %
     77| #a #_ %
     78] qed.
     79
     80lemma memb_to_present : ∀tag,A,l,m.l∈m → present tag A m l.
     81#tag #A * #l * #m whd in ⊢ (?%→%);
     82elim (lookup tag ???)
     83[ * | #a * % #ABS destruct(ABS) ] qed.
     84
     85(*
     86lemma All_fresh_not_memb : ∀tag,u,l,id,u'.
     87  All (identifier tag) (λid'.¬fresh_for_univ tag id' u) l →
     88  〈id, u'〉 = fresh tag u →
     89  ¬id ∈ l.
     90#tag #u #l elim l [2: #hd #tl #IH] #id #u' *
     91[ #hd_fresh #tl_fresh #EQfresh
     92  whd in ⊢ (?(?%));
     93  change with (eq_identifier ???) in match (?==?);
     94  >eq_identifier_sym
     95  >(eq_identifier_false … (fresh_distinct … hd_fresh EQfresh))
     96  normalize nodelta @(IH … tl_fresh EQfresh)
     97| #_ %
     98]
     99qed.
     100*)
     101
     102lemma fresh_was_fresh : ∀tag,id,id',u,u'.
     103〈id,u'〉 = fresh tag u →
     104fresh_for_univ tag id' u' →
     105id' ≠ id →
     106fresh_for_univ tag id' u.
     107#tag * #id * #id' * #u * #u'
     108normalize #EQfresh destruct
     109#H #NEQ
     110elim (le_to_or_lt_eq … H)
     111[ (* not recompiling... /2 by monotonic_pred/ *) /2/ ]
     112#H >(succ_injective … H) in NEQ;
     113* #G elim (G (refl …))
     114qed.
     115
     116
     117(* use Russell? *)
     118axiom adds_graph_list_ok :
     119  ∀g_pars,globals,b,src,def.
     120  fresh_for_univ … src (joint_if_luniverse … def) →
     121  luniverse_ok ?? def →
     122  let 〈def', dst〉 ≝ adds_graph_list g_pars globals b src def in
     123  luniverse_ok ?? def' ∧
     124  ∃l.bool_to_Prop (uniqueb … l) ∧
     125     All … (λlbl.¬fresh_for_univ … lbl (joint_if_luniverse … def) ∧
     126                  fresh_for_univ … lbl (joint_if_luniverse … def')) l ∧
     127     src ~❨b,l❩~> dst in joint_if_code … def'.
     128(* #p #g #l elim l
     129[ #src #def #_ #Hdef whd
     130  %{Hdef} %{[ ]} %%%
     131| #hd #tl #IH #src #def #src_fresh #Hdef
     132  whd in match (adds_graph_list ?????);
     133  whd in match (fresh_label ???);
     134  @(pair_elim … (fresh ??)) normalize nodelta
     135  #mid #luniverse' #EQfresh
     136  whd in ⊢ (match % with [ _ ⇒ ?]);
     137  letin def' ≝ (add_graph p g src (sequential … hd mid) (set_luniverse … def luniverse'))
     138  cut (joint_if_code p g (set_luniverse p g def luniverse') = joint_if_code … def)
     139  [ cases def // ] #EQ_aux
     140  lapply (IH mid def' ??)
     141  [ #l whd in match def'; #Hpres
     142    lapply (present_to_memb … Hpres) -Hpres
     143    >mem_set_add @eq_identifier_elim
     144    [ #EQ destruct(EQ) *
     145    | #NEQ change with (? ∈ joint_if_code p ??) in ⊢ (?%→?); >EQ_aux
     146      #l_in
     147    ]
     148    @(fresh_remains_fresh … (sym_eq … EQfresh))
     149    [2: @Hdef @memb_to_present ] assumption
     150  | whd in match def';
     151    cases def #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9
     152    whd in match (set_luniverse ????);
     153    @(fresh_is_fresh … (sym_eq … EQfresh))
     154  ]
     155  elim (adds_graph_list ?????) #def'' #mid' normalize nodelta
     156  * #Hdef'' * #l ** #Hl1 #Hl2 #Hl3 %{Hdef''} %{(mid::l)}
     157  % [ % ]
     158  [ whd in ⊢ (?%);
     159    elim (true_or_false_Prop (mid∈l)) #H >H normalize nodelta
     160    [ elim (All_memb … Hl2 H)
     161      cases def #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 normalize in ⊢ (%→?);
     162      #H #_ @(absurd ?? H)
     163      @(fresh_remains_fresh … (eqEQfresh)
     164      normalize #H10 #H11
     165     
     166    >(All_fresh_not_memb … (sym_eq … EQfresh))
     167    [ assumption ]
     168    @(All_mp … Hl2) #lbl *
     169    cases def in EQfresh; #H11 #H12 #H13 #H14 #H15 #H16 #H17 #H18 #H19
     170    normalize #EQfresh #H #lbl_not_mid
     171    lapply(fresh_remains_fresh … H (sym_eq … EQfresh))
     172   
     173    elim (true_or_false_Prop (mid∈l)) #mid_l >mid_l
     174    [ normalize
     175*)
    66176
    67177(* preserves first statement if a cost label (should be an invariant) *)
     
    132242  ].
    133243
     244 
     245
    134246(* translation with inline fresh register allocation *)
    135247definition b_graph_translate :
  • src/joint/lineariseProof.ma

    r2442 r2443  
    2020definition graph_abstract_status:
    2121 ∀p:unserialized_params.
    22   (∀F.more_sem_unserialized_params p F) →
     22  (∀F.sem_unserialized_params p F) →
    2323    joint_program (mk_graph_params p) →
    2424     abstract_status
     
    2727  joint_abstract_status
    2828   (mk_prog_params
    29     (make_sem_graph_params (mk_graph_params p) (p' ?))
    30     prog ⊥).
    31 @daemon (* I/O, TODO *)
    32 qed.
     29    (make_sem_graph_params p p')
     30    prog).
    3331
    3432definition lin_abstract_status:
    3533 ∀p:unserialized_params.
    36   (∀F.more_sem_unserialized_params p F) →
     34  (∀F.sem_unserialized_params p F) →
    3735    joint_program (mk_lin_params p) →
    3836     abstract_status
     
    4139  joint_abstract_status
    4240   (mk_prog_params
    43     (make_sem_lin_params (mk_lin_params p) (p' ?))
    44     prog ⊥).
    45 @daemon (* I/O, TODO *)
    46 qed.
     41    (make_sem_lin_params p p')
     42    prog).
    4743
    4844definition linearise_status_rel:
  • src/joint/semantics.ma

    r2437 r2443  
    3333 ; empty_framesT: framesT
    3434 ; regsT : Type[0]
    35  ; empty_regsT: xpointer → regsT (* Stack pointer *)
     35 ; empty_regsT: xpointer → regsT (* initial stack pointer *)
     36 ; load_sp : regsT → res xpointer
     37 ; save_sp : regsT → xpointer → regsT
    3638 }.
     39
     40inductive internal_stack : Type[0] ≝
     41| empty_is : internal_stack
     42| one_is : beval → internal_stack
     43| both_is : beval → beval → internal_stack.
     44
     45axiom InternalStackFull : String.
     46axiom InternalStackEmpty : String.
     47
     48definition is_push : internal_stack → beval → res internal_stack ≝
     49λis,bv.match is with
     50[ empty_is ⇒ return one_is bv
     51| one_is bv' ⇒ return both_is bv' bv
     52| both_is _ _ ⇒ Error … [MSG … InternalStackFull]
     53].
     54
     55definition is_pop : internal_stack → res (beval × internal_stack) ≝
     56λis.match is with
     57[ empty_is ⇒ Error … [MSG … InternalStackEmpty]
     58| one_is bv' ⇒ return 〈bv', empty_is〉
     59| both_is bv bv' ⇒ return 〈bv', one_is bv〉
     60].
    3761
    3862record state (semp: sem_state_params): Type[0] ≝
    3963 { st_frms: framesT semp
    40  ; sp: xpointer
    41  ; isp: xpointer
     64 ; istack : internal_stack
    4265 ; carry: bebit
    4366 ; regs: regsT semp
     
    4568 }.
    4669
    47 coercion sem_state_params_to_state nocomposites:
    48   ∀p : sem_state_params.Type[0] ≝ state on _p : sem_state_params to Type[0].
     70definition sp ≝ λp,st.load_sp p (regs ? st).
    4971
    5072record state_pc (semp : sem_state_params) : Type[0] ≝
     
    5476
    5577definition set_m: ∀p. bemem → state p → state p ≝
    56  λp,m,st. mk_state p (st_frms ?…st) (sp … st) (isp … st) (carry … st) (regs … st) m.
     78 λp,m,st. mk_state p (st_frms …st) (istack … st) (carry … st) (regs … st) m.
    5779
    5880definition set_regs: ∀p:sem_state_params. regsT p → state p → state p ≝
    59  λp,regs,st. mk_state p (st_frms … st) (sp … st) (isp … st) (carry … st) regs (m … st).
     81 λp,regs,st.mk_state p (st_frms … st) (istack … st) (carry … st) regs (m … st).
    6082
    6183definition set_sp: ∀p. ? → state p → state p ≝
    62  λp,sp,st. mk_state … (st_frms … st) sp (isp … st) (carry … st) (regs … st) (m … st).
    63 
    64 definition set_isp: ∀p. ? → state p → state p ≝
    65  λp,isp,st. mk_state … (st_frms … st) (sp … st) isp (carry … st) (regs … st) (m … st).
     84 λp,sp,st.let regs' ≝ save_sp … (regs … st) sp in
     85 mk_state p (st_frms … st) (istack … st) (carry … st) regs' (m … st).
    6686
    6787definition set_carry: ∀p. bebit → state p → state p ≝
    68  λp,carry,st. mk_state … (st_frms … st) (sp … st) (isp … st) carry (regs … st) (m … st).
     88 λp,carry,st. mk_state … (st_frms … st) (istack … st) carry (regs … st) (m … st).
     89
     90definition set_istack: ∀p. internal_stack → state p → state p ≝
     91 λp,is,st. mk_state … (st_frms … st) is (carry … st) (regs … st) (m … st).
    6992
    7093definition set_pc: ∀p. ? → state_pc p → state_pc p ≝
     
    7598
    7699definition set_frms: ∀p:sem_state_params. framesT p → state p → state p ≝
    77  λp,frms,st. mk_state … frms (sp … st) (isp … st) (carry … st) (regs … st) (m … st).
     100 λp,frms,st. mk_state … frms (istack … st) (carry … st) (regs … st) (m … st).
    78101
    79102axiom BadProgramCounter : String.
     
    111134  | FEnd2  : fin_step_flow p F Call. (* end flow *)
    112135
    113 record more_sem_unserialized_params
     136record sem_unserialized_params
    114137  (uns_pars : unserialized_params)
    115138  (F : list ident → Type[0]) : Type[1] ≝
    116   { st_pars :> sem_state_params (* automatic coercion has issues *)
     139  { st_pars :> sem_state_params
    117140  ; acca_store_ : acc_a_reg uns_pars → beval → regsT st_pars → res (regsT st_pars)
    118141  ; acca_retrieve_ : regsT st_pars → acc_a_reg uns_pars → res beval
     
    129152  ; snd_arg_retrieve_ : regsT st_pars → snd_arg uns_pars → res beval
    130153  ; pair_reg_move_ : regsT st_pars → pair_move uns_pars → res (regsT st_pars)
    131   ; fetch_ra: state st_pars → res ((state st_pars) × cpointer)
     154  ; fetch_ra: state st_pars → res (cpointer × (state st_pars))
    132155
    133156  ; allocate_local : localsT uns_pars → regsT st_pars → regsT st_pars
     
    169192definition helper_def_retrieve :
    170193  ∀X : ? → ? → ? → Type[0].
    171   (∀up,F.∀p:more_sem_unserialized_params up F. regsT (st_pars up F p) → X up F p → res beval) →
    172   ∀up,F.∀p : more_sem_unserialized_params up F.state (st_pars up F p) → X up F p → res beval ≝
     194  (∀up,F.∀p:sem_unserialized_params up F. regsT (st_pars up F p) → X up F p → res beval) →
     195  ∀up,F.∀p : sem_unserialized_params up F.state (st_pars up F p) → X up F p → res beval ≝
    173196    λX,f,up,F,p,st.f ?? p (regs … st).
    174197
    175198definition helper_def_store :
    176199  ∀X : ? → ? → ? → Type[0].
    177   (∀up,F.∀p : more_sem_unserialized_params up F.X up F p → beval → regsT (st_pars … p) → res (regsT (st_pars … p))) →
    178   ∀up,F.∀p : more_sem_unserialized_params up F.X up F p → beval → state (st_pars … p) → res (state (st_pars … p)) ≝
     200  (∀up,F.∀p : sem_unserialized_params up F.X up F p → beval → regsT (st_pars … p) → res (regsT (st_pars … p))) →
     201  ∀up,F.∀p : sem_unserialized_params up F.X up F p → beval → state (st_pars … p) → res (state (st_pars … p)) ≝
    179202  λX,f,up,F,p,x,v,st.! r ← f ?? p x v (regs … st) ; return set_regs … r st.
    180203
     
    193216definition snd_arg_retrieve ≝ helper_def_retrieve ? snd_arg_retrieve_.
    194217definition pair_reg_move ≝
    195   λup,F.λp : more_sem_unserialized_params up F.λst : state (st_pars … p).λpm : pair_move up.
     218  λup,F.λp : sem_unserialized_params up F.λst : state (st_pars … p).λpm : pair_move up.
    196219    ! r ← pair_reg_move_ ?? p (regs ? st) pm;
    197220    return set_regs ? r st.
    198 
    199221 
    200222axiom BadPointer : String.
     
    208230   serialization and on whether the call is a tail one. *)
    209231definition eval_call_block:
    210  ∀p,F.∀p':more_sem_unserialized_params p F.∀globals.
     232 ∀p,F.∀p':sem_unserialized_params p F.∀globals.
    211233  genv_t (fundef (F globals)) → state (st_pars ?? p') → block → call_args p → call_dest p →
    212234    IO io_out io_in ((step_flow p (F globals) Call)×(state (st_pars ?? p'))) ≝
     
    232254definition push: ∀p.state p → beval → res (state p) ≝
    233255 λp,st,v.
    234   let isp' ≝ isp ? st in
    235   do m ← opt_to_res ? (msg FailedStore) (bestorev (m … st) isp' v);
    236   let isp'' ≝ shift_pointer … isp' [[false;false;false;false;false;false;false;true]] in
    237   return set_m … m (set_isp … isp'' st).
    238   normalize elim (isp p st) #p #H @H
    239 qed.
    240 
    241 definition pop: ∀p. state p → res ((state p ) × beval) ≝
     256 ! is ← is_push (istack … st) v ;
     257 return set_istack … is st.
     258
     259definition pop: ∀p. state p → res (beval × (state p)) ≝
    242260 λp,st.
    243   let isp' ≝ isp ? st in
    244   let isp'' ≝ neg_shift_pointer ? isp' [[false;false;false;false;false;false;false;true]] in
    245   let ist ≝ set_isp … isp'' st in
    246   do v ← opt_to_res ? (msg FailedStore) (beloadv (m ? st) isp'');
    247   OK ? 〈ist,v〉.
    248   normalize elim (isp p st) #p #H @H
    249 qed.
     261 ! 〈bv, is〉 ← is_pop (istack … st) ;
     262 return 〈bv, set_istack … is st〉.
    250263
    251264definition save_ra : ∀p. state p → cpointer → res (state p) ≝
    252265 λp,st,l.
    253   ! 〈addrl,addrh〉 ← beval_pair_of_pointer l ; (* always succeeds *)
     266  let 〈addrl,addrh〉 ≝  beval_pair_of_pointer l in
    254267  ! st' ← push … st addrl;
    255268  push … st' addrh.
    256269
    257 definition load_ra : ∀p.state p → res ((state p) × cpointer) ≝
     270definition load_ra : ∀p.state p → res (cpointer × (state p)) ≝
    258271 λp,st.
    259   do 〈st',addrh〉 ← pop … st;
    260   do 〈st'',addrl〉 ← pop … st';
     272  do 〈addrh, st'〉 ← pop … st;
     273  do 〈addrl, st''〉 ← pop … st';
    261274  do pr ← pointer_of_address 〈addrh, addrl〉;
    262   match ptype pr return λx.ptype pr = x → res (? × cpointer) with
    263   [ Code ⇒ λprf.return 〈st'', «pr,prf»
     275  match ptype pr return λx.ptype pr = x → res (cpointer × ?) with
     276  [ Code ⇒ λprf.return 〈«pr,prf», st''
    264277  | _ ⇒ λ_.Error … [MSG BadPointer]
    265278  ] (refl …).
     
    267280(* parameters that are defined by serialization *)
    268281record more_sem_params (pp : params) : Type[1] ≝
    269   { msu_pars :> more_sem_unserialized_params pp (joint_closed_internal_function pp)
     282  { msu_pars :> sem_unserialized_params pp (joint_closed_internal_function pp)
    270283  ; offset_of_point : code_point pp → option offset (* can overflow *)
    271284  ; point_of_offset : offset → code_point pp
     
    463476    return set_m … m' st
    464477  | ADDRESS id prf ldest hdest ⇒
    465     let addr ≝ opt_safe ? (find_symbol … ge id) ? in
    466     ! 〈laddr,haddr〉 ← beval_pair_of_pointer (mk_pointer addr zero_offset) ;
     478    let addr_block ≝ opt_safe ? (find_symbol … ge id) ? in
     479    let 〈laddr,haddr〉 ≝ beval_pair_of_pointer (mk_pointer addr_block zero_offset) in
    467480    ! st' ← dpl_store … ldest laddr st;
    468481    dph_store … hdest haddr st'
     
    488501    accb_store … dacc_b_reg v2' st'
    489502  | POP dst ⇒
    490     ! 〈st',v〉 ← pop p st;
     503    ! 〈v, st'〉 ← pop p st;
    491504    acca_store … p dst v st'
    492505  | PUSH src ⇒
     
    601614    do_call … ge st id fn args
    602615  | _ ⇒
    603     ! 〈st',ra〉 ← fetch_ra … st ;
     616    ! 〈ra, st'〉 ← fetch_ra … st ;
    604617    ! fn ← fetch_function … ge curr ;
    605618    ! st'' ← pop_frame … ge fn st';
     
    640653    match s' with
    641654    [ RETURN ⇒
    642       do 〈st',ra〉 ← fetch_ra … st;
     655      do 〈ra, st'〉 ← fetch_ra … st;
    643656      if eq_pointer ra exit then
    644657       do vals ← read_result … ge (joint_if_result … fn) st' ;
  • src/utilities/deqsets.ma

    r2296 r2443  
    11include "basics/deqsets.ma".
     2include "basics/lists/listb.ma".
     3include "ASM/Util.ma".
    24
    35lemma eqb_elim : ∀D:DeqSet. ∀P:bool → Type[0]. ∀x,y:D.
     
    911| #_ #FF @F % #E destruct lapply (FF (refl ??)) #E destruct
    1012] qed.
     13
     14
     15(* is it already there? *)
     16lemma All_memb : ∀A : DeqSet.∀P,l,x.All A P l → x ∈ l → P x.
     17#A #P #l elim l
     18[ #x * *
     19| #hd #tl #IH #x * #Phd #Ptl
     20  normalize @(eqb_elim A) #H normalize nodelta [destruct * @Phd]
     21  @IH @Ptl
     22]
     23qed.
  • src/utilities/lists.ma

    r2440 r2443  
    150150definition Append : ∀A.Aop ? (nil A) ≝ λA.mk_Aop ? ? (append ?) ? ? ?.
    151151// qed.
    152 
    153 let rec range_strong_internal (start, how_many, end : ℕ)
    154   on how_many : start + how_many ≤ end → list (Σn : ℕ.n < end) ≝
    155 match how_many return λx.start + x ≤ end → ?
    156   with
    157 [ O ⇒ λ_.[ ]
    158 | S k ⇒ λprf.«start, ?» :: range_strong_internal (S start) k end ?
    159 ].
    160 [2: //]
    161 >(plus_n_O start) /2 by plus_lt_to_lt/
    162 qed.
    163 
    164 definition range_strong : ∀end : ℕ. list (Σn.n<end) ≝
    165   λend.range_strong_internal 0 end end (le_n …).
    166152
    167153definition List ≝ MakeMonadProps
     
    379365| cons h t ⇒ ordered_insert A lt h (insert_sort A lt t)
    380366].
     367
     368(* range from 0 to n excluded with proof of minoration *)
     369
     370let rec range_strong_internal (index, how_many, end : ℕ) on how_many :
     371  index + how_many = end →
     372  list (Σn.n<end) ≝
     373  match how_many return λhow_many.index + how_many = end → ? with
     374  [ O ⇒ λ_.[ ]
     375  | S k ⇒ λprf.«index, ?» :: range_strong_internal (S index) k end ?
     376  ].
     377<prf
     378[ >(plus_n_O index) in ⊢ (?%?); @monotonic_lt_plus_r @le_S_S @le_O_n
     379| @plus_n_Sm
     380]
     381qed.
     382
     383definition range_strong : ∀end.list (Σn.n < end) ≝
     384λend.range_strong_internal 0 ? end (refl …).
Note: See TracChangeset for help on using the changeset viewer.