intersectmbo / formal-ledger-specifications Goto Github PK

I can't get any of the build instructions to work. For example, nix-build -A ledger.docs gives (after a long time)

         Checking Interface.MonadReader.Instance (/build/src/Interface/MonadReader/Instance.agda).
         Checking Interface.MonadTC.Instance (/build/src/Interface/MonadTC/Instance.agda).
       Checking Tactic.Defaults (/build/src/Tactic/Defaults.agda).
/build/src/Axiom/Set/Rel.agda:78,22-31
<stdout>: commitBuffer: invalid argument (invalid character)

This looks like a locale issue, but adjusting locale variables in my shell doesn't help: I think it's probably something that needs to be fixed in the nix setup. I've tried this on three different computers and the same thing happens on each. I use nix in a number of other IOG repositories every day with no problems, so this issue seems to be specific to this repository.

It would be great to support pattern matching in the conclusion of a rule, to avoid having to write a bunch of let's and explicit binders at the beginning of a rule.

The current MA implementation is still missing a few things, in particular:

• One or more implementations of the Value type (Fig. 3)
• Adjusting scriptsNeeded to include the PolicyIDs of mint (Fig. 8)
• Preservation of value for token algebras (Lemma 8.1)
• Maybe more?

There are many places where we currently have to pass arguments manually that feel like they should be inferrable automatically. The purpose of this issue is to weed these out as much as possible. We should collect the functions that are likely to have this behavior, organize them into similar groups and document the issues that break inference. We can then make a plan to fix those issues.

• List functions with broken inference
• Group them into similar types
• Document why/how they are broken
• Fix as many as possible

We want the ability to donate money to the treasury. After some discussions, the easiest option seems to be to add a new field to the transaction body that contains the size of the donation & include that field in the transaction balancing equation. If we expose that field to plutus we can also do some extra logic with it, for example having some epoch where the unspent funds can only be moved back into the treasury.

We should automate the Nix build, probably using Hydra.

There are some questions remaining about the modeling of the axiomatic set theory:

1. Can we make things level-polymorphic (probably) and if so, is there a good way of allowing the model given by Set A = A → Type? The issue here is that Set is of type Type a → Type (max a 1), so only if a ≠ 0 it preserves the type. Allowing this would break some other stuff, for example the unions axiom.

2. The current SpecProperty situation is a bit messy. It might be worth replacing this by a simple sum type, where we allow either all properties or all decidable properties in the specification axiom. This would technically be less general, but I'm not aware of any situation where it wouldn't be one of those two. This would probably simplify things, but it might also not, we just have to try it.

3. Do we need a dependent version of the replacement axiom? This has come up twice now, and may be useful.

1. The tactics such as ∈⇔P are pretty nice, but there is of course the issue that we have to copy&paste it everywhere. Maybe there's some solution that doesn't require a major Agda patch.

2. Conversions between different types of sets with extra structure are a big source of clutter. #23 is related to this, but there's also an inverse problem of how to add structure to sets. Type classes might be a solution, but it would be nice to find something that doesn't pollute every definition. Related to this is that inference sometimes breaks because of this (since when we prove a theorem about things that are projected out from something, there's no information to unify it back from, even if it's obvious what it should be).

This repo has been marked as core tech and is part of initiative of repo preparation, part of this includes adding needed missing documentation.
This repo in particular needs:

• Include an informative README
• Include a High Level 2 Sentence Description for purpose of Repo
• Explain how to make a contribution (Contributing MD)
• Include the Standard Code of Conduct
• Use the Apache 2.0 License or agreed alternative
• Identify the Core Maintainers

There is a bunch of complexity coming from implementation details of the set theory leaking elsewhere. Usually set theory is axiomatic, so we can probably state the axioms that we need and have a cleaner interface.

Some people have observed a GHC panic when compiling the generated cabal package. This seems to be somewhat independent of the platform: There are linux and (arm) mac machines where the build works, and others where it fails.

On arm macs, it seems like this issue is caused by using x86 versions of nixpkgs, and putting import <nixpkgs> { system = "aarch64-darwin"; } in the first line of default.nix and shell.nix respectively solved this problem in these cases. I don't know why the x86 GHC fails but the arm one doesn't, especially since we use x86 Agda (since the arm version doesn't compile for some reason). And of course this doesn't solve the problem on linux, so there's still some debugging required.

We have many properties for which we need decidability. It would make sense to look into deriving that automatically.

As @Soupstraw pointed out, it's sometimes confusing to read something like proj₁, since it's not always clear if we're projecting out from something we think of as a pair, or if we're projecting away a proof. Related to this is the issue that we sometimes have records that have a 'principal' field, like the Carrier field in many algebraic structures for example. It would be nice to have a consistent way of projecting away less relevant parts of a record, for example with the following typeclass:

record HasDowncast {a b} (A : Set a) (B : Set b) : Set (a ⊔ b) where
  field _↓ : A → B

The current computation strategy is incompatible with nested rules. To fix this, instead of having clauses return a boolean, we can have them return a Maybe X, and do a monadic computation.

Babbage specification requires collInputs tx ̸= ∅ in feesOK. While in case when fee (and consequently collateral amount) is zero collInputs may be empty.

We need that case while working with Hydra. Collaterals seems to be the only reason to commit ADA onto L2 for us.

Details of our case are in this issue: mlabs-haskell/hydra-auction#193

Instead of electing the entire CC at once, we want to be able to hold elections that modify the CC in some ways. Specifically, we should be able to

• remove a set of cold keys,
• add a set of cold keys (each with a term length) and
• set a new threshold

in one election. Additionally, a cold key should be able to resign by publishing a ccRegHot certificate that contains nothing as a hot key. Resignation should have the same semantics as expiration of the term, which is that those should still count towards the size of the committee for voting, but not towards the size for minCCSize. I.e. if there are less active keys than minCCSize we go straight to 'no confidence'.

We pay deposits of proposed actions back to a reward address, and we should add the distribution of these stakes into the per-credential stake distribution before we aggregate it into the DRep stake distribution. This is to not disincentivise proposers.

We currently just put the literate (LaTeX) Agda in the HTML output, which produces a bunch of garbage. It would be nice to have good-looking HTML output as well, but I don't know what a good approach for this would be without a bunch of duplication.

We already have all the features in the transaction body, but we should split the governance into two fields, one for proposals and one for voting. The reasoning behind this is that while the ordering of those two are relevant, the ordering of mixed things has no semantic significance.

This is the companion issue to IntersectMBO/cardano-ledger#3145

We have two Prelude modules, Prelude and Ledger.Prelude. The former publicly re-exports general purpose definitions and the latter is the same but includes definitions used in Ledger.X modules.

The purpose of this issue is to discuss whether they should be renamed and to what.

The derivation strategy is currently quite slow. In particular, I've noticed that printing contexts at the start of a computation is pretty much instant, while it sometimes takes multiple seconds to print a single line deep into it.

We need two pre-defined DReps, who always count as having voted on every action:

• Abstain: abstains on every action
• No Confidence: counts as No on every action except No Confidence, where it counts as Yes

• We need to check for enactment in the order of proposal
• Enacting NoConfidence removes all proposed actions (Note: I still prefer delay, as other actions below)
• Enacting NewCommittee, NewConstitution and TriggerHF delays all other ratification
• Enacting always is delayed by 1 epoch
• We need to properly check the hashes on ratification

The interface that's currently provided is only a proof of concept, and is pretty bad in practice. We should have proper data types and a good general story for the interface.

This issue is for modifications that improve the overall presentation and design of the library.

Examples

• make coding style more consistent by conforming to a standard; e.g., the agda standard library style guide (permalink)
• make sure indentations are preserved by the Agda generated tex files and pdf documents; this requires adding an extra space before the column where successive lines should line up.

This is the companion to IntersectMBO/cardano-ledger#3147

This is the companion to IntersectMBO/cardano-ledger#3160

This is the companion to IntersectMBO/cardano-ledger#3145

For the UTXOS rule, we need to have some Plutus primitives. To use deriveComp on UTXOS we also need to resolve #3.

During bootstrap, DReps don't vote & the CC has some special emergency powers. Bootstrap will end when the term of the bootstrap CC runs out.

It would be nice to have a quick way of rebuilding the latex documents, which should probably be done with a makefile. I've played around with this a bit, but I couldn't really get it to work nicely. My WIP is here: https://github.com/input-output-hk/formal-ledger-specifications/blob/6bac4acad996159a271ea5f72a047f6f1dbd650d/Makefile

There are many properties that are currently part of the rules, which don't really fit into any particular rule thematically, and don't depend on anything but the signal. We could call these 'well-formedness properties', and bundle all of them into one place for them to be checked. This should improve consistency and readability of the STS rules.

Here are some:

• Addresses
  • Byron: bootstrapAddrsSize <= 64
  • Maybe networkID = NetworkID, though this needs access to global constants
• Transactions
  • txADhash ≡ map hash txAD
  • Maybe txins ≢ ∅
  • Maybe coin mint ≡ 0
• PParams has paramsWellFormed
• More for blocks (once we have those), maybe others

Implicit arguments can't currently be inferred from extensional set equality arguments. I.e., if we pass an argument of type s ≡ᵉ s' to a function, we still have to pass s and s' explicitly, which is pretty annoying. One way to fix this is by redefining _≡ᵉ_ as a data type, but this means that a bunch of things have to be rewritten. Maybe there is some better solution.

Tactics that call themselves recursively usually rely on some fuel value. Currently, all of this is quite ad-hoc and difficult to use. In particular there are two problems:

• there is no general mechanism to interact with fuel and we have some hard coded values
• we should raise good error messages that make it clear that we run out of fuel

For multi assets, we should implement token algebras as per the shelley MA spec.

We need to deal with branching. We should be able to turn a proof that only at most one constructor applies into an instance of Computational. This means that we'd have to do some proofs by hand, but they should be very easy in practice.

This is the companion to IntersectMBO/cardano-ledger#3149.

• #413
• #414
• #415
• #412
• #417

We want to use set comprehension to write sets and maps. There are some difficulties:

• The syntax keyword isn't powerful enough, but we could for example have a notation that has inverted binders
• Pattern matching is difficult to implement
• Constructing sets & maps also needs proofs that we can hopefully sometimes generate automatically

We have a bunch of structures with lots of name clashes that would likely benefit a lot from being turned into type classes. Here are some:

• Addition
• Subtraction
• Multiplication
• All the inequalities
• Decidable inequalities

The current plan for incentives is to simply disallow withdrawals for stake credentials (or maybe just keys?) that don't delegate to a DRep. Even pre-defined or non-existent DReps count for removing this restriction.

There are some things that would be nice to eventually have in CI:

• cached builds (should make running CI significantly faster)
• mac builds
• automatic hosting of the PDFs and HTML somewhere
• maybe split the actions into multiple parts (eg. Agda, Ledger, Midnight?)
• build the Haskell package (agda-ledger-executable-spec) and add it to a branch

We have different kinds of rules. Some are to do with the operation of the system (state transitions), others express properties/invariants. We could distinguish these (eg using colors). We should then also have high level consistency rules (is the system well formed, do transitions within an epoch terminate, are the rules confluent, etc), as well as the rules governing resource properties (rewards calculation, timing constraints etc). The latter will be extracted to provide your verifiable resource analysis (and can be embedded as a calculus within the executable spec).

Currently, the actual model lives entirely in Ledger.lagda, which has become a pretty large file. This should be split up into modules for certain topics.

A zipped transaction is one where all the pointers to information have been properly resolved. Currently it's not possible to zip a transaction without any extra information.

We've been considering adding such information (and maybe using the zipped transaction in the ledger rules) for a long time, but we've never gotten around to implementing it. We should investigate how to do this.

Instances for deciding various properties are scattered all over the files that contain proofs. We should find a good way of dealing with decidability consistently.

Vertical vectors make the PDF way more readable. The issue here is that the LaTeX environment for rendering Agda isn't compatible with that, at least what I tried didn't work.

If we have some way of fixing/working around this issue, the easiest way would be to wrap some marker around the tuples, and then run some preprocessing script, but maybe there are better solutions.

There are two steps:

• Produce a single working example by editing the LaTeX manually.
• Write some automation that we can hook into the build process.

Integration into CI isn't part of this issue, I can take care of that.

Make sure that the deposit for submitting a proposal is checked against the required amount in PParams.

This is the companion to IntersectMBO/cardano-ledger#3148

DReps should expire if they didn't vote for a sufficient amount of time. Here's the current design:

Every time a DRep votes, we remember the number currentEpoch + drepActivity. Then, when ratifying, we only count DReps in the denominator whose epoch we remembered is lower than the current epoch.

There are two optional additions to the design that we could consider:

• allow to publish a regdrep cert with no deposit to refresh the number without voting
• increment the number for every epoch that had no governance actions to vote on

• Missing: drepActivity, minCCSize
• Group the PParams & updates into their groups as mentioned in CIP-1694

This is the companion issue to IntersectMBO/cardano-ledger#3146