| -- SPDX-License-Identifier: LicenseRef-Sovereign-Leviathan-SL-AGPL3-001 |
| -- Licensing: see LICENSE in the repository root. |
|
|
| /- LatticeKernel.lean β Lean 4 specification of the relational kernel. |
| Theorems are the contracts; execution stays in miniKanren/Prolog/Formulog. |
| lake / lean LatticeKernel.lean (mathlib not required) |
| -/ |
|
|
| namespace LatticeKernel |
|
|
| inductive Peano where |
| | z |
| | s : Peano β Peano |
| deriving Repr, DecidableEq |
|
|
| def add : Peano β Peano β Peano |
| | .z, y => y |
| | .s x, y => .s (add x y) |
|
|
| def mul : Peano β Peano β Peano |
| | .z, _ => .z |
| | .s x, y => add y (mul x y) |
|
|
| theorem add_z (y : Peano) : add .z y = y := rfl |
| theorem add_s (x y : Peano) : add (.s x) y = .s (add x y) := rfl |
|
|
| inductive Bit where |
| | b0 | b1 |
| deriving Repr, DecidableEq |
|
|
| def bitXor : Bit β Bit β Bit |
| | .b0, .b0 => .b0 |
| | .b0, .b1 => .b1 |
| | .b1, .b0 => .b1 |
| | .b1, .b1 => .b0 |
|
|
| def bitAnd : Bit β Bit β Bit |
| | .b1, .b1 => .b1 |
| | _, _ => .b0 |
|
|
| def fullAdd (cin x y : Bit) : Bit Γ Bit := |
| let w := bitXor x y |
| let c1 := bitAnd x y |
| let r := bitXor w cin |
| let c2 := bitAnd w cin |
| (r, bitXor c1 c2) |
|
|
| inductive Smt where |
| | atom : String β Smt |
| | not : Smt β Smt |
| | and : Smt β Smt β Smt |
| deriving Repr |
|
|
| partial def atoms : Smt β List Smt |
| | .and a b => atoms a ++ atoms b |
| | p => [p] |
|
|
| def satStub (Ο : Smt) : Bool := |
| let as := atoms Ο |
| Β¬ as.any (fun p => |
| match p with |
| | .not q => as.contains q |
| | q => as.contains (.not q)) |
|
|
| inductive FsmState where |
| | s0 | s1 |
| deriving Repr, DecidableEq |
|
|
| def fsm (st : FsmState) (inp : Bit) : FsmState Γ Bit := |
| match st, inp with |
| | .s0, .b0 => (.s0, .b0) |
| | .s0, .b1 => (.s1, .b0) |
| | .s1, .b0 => (.s0, .b1) |
| | .s1, .b1 => (.s1, .b1) |
|
|
| inductive Abs where |
| | conc : Nat β Abs |
| | top |
| | interval : Nat β Nat β Abs |
| deriving Repr |
|
|
| def refines : Abs β Nat β Prop |
| | .conc c, n => c = n |
| | .top, _ => True |
| | .interval lo hi, n => lo β€ n β§ n β€ hi |
|
|
| end LatticeKernel |
|
|
