diff --git a/proof-language.md b/proof-language.md new file mode 100644 index 0000000000..fea4f7d320 --- /dev/null +++ b/proof-language.md @@ -0,0 +1,392 @@ +--- +geometry: margin=2cm +--- + +\newcommand{\limplies}{\to} +\renewcommand{\phi}{\varphi} + + +Matching logic proof format +=========================== + +This is a proposed matching logic proof format. + +## Relation to Metamath + +Note that this language heavily based on the metamath format for compressed proofs. +Besides being a binary rather than ASCII encoding, there are two major changes. + +1. We use the same mechanism for constructing terms and proofs, allowing better + compression. +2. We allow emmitting multiple proofs from the same representation. This allows + us to represent lemmas and compression uniformly. + That is, we can store the entire contents of a single metamath file in this format, + rather than just the proof of a single lemma. + +## Relation to postfix notation/RPN + +The format may be viewed as a generalization +of postfix notation (incidentally also called Lukaseiwicz notation), +for an expression computing the conclusion of a proof. + +We also allow marking subexpressions (i.e. either proofs or patterns) for reuse. This +allows us to represent lemmas, and compactly representing configurations and notation. + +(This needs input from ZK folk.) Finally, we allow marking constructed proofs +as public. This serves two purposes. First, it allows us to publish lemmas +that may be reused in other proofs. Second, it allows us to publish the main +result proved by the proof. + + +## As a stack machine + +It may also be viewed language interpreted using a stack machine. +This stack machines constructs terms---either patterns or proofs. We treat +patterns and proofs uniformly---at an abstract level, they are both terms we +must construct, with particular well-formedness criteria. It is intended for the +most part, that **the verifier only needs to keep proved conclusions in +memory**. + + +## Goals: + +- No upfront parsing cost. +- Easily verifiable using ZK. +- Low memory usage. +- Composability. + + +## Non-goals: + +- Parallization: I have not been thinking explicitly about parallel verification of this format, + because I expect parallization to happen by composing units of this format into larger proofs. + Even so I think with some additional metadata, we could make + this format parallizable. + +- Human readability: We aim to be a simple binary format. To become human + readable, we expect the user to run a secondary program to pretty-print the + proof. Note that symbols, lemmas, and notation do not have names. + + +Terms +===== + +As mentioned previously, we may view this format as a language for constructing +terms that meet particular well-formedness criteria. Let us first enumerate +those terms, in a python-esque pseudocode. + +`Term`s are of two types, `Pattern`, and `Proof`. +Every `Term` has a well-formedness check. +Every `Proof` has a conclusion. + +```python +abstract class Term: + abstract def well_formed: + ... + +abstract class Pattern(Term): + def well_formed(): + # Fails if any two MetaVars with the same id has + # different meta-requirements + # MetaVars are introduced later. + ... + +abstract class Proof(Term): + abstract def conclusion: + ... +``` + +`Pattern`s +---------- + +There are two classes of `Pattern`, +the expected concrete constructors for matching logic patterns, +and a representation for various "meta" patterns. + +### Standard patterns + +```python +class Symbol(Pattern): + name: uint32 + +class SVar(Pattern): + name: uint32 + +class EVar(Pattern): + name: uint32 + +class Implication(Pattern): + left: Pattern + right: Pattern + +class Application(Pattern): + left: Pattern + right: Pattern + +class Exists(Pattern): + var: EVar + subpattern : Pattern + +class Mu(Pattern): + var: SVar + subpattern : Pattern + + def well_formed(): + return super.well_formed() + and subpattern.var_occurs_positively(var) +``` + +### Meta-patterns + +Meta-patterns allow us to represent axiom- and theorem-schemas through the use +of metavariables: + +```python +class MetaVar(Pattern): + name: uint32 + + # Meta-requirements that must be satisfied by any instantiation. + fresh: list[EVar | SVar] # variables that must not occur in an instatiation + positive: list[SVar] # variables that must only occur positively in an instatiation + negative: list[SVar] # variables that must only occur negatively in an instatiation + application_context: list[EVar] # Variables that must only occur as a hole variable in an application context. +``` + +Each `MetaVar` has a list of requirements that must be met by any instantiation. +These may also be used by the well-formedness checks for `Proof`s. + +We also need to represent substitutions applied to `MetaVar`s. + +```python +class ESubst(Pattern): + pattern: MetaVar + var: EVar + plug: Pattern + +class SSubst(Pattern): + pattern: MetaVar + var: SVar + plug: Pattern +``` + + +`Proof`s +-------- + +### Axiom Schemas + +Axiom schemas are `Proof`s that do not need any input arguments. +They may use `MetaVar`s to represent their schematic nature. + +```python +class Lukaseiwicz(Proof): + def conclusion(): + phi1 = MetaVar('phi1') + return Implication(Implication(Implication(MetaVar(phi1) , ...)...)...) + +class Quantifier(Proof): + def conclusion(): + x = EVar('#x') + y = EVar('#y') + phi = MetaVar('phi', fresh=[y]) + return Implication(ESubst(phi, x, y), Exists(x, phi)) + +class PropagationOr(Proof): + def conclusion(): + hole = EVar('#hole') + C = MetaVar(application_context=(EVar('#hole'),)) + phi1 = MetaVar('#phi1') + phi2 = MetaVar('#phi2') + return Implication(ESubst(C, or(phi1, phi2), hole), or(ESubst(C, phi1, hole), ESubst(C, phi2, hole))) + +... +``` + + +### Meta Variable Instantiation + +Using a single rule of meta inference, we may instantiate metatheorems. +This allows us to prove theorem schemas, such as $\phi \limplies \phi$. + +```python +class InstantiateSchema(Proof): + subproof : Proof + metavar_id: uint32 + instantiation: Pattern + + def well_formed(): + # Fails if the instantiation does not meet the + # disjoint/positive/freshness/application ctx + # criterea of the metavar. + + def conclusion(): + return subproof.meta_substitute(metavar, instantiation) +``` + +We may also use metavariables to represent notation. + +```python +class InstantiateNotation(Pattern): + notation: Pattern + metavar_id: uint32 + instantiation: Pattern + + def well_formed(): + # Fails if the instantiation does not meet the + # disjoint/positive/freshness/application ctx + # criterea of the metavar. + + def conclusion(): + return notation.meta_substitute(metavar, instantiation) +``` + + +### Ordinary inference + +```python +class ModusPonens(Proof): + premise_left: Implication + premise_right: Pattern + + def conclusion(): + return premise_left.right + + def well_formed(): + assert premise_right == premise_left.left + +class Generalization(Proof): + premise: Implication + + def phi1(): + premise.left + def phi2(): + premise.right + + def conclusion(): + return Implication(ESubst(MetaVar(phi), EVar(x), EVar(y)), Exists(EVar(x), MetaVar(phi))) + + def well_formed(): + assert EVar(x) is fresh in phi1() +... +``` + +Instructions and semantics +========================== + +Each of these instructions checks that the constructed `Term` is well-formed before pushing onto the stack. +Otherwise, execution aborts, and verification fails. + +* Supporting: + + `List n:uint32` + : Consume $n$ items from the stack, and push a list containing those items to the stack. + +* Variables and Symbols: + + `EVar ` + : Push an `EVar` onto the stack. + + `SVar ` + : `Push an `SVar` onto the stack. + + `Symbol ` + : `Push an `Symbol` onto the stack. + + `MetaVar ` + : Consume the first four entries from the stack (corresponding to the meta-requirements), + and push an `MetaVar` onto the stack. + +* Connectives: + + `Implication`/`Application`/`Exists`/`Mu` + : Consume the first two patterns from the stack, and push an implication/application/exists/mu onto the stack with appropriate argumetns. + +* Axiom Schemas + + `Lukaseiwicz`/`Quantifier`/`PropagationOr`/`PropagationExists`/`PreFixpoint`/`Existance`/`Singleton` + : Push Proof term corresponding to axiom schema onto the stack. + +* Meta inference + + `InstantiateSchema ` + : Consume a `Proof` and `Pattern` off the stack, and push the instantiated proof term to the stack. + + `InstantiateNotation ` + : Consume two `Pattern`s off the stack, and push the instantiated proof term to the stack. + +* Inference rules + + `ModusPonens`/`Generalization`/`Frame`/`Substitution`/`KnasterTarski` + : Consume one or two `Proof` terms off the stack and push the new proof term. + +* Memory manipulation: + + `Save` + : Store the top of the stack to the lowest unused index in memory. + + `Load i:uint32` + : Push the `Term` at index $i$ to the top of the stack. + + `Delete i:uint32` + : Remove the `Term` at index $i$ from memory. This is not strictly needed, + but will allow the verifier to use less memory. The memory slot is not considered free. + +* Journal manipulation. + + `Publish` + : publish the entry at the top of the stack to the journal. + +* Stack manipulation. + + `Pop` + : Consume the top of the stack. (Do we need this? Probably not.) + +Verification +============ + +The verifier takes two inputs[^1]: + +1. `theory` A file with instructions to construct patterns + and place them on the stack to represent the theory $\Gamma$. + This is public. + + All patterns on the stack after running this file are considered axioms. + Before verification of the proof, these are moved to the first free memory locations (That is, after the notation). + + All patterns placed in memory using the `Save` instruction may be used as notation. + Note that these patterns are not considered proved, and can only be used to buildother patterns. + + TODO: We should review this. Do we want a specific instruction for publishing notation? + +2. `lemmas`: A file with instructions to construct patterns corresponding the + lemmas previously proved in other proof files. An aggregation circuit will + need to check that the theory used by that proof is a subset of the theory + for the corrent proof. + + All patterns on the stack after running this file are considered proved lemmas. + + TODO: Should we allow notation from these as well? + If we do, composing proofs may get difficult---notation may accumulate + forcing the checker to use a lot more memory than needed. + +3. `proof`: A file with instructions to construct proofs about the theory. + This file is private, and should be rolled-up by ZK. + +The verifier consumes the theory file. The stack should now only include `Pattern` terms. +These are moved into the initial entries of the memory, as `Proof` terms. +The verifier then consumes the `proof` file and produces a "journal"[^2], +containing a list of instructions to construct the patterns of theorems proved. + +[^1]: This needs input from the ZK folk for the exact input mechanism. +[^2]: Using Risc Zero terminology + +The verifier state consists of a stack of `Term`s, and +an indexed list of saved `Term`s, called the memory. + +Composition +=========== + +We may compose proofs together, by allowing proofs to reuse results contained in another proofs journal. +A subset of the contents of the journal of a proof $p$ may be included as the input lemmas of another proof $q$, +**so long as** the gamma of $p$ is subset of gamma of $q$. + diff --git a/src/checker/checker.py b/src/checker/checker.py new file mode 100644 index 0000000000..62f51489bb --- /dev/null +++ b/src/checker/checker.py @@ -0,0 +1,370 @@ +from __future__ import annotations + +from abc import abstractmethod +from dataclasses import dataclass +from enum import IntEnum +from typing import TYPE_CHECKING, cast + +if TYPE_CHECKING: + from collections.abc import Iterator + + +class Instruction(IntEnum): + List = 1 + + # Patterns + EVar = 2 + SVar = 3 + Symbol = 4 + Implication = 5 + Application = 6 + Mu = 7 + Exists = 8 + + # Meta Patterns + MetaVar = 9 + ESubst = 10 + SSubst = 11 + + # Axiom Schemas + Prop1 = 12 + Prop2 = 29 # TODO: Fix numbering + Prop3 = 30 # TODO: Fix numbering + Quantifier = 13 + PropagationOr = 14 + PropagationExists = 15 + PreFixpoint = 16 + Existance = 17 + Singleton = 18 + + # Inference rules + ModusPonens = 19 + Generalization = 20 + Frame = 21 + Substitution = 22 + KnasterTarski = 23 + + # Meta Incference rules + InstantiateSchema = 24 + + # Stack Manipulation + Pop = 25 + + # Memory Manipulation + Save = 26 + Load = 27 + + # Journal Manipulation + Publish = 28 + + +class Pattern: + @abstractmethod + def instantiate(self, var: MetaVar, plug: Pattern) -> Pattern: + ... + + +@dataclass(frozen=True) +class EVar(Pattern): + name: int + + def instantiate(self, var: MetaVar, plug: Pattern) -> EVar: + return self + + +@dataclass(frozen=True) +class SVar(Pattern): + name: int + + def instantiate(self, var: MetaVar, plug: Pattern) -> SVar: + return self + + +@dataclass(frozen=True) +class Symbol(Pattern): + name: int + + def instantiate(self, var: MetaVar, plug: Pattern) -> Symbol: + return self + + +@dataclass(frozen=True) +class Implication(Pattern): + left: Pattern + right: Pattern + + def instantiate(self, var: MetaVar, plug: Pattern) -> Implication: + return Implication(self.left.instantiate(var, plug), self.right.instantiate(var, plug)) + + def __repr__(self) -> str: + return '(' + str(self.left) + ' -> ' + str(self.right) + ')' + + +@dataclass(frozen=True) +class Application(Pattern): + left: Pattern + right: Pattern + + def instantiate(self, var: MetaVar, plug: Pattern) -> Application: + return Application(self.left.instantiate(var, plug), self.right.instantiate(var, plug)) + + +@dataclass(frozen=True) +class Exists(Pattern): + var: EVar + subpattern: Pattern + + def instantiate(self, var: MetaVar, plug: Pattern) -> Exists: + return Exists(self.var.instantiate(var, plug), self.subpattern.instantiate(var, plug)) + + +@dataclass(frozen=True) +class Mu(Pattern): + var: SVar + subpattern: Pattern + + def instantiate(self, var: MetaVar, plug: Pattern) -> Mu: + return Mu(self.var.instantiate(var, plug), self.subpattern.instantiate(var, plug)) + + +@dataclass(frozen=True) +class MetaVar(Pattern): + name: int + fresh: tuple[EVar | SVar, ...] + positive: tuple[SVar, ...] + negative: tuple[SVar, ...] + application_context: tuple[EVar, ...] + + def instantiate(self, var: MetaVar, plug: Pattern) -> Pattern: + if self == var: + # TODO: Check meta-requirements + return plug + return self + + def __repr__(self) -> str: + return str(self.name) + + +@dataclass(frozen=True) +class Proved: + pattern: Pattern + + def instantiate(self, var: MetaVar, plug: Pattern) -> Proved: + return Proved(self.pattern.instantiate(var, plug)) + + +Stack = list[Pattern | list[Pattern] | Proved] +Memory = list[Pattern | Proved] +Journal = list[Proved] + + +def execute_instructions(proof: Iterator[int], stack: Stack, memory: Memory, journal: Journal) -> None: + while True: + try: + instr = next(proof) + except StopIteration: + return + + match instr: + case Instruction.List: + len = next(proof) + items = [] + for _ in range(len): + pattern = stack.pop() + assert isinstance(pattern, Pattern) + items.append(pattern) + stack.append(items) + + case Instruction.EVar: + stack.append(EVar(next(proof))) + case Instruction.SVar: + stack.append(SVar(next(proof))) + case Instruction.Symbol: + stack.append(Symbol(next(proof))) + case Instruction.Implication: + left = stack.pop() + assert isinstance(left, Pattern) + right = stack.pop() + assert isinstance(right, Pattern) + stack.append(Implication(left, right)) + case Instruction.Application: + left = stack.pop() + assert isinstance(left, Pattern) + right = stack.pop() + assert isinstance(right, Pattern) + stack.append(Application(left, right)) + # TODO: Check metavariables are well named. + case Instruction.Exists: + var = stack.pop() + assert isinstance(var, EVar) + subpattern = stack.pop() + assert isinstance(subpattern, Pattern) + stack.append(Exists(var, subpattern)) + # TODO: Check metavariables are well named. + case Instruction.Mu: + var = stack.pop() + assert isinstance(var, SVar) + subpattern = stack.pop() + assert isinstance(subpattern, Pattern) + stack.append(Mu(var, subpattern)) + + case Instruction.MetaVar: + name = next(proof) + application_context = cast('list[EVar]', stack.pop()) + # TODO: We need assertions instead of typecasting + assert isinstance(application_context, list) + negative = cast('list[SVar]', stack.pop()) + assert isinstance(negative, list) + positive = cast('list[SVar]', stack.pop()) + assert isinstance(positive, list) + fresh = cast('list[EVar | SVar]', stack.pop()) + assert isinstance(fresh, list) + stack.append(MetaVar(name, tuple(fresh), tuple(positive), tuple(negative), tuple(application_context))) + + case Instruction.Prop1: + phi0 = MetaVar(0, (), (), (), ()) + phi1 = MetaVar(1, (), (), (), ()) + stack.append(Proved(Implication(phi0, Implication(phi1, phi0)))) + case Instruction.Prop2: + phi0 = MetaVar(0, (), (), (), ()) + phi1 = MetaVar(1, (), (), (), ()) + phi2 = MetaVar(2, (), (), (), ()) + stack.append( + Proved( + Implication( + Implication(phi0, Implication(phi1, phi2)), + Implication(Implication(phi0, phi1), Implication(phi0, phi2)), + ) + ) + ) + + case Instruction.InstantiateSchema: + plug = stack.pop() + assert isinstance(plug, Pattern) + var = stack.pop() + assert isinstance(var, MetaVar) + metatheorem = stack.pop() + assert isinstance(metatheorem, Proved), metatheorem + stack.append(metatheorem.instantiate(var, plug)) + + case Instruction.ModusPonens: + phi_implies_psi = stack.pop() + assert isinstance(phi_implies_psi, Proved), phi_implies_psi + assert isinstance(phi_implies_psi.pattern, Implication), phi_implies_psi + + phi = stack.pop() + assert isinstance(phi, Proved), phi + + assert phi.pattern == phi_implies_psi.pattern.left, (phi.pattern, phi_implies_psi.pattern.left) + stack.append(Proved(phi_implies_psi.pattern.right)) + + case Instruction.Save: + assert isinstance(stack[-1], (Pattern, Proved)) + memory.append(stack[-1]) + case Instruction.Load: + index = next(proof) + stack.append(memory[index]) + + case _: + raise AssertionError('Unknown Instruction: %s' % instr) + + +def verify(gamma: Iterator[int], proof: Iterator[int]) -> tuple[Stack, Memory, Journal]: + """Reads assumptions, proof, and emits a journal""" + stack: Stack = [] + memory: Memory = [] + journal: Journal = [] + + # TODO: Assert that no instructions use proof rules + execute_instructions(gamma, stack, memory, journal) + assert journal == [], 'Cannot publish from input.' + memory = [] + for item in stack: + assert isinstance(item, Pattern) + memory.append(Proved(item)) + stack = [] + execute_instructions(proof, stack, memory, journal) + return (stack, memory, journal) + + +# ---------------------------------------------------------------------------- +# --------------------------- Testing Harness -------------------------------- +# ---------------------------------------------------------------------------- + + +def test_construct_phi_implies_phi() -> None: + # fmt: off + proof : list[int] = [ + int(Instruction.List), 0, # Fresh + int(Instruction.List), 0, # Positive + int(Instruction.List), 0, # Negative + int(Instruction.List), 0, # Context + int(Instruction.MetaVar), 0, # Stack: Phi + int(Instruction.Save), # @ 0 + int(Instruction.Load), 0, # Phi ; Phi + int(Instruction.Implication), # Phi -> Phi + ] + # fmt: on + phi = MetaVar(0, (), (), (), ()) + stack, memory, journal = verify(iter([]), iter(proof[0:10])) + assert stack == [phi], stack + stack, memory, journal = verify(iter([]), iter(proof)) + assert stack == [Implication(phi, phi)], stack + + +def test_prove_phi_implies_phi() -> None: + # fmt: off + proof : list[int] = [ + int(Instruction.Prop1), # (p1: phi0 -> (phi1 -> phi0)) + + int(Instruction.List), 0, + int(Instruction.List), 0, + int(Instruction.List), 0, + int(Instruction.List), 0, + int(Instruction.MetaVar), 1, # Stack: p1 ; phi1 + int(Instruction.Save), + + int(Instruction.List), 0, + int(Instruction.List), 0, + int(Instruction.List), 0, + int(Instruction.List), 0, + int(Instruction.MetaVar), 0, # Stack: p1 ; phi1 ; phi0 + int(Instruction.Save), + + int(Instruction.InstantiateSchema), # Stack: (p2: phi0 -> (phi0 -> phi0)) + + int(Instruction.Prop1), # Stack: p2 ; p1 + int(Instruction.Load), 0, + int(Instruction.Load), 1, + int(Instruction.Load), 1, + int(Instruction.Implication), # Stack: p2 ; p1 ; phi1; phi0 -> phi0 + int(Instruction.Save), + + int(Instruction.InstantiateSchema), # Stack: p2 ; (p3: phi0 -> (phi0 -> phi0) -> phi0) + + int(Instruction.Prop2), + int(Instruction.Load), 0, + int(Instruction.Load), 2, + int(Instruction.InstantiateSchema), + int(Instruction.List), 0, + int(Instruction.List), 0, + int(Instruction.List), 0, + int(Instruction.List), 0, + int(Instruction.MetaVar), 2, + int(Instruction.Load), 1, + int(Instruction.InstantiateSchema), + + + int(Instruction.ModusPonens), + int(Instruction.ModusPonens), # Stack: phi0 -> phi0 + + int(Instruction.Publish), + ] + # fmt: on + phi0 = MetaVar(0, (), (), (), ()) + stack, memory, journal = verify(iter([]), iter(proof[0:55])) + assert stack == [Proved(Implication(phi0, phi0))], stack + + +test_construct_phi_implies_phi() +test_prove_phi_implies_phi()