From 51a6be99deb292161b0469b70b4d8410bd7a975f Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 16 Apr 2020 16:00:25 -0500 Subject: [PATCH] Add ProofNodeManager and ProofChecker (#4317) Further work on adding core utilities for ProofNode objects, in support of the new proof infrastructure. ProofNodeManager is analogous to NodeManager. It is a trusted way of generating only "well-formed" ProofNode pointers (according to a checker). ProofChecker is analogous to TypeChecker. It is intended to be infrastructure for our internal proof checker. This PR (and 1 more) is required to get to a place where Haniel and I can collaborate on further development for proofs. --- src/expr/CMakeLists.txt | 4 ++ src/expr/proof_checker.cpp | 82 ++++++++++++++++++++++ src/expr/proof_checker.h | 94 +++++++++++++++++++++++++ src/expr/proof_node.h | 4 ++ src/expr/proof_node_manager.cpp | 89 ++++++++++++++++++++++++ src/expr/proof_node_manager.h | 117 ++++++++++++++++++++++++++++++++ 6 files changed, 390 insertions(+) create mode 100644 src/expr/proof_checker.cpp create mode 100644 src/expr/proof_checker.h create mode 100644 src/expr/proof_node_manager.cpp create mode 100644 src/expr/proof_node_manager.h diff --git a/src/expr/CMakeLists.txt b/src/expr/CMakeLists.txt index aa928fdb7..f21241ef5 100644 --- a/src/expr/CMakeLists.txt +++ b/src/expr/CMakeLists.txt @@ -33,8 +33,12 @@ libcvc4_add_sources( node_value.cpp node_value.h node_visitor.h + proof_checker.cpp + proof_checker.h proof_node.cpp proof_node.h + proof_node_manager.cpp + proof_node_manager.h proof_rule.cpp proof_rule.h symbol_table.cpp diff --git a/src/expr/proof_checker.cpp b/src/expr/proof_checker.cpp new file mode 100644 index 000000000..f4c275c47 --- /dev/null +++ b/src/expr/proof_checker.cpp @@ -0,0 +1,82 @@ +/********************* */ +/*! \file proof_checker.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Implementation of proof checker + **/ + +#include "expr/proof_checker.h" + +namespace CVC4 { + +Node ProofChecker::check(ProofNode* pn, Node expected) +{ + return check(pn->getId(), pn->getChildren(), pn->getArguments(), expected); +} + +Node ProofChecker::check( + PfRule id, + const std::vector>& children, + const std::vector& args, + Node expected) +{ + std::map::iterator it = d_checker.find(id); + if (it == d_checker.end()) + { + // no checker for the rule + Trace("pfcheck") << "ProofChecker::check: no checker for rule " << id + << std::endl; + return Node::null(); + } + // check it with the corresponding checker + std::vector cchildren; + for (const std::shared_ptr& pc : children) + { + Assert(pc != nullptr); + Node cres = pc->getResult(); + if (cres.isNull()) + { + Trace("pfcheck") + << "ProofChecker::check: child proof was invalid (null conclusion)" + << std::endl; + // should not have been able to create such a proof node + Assert(false); + return Node::null(); + } + cchildren.push_back(cres); + } + Node res = it->second->check(id, cchildren, args); + if (!expected.isNull() && res != expected) + { + Trace("pfcheck") + << "ProofChecker::check: result does not match expected value." + << std::endl; + Trace("pfcheck") << " result: " << res << std::endl; + Trace("pfcheck") << " expected: " << expected << std::endl; + // it did not match the given expectation, fail + return Node::null(); + } + return res; +} + +void ProofChecker::registerChecker(PfRule id, ProofRuleChecker* psc) +{ + std::map::iterator it = d_checker.find(id); + if (it != d_checker.end()) + { + // checker is already provided + Notice() << "ProofChecker::registerChecker: checker already exists for " + << id << std::endl; + return; + } + d_checker[id] = psc; +} + +} // namespace CVC4 diff --git a/src/expr/proof_checker.h b/src/expr/proof_checker.h new file mode 100644 index 000000000..48b41453f --- /dev/null +++ b/src/expr/proof_checker.h @@ -0,0 +1,94 @@ +/********************* */ +/*! \file proof_checker.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Proof checker utility + **/ + +#include "cvc4_private.h" + +#ifndef CVC4__EXPR__PROOF_CHECKER_H +#define CVC4__EXPR__PROOF_CHECKER_H + +#include + +#include "expr/node.h" +#include "expr/proof_node.h" + +namespace CVC4 { + +/** A virtual base class for checking a proof rule */ +class ProofRuleChecker +{ + public: + ProofRuleChecker() {} + virtual ~ProofRuleChecker() {} + /** + * This checks a single step in a proof. + * + * Return the formula that is proven by a proof node with the given id, + * premises and arguments, or null if such a proof node is not well-formed. + * + * @param id The id of the proof node to check + * @param children The premises of the proof node to check. These are nodes + * corresponding to the conclusion (ProofNode::getResult) of the children + * of the proof node we are checking. + * @param args The arguments of the proof node to check + * @return The conclusion of the proof node if successful or null if such a + * proof node is malformed. + */ + virtual Node check(PfRule id, + const std::vector& children, + const std::vector& args) = 0; +}; + +/** A class for checking proofs */ +class ProofChecker +{ + public: + ProofChecker() {} + ~ProofChecker() {} + /** + * Return the formula that is proven by proof node pn, or null if pn is not + * well-formed. If expected is non-null, then we return null if pn does not + * prove expected. + * + * @param pn The proof node to check + * @param expected The (optional) formula that is the expected conclusion of + * the proof node. + * @return The conclusion of the proof node if successful or null if the + * proof is malformed, or if no checker is available for id. + */ + Node check(ProofNode* pn, Node expected = Node::null()); + /** Same as above, with explicit arguments + * + * @param id The id of the proof node to check + * @param children The children of the proof node to check + * @param args The arguments of the proof node to check + * @param expected The (optional) formula that is the expected conclusion of + * the proof node. + * @return The conclusion of the proof node if successful or null if the + * proof is malformed, or if no checker is available for id. + */ + Node check(PfRule id, + const std::vector>& children, + const std::vector& args, + Node expected = Node::null()); + /** Indicate that psc is the checker for proof rule id */ + void registerChecker(PfRule id, ProofRuleChecker* psc); + + private: + /** Maps proof steps to their checker */ + std::map d_checker; +}; + +} // namespace CVC4 + +#endif /* CVC4__EXPR__PROOF_CHECKER_H */ diff --git a/src/expr/proof_node.h b/src/expr/proof_node.h index 7bf7cb0b4..9a460c59b 100644 --- a/src/expr/proof_node.h +++ b/src/expr/proof_node.h @@ -24,6 +24,8 @@ namespace CVC4 { +class ProofNodeManager; + /** A node in a proof * * A ProofNode represents a single step in a proof. It contains: @@ -46,6 +48,8 @@ namespace CVC4 { */ class ProofNode { + friend class ProofNodeManager; + public: ProofNode(PfRule id, const std::vector>& children, diff --git a/src/expr/proof_node_manager.cpp b/src/expr/proof_node_manager.cpp new file mode 100644 index 000000000..e2f5ca2dc --- /dev/null +++ b/src/expr/proof_node_manager.cpp @@ -0,0 +1,89 @@ +/********************* */ +/*! \file proof_node_manager.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Implementation of proof node manager + **/ + +#include "expr/proof_node_manager.h" + +using namespace CVC4::kind; + +namespace CVC4 { + +ProofNodeManager::ProofNodeManager(ProofChecker* pc) : d_checker(pc) {} + +std::shared_ptr ProofNodeManager::mkNode( + PfRule id, + const std::vector>& children, + const std::vector& args, + Node expected) +{ + Node res = checkInternal(id, children, args, expected); + if (res.isNull()) + { + // if it was invalid, then we return the null node + return nullptr; + } + // otherwise construct the proof node and set its proven field + std::shared_ptr pn = + std::make_shared(id, children, args); + pn->d_proven = res; + return pn; +} + +bool ProofNodeManager::updateNode( + ProofNode* pn, + PfRule id, + const std::vector>& children, + const std::vector& args) +{ + // should have already computed what is proven + Assert(!pn->d_proven.isNull()) + << "ProofNodeManager::updateProofNode: invalid proof provided"; + // We expect to prove the same thing as before + Node res = checkInternal(id, children, args, pn->d_proven); + if (res.isNull()) + { + // if it was invalid, then we do not update + return false; + } + // we update its value + pn->setValue(id, children, args); + // proven field should already be the same as the result + Assert(res == pn->d_proven); + return true; +} + +Node ProofNodeManager::checkInternal( + PfRule id, + const std::vector>& children, + const std::vector& args, + Node expected) +{ + Node res; + if (d_checker) + { + // check with the checker, which takes expected as argument + res = d_checker->check(id, children, args, expected); + Assert(!res.isNull()) + << "ProofNodeManager::checkInternal: failed to check proof"; + } + else + { + // otherwise we trust the expected value, if it exists + Assert(!expected.isNull()) << "ProofNodeManager::checkInternal: no checker " + "or expected value provided"; + res = expected; + } + return res; +} + +} // namespace CVC4 diff --git a/src/expr/proof_node_manager.h b/src/expr/proof_node_manager.h new file mode 100644 index 000000000..17c5580bf --- /dev/null +++ b/src/expr/proof_node_manager.h @@ -0,0 +1,117 @@ +/********************* */ +/*! \file proof_node_manager.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Proof node manager utility + **/ + +#include "cvc4_private.h" + +#ifndef CVC4__EXPR__PROOF_NODE_MANAGER_H +#define CVC4__EXPR__PROOF_NODE_MANAGER_H + +#include + +#include "expr/proof_checker.h" +#include "expr/proof_node.h" + +namespace CVC4 { + +/** + * A manager for proof node objects. This is a trusted interface for creating + * and updating ProofNode objects. + * + * In more detail, we say a ProofNode is "well-formed (with respect to checker + * X)" if its d_proven field is non-null, and corresponds to the formula that + * the ProofNode proves according to X. The ProofNodeManager class constructs + * and update nodes that are well-formed with respect to its underlying checker. + * + * If no checker is provided, then the ProofNodeManager assigns the d_proven + * field of ProofNode based on the provided "expected" argument in mkNode below, + * which must be provided in this case. + * + * The ProofNodeManager is used as a trusted way of updating ProofNode objects + * via updateNode below. In particular, this method leaves the d_proven field + * unchanged and updates (if possible) the remaining content of a given proof + * node. + * + * Notice that ProofNode objects are mutable, and hence this class does not + * cache the results of mkNode. A version of this class that caches + * immutable version of ProofNode objects could be built as an extension + * or layer on top of this class. + */ +class ProofNodeManager +{ + public: + ProofNodeManager(ProofChecker* pc = nullptr); + ~ProofNodeManager() {} + /** + * This constructs a ProofNode with the given arguments. The expected + * argument, when provided, indicates the formula that the returned node + * is expected to prove. If we find that it does not, based on the underlying + * checker, this method returns nullptr. + * + * @param id The id of the proof node. + * @param children The children of the proof node. + * @param args The arguments of the proof node. + * @param expected (Optional) the expected conclusion of the proof node. + * @return the proof node, or nullptr if the given arguments do not + * consistute a proof of the expected conclusion according to the underlying + * checker, if both are provided. It also returns nullptr if neither the + * checker nor the expected field is provided, since in this case the + * conclusion is unknown. + */ + std::shared_ptr mkNode( + PfRule id, + const std::vector>& children, + const std::vector& args, + Node expected = Node::null()); + /** + * This method updates pn to be a proof of the form ( children, args ), + * while maintaining its d_proven field. This method returns false if this + * proof manager is using a checker, and we compute that the above proof + * is not a proof of the fact that pn previously proved. + * + * @param pn The proof node to update. + * @param id The updated id of the proof node. + * @param children The updated children of the proof node. + * @param args The updated arguments of the proof node. + * @return true if the update was successful. + * + * Notice that updateNode always returns true if there is no underlying + * checker. + */ + bool updateNode(ProofNode* pn, + PfRule id, + const std::vector>& children, + const std::vector& args); + + private: + /** The (optional) proof checker */ + ProofChecker* d_checker; + /** Check internal + * + * This returns the result of proof checking a ProofNode with the provided + * arguments with an expected conclusion, which may not null if there is + * no expected conclusion. + * + * This throws an assertion error if we fail to check such a proof node, or + * if expected is provided (non-null) and is different what is proven by the + * other arguments. + */ + Node checkInternal(PfRule id, + const std::vector>& children, + const std::vector& args, + Node expected); +}; + +} // namespace CVC4 + +#endif /* CVC4__EXPR__PROOF_NODE_H */ -- 2.30.2