signature TNet_auxfnsTheory = sig type thm = Thm.thm (* Definitions *) val FC_autobind_primitive_def : thm val FC_functions_def : thm val FC_unused_def : thm val F_context_def : thm val SC_autobind_primitive_def : thm val SC_unused_def : thm val dequeue_primitive_def : thm val doq_def : thm val dosend_primitive_def : thm val dsched_def : thm val enqueue_primitive_def : thm val ephemeralErrors_def : thm val ephemeral_def : thm val in_sockets_of_FC_def : thm val lookup_def : thm val match_arg_munge_def : thm val match_tupled_primitive_def : thm val mk_sc_def : thm val orderings_def : thm val outroute_def : thm val privileged_def : thm val score_def : thm val scs_functions_def : thm val sockets_of_FC_def : thm val socklist_context_def : thm val unused_def : thm val zombify_arg_munge_def : thm val zombify_tupled_primitive_def : thm (* Theorems *) val FC_accessors : thm val FC_autobind_def : thm val FC_autobind_ind : thm val SC_autobind_def : thm val SC_autobind_ind : thm val always_a_different_socket : thm val dequeue_def : thm val dequeue_ind : thm val dosend_def : thm val dosend_ind : thm val enqueue_def : thm val enqueue_ind : thm val match_def : thm val match_ind : thm val mk_sc_11 : thm val mk_sc_scontext : thm val sc_characterise : thm val sc_inversions : thm val zombify_def : thm val zombify_ind : thm val TNet_auxfns_grammars : parse_type.grammar * term_grammar.grammar (* [TNet_oks] Parent theory of "TNet_auxfns" [FC_autobind_primitive_def] Definition |- autobind = WFREC (@R. WF R) (\FC_autobind a. case a of (v,v1) -> case v of NONE -> unused v1 INTER ephemeral || SOME v2 -> {v2}) [FC_functions_def] Definition |- !FC. F_context FC ==> socklist_context (fc_sc FC) /\ !ifds tid t s. FC (ifds,tid,t,s) = <|ifds := ifds; ts := FUPDATE (fc_ts FC) (tid,t); s := fc_sc FC s; oq := fc_oq FC; oqf := fc_oqf FC|> [FC_unused_def] Definition |- !FC. unused FC = unused (fc_sc FC) [F_context_def] Definition |- !FC. F_context FC = ?SC ts oq oqf. socklist_context SC /\ !ifds tid t s. FC (ifds,tid,t,s) = <|ifds := ifds; ts := FUPDATE ts (tid,t); s := SC s; oq := oq; oqf := oqf|> [SC_autobind_primitive_def] Definition |- autobind = WFREC (@R. WF R) (\SC_autobind a. case a of (v,v1) -> case v of NONE -> unused v1 INTER ephemeral || SOME v2 -> {v2}) [SC_unused_def] Definition |- !SC. unused SC = unused (LIST_TO_SET (scs1 SC)) UNION unused (LIST_TO_SET (scs2 SC)) [dequeue_primitive_def] Definition |- dequeue = WFREC (@R. WF R) (\dequeue a. case a of (v,v1) -> case v of Timed v2 -> case v2 of (v3,v4) -> (if v3 = [] then {} else {(m,Timed (oqu',d'),oqf') | (m = LAST v3) /\ (oqu' = FRONT v3) /\ (d' = (if oqu' = [] then time_infty else doq)) /\ oqf' IN {v1 /\ (oqu' <> []); F}})) [doq_def] Definition |- doq = time (1 / 100) [dosend_primitive_def] Definition |- dosend = WFREC (@R. WF R) (\dosend a. case a of (v,v1) -> case v1 of (v2,v3) -> case v2 of (v4,v5) -> case v4 of NONE -> (case v3 of (v7,v8) -> case v7 of (v9,v10) -> case v9 of NONE -> ARB || SOME v11 -> case v10 of (v14,v15) -> case v14 of NONE -> ARB || SOME v16 -> case v15 of (v19,v20) -> case v19 of NONE -> ARB || SOME v21 -> case v8 of (v24, v25) -> enqueue (<|src := v11; dest := v21; body := UDP (SOME v16, v20, v5)|>, v24, v25)) || SOME v6 -> case v6 of (v26,v27) -> case v3 of (v28,v29) -> case v28 of (v30,v31) -> case v30 of NONE -> (case v31 of (v33,v34) -> case v33 of NONE -> ARB || SOME v35 -> case v34 of (v38, v39) -> case v38 of NONE -> (case v39 of NONE -> (case v29 of (v44, v45) -> BIGUNION {enqueue (<|src := i'; dest := i; body := UDP (SOME v35, SOME v27, v5)|>, v44, v45) | i' IN outroute (v, i)}) || SOME v42 -> ARB) || SOME v40 -> ARB) || SOME v32 -> case v31 of (v49,v50) -> case v49 of NONE -> ARB || SOME v51 -> case v50 of (v54, v55) -> case v29 of (v56, v57) -> enqueue (<|src := v32; dest := v26; body := UDP (SOME v51, SOME v27, v5)|>, v56, v57)) [dsched_def] Definition |- dsched = time (1 / 100) [enqueue_primitive_def] Definition |- enqueue = WFREC (@R. WF R) (\enqueue a. case a of (v,v1) -> case v1 of (v2,v3) -> case v2 of Timed v5 -> case v5 of (v8,v9) -> case v3 of T -> {(Timed (v8,v9),T,F)} || F -> {((if v8 = [] then Timed ([v],doq) else Timed (v::v8,v9)),oqf',T) | oqf' IN {T; F}}) [ephemeralErrors_def] Definition |- ephemeralErrors = {EAGAIN; EADDRINUSE} [ephemeral_def] Definition |- !p. ephemeral (Port p) = 1024 <= p /\ p <= 4999 [in_sockets_of_FC_def] Definition |- !s FC. s IN FC = s IN socks FC [lookup_def] Definition |- !slist quad. lookup slist quad = {s | MEM s slist /\ (let sn = score s quad in sn > 0 /\ ~?s'. MEM s' slist /\ score s' quad > sn)} [match_arg_munge_def] Definition |- !x x1. match x x1 = match_tupled (x,x1) [match_tupled_primitive_def] Definition |- match_tupled = WFREC (@R. WF R) (\match_tupled a. case a of (v,v1) -> case v of (v2,v3) -> case v2 of NONE -> (case v3 of (v5,v6) -> case v5 of NONE -> (case v6 of (v8,v9) -> case v8 of NONE -> (case v9 of NONE -> 0 || SOME v12 -> ARB) || SOME v10 -> ARB) || SOME v7 -> case v6 of (v17,v18) -> case v17 of NONE -> (case v18 of NONE -> (case v1 of (v23,v24) -> case v24 of (v25,v26) -> case v26 of (v27, v28) -> (if v28 = SOME v7 then 1 else 0)) || SOME v21 -> ARB) || SOME v19 -> ARB) || SOME v4 -> case v3 of (v32,v33) -> case v32 of NONE -> ARB || SOME v34 -> case v33 of (v37,v38) -> case v37 of NONE -> (case v38 of NONE -> (case v1 of (v42,v43) -> case v43 of (v44,v45) -> case v45 of (v46, v47) -> (if (v4 = v46) /\ (SOME v34 = v47) then 2 else 0)) || SOME v40 -> ARB) || SOME v39 -> case v38 of NONE -> (case v1 of (v50,v51) -> case v51 of (v52,v53) -> case v53 of (v54, v55) -> (if (v39 = v50) /\ (v4 = v54) /\ (SOME v34 = v55) then 3 else 0)) || SOME v49 -> case v1 of (v56,v57) -> case v57 of (v58,v59) -> case v59 of (v60, v61) -> (if (SOME v49 = v58) /\ (v39 = v56) /\ (v4 = v60) /\ (SOME v34 = v61) then 4 else 0)) [mk_sc_def] Definition |- !s1 s2 s. mk_sc s1 s2 s = APPEND s1 (s::s2) [orderings_def] Definition |- !s l. orderings s l = (LIST_TO_SET l = s) /\ (LENGTH l = CARD s) [outroute_def] Definition |- !ifdset i. outroute (ifdset,i) = (if i IN LOOPBACK then {localhost} else {r.primary | r IN ifdset /\ (r.ipset <> LOOPBACK)}) [privileged_def] Definition |- !p. privileged (Port p) = 0 <= p /\ p <= 1023 [score_def] Definition |- !s quad. score s quad = match (s.is1,s.ps1,s.is2,s.ps2) quad [scs_functions_def] Definition |- !SC. socklist_context SC ==> !s. SC s = APPEND (scs1 SC) (s::scs2 SC) [sockets_of_FC_def] Definition |- !FC. socks FC = LIST_TO_SET (APPEND (scs1 (fc_sc FC)) (scs2 (fc_sc FC))) [socklist_context_def] Definition |- !SC. socklist_context SC = ?s1 s2. !s. SC s = APPEND s1 (s::s2) [unused_def] Definition |- !s. unused s = {Port p | 1 <= p /\ p <= 65535 /\ ~?s'. (s'.ps1 = SOME (Port p)) /\ s' IN s} [zombify_arg_munge_def] Definition |- !x x1. zombify x x1 = zombify_tupled (x,x1) [zombify_tupled_primitive_def] Definition |- zombify_tupled = WFREC (@R. WF R) (\zombify_tupled a. case a of (v,v1) -> case v1 of Timed v2 -> case v2 of (v3,v4) -> case v3 of Run -> Timed (v3,v4) || Exit -> Timed (v3,v4) || Zombie -> Timed (v3,v4) || Ret v5 -> Timed (v3,v4) || Sendto2 v6 -> (case v6 of (v12,v13) -> (if v = v12 then Timed (Zombie,time_infty) else Timed (v3,v4))) || Recvfrom2 v7 -> (if v = v7 then Timed (Zombie,time_infty) else Timed (v3,v4)) || Select2 v8 -> (case v8 of (v16,v17) -> Timed (Select2 (FILTER (\fd'. ~(fd' = v)) v16, FILTER (\fd'. ~(fd' = v)) v17), v4)) || Delay2 -> Timed (v3,v4) || Print2 v9 -> Timed (v3,v4)) [FC_accessors] Theorem |- !FC ifds tid t s. F_context FC ==> ((FC (ifds,tid,t,s)).ts = FUPDATE (fc_ts FC) (tid,t)) /\ ((FC (ifds,tid,t,s)).ifds = ifds) /\ ((FC (ifds,tid,t,s)).oq = fc_oq FC) /\ ((FC (ifds,tid,t,s)).oqf = fc_oqf FC) /\ ((FC (ifds,tid,t,s)).s = APPEND (scs1 (fc_sc FC)) (s::scs2 (fc_sc FC))) [FC_autobind_def] Theorem |- (autobind (NONE,FC) = unused FC INTER ephemeral) /\ (autobind (SOME p,FC) = {p}) [FC_autobind_ind] Theorem |- !P. (!FC. P (NONE,FC)) /\ (!p FC. P (SOME p,FC)) ==> !v v1. P (v,v1) [SC_autobind_def] Theorem |- (autobind (NONE,SC) = unused SC INTER ephemeral) /\ (autobind (SOME p,SC) = {p}) [SC_autobind_ind] Theorem |- !P. (!SC. P (NONE,SC)) /\ (!p SC. P (SOME p,SC)) ==> !v v1. P (v,v1) [always_a_different_socket] Theorem |- !s. ?s'. ~(s' = s) [dequeue_def] Theorem |- dequeue (Timed (oqu,d),oqf) = (if oqu = [] then {} else {(m,Timed (oqu',d'),oqf') | (m = LAST oqu) /\ (oqu' = FRONT oqu) /\ (d' = (if oqu' = [] then time_infty else doq)) /\ oqf' IN {oqf /\ (oqu' <> []); F}}) [dequeue_ind] Theorem |- !P. (!oqu d oqf. P (Timed (oqu,d),oqf)) ==> !v v1. P (v,v1) [dosend_def] Theorem |- (dosend (ifds,(NONE,data),(SOME i1,SOME p1,SOME i2,ps2),oq,oqf) = enqueue (<|src := i1; dest := i2; body := UDP (SOME p1,ps2,data)|>,oq, oqf)) /\ (dosend (ifds,(SOME (i,p),data),(NONE,SOME p1,NONE,NONE),oq,oqf) = BIGUNION {enqueue (<|src := i'; dest := i; body := UDP (SOME p1,SOME p,data)|>, oq,oqf) | i' IN outroute (ifds,i)}) /\ (dosend (ifds,(SOME (i,p),data),(SOME i1,SOME p1,is2,ps2),oq,oqf) = enqueue (<|src := i1; dest := i; body := UDP (SOME p1,SOME p,data)|>,oq, oqf)) [dosend_ind] Theorem |- !P. (!ifds i p data i1 v52 v53. P (ifds,(SOME (i,p),data),(SOME i1,NONE,v52),v53)) /\ (!ifds i p data p1 v41 v47 v48. P (ifds,(SOME (i,p),data),(NONE,SOME p1,SOME v41,v47),v48)) /\ (!ifds i p data p1 v43 v46. P (ifds,(SOME (i,p),data),(NONE,SOME p1,NONE,SOME v43),v46)) /\ (!ifds i p data v36 v37. P (ifds,(SOME (i,p),data),(NONE,NONE,v36),v37)) /\ (!ifds data i1 p1 v22 v23. P (ifds,(NONE,data),(SOME i1,SOME p1,NONE,v22),v23)) /\ (!ifds data i1 v17 v18. P (ifds,(NONE,data),(SOME i1,NONE,v17),v18)) /\ (!ifds data v12 v13. P (ifds,(NONE,data),(NONE,v12),v13)) /\ (!ifds data i1 p1 i2 ps2 oq oqf. P (ifds,(NONE,data),(SOME i1,SOME p1,SOME i2,ps2),oq,oqf)) /\ (!ifds i p data p1 oq oqf. P (ifds,(SOME (i,p),data),(NONE,SOME p1,NONE,NONE),oq,oqf)) /\ (!ifds i p data i1 p1 is2 ps2 oq oqf. P (ifds,(SOME (i,p),data),(SOME i1,SOME p1,is2,ps2),oq,oqf)) ==> !v v1 v2 v3 v4 v5 v6 v7 v8. P (v,(v1,v2),(v3,v4,v5,v6),v7,v8) [enqueue_def] Theorem |- (enqueue (m,Timed (v6,v7),T) = {(Timed (v6,v7),T,F)}) /\ (enqueue (m,Timed (oqu,d),F) = {((if oqu = [] then Timed ([m],doq) else Timed (m::oqu,d)),oqf',T) | oqf' IN {T; F}}) [enqueue_ind] Theorem |- !P. (!m v6 v7. P (m,Timed (v6,v7),T)) /\ (!m oqu d. P (m,Timed (oqu,d),F)) ==> !v v1 v2. P (v,v1,v2) [match_def] Theorem |- (match (NONE,NONE,NONE,NONE) v0 = 0) /\ (match (NONE,SOME p1,NONE,NONE) (i3,ps3,i4,ps4) = (if ps4 = SOME p1 then 1 else 0)) /\ (match (SOME i1,SOME p1,NONE,NONE) (i3,ps3,i4,ps4) = (if (i1 = i4) /\ (SOME p1 = ps4) then 2 else 0)) /\ (match (SOME i1,SOME p1,SOME i2,NONE) (i3,ps3,i4,ps4) = (if (i2 = i3) /\ (i1 = i4) /\ (SOME p1 = ps4) then 3 else 0)) /\ (match (SOME i1,SOME p1,SOME i2,SOME p2) (i3,ps3,i4,ps4) = (if (SOME p2 = ps3) /\ (i2 = i3) /\ (i1 = i4) /\ (SOME p1 = ps4) then 4 else 0)) [match_ind] Theorem |- !P. (!i1 p1 v41 v48. P (SOME i1,SOME p1,NONE,SOME v41) v48) /\ (!i1 v35 v36. P (SOME i1,NONE,v35) v36) /\ (!p1 v20 v30 v31. P (NONE,SOME p1,SOME v20,v30) v31) /\ (!p1 v22 v29. P (NONE,SOME p1,NONE,SOME v22) v29) /\ (!v11 v15 v16. P (NONE,NONE,SOME v11,v15) v16) /\ (!v13 v14. P (NONE,NONE,NONE,SOME v13) v14) /\ (!v0. P (NONE,NONE,NONE,NONE) v0) /\ (!p1 i3 ps3 i4 ps4. P (NONE,SOME p1,NONE,NONE) (i3,ps3,i4,ps4)) /\ (!i1 p1 i3 ps3 i4 ps4. P (SOME i1,SOME p1,NONE,NONE) (i3,ps3,i4,ps4)) /\ (!i1 p1 i2 i3 ps3 i4 ps4. P (SOME i1,SOME p1,SOME i2,NONE) (i3,ps3,i4,ps4)) /\ (!i1 p1 i2 p2 i3 ps3 i4 ps4. P (SOME i1,SOME p1,SOME i2,SOME p2) (i3,ps3,i4,ps4)) ==> !v v1 v2 v3 v4 v5 v6 v7. P (v,v1,v2,v3) (v4,v5,v6,v7) [mk_sc_11] Theorem |- !s1 s2 s3 s4. (mk_sc s1 s2 = mk_sc s3 s4) = (s1 = s3) /\ (s2 = s4) [mk_sc_scontext] Theorem |- !s1 s2. socklist_context (mk_sc s1 s2) [sc_characterise] Theorem |- !SC. socklist_context SC ==> ?s1 s2. SC = mk_sc s1 s2 [sc_inversions] Theorem |- !s1 s2. (scs1 (mk_sc s1 s2) = s1) /\ (scs2 (mk_sc s1 s2) = s2) [zombify_def] Theorem |- zombify fd (Timed (ts,d)) = case ts of Run -> Timed (ts,d) || Exit -> Timed (ts,d) || Zombie -> Timed (ts,d) || Ret v5 -> Timed (ts,d) || Sendto2 v6 -> (case v6 of (v12,v13) -> (if fd = v12 then Timed (Zombie,time_infty) else Timed (ts,d))) || Recvfrom2 v7 -> (if fd = v7 then Timed (Zombie,time_infty) else Timed (ts,d)) || Select2 v8 -> (case v8 of (v16,v17) -> Timed (Select2 (FILTER (\fd'. ~(fd' = fd)) v16, FILTER (\fd'. ~(fd' = fd)) v17),d)) || Delay2 -> Timed (ts,d) || Print2 v9 -> Timed (ts,d) [zombify_ind] Theorem |- !P. (!fd ts d. P fd (Timed (ts,d))) ==> !v v1. P v v1 *) end