From 5f35178575b29c8b43708eecb6b6a5c82b7e4340 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?=C5=81ukasz=20Czajka?= <62751+lukaszcz@users.noreply.github.com> Date: Wed, 21 Jun 2023 13:08:19 +0200 Subject: [PATCH] Switch to Halo2 for VampIR backend tests (#2216) * Closes #2214 --- test/Core/Normalize/Positive.hs | 39 +------ test/Core/VampIR/LetHoist.hs | 5 +- test/Core/VampIR/Positive.hs | 2 +- test/VampIR/Compilation/Base.hs | 8 +- test/VampIR/Compilation/Positive.hs | 32 +----- test/VampIR/Core/Base.hs | 155 +++++++++++++++++----------- test/VampIR/Core/Positive.hs | 48 ++++----- 7 files changed, 136 insertions(+), 153 deletions(-) diff --git a/test/Core/Normalize/Positive.hs b/test/Core/Normalize/Positive.hs index 2ed45966d9..9f127495fe 100644 --- a/test/Core/Normalize/Positive.hs +++ b/test/Core/Normalize/Positive.hs @@ -4,8 +4,7 @@ import Base import Core.Normalize.Base data PosTest = PosTest - { _paramsNum :: Int, - _name :: String, + { _name :: String, _relDir :: Path Rel Dir, _file :: Path Rel File, _dataFile :: Path Rel File @@ -23,8 +22,7 @@ root :: Path Abs Dir root = relToProject $(mkRelDir "tests/VampIR/positive") toTestDescr' :: - ( Int -> - Path Abs File -> + ( Path Abs File -> Path Abs File -> (String -> IO ()) -> Assertion @@ -38,11 +36,11 @@ toTestDescr' assertion PosTest {..} = in TestDescr { _testName = _name, _testRoot = tRoot, - _testAssertion = Steps $ assertion _paramsNum file' expected' + _testAssertion = Steps $ assertion file' expected' } toTestDescr :: PosTest -> TestDescr -toTestDescr = toTestDescr' (const coreNormalizeAssertion) +toTestDescr = toTestDescr' coreNormalizeAssertion allTests :: TestTree allTests = @@ -53,175 +51,146 @@ allTests = tests :: [PosTest] tests = [ PosTest - 5 "Test001: not function" $(mkRelDir "Core") $(mkRelFile "test001.jvc") $(mkRelFile "data/test001.json"), PosTest - 5 "Test002: pattern matching" $(mkRelDir "Core") $(mkRelFile "test002.jvc") $(mkRelFile "data/test002.json"), PosTest - 6 "Test003: inductive types" $(mkRelDir "Core") $(mkRelFile "test003.jvc") $(mkRelFile "data/test003.json"), PosTest - 5 "Test004: definitions" $(mkRelDir "Core") $(mkRelFile "test004.jvc") $(mkRelFile "data/test004.json"), PosTest - 5 "Test005: basic arithmetic" $(mkRelDir "Core") $(mkRelFile "test005.jvc") $(mkRelFile "data/test005.json"), PosTest - 9 "Test006: arithmetic" $(mkRelDir "Core") $(mkRelFile "test006.jvc") $(mkRelFile "data/test006.json"), PosTest - 5 "Test007: single-constructor inductive types" $(mkRelDir "Core") $(mkRelFile "test007.jvc") $(mkRelFile "data/test007.json"), PosTest - 5 "Test008: higher-order inductive types" $(mkRelDir "Core") $(mkRelFile "test008.jvc") $(mkRelFile "data/test008.json"), PosTest - 9 "Test009: comparisons" $(mkRelDir "Core") $(mkRelFile "test009.jvc") $(mkRelFile "data/test009.json"), PosTest - 5 "Test010: let" $(mkRelDir "Core") $(mkRelFile "test010.jvc") $(mkRelFile "data/test010.json"), PosTest - 7 "Test011: functions returning functions with variable capture" $(mkRelDir "Core") $(mkRelFile "test011.jvc") $(mkRelFile "data/test011.json"), PosTest - 5 "Test012: partial application" $(mkRelDir "Core") $(mkRelFile "test012.jvc") $(mkRelFile "data/test012.json"), PosTest - 14 "Test013: mid-square hashing (unrolled)" $(mkRelDir "Core") $(mkRelFile "test013.jvc") $(mkRelFile "data/test013.json"), PosTest - 11 "Test014: recursion" $(mkRelDir "Core") $(mkRelFile "test014.jvc") $(mkRelFile "data/test014.json"), PosTest - 11 "Test015: tail recursion" $(mkRelDir "Core") $(mkRelFile "test015.jvc") $(mkRelFile "data/test015.json"), PosTest - 11 "Test016: tail recursion: Fibonacci numbers in linear time" $(mkRelDir "Core") $(mkRelFile "test016.jvc") $(mkRelFile "data/test016.json"), PosTest - 11 "Test017: recursion through higher-order functions" $(mkRelDir "Core") $(mkRelFile "test017.jvc") $(mkRelFile "data/test017.json"), PosTest - 11 "Test018: tail recursion through higher-order functions" $(mkRelDir "Core") $(mkRelFile "test018.jvc") $(mkRelFile "data/test018.json"), PosTest - 5 "Test019: higher-order functions" $(mkRelDir "Core") $(mkRelFile "test019.jvc") $(mkRelFile "data/test019.json"), PosTest - 5 "Test020: functional queues" $(mkRelDir "Core") $(mkRelFile "test020.jvc") $(mkRelFile "data/test020.json"), PosTest - 5 "Test021: polymorphism" $(mkRelDir "Core") $(mkRelFile "test021.jvc") $(mkRelFile "data/test021.json"), PosTest - 12 "Test022: mutual recursion" $(mkRelDir "Core") $(mkRelFile "test022.jvc") $(mkRelFile "data/test022.json"), PosTest - 5 "Test023: eta-expansion" $(mkRelDir "Core") $(mkRelFile "test023.jvc") $(mkRelFile "data/test023.json"), PosTest - 5 "Test024: eta-expansion of polymorphic constructors" $(mkRelDir "Core") $(mkRelFile "test024.jvc") $(mkRelFile "data/test024.json"), PosTest - 14 "Test025: mid-square hashing" $(mkRelDir "Core") $(mkRelFile "test025.jvc") $(mkRelFile "data/test025.json"), PosTest - 5 "Test026: letrec" $(mkRelDir "Core") $(mkRelFile "test026.jvc") $(mkRelFile "data/test026.json"), PosTest - 5 "Test027: type synonyms" $(mkRelDir "Core") $(mkRelFile "test027.jvc") $(mkRelFile "data/test027.json"), PosTest - 5 "Test028: let hoisting" $(mkRelDir "Core") $(mkRelFile "test028.jvc") $(mkRelFile "data/test028.json"), PosTest - 10 "Test029: let hoisting" $(mkRelDir "Core") $(mkRelFile "test029.jvc") diff --git a/test/Core/VampIR/LetHoist.hs b/test/Core/VampIR/LetHoist.hs index bd6d03a330..77b6f8d946 100644 --- a/test/Core/VampIR/LetHoist.hs +++ b/test/Core/VampIR/LetHoist.hs @@ -10,7 +10,7 @@ fromTest :: PosTest -> TestTree fromTest = mkTest . toTestDescr toTestDescr :: PosTest -> TestDescr -toTestDescr = Normalize.toTestDescr' (const (coreVampIRAssertion [LetHoisting])) +toTestDescr = Normalize.toTestDescr' (coreVampIRAssertion [LetHoisting]) allTests :: TestTree allTests = @@ -21,19 +21,16 @@ allTests = tests :: [PosTest] tests = [ PosTest - 5 "Test010: Lets" $(mkRelDir "Core") $(mkRelFile "test010.jvc") $(mkRelFile "data/test010.json"), PosTest - 5 "Test028: Let hoisting" $(mkRelDir "Core") $(mkRelFile "test028.jvc") $(mkRelFile "data/test028.json"), PosTest - 5 "Test029: Let hoisting" $(mkRelDir "Core") $(mkRelFile "test029.jvc") diff --git a/test/Core/VampIR/Positive.hs b/test/Core/VampIR/Positive.hs index b93a08e4a2..f91e0ee81e 100644 --- a/test/Core/VampIR/Positive.hs +++ b/test/Core/VampIR/Positive.hs @@ -10,7 +10,7 @@ fromTest :: PosTest -> TestTree fromTest = mkTest . toTestDescr toTestDescr :: PosTest -> TestDescr -toTestDescr = Normalize.toTestDescr' (const (coreVampIRAssertion toVampIRTransformations)) +toTestDescr = Normalize.toTestDescr' (coreVampIRAssertion toVampIRTransformations) allTests :: TestTree allTests = diff --git a/test/VampIR/Compilation/Base.hs b/test/VampIR/Compilation/Base.hs index 4008f2adb9..72b6665c27 100644 --- a/test/VampIR/Compilation/Base.hs +++ b/test/VampIR/Compilation/Base.hs @@ -4,15 +4,15 @@ import Base import Core.VampIR.Base (coreVampIRAssertion') import Juvix.Compiler.Core import Juvix.Compiler.Core.Data.TransformationId -import VampIR.Core.Base (vampirAssertion') +import VampIR.Core.Base (VampirBackend (..), vampirAssertion') -vampirCompileAssertion :: Int -> Path Abs File -> Path Abs File -> (String -> IO ()) -> Assertion -vampirCompileAssertion paramsNum mainFile dataFile step = do +vampirCompileAssertion :: Path Abs File -> Path Abs File -> (String -> IO ()) -> Assertion +vampirCompileAssertion mainFile dataFile step = do step "Translate to JuvixCore" entryPoint <- defaultEntryPointCwdIO mainFile tab <- (^. coreResultTable) . snd <$> runIO' entryPoint upToCore coreVampIRAssertion' tab toVampIRTransformations mainFile dataFile step - vampirAssertion' paramsNum tab dataFile step + vampirAssertion' VampirHalo2 tab dataFile step vampirCompileErrorAssertion :: Path Abs File -> diff --git a/test/VampIR/Compilation/Positive.hs b/test/VampIR/Compilation/Positive.hs index a0048c04e8..686944a29a 100644 --- a/test/VampIR/Compilation/Positive.hs +++ b/test/VampIR/Compilation/Positive.hs @@ -4,8 +4,7 @@ import Base import VampIR.Compilation.Base data PosTest = PosTest - { _paramsNum :: Int, - _name :: String, + { _name :: String, _dir :: Path Abs Dir, _file :: Path Abs File, _dataFile :: Path Abs File @@ -27,7 +26,7 @@ toTestDescr PosTest {..} = in TestDescr { _testName = _name, _testRoot = tRoot, - _testAssertion = Steps $ vampirCompileAssertion _paramsNum file' data' + _testAssertion = Steps $ vampirCompileAssertion file' data' } allTests :: TestTree @@ -36,8 +35,8 @@ allTests = "Juvix to VampIR compilation positive tests" (map (mkTest . toTestDescr) tests) -posTest :: Int -> String -> Path Rel Dir -> Path Rel File -> Path Rel File -> PosTest -posTest _paramsNum _name rdir rfile routfile = +posTest :: String -> Path Rel Dir -> Path Rel File -> Path Rel File -> PosTest +posTest _name rdir rfile routfile = let _dir = root rdir _file = _dir rfile _dataFile = root routfile @@ -46,139 +45,116 @@ posTest _paramsNum _name rdir rfile routfile = tests :: [PosTest] tests = [ posTest - 5 "Test001: not function" $(mkRelDir ".") $(mkRelFile "test001.juvix") $(mkRelFile "data/test001.json"), posTest - 5 "Test002: pattern matching" $(mkRelDir ".") $(mkRelFile "test002.juvix") $(mkRelFile "data/test002.json"), posTest - 6 "Test003: inductive types" $(mkRelDir ".") $(mkRelFile "test003.juvix") $(mkRelFile "data/test003.json"), posTest - 11 "Test004: arithmetic" $(mkRelDir ".") $(mkRelFile "test004.juvix") $(mkRelFile "data/test004.json"), posTest - 5 "Test005: single-constructor inductive types" $(mkRelDir ".") $(mkRelFile "test005.juvix") $(mkRelFile "data/test005.json"), posTest - 5 "Test006: higher-order inductive types" $(mkRelDir ".") $(mkRelFile "test006.juvix") $(mkRelFile "data/test006.json"), posTest - 5 "Test007: let" $(mkRelDir ".") $(mkRelFile "test007.juvix") $(mkRelFile "data/test007.json"), posTest - 8 "Test008: functions returning functions with variable capture" $(mkRelDir ".") $(mkRelFile "test008.juvix") $(mkRelFile "data/test008.json"), posTest - 6 "Test009: applications with lets and cases in function position" $(mkRelDir ".") $(mkRelFile "test009.juvix") $(mkRelFile "data/test009.json"), posTest - 14 "Test010: mid-square hashing (unrolled)" $(mkRelDir ".") $(mkRelFile "test010.juvix") $(mkRelFile "data/test010.json"), posTest - 8 "Test011: recursion" $(mkRelDir ".") $(mkRelFile "test011.juvix") $(mkRelFile "data/test011.json"), posTest - 8 "Test012: tail recursion" $(mkRelDir ".") $(mkRelFile "test012.juvix") $(mkRelFile "data/test012.json"), posTest - 8 "Test013: tail recursion: Fibonacci numbers in linear time" $(mkRelDir ".") $(mkRelFile "test013.juvix") $(mkRelFile "data/test013.json"), posTest - 8 "Test014: recursion through higher-order functions" $(mkRelDir ".") $(mkRelFile "test014.juvix") $(mkRelFile "data/test014.json"), posTest - 8 "Test015: tail recursion through higher-order functions" $(mkRelDir ".") $(mkRelFile "test015.juvix") $(mkRelFile "data/test015.json"), posTest - 5 "Test016: higher-order functions" $(mkRelDir ".") $(mkRelFile "test016.juvix") $(mkRelFile "data/test016.json"), posTest - 9 "Test017: mutual recursion" $(mkRelDir ".") $(mkRelFile "test017.juvix") $(mkRelFile "data/test017.json"), posTest - 14 "Test018: mid-square hashing" $(mkRelDir ".") $(mkRelFile "test018.juvix") $(mkRelFile "data/test018.json"), posTest - 3 "Test019: polymorphism" $(mkRelDir ".") $(mkRelFile "test019.juvix") $(mkRelFile "data/test019.json"), posTest - 8 "Test020: boolean target" $(mkRelDir ".") $(mkRelFile "test020.juvix") $(mkRelFile "data/test020.json"), posTest - 15 "Test021: fast exponentiation (exponential unrolling)" $(mkRelDir ".") $(mkRelFile "test021.juvix") $(mkRelFile "data/test021.json"), posTest - 14 "Test022: fast exponentiation" $(mkRelDir ".") $(mkRelFile "test022.juvix") $(mkRelFile "data/test022.json"), posTest - 5 "Test023: permutative conversions" $(mkRelDir ".") $(mkRelFile "test023.juvix") diff --git a/test/VampIR/Core/Base.hs b/test/VampIR/Core/Base.hs index 7cce5d7016..4e507a4c24 100644 --- a/test/VampIR/Core/Base.hs +++ b/test/VampIR/Core/Base.hs @@ -7,16 +7,18 @@ import Juvix.Compiler.Core import Juvix.Prelude.Pretty import System.Process qualified as P -vampirAssertion :: Int -> Path Abs File -> Path Abs File -> (String -> IO ()) -> Assertion -vampirAssertion paramsNum mainFile dataFile step = do +data VampirBackend = VampirHalo2 | VampirPlonk + +vampirAssertion :: VampirBackend -> Path Abs File -> Path Abs File -> (String -> IO ()) -> Assertion +vampirAssertion backend mainFile dataFile step = do step "Parse" s <- readFile (toFilePath mainFile) case runParserMain mainFile emptyInfoTable s of Left err -> assertFailure (show err) - Right tab -> vampirAssertion' paramsNum tab dataFile step + Right tab -> vampirAssertion' backend tab dataFile step -vampirAssertion' :: Int -> InfoTable -> Path Abs File -> (String -> IO ()) -> Assertion -vampirAssertion' paramsNum tab dataFile step = do +vampirAssertion' :: VampirBackend -> InfoTable -> Path Abs File -> (String -> IO ()) -> Assertion +vampirAssertion' backend tab dataFile step = do withTempDir' ( \dirPath -> do step "Translate to VampIR" @@ -29,64 +31,101 @@ vampirAssertion' paramsNum tab dataFile step = do step "Check vamp-ir on path" assertCmdExists $(mkRelFile "vamp-ir") - step "VampIR setup parameters" - P.callProcess "vamp-ir" (setupParamsArgs paramsNum dirPath) + vampirSetupArgs backend dirPath step + step "VampIR compile" - P.callProcess "vamp-ir" (compileArgs vampirFile dirPath) + P.callProcess "vamp-ir" (compileArgs vampirFile dirPath backend) step "VampIR prove" - P.callProcess "vamp-ir" (proveArgs dataFile dirPath) + P.callProcess "vamp-ir" (proveArgs dataFile dirPath backend) step "VampIR verify" - P.callProcess "vamp-ir" (verifyArgs dirPath) + P.callProcess "vamp-ir" (verifyArgs dirPath backend) ) -setupParamsArgs :: Int -> Path Abs Dir -> [String] -setupParamsArgs paramsNum dirPath = - [ "-q", - "plonk", - "setup", - "-m", - show paramsNum, - "-o", - toFilePath (dirPath $(mkRelFile "params.pp")) - ] +vampirSetupArgs :: VampirBackend -> Path Abs Dir -> (String -> IO ()) -> Assertion +vampirSetupArgs VampirHalo2 _ _ = return () +vampirSetupArgs VampirPlonk dirPath step = do + step "VampIR setup parameters" + P.callProcess "vamp-ir" setupParamsArgs + where + setupParamsArgs = + [ "-q", + "plonk", + "setup", + "-m", + "8", + "-o", + toFilePath (dirPath $(mkRelFile "params.pp")) + ] -compileArgs :: Path Abs File -> Path Abs Dir -> [String] -compileArgs inputFile dirPath = - [ "-q", - "plonk", - "compile", - "-u", - toFilePath (dirPath $(mkRelFile "params.pp")), - "-s", - toFilePath inputFile, - "-o", - toFilePath (dirPath $(mkRelFile "circuit.plonk")) - ] +compileArgs :: Path Abs File -> Path Abs Dir -> VampirBackend -> [String] +compileArgs inputFile dirPath = \case + VampirHalo2 -> + [ "-q", + "halo2", + "compile", + "-s", + toFilePath inputFile, + "-o", + toFilePath (dirPath $(mkRelFile "circuit.halo2")) + ] + VampirPlonk -> + [ "-q", + "plonk", + "compile", + "-u", + toFilePath (dirPath $(mkRelFile "params.pp")), + "-s", + toFilePath inputFile, + "-o", + toFilePath (dirPath $(mkRelFile "circuit.plonk")) + ] -proveArgs :: Path Abs File -> Path Abs Dir -> [String] -proveArgs dataFile dirPath = - [ "-q", - "plonk", - "prove", - "-u", - toFilePath (dirPath $(mkRelFile "params.pp")), - "-c", - toFilePath (dirPath $(mkRelFile "circuit.plonk")), - "-o", - toFilePath (dirPath $(mkRelFile "proof.plonk")), - "-i", - toFilePath dataFile - ] +proveArgs :: Path Abs File -> Path Abs Dir -> VampirBackend -> [String] +proveArgs dataFile dirPath = \case + VampirHalo2 -> + [ "-q", + "halo2", + "prove", + "-c", + toFilePath (dirPath $(mkRelFile "circuit.halo2")), + "-o", + toFilePath (dirPath $(mkRelFile "proof.halo2")), + "-i", + toFilePath dataFile + ] + VampirPlonk -> + [ "-q", + "plonk", + "prove", + "-u", + toFilePath (dirPath $(mkRelFile "params.pp")), + "-c", + toFilePath (dirPath $(mkRelFile "circuit.plonk")), + "-o", + toFilePath (dirPath $(mkRelFile "proof.plonk")), + "-i", + toFilePath dataFile + ] -verifyArgs :: Path Abs Dir -> [String] -verifyArgs dirPath = - [ "-q", - "plonk", - "verify", - "-u", - toFilePath (dirPath $(mkRelFile "params.pp")), - "-c", - toFilePath (dirPath $(mkRelFile "circuit.plonk")), - "-p", - toFilePath (dirPath $(mkRelFile "proof.plonk")) - ] +verifyArgs :: Path Abs Dir -> VampirBackend -> [String] +verifyArgs dirPath = \case + VampirHalo2 -> + [ "-q", + "halo2", + "verify", + "-c", + toFilePath (dirPath $(mkRelFile "circuit.halo2")), + "-p", + toFilePath (dirPath $(mkRelFile "proof.halo2")) + ] + VampirPlonk -> + [ "-q", + "plonk", + "verify", + "-u", + toFilePath (dirPath $(mkRelFile "params.pp")), + "-c", + toFilePath (dirPath $(mkRelFile "circuit.plonk")), + "-p", + toFilePath (dirPath $(mkRelFile "proof.plonk")) + ] diff --git a/test/VampIR/Core/Positive.hs b/test/VampIR/Core/Positive.hs index dff3ea7906..386c2ef41f 100644 --- a/test/VampIR/Core/Positive.hs +++ b/test/VampIR/Core/Positive.hs @@ -9,45 +9,47 @@ fromTest :: PosTest -> TestTree fromTest = mkTest . toTestDescr toTestDescr :: PosTest -> TestDescr -toTestDescr = Normalize.toTestDescr' vampirAssertion +toTestDescr = Normalize.toTestDescr' (vampirAssertion VampirHalo2) + +toPlonkTestDescr :: PosTest -> TestDescr +toPlonkTestDescr = Normalize.toTestDescr' (vampirAssertion VampirPlonk) allTests :: TestTree allTests = testGroup "Core to VampIR translation positive tests" - ( map - (mkTest . toTestDescr) - ( tests - ++ ( Normalize.filterOutTests - ( -- VampIR stack overflow - [ "Test020: functional queues", - "Test026: letrec" - ] - ++ - -- recursion takes too long - [ "Test014: recursion", - "Test015: tail recursion", - "Test016: tail recursion: Fibonacci numbers in linear time", - "Test017: recursion through higher-order functions", - "Test018: tail recursion through higher-order functions", - "Test022: mutual recursion" + ( map (mkTest . toPlonkTestDescr . (over Normalize.name (++ " (plonk)"))) tests + ++ map + (mkTest . toTestDescr) + ( tests + ++ ( Normalize.filterOutTests + ( -- VampIR stack overflow + [ "Test020: functional queues", + "Test026: letrec" ] - ) - Normalize.tests - ) - ) + ++ + -- recursion takes too long + [ "Test014: recursion", + "Test015: tail recursion", + "Test016: tail recursion: Fibonacci numbers in linear time", + "Test017: recursion through higher-order functions", + "Test018: tail recursion through higher-order functions", + "Test022: mutual recursion" + ] + ) + Normalize.tests + ) + ) ) tests :: [PosTest] tests = [ PosTest - 5 "Test001" $(mkRelDir "translation") $(mkRelFile "test001.jvc") $(mkRelFile "data/test001.json"), PosTest - 5 "Test002" $(mkRelDir "translation") $(mkRelFile "test002.jvc")