Generate SSD ZIP imports from typed Jerboa

ober

7c5895de39d429c2735c60bb2683a57a3e759040

diff --git a/templates/ssd-review.ss b/templates/ssd-review.ss
index 41824c7..1b0a6fb 100644
--- a/templates/ssd-review.ss
+++ b/templates/ssd-review.ss
@@ -15559,10 +15559,12 @@
                       (android content res AssetManager)
                       (android util Base64)
                       (java io File)
+                      (java io BufferedInputStream)
                       (java io BufferedOutputStream)
                       (java io InputStream)
                       (java io OutputStream)
                       (java net URL)
+                      (java nio file Files)
                       (java nio file LinkOption)
                       (java nio file Path)
                       (java security MessageDigest)
@@ -15589,6 +15591,7 @@
                 truthStoreTruthIndexEntriesLocal
                 truthStoreTruthIndexEntryLocal
                 truthStoreExportZipLocal
+                truthStoreImportZipLocal
                 truthStoreReadResponseTextLocal
                 truthStoreWriteRemoteTruthLocal
                 truthStoreApplyLearnedGuessesLocal
@@ -15608,6 +15611,7 @@
                 truthStorePullRemoteDumpLocal)
         (type AssetManager)
         (type Any)
+        (type BufferedInputStream)
         (type BufferedOutputStream)
         (type Context)
         (type DateTimeFormatter)
@@ -15801,6 +15805,19 @@
                   (input : InputStream)
                   (limit : Int)) : InputStream
           (kotlin-call LimitedInputStream))
+        (extern (truthStoreLimitedInputStreamForZip
+                  (input : InputStream)
+                  (limit : Int)) : LimitedInputStream
+          (kotlin-call LimitedInputStream))
+        (extern (truthStoreBufferedLimitedInputStream
+                  (input : LimitedInputStream)) : BufferedInputStream
+          (kotlin-call BufferedInputStream))
+        (extern (truthStoreZipInputStream
+                  (input : BufferedInputStream)) : ZipInputStream
+          (kotlin-call ZipInputStream))
+        (extern (truthStoreZipInputStreamClose
+                  (zip : ZipInputStream)) : Unit
+          (kotlin-member-call close))
         (extern (truthStoreLimitedOutputStream
                   (output : OutputStream)
                   (limit : Int)) : OutputStream
@@ -15814,6 +15831,12 @@
         (extern (truthStoreZipEntry
                   (name : String)) : ZipEntry
           (kotlin-call ZipEntry))
+        (extern (truthStoreZipEntryName
+                  (entry : ZipEntry)) : String
+          (kotlin-member-get name))
+        (extern (truthStoreZipEntryTime
+                  (entry : ZipEntry)) : Int
+          (kotlin-member-get time))
         (extern (truthStoreZipPutNextEntry
                   (zip : ZipOutputStream)
                   (entry : ZipEntry)) : Unit
@@ -15891,6 +15914,10 @@
         (extern (truthStorePathToString
                   (path : Path)) : String
           (kotlin-member-call toString))
+        (extern (truthStoreFilesCreateTempDirectory
+                  (directory : Path)
+                  (prefix : String)) : Path
+          (kotlin-call Files createTempDirectory))
         (extern (truthStoreCreateTempFile
                   (prefix : String)
                   (suffix : String)
@@ -15899,6 +15926,9 @@
         (extern (truthStoreFileDelete
                   (file : File)) : Bool
           (kotlin-member-call delete))
+        (extern (truthStoreFileDeleteRecursively
+                  (file : File)) : Bool
+          (kotlin-member-call deleteRecursively))
         (extern (truthStoreNoFollowLinks) : LinkOption
           (kotlin-value LinkOption NOFOLLOW_LINKS))
         (extern (truthStoreIllegalArgumentException
@@ -16602,6 +16632,179 @@
                     budget
                     (truthStoreReviewsDir store)))
                 (truthStoreZipClose zip)))))
+        (def (truthStoreDeleteRecursivelyUnit
+               (file : File)) : Unit
+          (begin
+            (truthStoreFileDeleteRecursively file)
+            (begin)))
+        (def (truthStoreCreateImportStage
+               (store : TruthStore)) : File
+          (truthStorePathToFile
+            (truthStoreFilesCreateTempDirectory
+              (truthStoreFileToPath
+                (truthStoreContextCacheDir
+                  (truthStoreContext store)))
+              "ssd-import-")))
+        (def (truthStoreAccountZipEntry!
+               (budget : ImportBudget)) : Unit
+          (begin
+            (ImportBudget-entries-set!
+              budget
+              (+ (ImportBudget-entries budget) (int32 1)))
+            (if (zipEntryCountExceeded
+                  (ImportBudget-entries budget)
+                  (truthStoreMaxZipEntries))
+              (throw
+                (truthStoreIllegalStateException
+                  (zipEntryCountLimitExceededMessage
+                    (ImportBudget-entries budget)
+                    (truthStoreMaxZipEntries)))
+                Unit)
+              (begin))))
+        (def (truthStoreImportZipEntryLocal
+               (store : TruthStore)
+               (zip : ZipInputStream)
+               (stage : File)
+               (compressed : LimitedInputStream)
+               (budget : ImportBudget)
+               (staged : (MutableList StagedZipEntry))
+               (entry : ZipEntry)) : Unit
+          (begin
+            (truthStoreAccountZipEntry! budget)
+            (let ((name (truthStoreZipEntryName entry)))
+              (begin
+                (if (zipEntryNameUnsafe name)
+                  (throw
+                    (truthStoreIllegalStateException
+                      "Unsafe ZIP entry")
+                    Unit)
+                  (begin))
+                (if (zipEntryIsFile entry)
+                  (begin
+                    (if (zipEntryDeclaresExcessiveSize
+                          entry
+                          (truthStoreMaxZipEntryBytes)
+                          (truthStoreMaxRemoteZipBytes))
+                      (throw
+                        (truthStoreIllegalStateException
+                          "ZIP entry declares excessive size")
+                        Unit)
+                      (begin))
+                    (let ((stagedFile
+                            (truthStoreChildFile
+                              stage
+                              (int32->string
+                                (ImportBudget-entries budget)))))
+                      (begin
+                        (truthStoreStreamZipEntryLocal
+                          zip
+                          stagedFile
+                          compressed
+                          budget)
+                        (truthStoreValidateImportedFileLocal
+                          name
+                          stagedFile)
+                        (mutable-list-add!
+                          staged
+                          (make-StagedZipEntry
+                            name
+                            stagedFile
+                            (truthStoreZipEntryTime entry))))))
+                  (begin))))))
+        (def (truthStoreReadImportZipLocal
+               (store : TruthStore)
+               (input : InputStream)
+               (stage : File)
+               (budget : ImportBudget)
+               (staged : (MutableList StagedZipEntry))) : Unit
+          (let ((compressed
+                  (truthStoreLimitedInputStreamForZip
+                    input
+                    (truthStoreMaxRemoteZipBytes))))
+            (let ((zip
+                    (truthStoreZipInputStream
+                      (truthStoreBufferedLimitedInputStream compressed))))
+              (try-finally
+                (forEachZipEntry
+                  zip
+                  (lambda ((entry : ZipEntry))
+                    (truthStoreImportZipEntryLocal
+                      store
+                      zip
+                      stage
+                      compressed
+                      budget
+                      staged
+                      entry)))
+                (truthStoreZipInputStreamClose zip)))))
+        (def (truthStoreRequireImportStorageCapacity
+               (store : TruthStore)
+               (budget : ImportBudget)
+               (staged : (MutableList StagedZipEntry))) : Unit
+          (let ((current (truthStoreStorageStatsLocal store)))
+            (truthStoreRequired
+              (storageCapacityWithinQuota
+                (+ (StorageStats-files current) (list-size staged))
+                (+ (StorageStats-bytes current)
+                   (ImportBudget-expandedBytes budget))
+                (truthStoreMaxStorageFiles)
+                (truthStoreMaxStorageBytes))
+              "Storage quota exceeded")))
+        (def (truthStoreInstallStagedEntriesLocal
+               (store : TruthStore)
+               (staged : (MutableList StagedZipEntry))) : Int32
+          (countInstalledStagedZipEntries
+            staged
+            (lambda ((entry : StagedZipEntry))
+              (truthStoreInstallStagedZipEntryLocal store entry))))
+        (def (truthStoreFinishImportedZipLocal
+               (store : TruthStore)
+               (count : Int32)) : Unit
+          (begin
+            (if (positiveCount count)
+              (truthStoreInvalidateTruthIndexLocal store)
+              (begin))
+            (if (learnedExamplesShouldRebuild
+                  count
+                  (truthStoreChildFile
+                    (truthStoreLearnedDir store)
+                    (learnedExamplesFileName)))
+              (truthStoreRebuildLearnedExamplesLocal store)
+              (begin))))
+        (def (truthStoreImportZipWithStageLocal
+               (store : TruthStore)
+               (input : InputStream)
+               (stage : File)) : Int32
+          (let ((staged (mutable-list-empty StagedZipEntry))
+                (budget (make-ImportBudget (int32 0) (int 0))))
+            (begin
+              (truthStoreReadImportZipLocal
+                store
+                input
+                stage
+                budget
+                staged)
+              (truthStoreRequireImportStorageCapacity
+                store
+                budget
+                staged)
+              (let ((count
+                      (truthStoreInstallStagedEntriesLocal
+                        store
+                        staged)))
+                (begin
+                  (truthStoreFinishImportedZipLocal store count)
+                  count)))))
+        (def (truthStoreImportZipLocal
+               (store : TruthStore)
+               (input : InputStream)) : Int32
+          (let ((stage (truthStoreCreateImportStage store)))
+            (try-finally
+              (truthStoreImportZipWithStageLocal
+                store
+                input
+                stage)
+              (truthStoreDeleteRecursivelyUnit stage))))
         (def (truthStoreSeedBundledTruthLocal
                (store : TruthStore)
                (context : Context)) : Int32
@@ -16611,7 +16814,7 @@
                       (truthStoreContextAssets context)
                       "seed_ssd_review.zip")))
               (try-finally
-                (truthStoreImportZipRaw store input)
+                (truthStoreImportZipLocal store input)
                 (truthStoreInputStreamClose input)))
             (catch (error : Exception)
               (int32 0))))
@@ -17410,44 +17613,8 @@
        "    fun exportZip(out: OutputStream) ="
        "        truthStoreExportZipLocal(this, out)"
        ""
-       "    fun importZip(input: InputStream): Int {"
-       "        val stage = Files.createTempDirectory(context.cacheDir.toPath(), \"ssd-import-\").toFile()"
-       "        val staged = mutableListOf<StagedZipEntry>()"
-       "        val budget = ImportBudget(0, 0L)"
-       "        var count = 0"
-       "        try {"
-       "            val compressed = LimitedInputStream(input, MAX_REMOTE_ZIP_BYTES)"
-       "            ZipInputStream(BufferedInputStream(compressed)).use { zip ->"
-       "                forEachZipEntry(zip) { entry ->"
-       "                    budget.entries += 1"
-       "                    if (zipEntryCountExceeded(budget.entries, MAX_ZIP_ENTRIES)) throw IllegalStateException(zipEntryCountLimitExceededMessage(budget.entries, MAX_ZIP_ENTRIES))"
-       "                    val name = entry.name"
-       "                    if (zipEntryNameUnsafe(name)) {"
-       "                        throw IllegalStateException(\"Unsafe ZIP entry\")"
-       "                    }"
-       "                    if (zipEntryIsFile(entry)) {"
-       "                        if (zipEntryDeclaresExcessiveSize(entry, MAX_ZIP_ENTRY_BYTES, MAX_REMOTE_ZIP_BYTES)) {"
-       "                            throw IllegalStateException(\"ZIP entry declares excessive size\")"
-       "                        }"
-       "                        val stagedFile = File(stage, budget.entries.toString())"
-       "                        streamZipEntry(zip, stagedFile, compressed, budget)"
-       "                        validateImportedFile(name, stagedFile)"
-       "                        staged.add(StagedZipEntry(name, stagedFile, entry.time))"
-       "                    }"
-       "                }"
-       "            }"
-       "            val current = storageStats()"
-       "            require(storageCapacityWithinQuota(current.files + staged.size, current.bytes + budget.expandedBytes, MAX_STORAGE_FILES, MAX_STORAGE_BYTES)) { \"Storage quota exceeded\" }"
-       "            count += countInstalledStagedZipEntries(staged) { installStagedZipEntry(it) }"
-       "            if (positiveCount(count)) invalidateTruthIndex()"
-       "        } finally {"
-       "            stage.deleteRecursively()"
-       "        }"
-       "        if (learnedExamplesShouldRebuild(count, File(learnedDir, learnedExamplesFileName()))) {"
-       "            rebuildLearnedExamples()"
-       "        }"
-       "        return count"
-       "    }"
+       "    fun importZip(input: InputStream): Int ="
+       "        truthStoreImportZipLocal(this, input)"
        ""
        "    private fun streamZipEntry("
        "        zip: ZipInputStream,"
diff --git a/tests/ssd-security-test.sh b/tests/ssd-security-test.sh
index e820722..65b9c8b 100755
--- a/tests/ssd-security-test.sh
+++ b/tests/ssd-security-test.sh
@@ -57,7 +57,7 @@ require_generated_text 'truthStoreSha256Hex'
 require_generated_text 'textUtf8Bytes(key)'
 require_text 'StandardCopyOption.ATOMIC_MOVE'
 require_text 'LinkOption.NOFOLLOW_LINKS'
-require_text 'LimitedInputStream(input, MAX_REMOTE_ZIP_BYTES)'
+require_generated_text 'LimitedInputStream(input, MAX_REMOTE_ZIP_BYTES)'
 require_generated_text 'LimitedInputStream(connection.inputStream, MAX_HTTP_COMPRESSED_BYTES)'
 require_generated_text 'MAX_HTTP_COMPRESSED_BYTES: Long = ((2L * 1024L) * 1024L)'
 require_generated_text 'MAX_ZIP_ENTRY_BYTES: Long = ((4L * 1024L) * 1024L)'
@@ -66,8 +66,8 @@ require_generated_text 'MAX_ZIP_ENTRIES: Int = 512'
 require_generated_text 'MAX_COMPRESSION_RATIO: Long = 100L'
 require_generated_text 'MAX_STORAGE_BYTES: Long = ((128L * 1024L) * 1024L)'
 require_generated_text 'MAX_LEARNED_EXAMPLES: Int = 10000'
-require_text 'validateImportedFile(name, stagedFile)'
-require_text 'stage.deleteRecursively()'
+require_generated_text 'truthStoreValidateImportedFileLocal(name, stagedFile)'
+require_generated_text '_file.deleteRecursively()'
 
 reject_text 'http://'
 reject_text 'HttpURLConnection'