path: root/source/Felix/Test/Unit/Identity.hs

{-# LANGUAGE NoImplicitPrelude #-}

module Felix.Test.Unit.Identity (unitTests) where

import Base
import Felix.Checking.Authority qualified as Authority
import Felix.Checking.Core qualified as Core
import Felix.Checking.Foundation qualified as Foundation
import Felix.Checking.Identity qualified as Identity
import Felix.Cache.Codec
import Felix.Math.Codec
import Felix.Module
import Felix.Source

import Control.Exception (bracket)
import Data.ByteString qualified as ByteString
import Data.Either (isLeft)
import Data.List.NonEmpty qualified as NonEmpty
import Data.Map.Strict qualified as Map
import Data.Set qualified as Set
import Data.Text qualified as Text
import Numeric.Natural (Natural)
import System.Directory qualified as Directory
import System.FilePath.Posix qualified as Posix
import Test.Tasty
import Test.Tasty.HUnit


unitTests :: TestTree
unitTests =
    testGroup "Content identities"
        [ testCase "uses the frozen mathematical hash framing"
            hashesCanonicalFields
        , testCase "orders exhaustive foundation rows by stable tags"
            ordersFoundationManifestTags
        , testCase "uses the frozen source path codecs"
            encodesSourcePaths
        , testCase "separates durable namespaces from mount labels"
            separatesModuleOwnership
        , testCase "rejects duplicate canonical collection encodings"
            rejectsDuplicateCanonicalCollections
        , testCase "matches every frozen mathematical identity vector"
            matchesMathematicalIdentityVectors
        , testCase "validates recursive transparent object content"
            validatesTransparentObjectClosure
        , testCase "rejects cyclic and mismatched object content"
            rejectsInvalidObjectContent
        , testCase "validates proposition content and theorem closure"
            validatesPropositionAndTheorem
        , testCase "round-trips deterministic epoch cache values"
            roundTripsEpochCacheValues
        , testCase "validates compact fact authority"
            validatesCompactFactAuthority
        , testCase "propagates candidate safety through local claims"
            propagatesCandidateSafety
        ]

ordersFoundationManifestTags :: Assertion
ordersFoundationManifestTags = do
    let (intrinsics, rules, axioms) =
            Identity.foundationManifestTags
    assertEqual
        "intrinsic stable-tag order"
        [ Core.Member
        , Core.Empty
        , Core.PairSet
        , Core.FamilyUnion
        , Core.PowerSet
        , Core.Sep
        , Core.Repl
        , Core.SetChoose
        , Core.UnivOf
        , Core.ISetLfp
        ]
        intrinsics
    assertEqual
        "kernel-rule stable-tag order"
        [ Foundation.SetLfpBound
        , Foundation.SetLfpLeast
        , Foundation.SetLfpFixed
        , Foundation.SetLfpInduct
        ]
        rules
    assertEqual
        "foundation-axiom stable-tag order"
        [ Foundation.EmptyCharacteristic
        , Foundation.PairSetCharacteristic
        , Foundation.FamilyUnionCharacteristic
        , Foundation.PowerSetCharacteristic
        , Foundation.SeparationCharacteristic
        , Foundation.ReplacementCharacteristic
        , Foundation.SetChooseWitness
        , Foundation.SetExtensionality
        , Foundation.SetInduction
        , Foundation.PropositionalExtensionality
        , Foundation.DoubleNegationElim
        , Foundation.UnivOfContains
        , Foundation.UnivOfTransitive
        , Foundation.UnivOfFamilyUnionClosed
        , Foundation.UnivOfPowerSetClosed
        , Foundation.UnivOfReplacementClosed
        , Foundation.UnivOfMinimal
        ]
        axioms

hashesCanonicalFields :: Assertion
hashesCanonicalFields = do
    let vectors =
            [ ( []
              , "09ace37213e33d80b79e5f21fd60d03f25855e528cc2f25da4762be81d34a8c2"
              )
            , ( [ByteString.empty]
              , "cd166f5b566ebd02f00f202792699803df09e9a020afbaaa987f5001cb1d095e"
              )
            , (["a", "bc"]
              , "70c43385ae5b28bb862bc461a3c8d85ab94fd616528e7d94a9e7a52217b5c657"
              )
            , (["ab", "c"]
              , "d3588d1b26aac958d9f393d8528ad68ed34354aee41d7e405a156b3ffff20c90"
              )
            ]
    traverse_
        (\(fields, expected) -> do
            digest <- expectRight
                (hashCanonicalFields "felix-test-v1" fields)
            assertEqual
                ("fields " <> show fields)
                expected
                (mathematicalDigestHex digest))
        vectors

encodesSourcePaths :: Assertion
encodesSourcePaths = do
    let absoluteVectors =
            [ ([]
              , "000000000000002266656c69782d6162736f6c7574652d736f757263652d726f6f742d706174682d763100000000"
              )
            , (["a"]
              , "000000000000002266656c69782d6162736f6c7574652d736f757263652d726f6f742d706174682d763100000001000000000000000161"
              )
            , (["a", "b"]
              , "000000000000002266656c69782d6162736f6c7574652d736f757263652d726f6f742d706174682d763100000002000000000000000161000000000000000162"
              )
            ]
        relativeVectors =
            [ (["a"]
              , "000000000000001b66656c69782d736166652d72656c61746976652d706174682d763100000001000000000000000161"
              )
            , (["a", "b"]
              , "000000000000001b66656c69782d736166652d72656c61746976652d706174682d763100000002000000000000000161000000000000000162"
              )
            ]
    traverse_
        (\(components, expected) -> do
            encoded <- expectRight
                (encodeCanonicalPathRecord
                    "felix-absolute-source-root-path-v1"
                    components)
            assertEqual
                (show components)
                expected
                (hex encoded))
        absoluteVectors
    traverse_
        (\(components, expected) -> do
            encoded <- expectRight
                (encodeCanonicalPathRecord
                    "felix-safe-relative-path-v1"
                    components)
            assertEqual
                (show components)
                expected
                (hex encoded))
        relativeVectors

separatesModuleOwnership :: Assertion
separatesModuleOwnership =
    withTemporaryDirectory "felix-module-owner" \root -> do
        writeFile (root Posix.</> "b.tex") ""
        mounts <- expectRight
            =<< prepareSourceMounts
                [(sourceMountId "display-only", root)]
        request <- expectRight (searchedRoot "b.tex")
        source <- expectRight =<< resolveRoot mounts request
        mount <- case sourceMountList mounts of
            [only] ->
                pure only
            _ ->
                assertFailure "expected one prepared mount"
                    >> fail "unreachable"
        relative <- expectRight (safeRelativePath "b.tex")
        let owner =
                moduleName (resolvedSourceAddress source)
        assertEqual
            "relative owner"
            relative
            (moduleNameRelativePath owner)
        assertEqual
            "namespace derives from the canonical root"
            (sourceNamespaceId (sourceMountRoot mount))
            (moduleNameNamespace owner)

rejectsDuplicateCanonicalCollections :: Assertion
rejectsDuplicateCanonicalCollections = do
    assertEqual
        "set duplicate"
        (Left (DuplicateCanonicalSetElement "a"))
        (encodeCanonicalSet ["b", "a", "a"])
    assertEqual
        "map duplicate"
        (Left (DuplicateCanonicalMapKey "a"))
        (encodeCanonicalMap [("a", "first"), ("a", "second")])

matchesMathematicalIdentityVectors :: Assertion
matchesMathematicalIdentityVectors = do
    fixture <- makeIdentityFixture
    let vectors =
            [ ( "theory"
              , Identity.theoryIdDigest
                    (fixtureTheory fixture)
              , "46665f15f80ad52d319188de307471f34905ec3849b84b9d6d0d5a584a90eb62"
              )
            , ( "intrinsic Empty"
              , Identity.objectIdDigest
                    (fixtureIntrinsic fixture)
              , "a11f641738714ac806f3c3b902841b3178d32fff38fea353aac409e3cc1a8efc"
              )
            , ( "transparent Empty"
              , Identity.objectIdDigest
                    (fixtureTransparent fixture)
              , "49dfb3c96f0db2cc81703bbed82c08e9d2eda7d4a2274f0529d22c592003d4d1"
              )
            , ( "opaque signature"
              , Identity.objectIdDigest
                    (fixtureOpaque fixture)
              , "8723488e60ed09ffad378bc6d9916d07c348d12d01548a7b482726e6e18b2c8d"
              )
            , ( "proposition"
              , Identity.propositionIdDigest
                    (Identity.checkedPropositionId
                        (fixtureProposition fixture))
              , "c40b403f0422f4125065d83b5eba64e4b0c4b24fb1559967ef986f5265829b65"
              )
            , ( "theorem"
              , Identity.theoremIdDigest
                    (fixtureTheorem fixture)
              , "6a328a4142fde3c9851186ea00f54d8978d2640dcbe51421536c9726f4f717d2"
              )
            ]
    traverse_
        (\(description, digest, expected) ->
            assertEqual
                description
                expected
                (mathematicalDigestHex digest))
        vectors
    assertEqual
        "opaque declaration seed"
        "27697d641220b8bb63b32631492646277b28e70c8b7149206580337254ecc123"
        (mathematicalDigestHex
            (Identity.opaqueDeclarationSeedDigest
                (fixtureOpaqueSeed fixture)))
    assertEqual
        "family domains remain distinct"
        (length vectors)
        (Set.size
            (Set.fromList
                [ digest
                | (_description, digest, _expected) <- vectors
                ]))

validatesTransparentObjectClosure :: Assertion
validatesTransparentObjectClosure = do
    fixture <- makeIdentityFixture
    let theory = fixtureTheory fixture
        child = fixtureTransparent fixture
        parentBody = Core.CGlobal child
        parent =
            Identity.transparentObjectId
                theory
                Core.TySet
                parentBody
        assertions =
            [ Identity.assertedObject
                parent
                (Identity.TransparentObjectContent
                    theory
                    Core.TySet
                    parentBody)
            , Identity.assertedObject
                child
                (Identity.TransparentObjectContent
                    theory
                    Core.TySet
                    (Core.CIntrinsic Core.Empty))
            , Identity.assertedObject
                (fixtureIntrinsic fixture)
                (Identity.IntrinsicObjectContent
                    theory
                    Core.Empty
                    Core.TySet)
            ]
    closure <- expectRight
        (Identity.validateObjectClosure theory assertions)
    assertEqual
        "all recursively checked objects"
        (Set.fromList
            [ fixtureIntrinsic fixture
            , child
            , parent
            ])
        (Identity.checkedObjectIds closure)
    assertEqual
        "parent type"
        (Just Core.TySet)
        (Identity.lookupCheckedObjectType parent closure)

rejectsInvalidObjectContent :: Assertion
rejectsInvalidObjectContent = do
    fixture <- makeIdentityFixture
    firstDigest <- expectRight
        (hashCanonicalFields "felix-invalid-object-a" [])
    secondDigest <- expectRight
        (hashCanonicalFields "felix-invalid-object-b" [])
    mismatchDigest <- expectRight
        (hashCanonicalFields "felix-invalid-object-mismatch" [])
    let theory = fixtureTheory fixture
        first =
            Identity.objectId
                Identity.TransparentObject
                firstDigest
        second =
            Identity.objectId
                Identity.TransparentObject
                secondDigest
        cycleAssertions =
            [ Identity.assertedObject
                first
                (Identity.TransparentObjectContent
                    theory
                    Core.TySet
                    (Core.CGlobal second))
            , Identity.assertedObject
                second
                (Identity.TransparentObjectContent
                    theory
                    Core.TySet
                    (Core.CGlobal first))
            ]
    case Identity.validateObjectClosure theory cycleAssertions of
        Left (Identity.TransparentObjectCycle path) -> do
            assertEqual
                "cycle closes"
                (NonEmpty.head path)
                (NonEmpty.last path)
            assertEqual
                "cycle members"
                (Set.fromList [first, second])
                (Set.fromList (NonEmpty.toList path))
        Left other ->
            assertFailure
                ("expected a transparent cycle, got " <> show other)
        Right _ ->
            assertFailure "expected a transparent cycle, got Right"
    let mismatched =
            Identity.objectId
                Identity.TransparentObject
                mismatchDigest
        content =
            Identity.TransparentObjectContent
                theory
                Core.TySet
                (Core.CIntrinsic Core.Empty)
    case
        Identity.validateObjectClosure
            theory
            [Identity.assertedObject mismatched content] of
        Left
            (Identity.ObjectIdPayloadMismatch
                supplied
                computed) -> do
                    assertEqual "supplied ID" mismatched supplied
                    assertEqual
                        "computed ID"
                        (fixtureTransparent fixture)
                        computed
        Left other ->
            assertFailure
                ("expected object ID disagreement, got " <> show other)
        Right _ ->
            assertFailure "expected object ID disagreement, got Right"

validatesPropositionAndTheorem :: Assertion
validatesPropositionAndTheorem = do
    fixture <- makeIdentityFixture
    let proposition =
            fixtureProposition fixture
        reference =
            fixtureTheoremRef fixture
    assertEqual
        "theorem retains its theory"
        (fixtureTheory fixture)
        (Identity.theoremRefTheory reference)
    assertEqual
        "theorem retains its proposition"
        (Identity.checkedPropositionId proposition)
        (Identity.theoremRefProposition reference)
    falsum <- expectRight
        (Identity.validatePropositionContent
            (fixtureClosure fixture)
            Core.CFalsum)
    case
        Identity.validateAssertedPropositionContent
            (fixtureClosure fixture)
            (Identity.checkedPropositionId falsum)
            (Core.frozenCoreTerm
                (Identity.checkedPropositionTerm proposition)) of
        Left
            (Identity.PropositionIdPayloadMismatch
                supplied
                computed) -> do
                    assertEqual
                        "supplied proposition ID"
                        (Identity.checkedPropositionId falsum)
                        supplied
                    assertEqual
                        "computed proposition ID"
                        (Identity.checkedPropositionId proposition)
                        computed
        Left other ->
            assertFailure
                ("expected proposition ID disagreement, got "
                    <> show other)
        Right _ ->
            assertFailure
                "expected proposition ID disagreement, got Right"

roundTripsEpochCacheValues :: Assertion
roundTripsEpochCacheValues = do
    fixture <- makeIdentityFixture
    let theory = fixtureTheory fixture
        contents =
            [ Identity.IntrinsicObjectContent
                theory
                Core.Empty
                Core.TySet
            , Identity.TransparentObjectContent
                theory
                Core.TySet
                (Core.CIntrinsic Core.Empty)
            , Identity.OpaqueObjectContent
                theory
                (fixtureOpaqueSeed fixture)
                Core.TySet
            ]
    traverse_
        (\content ->
            assertEqual
                "object-content cache round trip"
                (Right content)
                (decodeCache
                    Identity.getObjectContentCache
                    (encodeCache
                        (Identity.putObjectContentCache
                            content))))
        contents
    assertEqual
        "constructive theorem reference cache round trip"
        (Right (fixtureTheoremRef fixture))
        (decodeCache
            Identity.getTheoremRefCache
            (encodeCache
                (Identity.putTheoremRefCache
                    (fixtureTheoremRef fixture))))
    assertBool
        "cache bytes are not mathematical theorem-reference bytes"
        ( encodeCache
            (Identity.putTheoremRefCache
                (fixtureTheoremRef fixture))
            /= Identity.encodeTheoremRef
                (fixtureTheoremRef fixture)
        )
    let ascending =
            Map.fromList [("a", 1 :: Natural), ("b", 2)]
        putMap =
            putCanonicalCacheMap
                putCacheText
                putCacheNatural
    assertEqual
        "canonical cache map round trip"
        (Right ascending)
        (decodeCache
            (getCanonicalCacheMap
                getCacheText
                getCacheNatural)
            (encodeCache (putMap ascending)))

validatesCompactFactAuthority :: Assertion
validatesCompactFactAuthority = do
    fixture <- makeIdentityFixture
    let reference = fixtureTheoremRef fixture
        sourceKinds =
            Authority.singletonEscapeKind Authority.SourceAxiom
        bothKinds =
            Authority.escapeKinds
                [Authority.Omitted, Authority.SourceAxiom]
        sourceTarget =
            Authority.factAuthority
                reference
                (Authority.authoritySafety sourceKinds)
        bothTarget =
            Authority.factAuthority
                reference
                (Authority.authoritySafety bothKinds)
        requests =
            [ Authority.preparedRequestId
                Authority.PreparedRequestFof
                Authority.PreparedRequestDirect
                "first"
            , Authority.preparedRequestId
                Authority.PreparedRequestFof
                Authority.PreparedRequestDirect
                "first"
            , Authority.preparedRequestId
                Authority.PreparedRequestFof
                Authority.PreparedRequestDirect
                "second"
            ]
        directRequest =
            Authority.preparedRequestId
                Authority.PreparedRequestFof
                Authority.PreparedRequestDirect
                "same bytes"
        indirectRequest =
            Authority.preparedRequestId
                Authority.PreparedRequestFof
                Authority.PreparedRequestIndirect
                "same bytes"
        directAuthorizations =
            [ Authority.CheckedKernelConstruction
                (Authority.FoundationLeaf
                    Foundation.EmptyCharacteristic)
            , Authority.CheckedKernelConstruction
                (Authority.GuardedFoundationRules
                    (Authority.guardedRuleSet
                        (Foundation.SetLfpBound :| [])))
            , Authority.CheckedKernelConstruction
                (Authority.CheckedDefinitionEquation
                    (fixtureIntrinsic fixture))
            , Authority.CheckedKernelConstruction
                (Authority.CheckedSetConstructionExtensionality
                    (fixtureIntrinsic fixture)
                    (hashCacheFields
                        "test-named-construction" ["checked"]))
            , Authority.CheckedSourceProof requests
            , Authority.TrustedCompilation
                (Authority.DatatypeCompilation
                    (Authority.datatypeCompilationDescriptor
                        (fixtureIntrinsic fixture)
                        (NonEmpty.singleton
                            (fixtureIntrinsic fixture))
                        [reference]))
            , Authority.SourceAxiomAuthorization
            , Authority.OmittedAuthorization
            ]
    sourceCertificate <- expectRight
        (Authority.validationCertificate
            sourceTarget
            Authority.SourceAxiomAuthorization)
    proofCertificate <- expectRight
        (Authority.validationCertificate
            bothTarget
            (Authority.CheckedSourceProof requests))
    assertEqual
        "escape bits have canonical order"
        [Authority.SourceAxiom, Authority.Omitted]
        (Authority.escapeKindsToList bothKinds)
    traverse_
        (\direct ->
            assertEqual
                ("direct authorization round trip: " <> show direct)
                (Right direct)
                (decodeCache
                    Authority.getDirectAuthorizationCache
                    (encodeCache
                        (Authority.putDirectAuthorizationCache
                            direct))))
        directAuthorizations
    assertEqual
        "certificate cache retains repeated ordered requests"
        (Right proofCertificate)
        (decodeCache
            Authority.getValidationCertificateCache
            (encodeCache
                (Authority.putValidationCertificateCache
                    proofCertificate)))
    assertBool
        "request mode participates in exact request identity"
        (directRequest /= indirectRequest)
    assertEqual
        "prepared-request cache identity vector"
        "1d72b851cb8b1704617becbf9f2cf492aed1c674d9e6ca759e244f169b15f278"
        (hex
            (encodeCache
                (Authority.putPreparedRequestIdCache
                    directRequest)))
    assertEqual
        "source certificate round trip"
        (Right sourceCertificate)
        (decodeCache
            Authority.getValidationCertificateCache
            (encodeCache
                (Authority.putValidationCertificateCache
                    sourceCertificate)))
    assertBool
        "source axiom requires its exact singleton safety"
        (isLeft
            (Authority.validationCertificate
                bothTarget
                Authority.SourceAxiomAuthorization))
    assertBool
        "omitted authorization requires its distinct bit"
        (isLeft
            (Authority.validationCertificate
                sourceTarget
                Authority.OmittedAuthorization))
    assertBool
        "cache rejects an empty escape-backed value"
        (isLeft
            (decodeCache
                Authority.getAuthoritySafetyCache
                (encodeCache do
                    putCacheTag 0x01
                    putCacheTag 0x00)))
    let taintedCandidate =
            Authority.addCandidateEscape
                Authority.SourceAxiom
                Authority.initialCandidateSafety
    assertEqual
        "candidate completion freezes accumulated safety"
        sourceTarget
        (Authority.candidateFactAuthority
            reference
            taintedCandidate)

propagatesCandidateSafety :: Assertion
propagatesCandidateSafety = do
    fixture <- makeIdentityFixture
    let reference = fixtureTheoremRef fixture
        imported =
            Authority.factAuthority
                reference
                (Authority.authoritySafety
                    (Authority.singletonEscapeKind
                        Authority.SourceAxiom))
    afterImported <- expectRight
        (Authority.accumulateFactSafety
            reference
            imported
            Authority.initialCandidateSafety)
    -- A local claim shares the enclosing candidate value; citing that claim
    -- does not create a second support representation.
    afterLocalClaim <- expectRight
        (Authority.accumulateFactSafety
            reference
            (Authority.factAuthority
                reference
                Authority.cleanAuthoritySafety)
            afterImported)
    let finalSafety =
            Authority.addCandidateEscape
                Authority.Omitted
                afterLocalClaim
    assertEqual
        "local claim retains prior safety and direct omission"
        [Authority.SourceAxiom, Authority.Omitted]
        (Authority.escapeKindsToList
            (Authority.authoritySafetyEscapeKinds
                (Authority.candidateSafetyAuthority finalSafety)))

data IdentityFixture = IdentityFixture
    { fixtureTheory :: !Identity.TheoryId
    , fixtureIntrinsic :: !Identity.ObjectId
    , fixtureTransparent :: !Identity.ObjectId
    , fixtureOpaqueSeed :: !Identity.OpaqueDeclarationSeed
    , fixtureOpaque :: !Identity.ObjectId
    , fixtureClosure :: !Identity.CheckedObjectClosure
    , fixtureProposition :: !Identity.CheckedPropositionContent
    , fixtureTheoremRef :: !Identity.TheoremRef
    , fixtureTheorem :: !Identity.TheoremId
    }

makeIdentityFixture :: IO IdentityFixture
makeIdentityFixture = do
    foundation <- expectRight Foundation.checkedFoundation
    pathRecord <- expectRight
        (encodeCanonicalPathRecord
            "felix-absolute-source-root-path-v1"
            ["a"])
    namespaceDigest <- expectRight
        (hashCanonicalFields
            "felix-source-namespace-v1"
            [pathRecord])
    relative <- expectRight (safeRelativePath "b.tex")
    let theory =
            Identity.theoryId foundation
        intrinsic =
            Identity.intrinsicObjectId
                theory
                Core.Empty
                Core.TySet
        transparent =
            Identity.transparentObjectId
                theory
                Core.TySet
                (Core.CIntrinsic Core.Empty)
        owner =
            moduleNameFromParts
                (sourceNamespaceIdFromDigest
                    namespaceDigest)
                relative
        seed =
            Identity.opaqueDeclarationSeed
                owner
                (localDeclarationOrdinal 2)
                SignatureDeclaration
                (generatedObjectSlot 0)
        opaque =
            Identity.opaqueObjectId
                theory
                seed
                Core.TySet
    closure <- expectRight
        (Identity.validateObjectClosure
            theory
            [ Identity.assertedObject
                intrinsic
                (Identity.IntrinsicObjectContent
                    theory
                    Core.Empty
                    Core.TySet)
            ])
    proposition <- expectRight
        (Identity.validatePropositionContent
            closure
            (Core.CEq
                Core.TySet
                (Core.CGlobal intrinsic)
                (Core.CGlobal intrinsic)))
    let reference =
            Identity.theoremRef
                theory
                (Identity.checkedPropositionId proposition)
    pure
        IdentityFixture
            { fixtureTheory = theory
            , fixtureIntrinsic = intrinsic
            , fixtureTransparent = transparent
            , fixtureOpaqueSeed = seed
            , fixtureOpaque = opaque
            , fixtureClosure = closure
            , fixtureProposition = proposition
            , fixtureTheoremRef = reference
            , fixtureTheorem =
                Identity.theoremId reference
            }

hex :: ByteString.ByteString -> Text
hex =
    Text.pack
        . concatMap byteHex
        . ByteString.unpack
  where
    byteHex byte =
        let digits = "0123456789abcdef"
            high = fromIntegral (byte `div` 16)
            low = fromIntegral (byte `mod` 16)
        in [digits `at` high, digits `at` low]

    at characters index =
        fromMaybe
            (impossible "hex digit index")
            (nth index characters)

expectRight :: Show error => Either error value -> IO value
expectRight = \case
    Left err ->
        assertFailure (show err) >> fail "unreachable"
    Right value ->
        pure value

withTemporaryDirectory :: String -> (FilePath -> IO a) -> IO a
withTemporaryDirectory template =
    bracket create Directory.removePathForcibly
  where
    create = do
        systemTemp <- Directory.getTemporaryDirectory
        (path, handle) <- openTempFile systemTemp template
        hClose handle
        Directory.removeFile path
        Directory.createDirectory path
        pure path