Renaming

.github/workflows/certora.yml

@@ -9,9 +9,9 @@ jobs:
     strategy:
       fail-fast: false
       matrix:
-        ngt:
-          - ngt
-          - mkr-ngt
+        sky:
+          - sky
+          - mkr-sky
 
     steps:
       - name: Checkout
@@ -37,7 +37,7 @@ jobs:
       - name: Install Certora
         run: pip3 install certora-cli
 
-      - name: Verify ${{ matrix.ngt }}
-        run: make certora-${{ matrix.ngt }}
+      - name: Verify ${{ matrix.sky }}
+        run: make certora-${{ matrix.sky }}
         env:
           CERTORAKEY: ${{ secrets.CERTORAKEY }}

Makefile

@@ -1,3 +1,3 @@
 PATH := ~/.solc-select/artifacts/solc-0.8.21:~/.solc-select/artifacts:$(PATH)
-certora-ngt     :; PATH=${PATH} certoraRun certora/Ngt.conf$(if $(rule), --rule $(rule),)
-certora-mkr-ngt :; PATH=${PATH} certoraRun certora/MkrNgt.conf$(if $(rule), --rule $(rule),)
+certora-sky     :; PATH=${PATH} certoraRun certora/Sky.conf$(if $(rule), --rule $(rule),)
+certora-mkr-sky :; PATH=${PATH} certoraRun certora/MkrSky.conf$(if $(rule), --rule $(rule),)

README.md

@@ -1,19 +1,19 @@
-# NGT Token and contract associated
+# SKY Token and contract associated
 
 This repository includes 2 smart contracts:
 
-- NGT token
-- MkrNgt Converter
+- SKY token
+- MkrSky Converter
 
-### NGT token
+### SKY token
 
 This is a standard erc20 implementation with regular `permit` functionality + EIP-1271 smart contract signature validation.
-In principle `PauseProxy` and `MkrNgt` would be the only two contracts set as `wards(address)`.
+In principle `PauseProxy` and `MkrSky` would be the only two contracts set as `wards(address)`.
 
-### MkrNgt
+### MkrSky
 
-It is a converter between `Mkr` and `Ngt` (both ways). Using the `mint` and `burn` capabilities of both tokens it is possible to exchange one to the other. The exchange rate is 1:`rate` (value defined as `immutable`).
+It is a converter between `Mkr` and `Sky` (both ways). Using the `mint` and `burn` capabilities of both tokens it is possible to exchange one to the other. The exchange rate is 1:`rate` (value defined as `immutable`).
 
 **Note:** if one of the tokens removes `mint` capabilities to this contract, it means that the path which gives that token to the user won't be available.
 
-**Note 2:** In the MKR -> NGT conversion, if the user passes a `wad` amount not multiple of `rate`, it causes that a dusty value will be lost. 
+**Note 2:** In the MKR -> SKY conversion, if the user passes a `wad` amount not multiple of `rate`, it causes that a dusty value will be lost.

certora/MkrMock.sol

@@ -1,7 +1,7 @@
 pragma solidity ^0.8.21;
 
-import "../src/Ngt.sol";
+import "../src/Sky.sol";
 
-contract MkrMock is Ngt {
+contract MkrMock is Sky {
 
 }

certora/MkrNgt.conf → certora/MkrSky.conf

@@ -1,21 +1,21 @@
 {
     "files": [
-        "src/MkrNgt.sol",
-        "src/Ngt.sol",
+        "src/MkrSky.sol",
+        "src/Sky.sol",
         "certora/MkrMock.sol"
     ],
     "link": [
-        "MkrNgt:ngt=Ngt",
-        "MkrNgt:mkr=MkrMock"
+        "MkrSky:sky=Sky",
+        "MkrSky:mkr=MkrMock"
     ],
     "rule_sanity": "basic",
     "solc": "solc-0.8.21",
     "solc_optimize_map": {
-        "MkrNgt": "200",
-        "Ngt": "200",
+        "MkrSky": "200",
+        "Sky": "200",
         "MkrMock": "0"
     },
-    "verify": "MkrNgt:certora/MkrNgt.spec",
+    "verify": "MkrSky:certora/MkrSky.spec",
     "prover_args": [
         "-mediumTimeout 180"
     ],

certora/MkrNgt.spec → certora/MkrSky.spec

@@ -1,29 +1,29 @@
-// MkrNgt.spec
+// MkrSky.spec
 
-using Ngt as ngt;
+using Sky as sky;
 using MkrMock as mkr;
 
 methods {
     function rate() external returns (uint256) envfree;
-    function ngt.wards(address) external returns (uint256) envfree;
-    function ngt.totalSupply() external returns (uint256) envfree;
-    function ngt.balanceOf(address) external returns (uint256) envfree;
-    function ngt.allowance(address, address) external returns (uint256) envfree;
+    function sky.wards(address) external returns (uint256) envfree;
+    function sky.totalSupply() external returns (uint256) envfree;
+    function sky.balanceOf(address) external returns (uint256) envfree;
+    function sky.allowance(address, address) external returns (uint256) envfree;
     function mkr.wards(address) external returns (uint256) envfree;
     function mkr.totalSupply() external returns (uint256) envfree;
     function mkr.balanceOf(address) external returns (uint256) envfree;
     function mkr.allowance(address, address) external returns (uint256) envfree;
 }
 
-ghost balanceSumNgt() returns mathint {
-    init_state axiom balanceSumNgt() == 0;
+ghost balanceSumSky() returns mathint {
+    init_state axiom balanceSumSky() == 0;
 }
 
-hook Sstore ngt.balanceOf[KEY address a] uint256 balance (uint256 old_balance) {
-    havoc balanceSumNgt assuming balanceSumNgt@new() == balanceSumNgt@old() + balance - old_balance && balanceSumNgt@new() >= 0;
+hook Sstore sky.balanceOf[KEY address a] uint256 balance (uint256 old_balance) {
+    havoc balanceSumSky assuming balanceSumSky@new() == balanceSumSky@old() + balance - old_balance && balanceSumSky@new() >= 0;
 }
 
-invariant balanceSumNgt_equals_totalSupply() balanceSumNgt() == to_mathint(ngt.totalSupply());
+invariant balanceSumSky_equals_totalSupply() balanceSumSky() == to_mathint(sky.totalSupply());
 
 ghost balanceSumMkr() returns mathint {
     init_state axiom balanceSumMkr() == 0;
@@ -35,13 +35,13 @@ hook Sstore mkr.balanceOf[KEY address a] uint256 balance (uint256 old_balance) {
 
 invariant balanceSumMkr_equals_totalSupply() balanceSumMkr() == to_mathint(mkr.totalSupply());
 
-// Verify correct storage changes for non reverting mkrToNgt
-rule mkrToNgt(address usr, uint256 wad) {
+// Verify correct storage changes for non reverting mkrToSky
+rule mkrToSky(address usr, uint256 wad) {
     env e;
 
     require e.msg.sender != currentContract;
 
-    requireInvariant balanceSumNgt_equals_totalSupply();
+    requireInvariant balanceSumSky_equals_totalSupply();
     requireInvariant balanceSumMkr_equals_totalSupply();
 
     address other;
@@ -50,53 +50,53 @@ rule mkrToNgt(address usr, uint256 wad) {
     require other2 != e.msg.sender;
 
     mathint rate = rate();
-    mathint ngtTotalSupplyBefore = ngt.totalSupply();
-    mathint ngtBalanceOfUsrBefore = ngt.balanceOf(usr);
-    mathint ngtBalanceOfOtherBefore = ngt.balanceOf(other);
+    mathint skyTotalSupplyBefore = sky.totalSupply();
+    mathint skyBalanceOfUsrBefore = sky.balanceOf(usr);
+    mathint skyBalanceOfOtherBefore = sky.balanceOf(other);
     mathint mkrTotalSupplyBefore = mkr.totalSupply();
     mathint mkrBalanceOfSenderBefore = mkr.balanceOf(e.msg.sender);
     mathint mkrBalanceOfOtherBefore = mkr.balanceOf(other2);
 
-    mkrToNgt(e, usr, wad);
+    mkrToSky(e, usr, wad);
 
-    mathint ngtTotalSupplyAfter = ngt.totalSupply();
-    mathint ngtBalanceOfUsrAfter = ngt.balanceOf(usr);
-    mathint ngtBalanceOfOtherAfter = ngt.balanceOf(other);
+    mathint skyTotalSupplyAfter = sky.totalSupply();
+    mathint skyBalanceOfUsrAfter = sky.balanceOf(usr);
+    mathint skyBalanceOfOtherAfter = sky.balanceOf(other);
     mathint mkrTotalSupplyAfter = mkr.totalSupply();
     mathint mkrBalanceOfSenderAfter = mkr.balanceOf(e.msg.sender);
     mathint mkrBalanceOfOtherAfter = mkr.balanceOf(other2);
 
-    assert ngtTotalSupplyAfter == ngtTotalSupplyBefore + wad * rate, "mkrToNgt did not increase ngt.totalSupply by wad * rate";
-    assert ngtBalanceOfUsrAfter == ngtBalanceOfUsrBefore + wad * rate, "mkrToNgt did not increase ngt.balanceOf[usr] by wad * rate";
-    assert ngtBalanceOfOtherAfter == ngtBalanceOfOtherBefore, "mkrToNgt did not keep unchanged the rest of ngt.balanceOf[x]";
-    assert mkrTotalSupplyAfter == mkrTotalSupplyBefore - wad, "mkrToNgt did not decrease mkr.totalSupply by wad";
-    assert mkrBalanceOfSenderAfter == mkrBalanceOfSenderBefore - wad, "mkrToNgt did not decrease mkr.balanceOf[sender] by wad";
-    assert mkrBalanceOfOtherAfter == mkrBalanceOfOtherBefore, "mkrToNgt did not keep unchanged the rest of mkr.balanceOf[x]";
+    assert skyTotalSupplyAfter == skyTotalSupplyBefore + wad * rate, "mkrToSky did not increase sky.totalSupply by wad * rate";
+    assert skyBalanceOfUsrAfter == skyBalanceOfUsrBefore + wad * rate, "mkrToSky did not increase sky.balanceOf[usr] by wad * rate";
+    assert skyBalanceOfOtherAfter == skyBalanceOfOtherBefore, "mkrToSky did not keep unchanged the rest of sky.balanceOf[x]";
+    assert mkrTotalSupplyAfter == mkrTotalSupplyBefore - wad, "mkrToSky did not decrease mkr.totalSupply by wad";
+    assert mkrBalanceOfSenderAfter == mkrBalanceOfSenderBefore - wad, "mkrToSky did not decrease mkr.balanceOf[sender] by wad";
+    assert mkrBalanceOfOtherAfter == mkrBalanceOfOtherBefore, "mkrToSky did not keep unchanged the rest of mkr.balanceOf[x]";
 }
 
-// Verify revert rules on mkrToNgt
-rule mkrToNgt_revert(address usr, uint256 wad) {
+// Verify revert rules on mkrToSky
+rule mkrToSky_revert(address usr, uint256 wad) {
     env e;
 
-    requireInvariant balanceSumNgt_equals_totalSupply();
+    requireInvariant balanceSumSky_equals_totalSupply();
     requireInvariant balanceSumMkr_equals_totalSupply();
 
     require e.msg.sender != currentContract;
 
     mathint rate = rate();
     mathint mkrBalanceOfSender = mkr.balanceOf(e.msg.sender);
-    mathint mkrAllowanceSenderMkrNgt = mkr.allowance(e.msg.sender, currentContract);
-    mathint ngtWardsMkrNgt = ngt.wards(currentContract);
-    mathint ngtTotalSupply = ngt.totalSupply();
+    mathint mkrAllowanceSenderMkrSky = mkr.allowance(e.msg.sender, currentContract);
+    mathint skyWardsMkrSky = sky.wards(currentContract);
+    mathint skyTotalSupply = sky.totalSupply();
 
-    mkrToNgt@withrevert(e, usr, wad);
+    mkrToSky@withrevert(e, usr, wad);
 
     bool revert1 = e.msg.value > 0;
     bool revert2 = mkrBalanceOfSender < to_mathint(wad);
-    bool revert3 = mkrAllowanceSenderMkrNgt < to_mathint(wad);
-    bool revert4 = ngtWardsMkrNgt != 1;
-    bool revert5 = ngtTotalSupply + wad * rate > max_uint256;
-    bool revert6 = usr == 0 || usr == ngt;
+    bool revert3 = mkrAllowanceSenderMkrSky < to_mathint(wad);
+    bool revert4 = skyWardsMkrSky != 1;
+    bool revert5 = skyTotalSupply + wad * rate > max_uint256;
+    bool revert6 = usr == 0 || usr == sky;
 
     assert revert1 => lastReverted, "revert1 failed";
     assert revert2 => lastReverted, "revert2 failed";
@@ -108,13 +108,13 @@ rule mkrToNgt_revert(address usr, uint256 wad) {
                            revert4 || revert5 || revert6, "Revert rules are not covering all the cases";
 }
 
-// Verify correct storage changes for non reverting ngtToMkr
-rule ngtToMkr(address usr, uint256 wad) {
+// Verify correct storage changes for non reverting skyToMkr
+rule skyToMkr(address usr, uint256 wad) {
     env e;
 
     require e.msg.sender != currentContract;
 
-    requireInvariant balanceSumNgt_equals_totalSupply();
+    requireInvariant balanceSumSky_equals_totalSupply();
     requireInvariant balanceSumMkr_equals_totalSupply();
 
     address other;
@@ -123,52 +123,52 @@ rule ngtToMkr(address usr, uint256 wad) {
     require other2 != usr;
 
     mathint rate = rate();
-    mathint ngtTotalSupplyBefore = ngt.totalSupply();
-    mathint ngtBalanceOfSenderBefore = ngt.balanceOf(e.msg.sender);
-    mathint ngtBalanceOfOtherBefore = ngt.balanceOf(other);
+    mathint skyTotalSupplyBefore = sky.totalSupply();
+    mathint skyBalanceOfSenderBefore = sky.balanceOf(e.msg.sender);
+    mathint skyBalanceOfOtherBefore = sky.balanceOf(other);
     mathint mkrTotalSupplyBefore = mkr.totalSupply();
     mathint mkrBalanceOfUsrBefore = mkr.balanceOf(usr);
     mathint mkrBalanceOfOtherBefore = mkr.balanceOf(other2);
 
-    ngtToMkr(e, usr, wad);
+    skyToMkr(e, usr, wad);
 
-    mathint ngtTotalSupplyAfter = ngt.totalSupply();
-    mathint ngtBalanceOfSenderAfter = ngt.balanceOf(e.msg.sender);
-    mathint ngtBalanceOfOtherAfter = ngt.balanceOf(other);
+    mathint skyTotalSupplyAfter = sky.totalSupply();
+    mathint skyBalanceOfSenderAfter = sky.balanceOf(e.msg.sender);
+    mathint skyBalanceOfOtherAfter = sky.balanceOf(other);
     mathint mkrTotalSupplyAfter = mkr.totalSupply();
     mathint mkrBalanceOfUsrAfter = mkr.balanceOf(usr);
     mathint mkrBalanceOfOtherAfter = mkr.balanceOf(other2);
 
-    assert ngtTotalSupplyAfter == ngtTotalSupplyBefore - wad, "ngtToMkr did not decrease ngt.totalSupply by wad";
-    assert ngtBalanceOfSenderAfter == ngtBalanceOfSenderBefore - wad, "ngtToMkr did not decrease ngt.balanceOf[sender] by wad";
-    assert ngtBalanceOfOtherAfter == ngtBalanceOfOtherBefore, "ngtToMkr did not keep unchanged the rest of ngt.balanceOf[x]";
-    assert mkrTotalSupplyAfter == mkrTotalSupplyBefore + wad / rate, "ngtToMkr did not increase mkr.totalSupply by wad / rate";
-    assert mkrBalanceOfUsrAfter == mkrBalanceOfUsrBefore + wad / rate, "ngtToMkr did not increase mkr.balanceOf[usr] by wad / rate";
-    assert mkrBalanceOfOtherAfter == mkrBalanceOfOtherBefore, "ngtToMkr did not keep unchanged the rest of mkr.balanceOf[x]";
+    assert skyTotalSupplyAfter == skyTotalSupplyBefore - wad, "skyToMkr did not decrease sky.totalSupply by wad";
+    assert skyBalanceOfSenderAfter == skyBalanceOfSenderBefore - wad, "skyToMkr did not decrease sky.balanceOf[sender] by wad";
+    assert skyBalanceOfOtherAfter == skyBalanceOfOtherBefore, "skyToMkr did not keep unchanged the rest of sky.balanceOf[x]";
+    assert mkrTotalSupplyAfter == mkrTotalSupplyBefore + wad / rate, "skyToMkr did not increase mkr.totalSupply by wad / rate";
+    assert mkrBalanceOfUsrAfter == mkrBalanceOfUsrBefore + wad / rate, "skyToMkr did not increase mkr.balanceOf[usr] by wad / rate";
+    assert mkrBalanceOfOtherAfter == mkrBalanceOfOtherBefore, "skyToMkr did not keep unchanged the rest of mkr.balanceOf[x]";
 }
 
-// Verify revert rules on ngtToMkr
-rule ngtToMkr_revert(address usr, uint256 wad) {
+// Verify revert rules on skyToMkr
+rule skyToMkr_revert(address usr, uint256 wad) {
     env e;
 
-    requireInvariant balanceSumNgt_equals_totalSupply();
+    requireInvariant balanceSumSky_equals_totalSupply();
     requireInvariant balanceSumMkr_equals_totalSupply();
 
     require e.msg.sender != currentContract;
 
     mathint rate = rate();
     require rate > 0;
-    mathint ngtBalanceOfSender = ngt.balanceOf(e.msg.sender);
-    mathint ngtAllowanceSenderMkrNgt = ngt.allowance(e.msg.sender, currentContract);
-    mathint mkrWardsMkrNgt = mkr.wards(currentContract);
+    mathint skyBalanceOfSender = sky.balanceOf(e.msg.sender);
+    mathint skyAllowanceSenderMkrSky = sky.allowance(e.msg.sender, currentContract);
+    mathint mkrWardsMkrSky = mkr.wards(currentContract);
     mathint mkrTotalSupply = mkr.totalSupply();
 
-    ngtToMkr@withrevert(e, usr, wad);
+    skyToMkr@withrevert(e, usr, wad);
 
     bool revert1 = e.msg.value > 0;
-    bool revert2 = ngtBalanceOfSender < to_mathint(wad);
-    bool revert3 = ngtAllowanceSenderMkrNgt < to_mathint(wad);
-    bool revert4 = mkrWardsMkrNgt != 1;
+    bool revert2 = skyBalanceOfSender < to_mathint(wad);
+    bool revert3 = skyAllowanceSenderMkrSky < to_mathint(wad);
+    bool revert4 = mkrWardsMkrSky != 1;
     bool revert5 = mkrTotalSupply + wad / rate > max_uint256;
     bool revert6 = usr == 0 || usr == mkr;
 

certora/Ngt.conf → certora/Sky.conf

@@ -1,17 +1,17 @@
 {
     "files": [
-        "src/Ngt.sol",
+        "src/Sky.sol",
         "certora/Auxiliar.sol",
         "certora/SignerMock.sol"
     ],
     "rule_sanity": "basic",
     "solc": "solc-0.8.21",
     "solc_optimize_map": {
-        "Ngt": "200",
+        "Sky": "200",
         "Auxiliar": "0",
         "SignerMock": "0"
     },
-    "verify": "Ngt:certora/Ngt.spec",
+    "verify": "Sky:certora/Sky.spec",
     "prover_args": [
         "-mediumTimeout 180"
     ],

certora/Ngt.spec → certora/Sky.spec

@@ -1,4 +1,4 @@
-// Ngt.spec
+// Sky.spec
 
 using Auxiliar as aux;
 using SignerMock as signer;

deploy/NgtDeploy.sol → deploy/SkyDeploy.sol

@@ -18,24 +18,24 @@ pragma solidity ^0.8.21;
 
 import { ScriptTools } from "dss-test/ScriptTools.sol";
 
-import { Ngt } from "src/Ngt.sol";
-import { MkrNgt } from "src/MkrNgt.sol";
+import { Sky } from "src/Sky.sol";
+import { MkrSky } from "src/MkrSky.sol";
 
-import { NgtInstance } from "./NgtInstance.sol";
+import { SkyInstance } from "./SkyInstance.sol";
 
-library NgtDeploy {
+library SkyDeploy {
     function deploy(
         address deployer,
         address owner,
         address mkr,
         uint256 rate
-    ) internal returns (NgtInstance memory instance) {
-        address _ngt = address(new Ngt());
-        ScriptTools.switchOwner(_ngt, deployer, owner);
+    ) internal returns (SkyInstance memory instance) {
+        address _sky = address(new Sky());
+        ScriptTools.switchOwner(_sky, deployer, owner);
 
-        address _mkrNgt = address(new MkrNgt(mkr, _ngt, rate));
+        address _mkrSky = address(new MkrSky(mkr, _sky, rate));
 
-        instance.ngt    = _ngt;
-        instance.mkrNgt = _mkrNgt;
+        instance.sky    = _sky;
+        instance.mkrSky = _mkrSky;
     }
 }