Changeset 2767 for src/ASM/CodeMemory.ma


Ignore:
Timestamp:
Mar 3, 2013, 2:03:58 PM (7 years ago)
Author:
mckinna
Message:

WARNING: BIG commit, which pushes code_size_opt check into LIN/LINToASM.ma
following CSC's comment on my previous partial commit
plus rolls all the miscellaneous code motion into the rest of the repo.

suggest REBUILD compiler.ma/correctness.ma from scratch.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/CodeMemory.ma

    r2754 r2767  
    44(*include "ASM/UtilBranch.ma". *)
    55
     6include "utilities/option.ma".
     7
    68include alias "arithmetics/nat.ma".
     9
     10let rec nat_bound_opt (N:nat) (n:nat) : option (n < N) ≝
     11match N return λy. option (n < y) with
     12[ O ⇒ None ?
     13| S N' ⇒
     14    match n return λx. option (x < S N') with
     15    [ O ⇒ (return (lt_O_S ?))
     16    | S n' ⇒ (! prf ← nat_bounded N' n' ; return (le_S_S ?? prf))
     17    ]
     18].
     19
    720
    821(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     
    247260(* ***** Object-code ***** JHM: push elsewherein ASM/*.ma? *)
    248261
     262(*
    249263inductive nat_bounded : nat → nat → Type[0] ≝
    250264| nat_ok : ∀n,m:nat. nat_bounded n (n+m)
     
    270284  ]
    271285qed. 
    272 
    273 definition program_ok_opt : ∀A. ∀instrs : list A. option (program_size_ok (S(S(|instrs|))))
    274   ≝ λA.λinstrs. nat_bound_opt max_program_size (S(S(|instrs|))). (* for Policy.ma etc. *)
    275 
    276 
    277 
    278 
    279 
    280  
     286*)
     287
     288definition program_ok_opt : ∀A. ∀instrs : list A. option (program_size_ok (S(|instrs|)))
     289  ≝ λA.λinstrs. nat_bound_opt max_program_size (S(|instrs|)). (* for Policy.ma etc. *)
     290
Note: See TracChangeset for help on using the changeset viewer.