From b670ec39f98eaa6cbe34e197241be5396b202ba8 Mon Sep 17 00:00:00 2001
From: BowTiedRadone <bowtiedradone@gmail.com>
Date: Wed, 17 Jul 2024 12:54:36 +0300
Subject: [PATCH] Add CanNamespaceBeRegisteredTrue invariant

This commit:
- Adds the CanNamespaceBeRegisteredTrue invariant. This checks that can-namespace-be-registered always returns (ok true) when namespace is not yet registered or its launchability period has passed since its reveal.
- Adds the burnBlockHeight to the model.
- Adds the newly generated invariant to the invariants list.
---
 tests/BNS-V2.stateful.test.ts           |  3 ++
 tests/state/CanNamespaceBeRegistered.ts | 57 +++++++++++++++++++++++++
 tests/state/types.ts                    |  1 +
 3 files changed, 61 insertions(+)
 create mode 100644 tests/state/CanNamespaceBeRegistered.ts

diff --git a/tests/BNS-V2.stateful.test.ts b/tests/BNS-V2.stateful.test.ts
index 23b791d..03faae2 100644
--- a/tests/BNS-V2.stateful.test.ts
+++ b/tests/BNS-V2.stateful.test.ts
@@ -7,6 +7,7 @@ import { GetBnsFromIdNone } from "./state/GetBnsFromIdNone.ts";
 import { GetPrimaryNameNone } from "./state/GetPrimaryNameNone.ts";
 import { GetNamespacePropertiesErr } from "./state/GetNamespacePropertiesErr.ts";
 import { GetNamespacePrice } from "./state/GetNamespacePrice.ts";
+import { CanNamespaceBeRegisteredTrue } from "./state/CanNamespaceBeRegistered.ts";
 
 it("executes BNS-V2 state interactions", async () => {
   const excludedAccounts = ["faucet", "deployer"];
@@ -23,9 +24,11 @@ it("executes BNS-V2 state interactions", async () => {
     GetPrimaryNameNone(filteredAccounts),
     GetNamespacePropertiesErr(filteredAccounts),
     GetNamespacePrice(filteredAccounts),
+    CanNamespaceBeRegisteredTrue(filteredAccounts),
   ];
 
   const model = {
+    burnBlockHeight: 0,
     lastTokenId: 0,
     owners: new Map(),
     indexToName: new Map(),
diff --git a/tests/state/CanNamespaceBeRegistered.ts b/tests/state/CanNamespaceBeRegistered.ts
new file mode 100644
index 0000000..c50d418
--- /dev/null
+++ b/tests/state/CanNamespaceBeRegistered.ts
@@ -0,0 +1,57 @@
+import fc from "fast-check";
+import { Model } from "./types";
+import { Simnet } from "@hirosystems/clarinet-sdk";
+import { expect } from "vitest";
+import { Cl } from "@stacks/transactions";
+import { encoder, prettyConsoleLog } from "../BNS-V2.helper";
+
+const NAMESPACE_LAUNCHABILITY_TTL = 52595;
+
+export const CanNamespaceBeRegisteredTrue = (
+  accounts: Map<string, string>,
+) =>
+  fc
+    .record({
+      sender: fc.constantFrom(...accounts),
+      namespace: fc.string({ maxLength: 20 }),
+    })
+    .map((r) => ({
+      check: (model: Readonly<Model>) => {
+        const namespace = model.namespaces.get(r.namespace);
+
+        if (
+          !namespace || namespace.launchedAt === undefined ||
+          namespace.revealedAt === undefined
+        ) {
+          return true;
+        }
+
+        return model.burnBlockHeight >
+          namespace.revealedAt + NAMESPACE_LAUNCHABILITY_TTL;
+      },
+      run: (_model: Model, real: Simnet) => {
+        const [wallet, address] = r.sender;
+        const namespaceBuff = encoder.encode(r.namespace);
+        // Act
+        const { result: canRegisterNamespaceOptional } = real.callReadOnlyFn(
+          "BNS-V2",
+          "can-namespace-be-registered",
+          [Cl.buffer(namespaceBuff)],
+          address,
+        );
+
+        // Assert
+        expect(canRegisterNamespaceOptional).toBeOk(Cl.bool(true));
+
+        prettyConsoleLog(
+          "Ӿ tx-sender",
+          wallet,
+          "✓",
+          "can-namespace-be-registered",
+          `namespace: "${r.namespace}"`,
+          "response: (ok true)",
+        );
+      },
+      toString: () =>
+        `can-namespace-be-registered namespace "${r.namespace}" response (ok true)`,
+    }));
diff --git a/tests/state/types.ts b/tests/state/types.ts
index ed2a066..0745214 100644
--- a/tests/state/types.ts
+++ b/tests/state/types.ts
@@ -1,4 +1,5 @@
 export type Model = {
+  burnBlockHeight: number;
   lastTokenId: number;
   owners: Map<number, string>;
   indexToName: Map<number, Name>;