Adding the Agda changes and CIP edits

CIP/Readme.md

@@ -1166,6 +1166,54 @@ The current **maximum block header size** in Cardano is **1100 bytes**, although
 
 This would **exceed the 1500-bytes limit**, risking fragmentation and violating guidance from the Cardano networking team. We could safely decrease the group element size by decreasing the security parameters if we were to generate new class groups at each epoch. Doing so would however render the protocol more complex and potentially weaken the security of the protocol as we may have more chances to generate a weak class group.
 
+**Protocol Parameter Update Changes**. The Phalanx update also requires the addition of two new protocol parameters,
+`phalanx_security_parameter` and `phalanx_i_parameter`, as follows:
+
+```
+phalanx_security_parameter = uint .size 4
+phalanx_i_parameter = uint .size 4
+protocol_param_update =
+  { ? 0  : coin                   ; minfeeA
+    ...
+  , ? 33 : nonnegative_interval   ; minfee refscriptcoinsperbyte
+  , ? 34 : phalanx_security_parameter
+  , ? 35 : phalanx_i_parameter
+  }
+```
+
+### 7. Formal specification in Agda
+
+We also provide an update to the [Agda formal specfication](https://github.com/IntersectMBO/ouroboros-consensus/tree/polina/anti-grinding)
+of the (on-chain component of the) consensus protocol that implements the anti-grinding measures. The following modules  
+contain the majority of the relevant changes, which we summarize here :
+
+- `Spec.VDF` : Defines a type representing VDF functionality, which is not instantiated with actual VDFs
+
+- `Spec.OutsVec` : Contains functionality for manipulating vectors of VDF outputs
+
+- `Spec.UpdateNonce` : Specifies a new transition type `UPDNONESTREAM`, which corresponds to a single stream in the Phalanx State Transition Diagram. Also, the `UPDN` transition is updated to represent the rules of three nonce streams being updated simultaneously :
+  (1) `pre-η-candidate` which is the VRF output of the previous epoch, and is being stabilized for several intervals,
+
+  (2) `ηstate` which is the state of the Phalanx state machine, using the VDF procedure to evolve the nonce, and
+
+  (3) `next-η` which is the output of the state machine once it has finished a complete VDF round, and it will become the real current epoch nonce in several intervals.
+
+- `InterfaceLibrary.Ledger` : Updated to include a `LedgerInterface` API call `getPhalanxCommand  : BlockBody -> UpdateNonceCommand`
+which returns the command (either nothing or a pair of group elements) to the Phalanx state machine
+
+- `Spec.TickNonce` : Just some renaming here
+
+- `Ledger.PParams` : Updated to support a new parameter group *Phalanx Security Group*, which contains the two parameters
+required to parametrize Phalanx, `phalanxSecurityParam` and `phalanxSecurityParam`, which will be adopted by the Phalanx
+protocol when entering the Initialized state
+
+- `Spec.Protocol` : Updated to call `UPDN` rule with the appropriate parameters. This
+includes the stake
+distribution from the correct epoch (which is one epoch before than the one used in Praos),
+the relevant values from the nonce streams, and the correct Phalanx parameters.
+
+- `Spec.ChainHead` : Updated to call the `PRTCL` and `TICKN` rules with the appropriate signal, state, and environment.
+
 ## Rationale: How does this CIP achieve its goals?
 
 ### 1. How Phalanx Addresses CPS-21 - Ouroboros Randomness Manipulation?

agda-spec/.gitignore

@@ -0,0 +1,12 @@
+*.agdai
+.DS_Store
+**/dist-newstyle/
+.editorconfig
+result*
+
+*.pdf
+src/latex/
+
+dist/
+
+*.time

agda-spec/Makefile

@@ -0,0 +1,2 @@
+%:
+	$(MAKE) -C src/ $@

agda-spec/nix/sources.json

@@ -0,0 +1,27 @@
+{
+    "agda-nixpkgs": {
+        "branch": "nixpkgs-unstable",
+        "description": "Nix Packages collection",
+        "homepage": "",
+        "owner": "NixOS",
+        "repo": "nixpkgs",
+        "rev": "7148a46c2a1163faecb2915f5f1e6e6c43bcd3ee",
+        "sha256": "1aygdbj86xiyalgy21xk4gzgvjphhm7dr0ni1j4n32rmziwr4r97",
+        "type": "tarball",
+        "url": "https://github.com/NixOS/nixpkgs/archive/7148a46c2a1163faecb2915f5f1e6e6c43bcd3ee.tar.gz",
+        "url_template": "https://github.com/<owner>/<repo>/archive/<rev>.tar.gz"
+    },
+    "nixpkgs": {
+        "branch": "release-21.05",
+        "description": "Nix Packages collection",
+        "homepage": "",
+        "owner": "NixOS",
+        "repo": "nixpkgs",
+        "rev": "7148a46c2a1163faecb2915f5f1e6e6c43bcd3ee",
+        "sha256": "1aygdbj86xiyalgy21xk4gzgvjphhm7dr0ni1j4n32rmziwr4r97",
+        "type": "tarball",
+        "url": "https://github.com/NixOS/nixpkgs/archive/7148a46c2a1163faecb2915f5f1e6e6c43bcd3ee.tar.gz",
+        "url_template": "https://github.com/<owner>/<repo>/archive/<rev>.tar.gz",
+        "version": "21.11.337905.902d91def1e"
+    }
+}

agda-spec/nix/sources.nix

@@ -0,0 +1,198 @@
+# This file has been generated by Niv.
+
+let
+
+  #
+  # The fetchers. fetch_<type> fetches specs of type <type>.
+  #
+
+  fetch_file = pkgs: name: spec:
+    let
+      name' = sanitizeName name + "-src";
+    in
+    if spec.builtin or true then
+      builtins_fetchurl { inherit (spec) url sha256; name = name'; }
+    else
+      pkgs.fetchurl { inherit (spec) url sha256; name = name'; };
+
+  fetch_tarball = pkgs: name: spec:
+    let
+      name' = sanitizeName name + "-src";
+    in
+    if spec.builtin or true then
+      builtins_fetchTarball { name = name'; inherit (spec) url sha256; }
+    else
+      pkgs.fetchzip { name = name'; inherit (spec) url sha256; };
+
+  fetch_git = name: spec:
+    let
+      ref =
+        spec.ref or (
+          if spec ? branch then "refs/heads/${spec.branch}" else
+          if spec ? tag then "refs/tags/${spec.tag}" else
+          abort "In git source '${name}': Please specify `ref`, `tag` or `branch`!"
+        );
+      submodules = spec.submodules or false;
+      submoduleArg =
+        let
+          nixSupportsSubmodules = builtins.compareVersions builtins.nixVersion "2.4" >= 0;
+          emptyArgWithWarning =
+            if submodules
+            then
+              builtins.trace
+                (
+                  "The niv input \"${name}\" uses submodules "
+                  + "but your nix's (${builtins.nixVersion}) builtins.fetchGit "
+                  + "does not support them"
+                )
+                { }
+            else { };
+        in
+        if nixSupportsSubmodules
+        then { inherit submodules; }
+        else emptyArgWithWarning;
+    in
+    builtins.fetchGit
+      ({ url = spec.repo; inherit (spec) rev; inherit ref; } // submoduleArg);
+
+  fetch_local = spec: spec.path;
+
+  fetch_builtin-tarball = name: throw
+    ''[${name}] The niv type "builtin-tarball" is deprecated. You should instead use `builtin = true`.
+        $ niv modify ${name} -a type=tarball -a builtin=true'';
+
+  fetch_builtin-url = name: throw
+    ''[${name}] The niv type "builtin-url" will soon be deprecated. You should instead use `builtin = true`.
+        $ niv modify ${name} -a type=file -a builtin=true'';
+
+  #
+  # Various helpers
+  #
+
+  # https://github.com/NixOS/nixpkgs/pull/83241/files#diff-c6f540a4f3bfa4b0e8b6bafd4cd54e8bR695
+  sanitizeName = name:
+    (
+      concatMapStrings (s: if builtins.isList s then "-" else s)
+        (
+          builtins.split "[^[:alnum:]+._?=-]+"
+            ((x: builtins.elemAt (builtins.match "\\.*(.*)" x) 0) name)
+        )
+    );
+
+  # The set of packages used when specs are fetched using non-builtins.
+  mkPkgs = sources: system:
+    let
+      sourcesNixpkgs =
+        import (builtins_fetchTarball { inherit (sources.nixpkgs) url sha256; }) { inherit system; };
+      hasNixpkgsPath = builtins.any (x: x.prefix == "nixpkgs") builtins.nixPath;
+      hasThisAsNixpkgsPath = <nixpkgs> == ./.;
+    in
+    if builtins.hasAttr "nixpkgs" sources
+    then sourcesNixpkgs
+    else if hasNixpkgsPath && ! hasThisAsNixpkgsPath then
+      import <nixpkgs> { }
+    else
+      abort
+        ''
+          Please specify either <nixpkgs> (through -I or NIX_PATH=nixpkgs=...) or
+          add a package called "nixpkgs" to your sources.json.
+        '';
+
+  # The actual fetching function.
+  fetch = pkgs: name: spec:
+
+    if ! builtins.hasAttr "type" spec then
+      abort "ERROR: niv spec ${name} does not have a 'type' attribute"
+    else if spec.type == "file" then fetch_file pkgs name spec
+    else if spec.type == "tarball" then fetch_tarball pkgs name spec
+    else if spec.type == "git" then fetch_git name spec
+    else if spec.type == "local" then fetch_local spec
+    else if spec.type == "builtin-tarball" then fetch_builtin-tarball name
+    else if spec.type == "builtin-url" then fetch_builtin-url name
+    else
+      abort "ERROR: niv spec ${name} has unknown type ${builtins.toJSON spec.type}";
+
+  # If the environment variable NIV_OVERRIDE_${name} is set, then use
+  # the path directly as opposed to the fetched source.
+  replace = name: drv:
+    let
+      saneName = stringAsChars (c: if (builtins.match "[a-zA-Z0-9]" c) == null then "_" else c) name;
+      ersatz = builtins.getEnv "NIV_OVERRIDE_${saneName}";
+    in
+    if ersatz == "" then drv else
+      # this turns the string into an actual Nix path (for both absolute and
+      # relative paths)
+    if builtins.substring 0 1 ersatz == "/" then /. + ersatz else /. + builtins.getEnv "PWD" + "/${ersatz}";
+
+  # Ports of functions for older nix versions
+
+  # a Nix version of mapAttrs if the built-in doesn't exist
+  mapAttrs = builtins.mapAttrs or (
+    f: set: with builtins;
+    listToAttrs (map (attr: { name = attr; value = f attr set.${attr}; }) (attrNames set))
+  );
+
+  # https://github.com/NixOS/nixpkgs/blob/0258808f5744ca980b9a1f24fe0b1e6f0fecee9c/lib/lists.nix#L295
+  range = first: last: if first > last then [ ] else builtins.genList (n: first + n) (last - first + 1);
+
+  # https://github.com/NixOS/nixpkgs/blob/0258808f5744ca980b9a1f24fe0b1e6f0fecee9c/lib/strings.nix#L257
+  stringToCharacters = s: map (p: builtins.substring p 1 s) (range 0 (builtins.stringLength s - 1));
+
+  # https://github.com/NixOS/nixpkgs/blob/0258808f5744ca980b9a1f24fe0b1e6f0fecee9c/lib/strings.nix#L269
+  stringAsChars = f: s: concatStrings (map f (stringToCharacters s));
+  concatMapStrings = f: list: concatStrings (map f list);
+  concatStrings = builtins.concatStringsSep "";
+
+  # https://github.com/NixOS/nixpkgs/blob/8a9f58a375c401b96da862d969f66429def1d118/lib/attrsets.nix#L331
+  optionalAttrs = cond: as: if cond then as else { };
+
+  # fetchTarball version that is compatible between all the versions of Nix
+  builtins_fetchTarball = { url, name ? null, sha256 }@attrs:
+    let
+      inherit (builtins) lessThan nixVersion fetchTarball;
+    in
+    if lessThan nixVersion "1.12" then
+      fetchTarball ({ inherit url; } // (optionalAttrs (name != null) { inherit name; }))
+    else
+      fetchTarball attrs;
+
+  # fetchurl version that is compatible between all the versions of Nix
+  builtins_fetchurl = { url, name ? null, sha256 }@attrs:
+    let
+      inherit (builtins) lessThan nixVersion fetchurl;
+    in
+    if lessThan nixVersion "1.12" then
+      fetchurl ({ inherit url; } // (optionalAttrs (name != null) { inherit name; }))
+    else
+      fetchurl attrs;
+
+  # Create the final "sources" from the config
+  mkSources = config:
+    mapAttrs
+      (
+        name: spec:
+          if builtins.hasAttr "outPath" spec
+          then
+            abort
+              "The values in sources.json should not have an 'outPath' attribute"
+          else
+            spec // { outPath = replace name (fetch config.pkgs name spec); }
+      )
+      config.sources;
+
+  # The "config" used by the fetchers
+  mkConfig =
+    { sourcesFile ? if builtins.pathExists ./sources.json then ./sources.json else null
+    , sources ? if sourcesFile == null then { } else builtins.fromJSON (builtins.readFile sourcesFile)
+    , system ? builtins.currentSystem
+    , pkgs ? mkPkgs sources system
+    }: rec {
+      # The sources, i.e. the attribute set of spec name to spec
+      inherit sources;
+
+      # The "pkgs" (evaluated nixpkgs) to use for e.g. non-builtin fetchers
+      inherit pkgs;
+    };
+
+in
+mkSources (mkConfig { }) // { __functor = _: settings: mkSources (mkConfig settings); }

agda-spec/src/.gitignore

@@ -0,0 +1,3 @@
+*.lof
+!consensus-spec.bbl
+!rules.pdf