
Verification of Higher-Order Non-deterministic Programs with Refinement Types
Explore a novel dependent refinement type system for verifying higher-order non-deterministic programs, ensuring safety, termination, and more. Learn about universal and existential reasoning, meta-theoretic properties, and the extension of type systems with qualified types.
Download Presentation

Please find below an Image/Link to download the presentation.
The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author. If you encounter any issues during the download, it is possible that the publisher has removed the file from their server.
You are allowed to download the files provided on this website for personal or commercial use, subject to the condition that they are used lawfully. All files are the property of their respective owners.
The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author.
E N D
Presentation Transcript
Relatively Complete Refinement Type System for Verification of Higher-Order Non-deterministic Programs Hiroshi Unno (University of Tsukuba) Yuki Satake (University of Tsukuba) Tachio Terauchi (Waseda University) POPL'18, Los Angeles, United States 1
Background Recent advances in (semi-)automated methods for verifying higher-order functional programs safety [Rondon+ 08; U. & Kobayashi 08, 09; Terauchi 10; Ong & Ramsay 11; Jhala+ 11; Kobayashi+ 11; U.+ 13; ] termination [Sereni & Jones 05; Giesl+ 11; Kuwahara+ 14; Vazou+ 14] non-termination [Kuwahara+ 15; Hashimoto & U. 15] temporal properties [Koskinen & Terauchi 14; Murase+ 16] Different techniques are used to verify the different classes of properties, and are hard to combine in a unified framework dependent refinement types, predicate abstraction for higher-order model checking, program transformation for (binary) reachability analysis, POPL'18, Los Angeles, United States 2
Our Contributions Novel dependent refinement type system that can: uniformly express and verify universal and existential branching properties of call-by-value, higher-order, and non-deterministic programs: (cond.) safety, non-safety, termination, and non-termination seamlessly combine universal and existential reasoning e.g., Prove non-safety via termination e.g., Prove non-termination via safety e.g., Prove termination and non-termination simultaneously Meta-theoretic properties of the type system: Closure of types under complement Soundness Relative completeness POPL'18, Los Angeles, United States 3
Our Contributions Novel dependent refinement type system that can: uniformly express and verify universal and existential branching properties of call-by-value, higher-order, and non-deterministic programs: (cond.) safety, non-safety, termination, and non-termination seamlessly combine universal and existential reasoning e.g., Prove non-safety via termination e.g., Prove non-termination via safety e.g., Prove termination and non-termination simultaneously Meta-theoretic properties of the type system: Closure of types under complement Soundness Relative completeness POPL'18, Los Angeles, United States 4
Dependent Refinement Types ? predicates on ? ??? | ? ? Non-negative integers program values ? ??? {? ??? | ? ?} Functions that take an integer ? and (if terminated) return ? not less than ? A type system ensures that a type-checked expression behaves according to the type Only universal branching properties can be expressed POPL'18, Los Angeles, United States 5
Overview: Our Type System Extends dependent refinement types with: Qualified types ????? to express universal/existential branching behaviors and partial/total correctness Qualified bindings ? ?? to cope with non-determinism from program inputs G del encoding of function-type values & guarded intersection types to achieve relative completeness POPL'18, Los Angeles, United States 6
Overview: Our Type System Extends dependent refinement types with: Qualified types ????? to express universal/existential branching behaviors and partial/total correctness Qualified bindings ? ?? to cope with non-determinism from program inputs G del encoding of function-type values & guarded intersection types to achieve relative completeness POPL'18, Los Angeles, United States 7
Qualified Types ????? ?? , (universal/existential non-det.) specifies whether the expression being typed behaves according to the type: for any non-det. evaluation (??= ), or for some non-det. evaluation (??= ) ?? , (partial/total correctness) specifies whether: ? holds for all value obtained (??= ), or there exists a final value for which ? holds (??= ) POPL'18, Los Angeles, United States 8
Qualified Types ????? ?? , (universal/existential non-det.) specifies whether the expression being typed behaves according to the type: for any non-det. evaluation (??= ), or for some non-det. evaluation (??= ) ?? , (partial/total correctness) specifies whether: the evaluation diverges or ? is satisfied (??= ), or the evaluation terminates and ? is satisfied (??= ) POPL'18, Los Angeles, United States 9
Examples: Qualified Types ????? ? ? ??? ? > ? for any non-deterministic evaluation of ?, if any integer ? is obtained, then ? is positive ? ? ??? ? > ? for some non-deterministic evaluation of ?, some integer ? is obtained, and ? is positive POPL'18, Los Angeles, United States 10
Typing Integer Constants Integer constant Rule: ? ? ? ??? ? = ? Type Universal and Total environment POPL'18, Los Angeles, United States 11
Converting Qualified Types Subtyping Rule: ???? ???? ? ??< ?? ???? ???? ? ?? < ?? Universal and Partial Universal and Total Existential and Partial Existential POPL'18, Los Angeles, United States and Total 12
Typing Let-Bindings Rule: ???? ? ?? ?? ???? ?,? ?? ?? ?? ? ??? ? = ?? ?? ?? ?? ? ??? ?? ???? POPL'18, Los Angeles, United States 13
Typing Recursive Functions for Partial Correctness Rule: ? ? ?? ? ?,? ??,? ? ?? ?? ? ??? ?,?,? ? ?? ?? ? (recursive) function ??? ??? ? ? = ? POPL'18, Los Angeles, United States 14
Typing Recursive Functions for Total Correctness (cf. [Xi 01]) Well-founded relation witnessing the termination of ?, as a recursion guard Rule: ? ????= ? :?? ? ?? ? =? ? ?? ?? ? ?? ? ?,? .? ?,? ??,? ???? ? ?? ? ??? ?,?,? ? ?? ?? Example: ? ? ? ? ,??? ???? ?? ? = ? ???? ? ???? ??? ?? ? ?,? .? > ? ? ??? ???,?,?? ? = ? ???? ? ???? ? + ??? ? ? ? ? ? > ? ? ? ? ? ? ? ? ? ? ??? ? ? ? ? POPL'18, Los Angeles, United States 15
Overview: Our Type System Extends dependent refinement types with: Qualified types ????? to express universal/existential branching behaviors and partial/total correctness Qualified bindings ? ?? to cope with non-determinism from program inputs G del encoding of function-type values & guarded intersection types to achieve relative completeness POPL'18, Los Angeles, United States 16
Qualified Bindings ??? Occur in type environments and the argument of dependent function types ? , specifies whether a certain fact must hold for: any input ? that satisfies ? (? = ), or some input ? that satisfies ? (? = ) POPL'18, Los Angeles, United States 17
Examples: Qualified Bindings ??? ? ??? ? ??? ? > ? functions that, for any integer ? and for any run with the argument ?, return some integer ?, which is greater than ? ? ??? ? ??? ? > ? functions that, there exists an integer ?, for any run with the argument ?, return some integer ?, which is greater than ? POPL'18, Los Angeles, United States 18
Skolemizing Existential Bindings Rule: Skolemization Predicate ?,? : ? ? ?,? : ?,?,? ? ? ?,? : ?,? ? ? Type environment consisting of only -bindings Type environment consisting of both - and -bindings Example: ? : ???,? : ??? ? = ? ? : ???,? : ???,? = ? ? + ? ? ? = ? ? : ???,? : ??? ? + ? ? ? = ? POPL'18, Los Angeles, United States 19
Typing Non-deterministic Choice Rule: ?,? ????? ? ????? ? ??? ? = ?? ? ????? ? ??? ? Example: ? ???,? ??? ? + ? ? ? = ? ? ??? ??? ? = ?? ? + ? ? ? = ? POPL'18, Los Angeles, United States 20
Typing Function Applications (Universal Bindings) Rule: ? ?? ? : ? ? ? ?? ?? [??/?]? ? ?? ? POPL'18, Los Angeles, United States 21
Typing Function Applications (Existential Bindings) Rule: Observational equivalence ? ?? ? ? ? ?,? ?? ?? [??/?]? ?,? ?,? ? ?? Example: ? ? ? ? ? ?,? ???,? ??? ? = ? ? ?,? ??? ? ? ? ? ? ??? ? = ?? ? ? ? ? : ??? ? POPL'18, Los Angeles, United States 22
Converting Function Types (1/4) Subtyping Rule: ?,? ?? ??< ?? ? ??< ?? ? ? ?? ??< ? ?? ?? Example: ? ??? ? ? = ? < ? ? ? ? ? ? ? POPL'18, Los Angeles, United States 23
Converting Function Types (2/4) Subtyping Rule: ?,? ?? ??< ?? ? ??< ?? ? ? ?? ??< ? ?? ?? Example: ? ? ? ? < ? ??? ? ? ? ? ? = ? POPL'18, Los Angeles, United States 24
Converting Function Types (3/4) Subtyping Rule: ? ? < ?? ?,? ? ??< ?? ? ? ?? ??< ? ?? ?? ? ? < ?? Example: ? ? ? < ??? ? ? ? ? ? ? = ? < ? ? = ? ? ??? ? ? = ? < ? ??? ? ? = ? ? ? ? < ??? POPL'18, Los Angeles, United States 25
Converting Function Types (4/4) Subtyping Rule: ?,? ?? ??,? ?? ?? ? ? ?,? ?? ?? ??< ?? ?,? ?? ?? ??< ?,? ?? ?? < ?? ? ? ?? ??< ? ?? ?? Example: Observational equivalence ? ? ? = ? < ? ? ? = ? ? ? = ? ? ? = ? POPL'18, Los Angeles, United States 26
Overview: Our Type System Extends dependent refinement types with: Qualified types ????? to express universal/existential branching behaviors and partial/total correctness Qualified bindings ? ?? to cope with non-determinism from program inputs G del encoding of function-type values & guarded intersection types to achieve relative completeness POPL'18, Los Angeles, United States 27
Gdel Encoding of Function-Type Values Enables predicates of the underlying logic ? (e.g., second-order arithmetic) to depend on function-type arguments encoded as ?-objects ? ??? ??? ? ??? ??? ? ? ? Functions that, given two terminating functions ? and ?, always diverge if ? is not observationally equivalent to ? POPL'18, Los Angeles, United States 28
Guarded Intersection Types ??? ?? ???? Collectively express different behaviors of functions depending on the arguments ? > ? ??? ? < ? ? ? = ? ??? ? = ? ? Functions that, given the argument ? : always terminate if ? > ?, always diverge if ? < ?, and otherwise, non-deterministically terminate or diverge ? : ??? POPL'18, Los Angeles, United States 29
Our Contributions Novel dependent refinement type system that can: uniformly express and verify universal and existential branching properties of call-by-value, higher-order, and non-deterministic programs: (cond.) safety, non-safety, termination, and non-termination seamlessly combine universal and existential reasoning e.g., Prove non-safety via termination e.g., Prove non-termination via safety e.g., Prove termination and non-termination simultaneously Meta-theoretic properties of the type system: Closure of types under complement Soundness Relative completeness POPL'18, Los Angeles, United States 30
Complement Types ? Thanks to having both modes of non-determinism, the type complement operator can be defined: ????? ? ? ??? ? ? ??? ? ? ?? ? ? : ?? ? ?? ?? POPL'18, Los Angeles, United States 31
Example: Complement Types ? ? ? ??? ? ??? ? = ? functions that, for any integer ? and for any run with the argument ?, diverge or return an integer ? = ? ? = ? ??? ? ??? ? ? functions that, for some integer ? and for some run with the argument ?, terminate and return an integer ? ? POPL'18, Los Angeles, United States 32
Example: Combined Reasoning (Non-safety via Termination) Goal: prove that ??? ??? ? ? ? = ?? ? = ? ???? ? ???? ? ? ? ? ??? ? = ? ??? ? ?? ??? ? = ?? ? + ? violates ? ? = ? POPL'18, Los Angeles, United States 33
Example: Combined Reasoning (Non-safety via Termination) Goal: prove that ??? ??? ? ? ? = ?? ? = ? ???? ? ???? ? ? ? ? ??? ? = ? ??? ? ?? ??? ? = ?? ? + ? satisfies ? ? = ? POPL'18, Los Angeles, United States 34
Example: Combined Reasoning (Non-safety via Termination) Goal: prove that ??? ??? ? ? ? = ?? ? = ? ???? ? ???? ? ? ? ? ??? ? = ? ??? ? ?? ??? ? = ?? ? + ? satisfies ? ? ? 1. Show that ? is conditionally terminating: The well-founded relation ? ?,? , ? ,? . ? > ? ? = ? ? ? witnesses that ? has the type: ? ??? ? ? ? ? 2. Show that the actual call ? ??? ? always terminates by checking ? ??? 3. Show that, for any integer ?, we can choose an integer ? such that ? + ? ? ??? Q.E.D. POPL'18, Los Angeles, United States 35
Our Contributions Novel dependent refinement type system that can: uniformly express and verify universal and existential branching properties of call-by-value, higher-order, and non-deterministic programs: (cond.) safety, non-safety, termination, and non-termination seamlessly combine universal and existential reasoning e.g., Prove non-safety via termination e.g., Prove non-termination via safety e.g., Prove termination and non-termination simultaneously Meta-theoretic properties of the type system: Closure of types under complement Soundness Relative completeness POPL'18, Los Angeles, United States 36
Closure of Types under Complement For any type ? refining a simple type ?, ? ? = and ? ? = ? where ? : the set of expressions that behave according to ? ? : the set of expressions of the type ? POPL'18, Los Angeles, United States 37
Soundness ? ? ? implies ? ? ? the set of expressions that behave according to ? under any valuation conforming to ? POPL'18, Los Angeles, United States 38
Relative Completeness ? ? implies ? ? under the assumption that the underlying logic is sufficiently expressible to G del encode arbitrary functions definable in the target programming language to represent well-founded relations witnessing the termination of the definable functions POPL'18, Los Angeles, United States 39
Summary Novel dependent refinement type system that can: uniformly express and verify universal and existential branching properties of call-by-value, higher-order, and non-deterministic programs: (cond.) safety, non-safety, termination, and non-termination seamlessly combine universal and existential reasoning e.g., Prove non-safety via termination e.g., Prove non-termination via safety e.g., Prove termination and non-termination simultaneously Meta-theoretic properties of the type system: Closure of types under complement Soundness Relative completeness POPL'18, Los Angeles, United States 40
Future Work Extensions with temporal specifications: Temporal trace specs. (e.g., LTL) Branching temporal specs. (e.g., CTL, modal-?) Extensions with language features: Recursive data structures Linked data structures Call-by-name evaluation Probabilistic choice Automation of type checking and inference POPL'18, Los Angeles, United States 41
Towards Automation (Ongoing) Type Checking How to leverage off-the-shelf SMT solvers? Abstraction and counterexample guided refinement for the encoding of function-type values Type Inference How to synthesize inductive invariants, well-founded relations, and Skolemization predicates? Reduction to existentially-quantified Horn clause and well-foundedness constraints How to achieve scalable inference? Combination of universal and existential reasoning POPL'18, Los Angeles, United States 42