diff --git a/.github/workflows/lean_action_ci.yml b/.github/workflows/lean_action_ci.yml new file mode 100644 index 000000000..58c72ad02 --- /dev/null +++ b/.github/workflows/lean_action_ci.yml @@ -0,0 +1,20 @@ +name: Lean Action CI + +on: + pull_request: + paths: + - "analysis/markov/**" + push: + branches: + - main + paths: + - "analysis/markov/**" + +jobs: + build: + runs-on: ubuntu-latest + steps: + - uses: actions/checkout@v4 + - uses: leanprover/lean-action@v1 + with: + lake-package-directory: analysis/markov diff --git a/Logbook.md b/Logbook.md index fc917341e..6b6d90f79 100644 --- a/Logbook.md +++ b/Logbook.md @@ -1,5 +1,18 @@ # Leios logbook +## 2025-10-02 + +### Markovian simulator for Linear Leios + +A new [Markovian simulation of Linear Leios](analysis/markov/ReadMe.md) computes the probability of EB certifications as RBs are produced. It probabilistically models four key transitions in Linear Leios and computes the efficiency of RB and EB production under potential adversarial conditions. + +1. *Forge RB:* create a new RB. +2. *Certify:* include a certificate in the RB. +3. *Forge EB:* create a new EB. +4. *Vote:* cast votes to reach a quorum. + +![Example results](analysis/markov/example-results.png) + ## 2025-09-19 ### Antithesis configuration for Rust simulator diff --git a/analysis/markov/.gitignore b/analysis/markov/.gitignore new file mode 100644 index 000000000..bfb30ec8c --- /dev/null +++ b/analysis/markov/.gitignore @@ -0,0 +1 @@ +/.lake diff --git a/analysis/markov/Linleios.lean b/analysis/markov/Linleios.lean new file mode 100644 index 000000000..3920332dc --- /dev/null +++ b/analysis/markov/Linleios.lean @@ -0,0 +1 @@ +import Linleios.Evolve diff --git a/analysis/markov/Linleios/Evolve.lean b/analysis/markov/Linleios/Evolve.lean new file mode 100644 index 000000000..498207ca6 --- /dev/null +++ b/analysis/markov/Linleios/Evolve.lean @@ -0,0 +1,122 @@ + +import Std.Data.HashMap +import Batteries.Lean.HashMap +import Lean.Data.Json.FromToJson + +import Linleios.Types + + +open Lean (Json) +open Lean.ToJson (toJson) +open Std (HashMap) + + +def forgeRb {env : Environment} (state : State) : Outcomes := + let state' := + { + state with + clock := state.clock + 1 + } + let p := 1 - env.fAdversary + [ + ({state' with hasRb := true, rbCount := state.rbCount + 1}, p) + , ({state' with hasRb := false, canCertify := false}, 1 - p) + ] + +def certify {env : Environment} (state : State) : Outcomes := + if state.hasRb && state.canCertify + then let p := env.pSpacingOkay + [ + ⟨{state with ebCount := state.ebCount + 1}, p⟩ + , ⟨state, 1 - p⟩ + ] + else [(state, 1)] + +def forgeEb {env : Environment} (state : State) : Outcomes := + if state.hasRb + then let p := 1 - env.pLate + [ + ({state with canCertify := true}, p) + , ({state with canCertify := false}, 1 - p) + ] + else [(state, 1)] + +def vote {env : Environment} (state : State) : Outcomes := + if state.hasRb + then let p := env.pQuorum + [ + (state, p) + , ({state with canCertify := false}, 1 - p) + ] + else [(state, 1)] + +def step {env : Environment} : List (State → Outcomes) := + [@forgeRb env, @certify env, @forgeEb env, @vote env] + + +def prune (ε : Float) : Probabilities → Probabilities := + HashMap.filter (fun _ p => p > ε) + +def evolve (transition : State → Outcomes) : Probabilities → Probabilities := + HashMap.fold + ( + fun acc state p => + HashMap.mergeWith (fun _ => Add.add) acc + ∘ HashMap.map (fun _ => Mul.mul p ∘ List.sum ∘ List.map Prod.snd) + ∘ List.groupByKey Prod.fst + $ transition state + ) + ∅ + +def chain (transitions : List (State → Outcomes)) : Probabilities → Probabilities := + match transitions with + | [] => id + | (t :: ts) => chain ts ∘ evolve t + +def simulate (env : Environment) (start : Probabilities) (ε : Float) : Nat → Probabilities +| 0 => start +| n + 1 => let state' := prune ε $ chain (@step env) start + simulate env state' ε n + +def totalProbability (states : Probabilities) : Probability := + states.values.sum + +def ebDistribution : Probabilities → HashMap Nat Probability := + HashMap.fold + ( + fun acc state p => + HashMap.mergeWith (fun _ => Add.add) acc + $ singleton ⟨ state.ebCount , p ⟩ + ) + ∅ + +def ebDistributionJson : Probabilities → Json := + Json.mkObj + ∘ List.map (fun ⟨k, v⟩ => ⟨toString k, toJson v⟩) + ∘ (fun z => z.mergeSort (by exact fun x y => x.fst ≤ y.fst)) + ∘ HashMap.toList + ∘ ebDistribution + +def rbEfficiency (states : Probabilities) : Float := + let clock := states.keys.head!.clock + let rbCount := + HashMap.fold + (fun acc state p =>acc + state.rbCount.toFloat * p) + 0 + states + rbCount / clock.toFloat + +def ebEfficiency (states : Probabilities) : Float := + let clock := states.keys.head!.clock + let ebCount := + HashMap.fold + (fun acc state p =>acc + state.ebCount.toFloat * p) + 0 + states + ebCount / (clock.toFloat - 1) + +def efficiency (states : Probabilities) : Float := + let rb := rbEfficiency states + let eb := ebEfficiency states + let ρ := 12.5 / 0.9 + (rb + ρ * eb) / (1 + ρ) diff --git a/analysis/markov/Linleios/Probability.lean b/analysis/markov/Linleios/Probability.lean new file mode 100644 index 000000000..5c061ca71 --- /dev/null +++ b/analysis/markov/Linleios/Probability.lean @@ -0,0 +1,27 @@ + +import Linleios.Util + + +def nPools : Nat := 2500 + +def stakeDistribution (nPools : Nat) : List Float := + (List.range nPools).map (fun k => ((k + 1).toFloat / nPools.toFloat)^10 - (k.toFloat / nPools.toFloat)^10) + +private def calibrateCommittee(committeeSize : Float) : Float := + let stakes : List Float := stakeDistribution nPools + let f (m : Float) : Float := + let ps : List Float := stakes.map (fun s => 1 - Float.exp (- m * s)) + ps.sum - committeeSize + bisectionSearch f committeeSize nPools.toFloat 0.5 10 + +private def committeeDistribution (pSuccessfulVote committeeSize : Float) : Float × Float := + let stakes : List Float := stakeDistribution nPools + let m := calibrateCommittee committeeSize + let ps : List Float := stakes.map (fun s => pSuccessfulVote * (1 - Float.exp (- m * s))) + let μ := ps.sum + let σ := (ps.map (fun p => p * (1 - p))).sum.sqrt + ⟨ μ , σ ⟩ + +def pQuorum (pSuccessfulVote committeeSize τ : Float) : Float := + let ⟨ μ , σ ⟩ := committeeDistribution pSuccessfulVote committeeSize + 1 - cdfGaussian (τ * committeeSize) μ σ diff --git a/analysis/markov/Linleios/Types.lean b/analysis/markov/Linleios/Types.lean new file mode 100644 index 000000000..f1051b0a9 --- /dev/null +++ b/analysis/markov/Linleios/Types.lean @@ -0,0 +1,60 @@ +import Std.Data.HashMap +import Batteries.Lean.HashMap + +import Linleios.Probability + + +open Std (HashMap) + + +abbrev Probability := Float + + +structure Environment where + activeSlotCoefficient : Probability + Lheader : Nat + Lvote : Nat + Ldiff : Nat + pSpacingOkay : Probability + pQuorum : Probability + pLate : Probability + fAdversary : Float +deriving Repr + +def makeEnvironment (Lheader Lvote Ldiff : Nat) (activeSlotCoefficient committeeSize τ pRbHeaderArrives pEbValidates pEbUnvalidated fAdversary : Float) : Environment := + { + activeSlotCoefficient := activeSlotCoefficient + Lheader := Lheader + Lvote := Lvote + Ldiff := Ldiff + pSpacingOkay := (1 - activeSlotCoefficient).pow (3 * Lheader + Lvote + Ldiff - 1).toFloat + pQuorum := pQuorum (pRbHeaderArrives * pEbValidates * (1 - fAdversary)) committeeSize τ + pLate := pEbUnvalidated * (1 - committeeSize / nPools.toFloat) + fAdversary := fAdversary + } + + +structure State where + clock : Nat + rbCount : Nat + ebCount : Nat + hasRb : Bool + canCertify : Bool +deriving Repr, BEq, Hashable, Inhabited + +theorem genesis : (default : State).clock = 0 ∧ (default : State).rbCount = 0 ∧ (default : State).ebCount = 0 := by + constructor + rfl + constructor + rfl + rfl + + +def Probabilities := HashMap State Probability +deriving Repr, EmptyCollection + +instance : Inhabited Probabilities where + default := (∅ : Probabilities).insert Inhabited.default 1 + + +abbrev Outcomes := List (State × Probability) diff --git a/analysis/markov/Linleios/Util.lean b/analysis/markov/Linleios/Util.lean new file mode 100644 index 000000000..9c55bd4e7 --- /dev/null +++ b/analysis/markov/Linleios/Util.lean @@ -0,0 +1,30 @@ + +partial def erf (x : Float) : Float := + if x < 0 + then - erf (- x) + else + let p := 0.3275911 + let a₁ := 0.254829592 + let a₂ := -0.284496736 + let a₃ := 1.421413741 + let a₄ := -1.453152027 + let a₅ := 1.061405429 + let t := 1 / (1 + p * x) + 1 - (a₁ * t + a₂ * t^2 + a₃ * t^3 + a₄ * t^4 + a₅ * t^5) * Float.exp (- x^2) + +def cdfGaussian (x μ σ : Float) : Float := + (1 + erf ((x - μ) / σ / Float.sqrt 2)) / 2 + +def bisectionSearch (f : Float → Float) (low high : Float) (ε : Float) (maxIter : Nat) : Float := + match maxIter with + | 0 => (low + high) / 2 + | maxIter' + 1 => + let mid := (low + high) / 2 + let fmid := f mid + if high - low < ε || Float.abs fmid < ε then + mid + else if f low * fmid < 0 then + bisectionSearch f low mid ε maxIter' + else + bisectionSearch f mid high ε maxIter' +termination_by maxIter diff --git a/analysis/markov/Main.lean b/analysis/markov/Main.lean new file mode 100644 index 000000000..08487ae68 --- /dev/null +++ b/analysis/markov/Main.lean @@ -0,0 +1,77 @@ + +import Cli +import Linleios +import Parser.Char.Numeric +import Parser.Stream + +open Cli +open Lean (Json) + + +instance : ParseableType Float where + name := "Float" + parse? x := match (Parser.Char.ASCII.parseFloat : SimpleParser Substring Char Float).run x with + | .ok _ y => some y + | _ => none + + +def runMarkovCmd (p : Parsed) : IO UInt32 := + do + let activeSlotCoefficient : Float := p.flag! "active-slot-coefficient" |>.as! Float + let Lheader : Nat := p.flag! "l-header" |>.as! Nat + let Lvote : Nat := p.flag! "l-vote" |>.as! Nat + let Ldiff : Nat := p.flag! "l-diff" |>.as! Nat + let committeeSize : Nat := p.flag! "committee-size" |>.as! Nat + let τ : Float := p.flag! "quorum-fraction" |>.as! Float + let pRbHeaderArrives : Float := p.flag! "p-rb-header-arrives" |>.as! Float + let pEbValidates : Float := p.flag! "p-eb-validates" |>.as! Float + let pLateDiffusion : Float := p.flag! "p-late-diffusion" |>.as! Float + let fAdversary : Float := p.flag! "adversary-fraction" |>.as! Float + let ε : Float := p.flag! "tolerance" |>.as! Float + let rbCount : Nat := p.flag! "rb-count" |>.as! Nat + let env := makeEnvironment Lheader Lvote Ldiff activeSlotCoefficient committeeSize.toFloat τ pRbHeaderArrives pEbValidates pLateDiffusion fAdversary + let sn := simulate env default ε rbCount + if p.hasFlag "output-file" + then IO.FS.writeFile (p.flag! "output-file" |>.as! String) (Json.pretty $ ebDistributionJson sn) + IO.println s!"RB efficiency: {(reprPrec (rbEfficiency sn) 0).pretty}" + IO.println s!"EB efficiency: {(reprPrec (ebEfficiency sn) 0).pretty}" + IO.println s!"Overall efficiency: {(reprPrec (efficiency sn) 0).pretty}" + IO.eprintln s!"Missing probability: {1 - totalProbability sn}" + pure 0 + +def markov : Cmd := `[Cli| + markov VIA runMarkovCmd; ["0.0.1"] + "Run a Markov simulation of Linear Leios." + FLAGS: + "active-slot-coefficient" : Float ; "The active slot coefficient for RBs, in probability per slot." + "l-header" : Nat ; "L_header protocol parameter, in slots." + "l-vote" : Nat ; "L_vote protocol parameter, in slots." + "l-diff" : Nat ; "L_diff protocol parameter, in slots." + "committee-size" : Nat ; "Expected number of voters in the committee, out of 2500 stakepools total." + "quorum-fraction" : Float ; "τ protocol parameter, in %/100." + "p-rb-header-arrives" : Float ; "Probability that the RB header arrives before L_header." + "p-eb-validates" : Float ; "Probability that the EB is fully validated before 3 L_header + L_vote." + "p-late-diffusion" : Float ; "Probability than a RB producer hasn't validated the previous EB." + "adversary-fraction" : Float ; "Fraction of stake that is adversarial: the adversary never produces RBs or EBs and never votes." + "tolerance" : Float ; "Discard states with less than this probability." + "rb-count" : Nat ; "Number of potential RBs to simulate." + "output-file" : String ; "Path to the JSON output file for the EB distribution." + EXTENSIONS: + defaultValues! #[ + ("active-slot-coefficient", "0.05") + , ("l-header" , "1" ) + , ("l-vote" , "4" ) + , ("l-diff" , "7" ) + , ("committee-size" , "600" ) + , ("quorum-fraction" , "0.75") + , ("p-rb-header-arrives" , "0.95") + , ("p-eb-validates" , "0.90") + , ("p-late-diffusion" , "0.05") + , ("adversary-fraction" , "0" ) + , ("tolerance" , "1e-8") + , ("rb-count" , "100" ) + ] +] + +def main (args : List String) : IO UInt32 := + markov.validate args diff --git a/analysis/markov/ReadMe.md b/analysis/markov/ReadMe.md new file mode 100644 index 000000000..c7c26dd88 --- /dev/null +++ b/analysis/markov/ReadMe.md @@ -0,0 +1,231 @@ +# Markovian simulation of Linear Leios + +This Markovian simulation of Linear Leios computes the probability of EB certifications as RBs are produced. + + +## Contents + +- [Model](#model) +- [Parameters](#parameters) +- [Example](#example) +- [Usage](#usage) +- [Building](#building) + + +## Model + +The protocol state is represented by three quantities. + +- The number of RBs that have been produced. +- The number of EBs that have been produced. +- Whether an honest RB was produced. +- Whether a certificate is ready for inclusion in the next RB. + +Time is tracked in terms of block-forging opportunties instead of in terms of slots. + +Transitions occur in several substeps: + +1. *Forge RB:* create a new RB. +2. *Certify:* include a certificate in the RB. +3. *Forge EB:* create a new EB. +4. *Vote:* cast votes to reach a quorum. + + +### Substep 1: Forge RB + +The adversarial model assumes that adversaries obstain from producing RBs, EBs, and votes. Let $f_\text{adv}$ be the fraction of stake held by the adversary. Two transitions are possible: + +- *Forge a new RB:* probability $1 - f_\text{adv}$. +- *Abstain from forging a new RB:* probability $f_\text{adv}$. + + +### Substep 2: Certify + +Provided that a quorum of votes have endorsed the EB, the following conditions are required for certifying it in the RB that was just forged. + +- *RB spacing:* The previous RB must have been forged at least $3 L_\text{hdr} + L_\text{vote} + L_\text{diff}$ slots previously. + - The distribution of gaps between RBs follows the negative-binomial distribution. +- *Quorum:* The voting yielded a quorum. +- *Not an adversary:* There is no RB if an adversary is the designated block producer. + + +### Substep 3: Forge EB + +Provided that an honest RB exists, an EB can be forged if the node has received the previous EB and computed the ledger state. + +- Because of their membership in the previous vote, a fraction $n_\text{comm} / n_\text{pools}$ of the pools have already updated their ledger state. +- Of the pools not having voted on the block we define $p_\text{late}$ as the probability that the EB has arrived too late to compute the ledger state needed to produce the next EB. + + +### Substep 4: Vote + +Obtaining a successful quorum of votes is distributed according to bernoulli trials where the expected number of successes is the mean committee size and the success probabilities of individual pools accord with the stake distribution. Those success probabilities are modified in several ways: + +- *Adversaries do not vote:* probability $f_\text{adv}$. +- *RB header arrives within* $L_\text{hdr}$ *slots:* probability $p_\text{rb}$. +- *EB is fully validated within* $3 L_\text{hdr} + L_\text{vote}$ *slots*: probability $p_\text{eb}$. + + +## Parameters + +| Symbol | Flag | Default | Description | +|------------------|-------------------------|--------:|------------------------------------------------------------------------------------------------------| +| $L_\text{hdr}$ | `--l-header` | 1 | Constraint on header diffusion time. | +| $L_\text{vote}$ | `--l-vote` | 4 | Constraint on voting time. | +| $L_\text{diff}$ | `--l-diff` | 7 | Constraint on diffusion time. | +| $n_\text{comm}$ | | 2500 | Number of stakepools (constant). | +| $n_\text{pools}$ | `--committee-size` | 600 | Number of members on the voting committee. | +| $\tau$ | `--quorum-fraction` | 0.75 | Stake-weighted fraction of committee's votes required to produce a certificate. | +| $p_\text{rb}$ | `--p-rb-header-arrives` | 0.95 | Probability that the RB header arrives at a node before $L_\text{hdr}$ seconds. | +| $p_\text{eb}$ | `--p-eb-validates` | 0.90 | Probability that the EB is fully validated by a node before $3 L_\text{hdr} + L_\text{vote}$. | +| $p_\text{late}$ | `--p-late-diffusion` | 0.05 | Probability that an RB producer hasn't yet validated the EB by the time they need to forge their RB. | +| $f_\text{adv}$ | `--adversary-fraction` | 0.00 | Fraction of stake held by adversaries. | + + +## Example + +The `linleios` program executes the Markov model for EB production in Linear Leios. The protocol parameters and network characteristic are specified as flags on the command line. The program outputs the following information: + +- The efficiencies, on `/dev/stdout`. + - RB efficiency: the fraction of possible RBs that were actually produced. + - EB efficiency: the fraction of possible EBs that were actually produced. + - Efficiency: the fraction o possible payload bytes that were actual produced. +- The "missing probability" resulting from the finite-resolution arithmetic of the computations, on `/dev/stderr`. +- Optionally, a JSON file containing the probabilities of the given number of certified EBs. + +```bash +lake exe linleios \ + --l-header 1 \ + --l-vote 4 \ + --l-diff 5 \ + --committee-size 600 \ + --quorum-fraction 0.80 \ + --p-rb-header-arrives 0.95 \ + --p-eb-validates 0.95 \ + --p-late-diffusion 0.05 \ + --rb-count 100 \ + --adversary-fraction 0.1 \ + --output-file tmp.json +``` + +```console +RB efficiency: 0.899974 +EB efficiency: 0.313049 +Overall efficiency: 0.352469 +Missing probability: 0.000030 +``` + +```bash +jq 'to_entries | sort_by(.key | tonumber) | from_entries' tmp.json +``` + +```console +{ + "10": 0, + "11": 0.000003, + "12": 0.00001, + "13": 0.000031, + "14": 0.000081, + "15": 0.000196, + "16": 0.00044, + "17": 0.000919, + "18": 0.001799, + "19": 0.003308, + "20": 0.005731, + "21": 0.009381, + "22": 0.014533, + "23": 0.021353, + "24": 0.029805, + "25": 0.039585, + "26": 0.050095, + "27": 0.060484, + "28": 0.069757, + "29": 0.07693, + "30": 0.081208, + "31": 0.082129, + "32": 0.079641, + "33": 0.074106, + "34": 0.066214, + "35": 0.056847, + "36": 0.04692, + "37": 0.037253, + "38": 0.028464, + "39": 0.020939, + "40": 0.014837, + "41": 0.010129, + "42": 0.006664, + "43": 0.004227, + "44": 0.002586, + "45": 0.001525, + "46": 0.000868, + "47": 0.000476, + "48": 0.000252, + "49": 0.000128, + "50": 0.000063, + "51": 0.00003, + "52": 0.000013, + "53": 0.000005, + "54": 0.000002, + "55": 0.000001, + "56": 0 +} +``` + +![Example results](example-results.png) + + +## Usage + +```console +$ lake exe linleios --help + +markov [0.0.1] +Run a Markov simulation of Linear Leios. + +USAGE: + markov [FLAGS] + + -h, --help Prints this message. + --version Prints the version. + --active-slot-coefficient : Float The active slot coefficient for RBs, in + probability per slot. [Default: `0.05`] + --l-header : Nat L_header protocol parameter, in slots. + [Default: `1`] + --l-vote : Nat L_vote protocol parameter, in slots. + [Default: `4`] + --l-diff : Nat L_diff protocol parameter, in slots. + [Default: `7`] + --committee-size : Nat Expected number of voters in the + committee, out of 2500 stakepools total. + [Default: `600`] + --quorum-fraction : Float τ protocol parameter, in %/100. [Default: + `0.75`] + --p-rb-header-arrives : Float Probability that the RB header arrives + before L_header. [Default: `0.95`] + --p-eb-validates : Float Probability that the EB is fully + validated before 3 L_header + L_vote. + [Default: `0.90`] + --p-late-diffusion : Float Probability than a RB producer hasn't + validated the previous EB. [Default: + `0.05`] + --adversary-fraction : Float Fraction of stake that is adversarial: + the adversary never produces RBs or EBs + and never votes. [Default: `0`] + --tolerance : Float Discard states with less than this + probability. [Default: `1e-8`] + --rb-count : Nat Number of potential RBs to simulate. + [Default: `100`] + --output-file : String Path to the JSON output file for the EB + distribution. +``` + + +## Building + +```console +$ nix-shell -p lean4 elan + +$ lake build +``` + +The executable program will reside at `.lake/build/bin/linleios`. diff --git a/analysis/markov/example-results.png b/analysis/markov/example-results.png new file mode 100644 index 000000000..9efe11f05 Binary files /dev/null and b/analysis/markov/example-results.png differ diff --git a/analysis/markov/lake-manifest.json b/analysis/markov/lake-manifest.json new file mode 100644 index 000000000..e8e8006b8 --- /dev/null +++ b/analysis/markov/lake-manifest.json @@ -0,0 +1,115 @@ +{"version": "1.1.0", + "packagesDir": ".lake/packages", + "packages": + [{"url": "https://github.com/mhuisi/lean4-cli", + "type": "git", + "subDir": null, + "scope": "", + "rev": "f9e25dcbed001489c53bceeb1f1d50bbaf7451d4", + "name": "Cli", + "manifestFile": "lake-manifest.json", + "inputRev": "v4.20.0", + "inherited": false, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/fgdorais/lean4-parser", + "type": "git", + "subDir": null, + "scope": "", + "rev": "26d5ce4d60195a869b1fdb100b442794ea63e1ad", + "name": "Parser", + "manifestFile": "lake-manifest.json", + "inputRev": "26d5ce4d60195a869b1fdb100b442794ea63e1ad", + "inherited": false, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/mathlib4", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "c211948581bde9846a99e32d97a03f0d5307c31e", + "name": "mathlib", + "manifestFile": "lake-manifest.json", + "inputRev": "v4.20.0", + "inherited": false, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/fgdorais/lean4-unicode-basic", + "type": "git", + "subDir": null, + "scope": "", + "rev": "45c426d1cb016fcb4fcbe043f1cd2d97acb2dbc3", + "name": "UnicodeBasic", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover-community/batteries", + "type": "git", + "subDir": null, + "scope": "", + "rev": "7a0d63fbf8fd350e891868a06d9927efa545ac1e", + "name": "batteries", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/plausible", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "2ac43674e92a695e96caac19f4002b25434636da", + "name": "plausible", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/LeanSearchClient", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "6c62474116f525d2814f0157bb468bf3a4f9f120", + "name": "LeanSearchClient", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/import-graph", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "a11bcb5238149ae5d8a0aa5e2f8eddf8a3a9b27d", + "name": "importGraph", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/ProofWidgets4", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "21e6a0522cd2ae6cf88e9da99a1dd010408ab306", + "name": "proofwidgets", + "manifestFile": "lake-manifest.json", + "inputRev": "v0.0.60", + "inherited": true, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover-community/aesop", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "ddfca7829bf8aa4083cdf9633935dddbb28b7b2a", + "name": "aesop", + "manifestFile": "lake-manifest.json", + "inputRev": "master", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/quote4", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "2865ea099ab1dd8d6fc93381d77a4ac87a85527a", + "name": "Qq", + "manifestFile": "lake-manifest.json", + "inputRev": "master", + "inherited": true, + "configFile": "lakefile.toml"}], + "name": "linleios", + "lakeDir": ".lake"} diff --git a/analysis/markov/lakefile.toml b/analysis/markov/lakefile.toml new file mode 100644 index 000000000..b2a3c08ff --- /dev/null +++ b/analysis/markov/lakefile.toml @@ -0,0 +1,36 @@ +name = "linleios" +version = "0.1.0" +keywords = ["math"] +defaultTargets = ["linleios"] + +[[lean_lib]] +name = "Linleios" + +[[lean_exe]] +name = "linleios" +root = "Main" + +[leanOptions] +pp.unicode.fun = true # pretty-prints `fun a ↦ b` +autoImplicit = false + +[[require]] +name = "mathlib" +scope = "leanprover-community" +version = "git#v4.20.0" + +[[require]] +name = "Parser" +git = "https://github.com/fgdorais/lean4-parser" +rev = "26d5ce4d60195a869b1fdb100b442794ea63e1ad" + +[[require]] +name = "Cli" +git = "https://github.com/mhuisi/lean4-cli" +rev = "v4.20.0" + +[lean] +server-options = [ + ["checkBinderAnnotations", "false"], + ["diagnostics", "true"] +] diff --git a/analysis/markov/lean-toolchain b/analysis/markov/lean-toolchain new file mode 100644 index 000000000..52fe77473 --- /dev/null +++ b/analysis/markov/lean-toolchain @@ -0,0 +1 @@ +leanprover/lean4:v4.20.0 diff --git a/analysis/sims/kernels.nix b/analysis/sims/kernels.nix index 5846a1e15..0fe971a14 100644 --- a/analysis/sims/kernels.nix +++ b/analysis/sims/kernels.nix @@ -33,6 +33,7 @@ in igraph lubridate mongolite + poibin quantreg RPostgres R_utils