Theory DS_Clause_Builder

section ‹Clause Builder›  
theory DS_Clause_Builder
imports 
  LRAT_Sepref_Base
  DS_Clause
begin


  subsection ‹Functional Level›    
  (* Clause builder: Assemble in intermediate buffer, then make clause *)  
    
  (* max-lit × buf × bound *)  
  type_synonym cbld = "nat × cbuf × nat"
    
  definition cbld_invar :: "cbld ⇒ bool" where 
    "cbld_invar ≡ λ(ml,cb,bnd). length cb ≤ bnd ∧ (∀l∈cbuf_α cb. ulit_of l ≤ ml)"
  
  definition cbld_α_clause :: "cbld ⇒ dv_clause" where 
    "cbld_α_clause ≡ λ(ml,cb,bnd). cbuf_α cb"  
  
  definition cbld_α_cap :: "cbld ⇒ nat" where "cbld_α_cap ≡ λ(ml,cb,bnd). bnd - length cb"
  
  definition cbld_α_maxlit :: "cbld ⇒ nat" where "cbld_α_maxlit ≡ λ(ml,cb,bnd). ml"

  
  lemma cbld_α_maxlit_bound: "⟦cbld_invar bld; x∈cbld_α_clause bld⟧ ⟹ ulit_of x  ≤ cbld_α_maxlit bld"
    unfolding cbld_invar_def cbld_α_clause_def cbld_α_maxlit_def
    by (auto)
  
    
  
    
  definition cbld_make :: "_ ⇒ _ ⇒ _ ⇒ cbld" where [simp]: "cbld_make ml cb bnd ≡ (ml,cb,bnd)"
  definition cbld_dest :: "cbld ⇒ _" where [simp]: "cbld_dest bld ≡ bld"
  
  
  definition cbld_new :: "nat ⇒ cbld" where "cbld_new cap ≡ cbld_make 0 cbuf_empty cap"
  
  lemma cbld_new_correct[simp]:
    shows
      "cbld_invar (cbld_new n)"
      "cbld_α_clause (cbld_new n) = {}"
      "cbld_α_cap (cbld_new n) = n"
      "cbld_α_maxlit (cbld_new n) = 0"
    unfolding cbld_invar_def cbld_α_clause_def cbld_α_cap_def cbld_new_def cbld_α_maxlit_def
    by auto
  
  
  definition cbld_add_lit :: "dv_lit ⇒ cbld ⇒ cbld nres" where
    "cbld_add_lit l bld ≡ doN {
      let (ml,cb,bnd) = cbld_dest bld;
      ASSERT(length cb < bnd);
      let ml = max (ulit_of l) ml;
      let cb = cbuf_insert l cb;
      RETURN (cbld_make ml cb bnd)
    }"
      
  lemma cbld_add_lit_correct[refine_vcg]: 
    "⟦cbld_invar bld; cbld_α_cap bld > 0⟧ ⟹ cbld_add_lit l bld ≤ SPEC (λbld'. 
      cbld_invar bld'
    ∧ cbld_α_clause bld' = insert l (cbld_α_clause bld)
    ∧ cbld_α_cap bld' = cbld_α_cap bld - 1
    ∧ cbld_α_maxlit bld' = max (cbld_α_maxlit bld) (ulit_of l)
    )"
    unfolding cbld_add_lit_def
    apply refine_vcg
    unfolding cbld_invar_def cbld_α_clause_def cbld_α_cap_def cbld_α_maxlit_def
    by auto
  
  definition cbld_finish_clause :: "cbld ⇒ (dv_clause × cbld) nres" where
    "cbld_finish_clause bld ≡ doN {
      let (ml,cb,bnd) = cbld_dest bld;
      ASSERT (length cb < bnd);
      cl ← zcl_make cb;
      let cb = cbuf_flush cb;
      RETURN (cl,cbld_make ml cb bnd)
    }"
  
  lemma cbld_finish_clause_correct[refine_vcg]: "⟦ cbld_invar bld; cbld_α_cap bld > 0 ⟧ 
    ⟹ cbld_finish_clause bld ≤ SPEC (λ(cl,bld').     
       cl = cbld_α_clause bld
    ∧ cbld_invar bld'
    ∧ cbld_α_clause bld' = {}
    ∧ cbld_α_cap bld' ≥ cbld_α_cap bld
    ∧ cbld_α_maxlit bld' = cbld_α_maxlit bld
    )"  
    unfolding cbld_finish_clause_def
    apply refine_vcg
    unfolding cbld_invar_def cbld_α_clause_def cbld_α_cap_def cbld_α_maxlit_def
    apply simp_all
    subgoal (* TODO: slight breaking of abstraction *)
      unfolding cbuf_α_def by auto
    done

  definition cbld_abort_clause :: "cbld ⇒ cbld nres" where
    "cbld_abort_clause bld ≡ doN {
      let (ml,cb,bnd) = cbld_dest bld;
      let cb = cbuf_flush cb;
      RETURN (cbld_make ml cb bnd)
    }"
    
  lemma cbld_abort_clause_correct[refine_vcg]: "⟦ cbld_invar bld ⟧ 
    ⟹ cbld_abort_clause bld ≤ SPEC (λbld'.     
      cbld_invar bld'
    ∧ cbld_α_clause bld' = {}
    ∧ cbld_α_cap bld' ≥ cbld_α_cap bld
    ∧ cbld_α_maxlit bld' = cbld_α_maxlit bld
    )"  
    unfolding cbld_abort_clause_def
    apply refine_vcg
    unfolding cbld_invar_def cbld_α_clause_def cbld_α_cap_def cbld_α_maxlit_def
    by simp_all
    
        
  definition cbld_is_empty :: "cbld ⇒ bool nres" where
    "cbld_is_empty bld ≡ doN {
      let (ml,cb,bnd) = cbld_dest bld;
      let r = (length cb = 0);
      let bld' = cbld_make ml cb bnd;
      unborrow bld' bld;
      RETURN r
    }"

  lemma cbld_is_empty_correct[refine_vcg]: "cbld_invar bld ⟹ cbld_is_empty bld ≤ SPEC (λr. r ⟷ cbld_α_clause bld = {})"  
    unfolding cbld_is_empty_def
    apply refine_vcg
    unfolding cbld_invar_def cbld_α_clause_def cbuf_α_def
    by auto
    
  definition cbld_get_maxlit :: "cbld ⇒ nat nres" where
    "cbld_get_maxlit bld ≡ doN {
      let (ml,cb,bnd) = cbld_dest bld;
      let bld' = cbld_make ml cb bnd;
      unborrow bld' bld;
      RETURN ml
    }"
    
  lemma dbld_get_maxlit_correct[refine_vcg]: "cbld_invar bld ⟹ cbld_get_maxlit bld ≤ SPEC (λr. r = cbld_α_maxlit bld)"
    unfolding cbld_get_maxlit_def
    apply refine_vcg
    apply (auto simp: cbld_α_maxlit_def)
    done
        

  subsection ‹Refinement to Imperative Code›  
    
  type_synonym cbldi = "lit_size_t word × (lit_size_t word,size_t) array_list"  
  definition cbld_assn :: "cbld ⇒ cbldi ⇒ assn" where "cbld_assn ≡ λ(ml,cb,bnd) (mli,cbi). 
      lit_assn ml mli 
    ** cbuf_aux_assn cb cbi 
    ** dropi_assn (rdomp size_assn) bnd ghost_var"
    
  sepref_register cbld_make cbld_dest cbld_new cbld_add_lit cbld_finish_clause cbld_is_empty

      
  definition cbld_make_impl :: "_ ⇒ _ ⇒ 'a word ⇒ cbldi llM" 
    where [llvm_inline]: "cbld_make_impl mli cbi _ ≡ Mreturn (mli,cbi)"
  
  lemma cbld_make_impl_refine[sepref_fr_rules]: 
    "(uncurry2 cbld_make_impl,uncurry2 (RETURN ooo cbld_make)) 
    ∈ [λ_. True]⇩c lit_assn⇧k *⇩a cbuf_aux_assn⇧d *⇩a size_assn⇧k → cbld_assn [λ((ml,cb),_) r. r = (ml,cb) ]⇩c"
    unfolding cbld_make_def cbld_make_impl_def cbld_assn_def any_rel_def
    apply sepref_to_hoare
    apply vcg_normalize
    
    apply (simp named_ss HOL_basic_ss_nomatch: move_resolve_ex_eq)
    
    supply [simp] = rdomp_pure_rel_eq
    apply vcg
    done    
  
  lemma cbld_make_impl_refine2[sepref_fr_rules]: 
    "(uncurry2 cbld_make_impl,uncurry2 (RETURN ooo cbld_make)) 
    ∈ [λ_. True]⇩c lit_assn⇧k *⇩a cbuf_aux_assn⇧d *⇩a (dropi_assn (rdomp size_assn))⇧k → cbld_assn [λ((ml,cb),_) r. r = (ml,cb) ]⇩c"
    unfolding cbld_make_def cbld_make_impl_def cbld_assn_def any_rel_def
    apply sepref_to_hoare
    apply vcg_normalize
    
    apply (simp named_ss HOL_basic_ss_nomatch: move_resolve_ex_eq)
    
    supply [simp] = rdomp_pure_rel_eq
    apply vcg
    done    
    
  lemma cbld_dest_impl_refine[sepref_fr_rules]: 
    "(λ(a,b). Mreturn (a,b,ghost_var::1 word), RETURN o cbld_dest) 
    ∈ [λ_. True]⇩c cbld_assn⇧d → lit_assn ×⇩a cbuf_aux_assn ×⇩a dropi_assn (rdomp size_assn) [λ(ml,cb) (ml',cb',_). ml'=ml ∧ cb'=cb]⇩c"  
    unfolding cbld_dest_def cbld_assn_def any_rel_def
    apply sepref_to_hoare
    apply vcg_normalize
    apply (simp named_ss HOL_basic_ss_nomatch: move_resolve_ex_eq)
    by vcg
  
  
  sepref_def cbld_new_impl is "RETURN o cbld_new" :: "size_assn⇧k →⇩a cbld_assn"  
    unfolding cbld_new_def
    apply (rewrite unat_const_fold[where 'a=lit_size_t])
    by sepref

  sepref_def cbld_add_lit_impl is "uncurry cbld_add_lit" :: "ulit_assn⇧k *⇩a cbld_assn⇧d →⇩a cbld_assn"  
    unfolding cbld_add_lit_def max_def
    by sepref
    
  sepref_def cbld_finish_clause_impl is "cbld_finish_clause" :: "cbld_assn⇧d →⇩a zcl_assn ×⇩a cbld_assn"
    unfolding cbld_finish_clause_def
    by sepref

  sepref_def cbld_abort_clause_impl is "cbld_abort_clause" :: "cbld_assn⇧d →⇩a cbld_assn"
    unfolding cbld_abort_clause_def
    by sepref
            
  sepref_def cbld_is_empty_impl is "cbld_is_empty" :: "cbld_assn⇧k →⇩a bool1_assn"
    unfolding cbld_is_empty_def
    apply (annot_snat_const size_T)
    by sepref
    
  sepref_def cbld_get_maxlit_impl is "cbld_get_maxlit" :: "cbld_assn⇧k →⇩a lit_assn"  
    unfolding cbld_get_maxlit_def
    by sepref
    
        
  sepref_definition cbld_free [llvm_code] is "λcbld. doN {let _ = cbld_dest cbld; RETURN ()}" :: "cbld_assn⇧d →⇩a unit_assn"  
    by sepref
  
  lemma cbld_free[sepref_frame_free_rules]: "MK_FREE cbld_assn cbld_free"
    apply (rule MK_FREE_hfrefI[OF cbld_free.refine])
    by auto
    
    
  subsection ‹Interface›  
  
  term cbld_α_clause term cbld_α_cap term cbld_invar
  
  term cbld_new thm cbld_new_correct cbld_new_impl.refine
    
  term cbld_add_lit thm cbld_add_lit_correct cbld_add_lit_impl.refine
  term cbld_add_lit_impl
    
  term cbld_finish_clause thm cbld_finish_clause_correct cbld_finish_clause_impl.refine
  
  term cbld_abort_clause thm cbld_abort_clause_correct cbld_abort_clause_impl.refine

  term cbld_is_empty thm cbld_is_empty_correct cbld_is_empty_impl.refine
    
end