Theory fnptr_proto

(*
 * Copyright (c) 2025 Apple Inc. All rights reserved.
 *
 * SPDX-License-Identifier: BSD-2-Clause
 *)

theory fnptr_proto
  imports 
    AutoCorres2_Main.AutoCorres_Main

begin

typedecl environment
consts callback_step::
  "8 word list ⇒ environment ⇒ (32 word * environment)"

consts callback_info::
  "8 word list ⇒ environment ⇒ (32 word)"

consts callback_void_step::
  "environment ⇒ environment"

ML ‹IsarInstall.installed_C_files @{theory}›


text ‹When functions are called within expressions the C-parser analyses which global variables
are affected by those functions (read and write dependencies) and only accepts functions that
have no overlapping and thus potentially conflicting dependencies. 
To do this analysis the C-parser looks into the function bodies.
As function prototypes have no bodies the C-Parser by default assumes the "worst" for those 
functions: They are considered to read and write everything. So this by default prohibits the
use of function prototypes within expressions.
When you need more flexibility here you can specifiy the dependencies explicitly as demonstrated
in this file.
You can later define specifications for those prototypes and declare them to autocorres
via overloading and command ‹declare_prototype› or more low level with @{attribute autocorres_definition} 
Autocorres then generates a proof obligation that this specification behaves according to the
declared dependencies.
›

setup ‹
let
  open AstDatatype
in
IsarInstall.add_prototype_dependencies "fnptr_proto.c" 
  ("w", read_anything_write_phantom_machine_state) #>
IsarInstall.add_prototype_dependencies "fnptr_proto.c" 
  ("w1", read_heap_and_phantom_machine_state_write_phantom_machine_state)
end
›


ML ‹IsarInstall.installed_C_files @{theory}›

install_C_file "fnptr_proto.c" [machinety=environment]

ML ‹IsarInstall.installed_C_files @{theory}›
ML ‹
val embedded_fncall_exprs = ProgramAnalysis.get_embedded_fncall_exprs (the (CalculateState.get_csenv @{theory} "fnptr_proto.c"))
›
ML ‹
val deps = ProgramAnalysis.get_variable_dependencies (the (CalculateState.get_csenv @{theory} "fnptr_proto.c"))
›


term w_body
context fnptr_proto_global_addresses
begin
thm fun_ptr_simps
end

init-autocorres [
    in_out_parameters = inc_ptr() and dec_ptr() and w() where disjoint [], 
    in_out_globals = w w_buf w2 w1 func do_call do_call_exit do_call_buff embedded_prototypes assign_w, 
    no_heap_abs = dec_ptr w w_buf w2 w1, 
    ts_force exit = do_call_exit] "fnptr_proto.c"

text ‹›

declare [[verbose=1]]
overloading w_body ≡ w_body
begin
definition 
  "w_body ≡ exec_spec_monad global_exn_var'_' global_exn_var'_'_update (globals) 
     (λs. (clookup 0 (locals s), clookup 1 (locals s)))

     (λ(p::8 word ptr, n::32 word). 
        L2_pre_post (ptr_span_buffer p (unat n) ⊆ 𝒢) (λs. {(r, t). 
          ∃env. t = phantom_machine_state_'_update (λ_. env) s ∧ 
          (r, env) = callback_step (of_buffer_heap (hrs_mem (t_hrs_' s)) p (unat n)) (phantom_machine_state_' s) })) 

     (λupd. locals_update (cupdate 2 upd))"
end

declare_prototype w_body_def 
  by read_write_confined


overloading w2_body ≡ w2_body
begin
definition 
  "w2_body ≡ exec_spec_monad global_exn_var'_' global_exn_var'_'_update (globals) 
     (λs. (clookup 0 (locals s), clookup 1 (locals s)))

     (λ(p::8 word ptr, n::32 word). 
        L2_pre_post (ptr_span_buffer p (unat n) ⊆ 𝒢) (λs. {(r, t). 
          t = s ∧ 
          r = callback_info (of_buffer_heap (hrs_mem (t_hrs_' s)) p (unat n)) (phantom_machine_state_' s) })) 

     (λupd. locals_update (cupdate 2 upd))"
end
declare_prototype w2_body_def 
  by read_write_confined

overloading w1_body ≡ w1_body
begin
definition 
  "w1_body ≡ exec_spec_monad global_exn_var'_' global_exn_var'_'_update (globals) 
     (λs. (clookup 0 (locals s), clookup 1 (locals s)))

     (λ(p::8 word ptr, n::32 word). 
        L2_pre_post_read_write (λs. (t_hrs_' s, phantom_machine_state_' s)) phantom_machine_state_'_update  
      (ptr_span_buffer p (unat n) ⊆ 𝒢) (λ(h, env). {(v, env'). (v, env') = callback_step (of_buffer_heap (hrs_mem h) p (unat n)) env  })) 

     (λupd. locals_update (cupdate 2 upd))"
end
declare_prototype w1_body_def 
  by read_write_confined



overloading w_buf_body ≡ w_buf_body
begin
definition 
  "w_buf_body ≡ exec_spec_monad global_exn_var'_' global_exn_var'_'_update (globals) 
     (λs. (clookup 0 (locals s)))

     (λ(p0::buffer_C ptr). 
        L2_seq 
          (L2_gets (λs. (buf_C (h_val (hrs_mem (t_hrs_' s)) p0))) [clocals_string_embedding ''p'']) (λp.
          (L2_seq
            (L2_gets (λs. (len_C (h_val (hrs_mem (t_hrs_' s)) p0))) [clocals_string_embedding ''n'']) (λn. 
            L2_pre_post (ptr_span_buffer p (unat n) ⊆ 𝒢) (λs. {(r, t). 
             ∃env. t = phantom_machine_state_'_update (λ_. env) s ∧ 
             (r, env) = callback_step (of_buffer_heap (hrs_mem (t_hrs_' s)) 
             p (unat n)) (phantom_machine_state_' s) }))))) 

     (λupd. locals_update (cupdate 1 upd))"
end

declare w_buf_body_def [autocorres_definition fnptr_proto CP w_buf]



overloading u_body ≡ u_body
begin
definition  
  "u_body ≡ exec_spec_monad global_exn_var'_' global_exn_var'_'_update (globals)
    (λs. ())
    (λ(_::unit).
     L2_pre_post (True) (λs. {(r::unit, t).
      ∃env. t = phantom_machine_state_'_update (λ_. env) s ∧
       env = callback_void_step (phantom_machine_state_' s)}))
     (λupd. (λs. s))"
end
declare u_body_def [autocorres_definition fnptr_proto CP u]

declare [[verbose=0]]
autocorres [no_body = v] "fnptr_proto.c"

thm l1_v'_def
thm l1_w2'_def
thm l2_v'_def
thm io_v'_def
thm hl_v'_def
thm wa_v'_def
thm ts.v'_def
thm l1_u'_def
thm l2_u'_def
thm ts.u'_def
thm l1_w'_def
thm final_defs
thm 𝒫_defs
context fnptr_proto_global_addresses
begin
thm io_corres
end

end