include "ASM/BitVectorTrie.ma".
include "ASM/Arithmetic.ma".
(*include "ASM/UtilBranch.ma". *)

include "utilities/option.ma".

include alias "arithmetics/nat.ma".

let rec nat_bound_opt (N:nat) (n:nat) : option (n < N) ≝
match N return λy. option (n < y) with
[ O ⇒ None ?
| S N' ⇒
    match n return λx. option (x < S N') with
    [ O ⇒ (return (lt_O_S ?))
    | S n' ⇒ (! prf ← nat_bounded N' n' ; return (le_S_S ?? prf))
    ]
].


(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
(* Program Counters & Object Code: BitVectors, Nats  and Lists of Bytes       *)
(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)

(* from Fetch.ma *)
definition bitvector_max_nat ≝ λlength: nat. 2^length.

definition size_ok ≝ 
  λn.λsize. size ≤ bitvector_max_nat n. 

lemma size_ok_mono : 
  ∀n. ∀s,s'. s' ≤ s → size_ok n s -> size_ok n s'. 
  #n #s #s' #mono #ok @(transitive_le … ok) //
qed. 

lemma size_okS : 
  ∀n. ∀s. size_ok n (S s) → size_ok n s. 
  #n #s #ok @size_ok_mono //
qed. 

lemma size_okS' : 
  ∀n. ∀s. size_ok n (s+1) → size_ok n s. 
  #n #s #ok @size_ok_mono //
qed. 

definition address_ok ≝ 
  λn.λaddr. size_ok n (S addr). 

lemma size_okS_to_address_ok : 
  ∀n. ∀s. size_ok n (S s) → address_ok n s. 
  #n #s #ok assumption. 
qed. 

lemma address_ok_to_size_okS : 
  ∀n. ∀pc. address_ok n pc → size_ok n (S pc). 
  #n #pc #ok assumption. 
qed. 

lemma size_ok_neq_to_address_ok : 
  ∀n. ∀s. size_ok n s → s ≠ bitvector_max_nat n → address_ok n s. 
  #n #s #s_ok #s_neq
  @not_eq_to_le_to_lt assumption
qed.

lemma address_ok_mono : 
  ∀n. ∀pc,pc'. pc' ≤ pc → address_ok n pc -> address_ok n pc'. 
  #n #pc #pc' #mono #ok 
  @size_okS_to_address_ok
  @(size_ok_mono … (le_S_S …)) 
  assumption
qed. 

lemma address_okS : 
  ∀n. ∀pc. address_ok n (S pc) → address_ok n pc. 
  #n #pc #ok @address_ok_mono //
qed. 

lemma address_okS' : 
  ∀n. ∀pc. address_ok n (pc+1) → address_ok n pc. 
  #n #pc #ok @address_ok_mono //
qed. 

definition addrS : ∀n. BitVector n → BitVector n ≝ (* can overflow back to 0 *)
  λn.λpc. add n pc (bitvector_of_nat n 1).
  
lemma addrS_is_Saddr : ∀n. ∀pc. 
  let npcS ≝ S (nat_of_bitvector n pc) in 
    address_ok n npcS → 
      nat_of_bitvector ? (addrS ? pc) = npcS.
  #n #pc #pcS_ok cases daemon 
  (* XXX: needs UtilBranch.ma; needs re-proving!
  >succ_nat_of_bitvector_half_add_1
  [2: 
    @le_plus_to_minus_r
    change with (S ? ≤ ?) <plus_n_Sm <plus_n_O assumption
  |1: cases daemon
  ] *)
qed. 

lemma addrS_useful : ∀n. ∀pc. 
  let npcS ≝ S (nat_of_bitvector n pc) in 
    ∀m. plus npcS (S m) = bitvector_max_nat n →  
      nat_of_bitvector ? (addrS ? pc) = npcS.
#n #pc #offset #npcS_ok
@addrS_is_Saddr //
qed. 

lemma addr_useful : ∀n. ∀pc. 
  let npc ≝ nat_of_bitvector n pc in 
    ∀k,m. plus npc m = bitvector_max_nat n → 
      k < m → address_ok n (npc + k). 
#n #pc #k #m #max #lt change with (? < ?)
<max @monotonic_lt_plus_r assumption
qed.    

lemma addr_max : ∀n. ∀pc. 
  let npc ≝ nat_of_bitvector n pc in 
    address_ok n npc ->  address_ok n (S npc) ∨ S npc = bitvector_max_nat n. 
#n #pc #ok @(le_to_or_lt_eq … (lt_nat_of_bitvector … pc))
qed.    

lemma addr_overflow_offset : ∀n.∀pc. 
  let npc ≝ nat_of_bitvector n pc in 
    ∀m. npc + m = bitvector_max_nat n → add n pc (bitvector_of_nat n m) = (zero n).
  #n #pc #m #eq <(add_overflow … eq) >bitvector_of_nat_inverse_nat_of_bitvector //
qed. 

lemma addrS_overflow : ∀n. ∀pc. 
  let npc ≝ nat_of_bitvector n pc in 
    S npc = bitvector_max_nat n → addrS n pc = (zero n). 
#n #pc #max change with (add ? ? ? = ?) 
@addr_overflow_offset >commutative_plus assumption
qed.

(* now we fix the magic number 16 *)

definition ADDRESS_WIDTH ≝ 16. 

definition PC  ≝ BitVector ADDRESS_WIDTH. 

definition pc0 : PC ≝ zero ?. 

definition nat_of_PC : PC → nat ≝ nat_of_bitvector ?. 

definition PC_of_nat : nat → PC ≝ bitvector_of_nat ?. 

definition pcS : PC → PC ≝ addrS ?.

definition max_program_size ≝ bitvector_max_nat ADDRESS_WIDTH.

definition program_size_ok ≝ size_ok ADDRESS_WIDTH. 

definition program_size_ok_mono ≝ size_ok_mono ADDRESS_WIDTH. 

definition program_size_okS_to_program_counter_ok ≝ size_okS_to_address_ok ADDRESS_WIDTH.  

definition program_size_okS ≝ size_okS ADDRESS_WIDTH. 

definition program_size_okS' ≝ size_okS' ADDRESS_WIDTH. 

definition program_counter_ok ≝ address_ok ADDRESS_WIDTH. 

definition program_counter_ok_mono ≝ address_ok_mono ADDRESS_WIDTH. 

definition program_counter_okS ≝ address_okS ADDRESS_WIDTH. 

definition program_counter_okS' ≝ address_okS' ADDRESS_WIDTH. 

definition program_size_ok_neq_to_program_counter_ok: 
  ∀s. program_size_ok s → s ≠ max_program_size → program_counter_ok s ≝ 
  size_ok_neq_to_address_ok ?.

lemma nat_of_PC_inverse_PC_of_nat : 
  ∀n. program_counter_ok n →  
    nat_of_PC (PC_of_nat n) = n. 
  #n #n_ok @nat_of_bitvector_bitvector_of_nat_inverse assumption
qed.

lemma PC_of_nat_inverse_nat_of_PC : 
  ∀pc. PC_of_nat (nat_of_PC pc) = pc. 
  #pc @bitvector_of_nat_inverse_nat_of_bitvector 
qed.

lemma nat_of_PC_offset :  ∀n.∀pc: PC. 
  program_counter_ok (n + nat_of_PC pc) →  
    nat_of_PC (add … (PC_of_nat n) pc) = n + nat_of_PC pc. 
  #n #pc #n_pc_ok
  cut (program_counter_ok n)
    [@program_counter_ok_mono //]
  #n_ok change with (nat_of_bitvector … (add ? ? ?) = ?)
  >nat_of_bitvector_add 
    [1: change with (((nat_of_PC ?) + (nat_of_PC ?)) = ?)
    |2: change with (program_counter_ok ((nat_of_PC ?) + (nat_of_PC ?)))
    ]
  >nat_of_PC_inverse_PC_of_nat //
qed. 

lemma nat_of_PC_offset' :  ∀n.∀pc: PC. 
  program_counter_ok (nat_of_PC pc + n) →  
    nat_of_PC (add … pc (PC_of_nat n)) = nat_of_PC pc + n. 
  #n #pc >commutative_plus >add_commutative @nat_of_PC_offset
qed.

definition pcS_useful : ∀pc. 
  let npcS ≝ S (nat_of_PC pc) in 
    ∀m. plus npcS (S m) = max_program_size →  
      nat_of_PC (pcS pc) = npcS ≝ 
      addrS_useful ?.

lemma pc_useful : ∀pc. 
  let npc ≝ nat_of_PC pc in 
    ∀k,m. plus npc k = max_program_size → 
      m < k → address_ok ? (npc + m) ≝ 
  λpc.λk,m.λEQ.λLT.(addr_useful … EQ LT).   

definition pcS_is_Spc : ∀pc: PC. 
  let npcS ≝ S (nat_of_PC pc) in 
    address_ok ? npcS → 
      nat_of_PC (pcS pc) = npcS ≝ 
      addrS_is_Saddr ?.
      
definition pc_max : ∀pc. 
  let npc ≝ nat_of_PC pc in 
    program_counter_ok npc -> 
      program_counter_ok (S npc) ∨ S npc = max_program_size ≝ 
  addr_max ?.
  
definition pcS_overflow : ∀pc. 
  let npc ≝ nat_of_PC pc in 
    S npc = max_program_size -> pcS pc = pc0 ≝ addrS_overflow ?.  

definition pc_overflow_offset : ∀m.∀pc. 
  let npc ≝ nat_of_PC pc in 
    npc + m = max_program_size -> add ? pc (PC_of_nat m) = pc0.
  #m #pc #max @addr_overflow_offset assumption
qed. 

(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
(* Memory: one of two distinguished instances of BitVectorTrie.               *)
(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)

definition byte0 : Byte ≝ zero ?. 

definition RAM ≝ BitVectorTrie Byte.  

definition ram0 : ∀n. RAM n ≝   
  λn. Stub …. 

definition memory_lookup : ∀n. BitVector n → RAM n → Byte ≝   
  λn,addr,mem. lookup ? n addr mem byte0. 

(* instances *)

definition code_memory ≝ RAM ADDRESS_WIDTH. 

definition code_memory0 : code_memory ≝ ram0 ?. 

definition code_memory_lookup : PC → code_memory → Byte ≝ memory_lookup ?.

(* ***** Object-code ***** JHM: push elsewherein ASM/*.ma? *)

(*
inductive nat_bounded : nat → nat → Type[0] ≝
| nat_ok : ∀n,m:nat. nat_bounded n (n+m)
| nat_overflow : ∀n,m:nat. nat_bounded (n+S m) n.

let rec nat_bound (n:nat) (m:nat) : nat_bounded n m ≝
match n return λx. nat_bounded x m with
[ O ⇒ nat_ok ??
| S n' ⇒
    match m return λy. nat_bounded (S n') y with
    [ O ⇒ nat_overflow O ?
    | S m' ⇒ match nat_bound n' m' return λx,y.λ_. nat_bounded (S x) (S y) with
             [ nat_ok x y ⇒ nat_ok ??
             | nat_overflow x y ⇒ nat_overflow (S x) y
             ]
    ]
].

lemma nat_bound_opt : ∀N,n:nat. option (n ≤ N). 
  #N #n elim (nat_bound n N) -n #n #offset 
  [ @Some //
  | @None
  ]
qed.  
*)

definition program_ok_opt : ∀A. ∀instrs : list A. option (program_size_ok (S(|instrs|)))
  ≝ λA.λinstrs. nat_bound_opt max_program_size (S(|instrs|)). (* for Policy.ma etc. *)