diff --git a/Benchmarks/Compile/lake-manifest.json b/Benchmarks/Compile/lake-manifest.json index bb381a33a..5c9402ede 100644 --- a/Benchmarks/Compile/lake-manifest.json +++ b/Benchmarks/Compile/lake-manifest.json @@ -132,10 +132,10 @@ "type": "git", "subDir": null, "scope": "", - "rev": "db25a8a21579d8211eec4347402721f5674bf2c1", + "rev": "e6e908bfd3af607ab44fb462fa2276a2c81addba", "name": "Blake3", "manifestFile": "lake-manifest.json", - "inputRev": "db25a8a21579d8211eec4347402721f5674bf2c1", + "inputRev": "e6e908bfd3af607ab44fb462fa2276a2c81addba", "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/argumentcomputer/LSpec", diff --git a/Benchmarks/RecursionDebug.lean b/Benchmarks/RecursionDebug.lean index 1b5bff892..9b3f04607 100644 --- a/Benchmarks/RecursionDebug.lean +++ b/Benchmarks/RecursionDebug.lean @@ -101,19 +101,24 @@ def proveConst (ixePath constName : String) (skipDeps : Bool) match aiurSystem.proveAddrWithEnv funIdx envHandle addr.hash with | .error e => IO.eprintln s!"proveAddrWithEnv failed: {e}"; return none | .ok (claimBytes, proof, _) => - -- `verify_claim`'s public input is the 32-G blake3 digest of the - -- serialized `Ix.Claim` (same recipe as `ix verify` / bench-typecheck). + -- `verify_claim`'s public input is the packed blake3 digest of the + -- serialized `Ix.Claim` (same recipe as `ix verify` / bench-typecheck: + -- 8 G elements of 4 LE bytes each, `ClaimHarness.packedDigestKey`). let digest := Address.blake3 claimBytes - pure (Aiur.buildClaim funIdx (digest.hash.data.map .ofUInt8) #[], proof) + pure (Aiur.buildClaim funIdx (IxVM.ClaimHarness.packedDigestKey digest) #[], proof) let t1 ← IO.monoNanosNow - let proofBytes := proof.toBytes - IO.println s!"inner prove: {secs t0 t1} s, proof {proofBytes.size} bytes" + IO.println s!"inner prove: {secs t0 t1} s, proof {proof.toBytes.size} bytes" -- Sanity: the inner proof must verify out-of-circuit before we chase the -- recursive verifier. match aiurSystem.verify claim proof with | .ok () => IO.println "inner proof verifies out-of-circuit: ok" | .error e => IO.eprintln s!"⚠ inner proof FAILS out-of-circuit verify: {e}" - return some (proofBytes, aiurSystem.vkBytes, MultiStark.serializeClaims #[claim]) + -- The in-circuit verifier consumes the per-query advice transport, not + -- the pruned-multiproof wire format. + match aiurSystem.proofToAdviceBytes claim proof with + | .error e => IO.eprintln s!"advice re-encoding failed: {e}"; return none + | .ok adviceBytes => + return some (adviceBytes, aiurSystem.vkBytes, MultiStark.serializeClaims #[claim]) def main (args : List String) : IO UInt32 := do let ixePath := (argStr args "--ixe").getD "init.ixe" diff --git a/Benchmarks/Typecheck.lean b/Benchmarks/Typecheck.lean index 4bdd9e125..8a177e454 100644 --- a/Benchmarks/Typecheck.lean +++ b/Benchmarks/Typecheck.lean @@ -595,10 +595,18 @@ def runTypecheckCmd (p : Cli.Parsed) : IO UInt32 := do let claimBytes := MultiStark.serializeClaims #[claim] let vkBytes := aiurSystem.vkBytes let pubInput := MultiStark.verifierPubInput vkBytes claimBytes + -- The in-circuit verifier consumes the per-query advice transport; + -- `proofBytes` (the pruned-multiproof wire format) stays the + -- reported proof size but is not parseable in-circuit. + let adviceBytes ← match aiurSystem.proofToAdviceBytes claim proof with + | .ok bytes => pure bytes + | .error e => + IO.eprintln s!" ❌ advice re-encoding for {r.name} FAILED: {e}" + continue -- Native path: the advice buffer is built in Rust from the raw -- byte blobs and execution routes through the codegen'd verifier. let (rvRes, rvSec) ← timed fun _ => - vCompiled.bytecode.executeMultiStark vIdx pubInput proofBytes + vCompiled.bytecode.executeMultiStark vIdx pubInput adviceBytes vkBytes claimBytes useInterp match rvRes with | .error e => @@ -624,7 +632,7 @@ def runTypecheckCmd (p : Cli.Parsed) : IO UInt32 := do (← IO.getStdout).flush TracingTexray.resetPeakTreeRss let ((rvClaim, rvProof), rvProveSec) ← timed fun _ => - vSystem.proveMultiStark vIdx pubInput proofBytes vkBytes + vSystem.proveMultiStark vIdx pubInput adviceBytes vkBytes claimBytes useInterp let rvPeak ← TracingTexray.peakTreeRssBytes let rvProofBytes := Aiur.Proof.toBytes rvProof diff --git a/Cargo.lock b/Cargo.lock index eebdffbbc..581bc3ce1 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -54,7 +54,7 @@ dependencies = [ "indexmap", "libc", "multi-stark", - "num-bigint", + "num-bigint 0.4.6", "rayon", "rustc-hash", "tracing", @@ -190,9 +190,9 @@ checksum = "2af50177e190e07a26ab74f8b1efbfe2ef87da2116221318cb1c2e82baf7de06" [[package]] name = "bignat" version = "0.1.0" -source = "git+https://github.com/argumentcomputer/lean-ffi.git?rev=2a9c91eba44ea791978a086a6a19b3a922edfee5#2a9c91eba44ea791978a086a6a19b3a922edfee5" +source = "git+https://github.com/argumentcomputer/lean-ffi.git?rev=93c7e52952ae94546be08313f4ff3922984c84d5#93c7e52952ae94546be08313f4ff3922984c84d5" dependencies = [ - "num-bigint", + "num-bigint 0.4.6", ] [[package]] @@ -331,6 +331,17 @@ version = "0.2.1" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "613afe47fcd5fac7ccf1db93babcb082c5994d996f20b8b159f2ad1658eb5724" +[[package]] +name = "chacha20" +version = "0.10.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "d524456ba66e72eb8b115ff89e01e497f8e6d11d78b70b1aa13c0fbd97540a81" +dependencies = [ + "cfg-if", + "cpufeatures 0.3.0", + "rand_core 0.10.1", +] + [[package]] name = "chrono" version = "0.4.44" @@ -1735,6 +1746,15 @@ dependencies = [ "either", ] +[[package]] +name = "itertools" +version = "0.15.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "8b4baf93f58d4425749ca49a51c50ebab072c5df6994d08fed93541c331481dc" +dependencies = [ + "either", +] + [[package]] name = "itoa" version = "1.0.18" @@ -1774,7 +1794,7 @@ dependencies = [ "ix-common", "ix-kernel", "ixon", - "num-bigint", + "num-bigint 0.4.6", "rayon", "rustc-hash", "sha2 0.10.9", @@ -1807,7 +1827,7 @@ dependencies = [ "mimalloc", "multi-stark", "n0-error", - "num-bigint", + "num-bigint 0.4.6", "rayon", "rustc-hash", "serde", @@ -1839,7 +1859,7 @@ dependencies = [ "ix-common", "ixon", "log", - "num-bigint", + "num-bigint 0.4.6", "quickcheck", "quickcheck_macros", "rayon", @@ -1857,7 +1877,7 @@ dependencies = [ "ix-common", "memmap2", "nom", - "num-bigint", + "num-bigint 0.4.6", "quickcheck", "quickcheck_macros", "rayon", @@ -1875,7 +1895,7 @@ dependencies = [ "ix-common", "ixon", "multi-stark", - "num-bigint", + "num-bigint 0.4.6", "rayon", "rustc-hash", "stacker", @@ -1902,12 +1922,12 @@ checksum = "bbd2bcb4c963f2ddae06a2efc7e9f3591312473c50c6685e1f298068316e66fe" [[package]] name = "lean-ffi" version = "0.1.0" -source = "git+https://github.com/argumentcomputer/lean-ffi.git?rev=2a9c91eba44ea791978a086a6a19b3a922edfee5#2a9c91eba44ea791978a086a6a19b3a922edfee5" +source = "git+https://github.com/argumentcomputer/lean-ffi.git?rev=93c7e52952ae94546be08313f4ff3922984c84d5#93c7e52952ae94546be08313f4ff3922984c84d5" dependencies = [ "bignat", "bindgen", "cc", - "num-bigint", + "num-bigint 0.4.6", ] [[package]] @@ -2084,9 +2104,10 @@ dependencies = [ [[package]] name = "multi-stark" version = "0.1.0" -source = "git+https://github.com/argumentcomputer/multi-stark.git?rev=c72d32130eb084327b73849e39c92734a8829011#c72d32130eb084327b73849e39c92734a8829011" +source = "git+https://github.com/argumentcomputer/multi-stark.git?rev=249b74053c9dac775c5954af7d01fd3dae9d98ed#249b74053c9dac775c5954af7d01fd3dae9d98ed" dependencies = [ "bincode", + "num-bigint 0.5.1", "p3-air", "p3-blake3", "p3-challenger", @@ -2369,6 +2390,16 @@ dependencies = [ "num-traits", ] +[[package]] +name = "num-bigint" +version = "0.5.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "93e7820bc0a80a0238e650327316f929ba18d5be054b647490a3a6a339f3e7c0" +dependencies = [ + "num-integer", + "num-traits", +] + [[package]] name = "num-conv" version = "0.2.1" @@ -2504,18 +2535,19 @@ checksum = "c08d65885ee38876c4f86fa503fb49d7b507c2b62552df7c70b2fce627e06381" [[package]] name = "p3-air" -version = "0.5.1" -source = "git+https://github.com/Plonky3/Plonky3?rev=e9d75614dd6816f9b5dbb4413c69be63536efd64#e9d75614dd6816f9b5dbb4413c69be63536efd64" +version = "0.6.0" +source = "git+https://github.com/Plonky3/Plonky3?rev=3c84c158c0939345a3becba60a387643935593d2#3c84c158c0939345a3becba60a387643935593d2" dependencies = [ "p3-field", "p3-matrix", + "serde", "tracing", ] [[package]] name = "p3-blake3" -version = "0.5.1" -source = "git+https://github.com/Plonky3/Plonky3?rev=e9d75614dd6816f9b5dbb4413c69be63536efd64#e9d75614dd6816f9b5dbb4413c69be63536efd64" +version = "0.6.0" +source = "git+https://github.com/Plonky3/Plonky3?rev=3c84c158c0939345a3becba60a387643935593d2#3c84c158c0939345a3becba60a387643935593d2" dependencies = [ "blake3", "p3-symmetric", @@ -2524,12 +2556,11 @@ dependencies = [ [[package]] name = "p3-challenger" -version = "0.5.1" -source = "git+https://github.com/Plonky3/Plonky3?rev=e9d75614dd6816f9b5dbb4413c69be63536efd64#e9d75614dd6816f9b5dbb4413c69be63536efd64" +version = "0.6.0" +source = "git+https://github.com/Plonky3/Plonky3?rev=3c84c158c0939345a3becba60a387643935593d2#3c84c158c0939345a3becba60a387643935593d2" dependencies = [ "p3-field", "p3-maybe-rayon", - "p3-monty-31", "p3-symmetric", "p3-util", "tracing", @@ -2537,40 +2568,38 @@ dependencies = [ [[package]] name = "p3-commit" -version = "0.5.1" -source = "git+https://github.com/Plonky3/Plonky3?rev=e9d75614dd6816f9b5dbb4413c69be63536efd64#e9d75614dd6816f9b5dbb4413c69be63536efd64" +version = "0.6.0" +source = "git+https://github.com/Plonky3/Plonky3?rev=3c84c158c0939345a3becba60a387643935593d2#3c84c158c0939345a3becba60a387643935593d2" dependencies = [ - "itertools 0.14.0", - "p3-challenger", - "p3-dft", + "itertools 0.15.0", "p3-field", - "p3-interpolation", "p3-matrix", + "p3-multilinear-util", "p3-util", "serde", ] [[package]] name = "p3-dft" -version = "0.5.1" -source = "git+https://github.com/Plonky3/Plonky3?rev=e9d75614dd6816f9b5dbb4413c69be63536efd64#e9d75614dd6816f9b5dbb4413c69be63536efd64" +version = "0.6.0" +source = "git+https://github.com/Plonky3/Plonky3?rev=3c84c158c0939345a3becba60a387643935593d2#3c84c158c0939345a3becba60a387643935593d2" dependencies = [ - "itertools 0.14.0", + "itertools 0.15.0", "p3-field", "p3-matrix", "p3-maybe-rayon", "p3-util", - "spin 0.10.1", + "spin 0.12.3", "tracing", ] [[package]] name = "p3-field" -version = "0.5.1" -source = "git+https://github.com/Plonky3/Plonky3?rev=e9d75614dd6816f9b5dbb4413c69be63536efd64#e9d75614dd6816f9b5dbb4413c69be63536efd64" +version = "0.6.0" +source = "git+https://github.com/Plonky3/Plonky3?rev=3c84c158c0939345a3becba60a387643935593d2#3c84c158c0939345a3becba60a387643935593d2" dependencies = [ - "itertools 0.14.0", - "num-bigint", + "itertools 0.15.0", + "num-bigint 0.5.1", "p3-maybe-rayon", "p3-util", "paste", @@ -2581,32 +2610,31 @@ dependencies = [ [[package]] name = "p3-fri" -version = "0.5.1" -source = "git+https://github.com/Plonky3/Plonky3?rev=e9d75614dd6816f9b5dbb4413c69be63536efd64#e9d75614dd6816f9b5dbb4413c69be63536efd64" +version = "0.6.0" +source = "git+https://github.com/Plonky3/Plonky3?rev=3c84c158c0939345a3becba60a387643935593d2#3c84c158c0939345a3becba60a387643935593d2" dependencies = [ - "itertools 0.14.0", + "itertools 0.15.0", "p3-challenger", "p3-commit", "p3-dft", "p3-field", - "p3-interpolation", "p3-matrix", "p3-maybe-rayon", + "p3-security", "p3-util", "rand 0.10.1", "serde", - "spin 0.10.1", + "spin 0.12.3", "thiserror", "tracing", ] [[package]] name = "p3-goldilocks" -version = "0.5.1" -source = "git+https://github.com/Plonky3/Plonky3?rev=e9d75614dd6816f9b5dbb4413c69be63536efd64#e9d75614dd6816f9b5dbb4413c69be63536efd64" +version = "0.6.0" +source = "git+https://github.com/Plonky3/Plonky3?rev=3c84c158c0939345a3becba60a387643935593d2#3c84c158c0939345a3becba60a387643935593d2" dependencies = [ - "num-bigint", - "p3-challenger", + "num-bigint 0.5.1", "p3-dft", "p3-field", "p3-mds", @@ -2617,23 +2645,13 @@ dependencies = [ "paste", "rand 0.10.1", "serde", -] - -[[package]] -name = "p3-interpolation" -version = "0.5.1" -source = "git+https://github.com/Plonky3/Plonky3?rev=e9d75614dd6816f9b5dbb4413c69be63536efd64#e9d75614dd6816f9b5dbb4413c69be63536efd64" -dependencies = [ - "p3-field", - "p3-matrix", - "p3-maybe-rayon", - "p3-util", + "spin 0.12.3", ] [[package]] name = "p3-keccak" -version = "0.5.1" -source = "git+https://github.com/Plonky3/Plonky3?rev=e9d75614dd6816f9b5dbb4413c69be63536efd64#e9d75614dd6816f9b5dbb4413c69be63536efd64" +version = "0.6.0" +source = "git+https://github.com/Plonky3/Plonky3?rev=3c84c158c0939345a3becba60a387643935593d2#3c84c158c0939345a3becba60a387643935593d2" dependencies = [ "p3-symmetric", "p3-util", @@ -2642,10 +2660,10 @@ dependencies = [ [[package]] name = "p3-matrix" -version = "0.5.1" -source = "git+https://github.com/Plonky3/Plonky3?rev=e9d75614dd6816f9b5dbb4413c69be63536efd64#e9d75614dd6816f9b5dbb4413c69be63536efd64" +version = "0.6.0" +source = "git+https://github.com/Plonky3/Plonky3?rev=3c84c158c0939345a3becba60a387643935593d2#3c84c158c0939345a3becba60a387643935593d2" dependencies = [ - "itertools 0.14.0", + "itertools 0.15.0", "p3-field", "p3-maybe-rayon", "p3-util", @@ -2656,16 +2674,16 @@ dependencies = [ [[package]] name = "p3-maybe-rayon" -version = "0.5.1" -source = "git+https://github.com/Plonky3/Plonky3?rev=e9d75614dd6816f9b5dbb4413c69be63536efd64#e9d75614dd6816f9b5dbb4413c69be63536efd64" +version = "0.6.0" +source = "git+https://github.com/Plonky3/Plonky3?rev=3c84c158c0939345a3becba60a387643935593d2#3c84c158c0939345a3becba60a387643935593d2" dependencies = [ "rayon", ] [[package]] name = "p3-mds" -version = "0.5.1" -source = "git+https://github.com/Plonky3/Plonky3?rev=e9d75614dd6816f9b5dbb4413c69be63536efd64#e9d75614dd6816f9b5dbb4413c69be63536efd64" +version = "0.6.0" +source = "git+https://github.com/Plonky3/Plonky3?rev=3c84c158c0939345a3becba60a387643935593d2#3c84c158c0939345a3becba60a387643935593d2" dependencies = [ "p3-dft", "p3-field", @@ -2676,10 +2694,10 @@ dependencies = [ [[package]] name = "p3-merkle-tree" -version = "0.5.1" -source = "git+https://github.com/Plonky3/Plonky3?rev=e9d75614dd6816f9b5dbb4413c69be63536efd64#e9d75614dd6816f9b5dbb4413c69be63536efd64" +version = "0.6.0" +source = "git+https://github.com/Plonky3/Plonky3?rev=3c84c158c0939345a3becba60a387643935593d2#3c84c158c0939345a3becba60a387643935593d2" dependencies = [ - "itertools 0.14.0", + "itertools 0.15.0", "p3-commit", "p3-field", "p3-matrix", @@ -2688,47 +2706,41 @@ dependencies = [ "p3-util", "rand 0.10.1", "serde", + "spin 0.12.3", "thiserror", "tracing", ] [[package]] -name = "p3-monty-31" -version = "0.5.1" -source = "git+https://github.com/Plonky3/Plonky3?rev=e9d75614dd6816f9b5dbb4413c69be63536efd64#e9d75614dd6816f9b5dbb4413c69be63536efd64" +name = "p3-multilinear-util" +version = "0.6.0" +source = "git+https://github.com/Plonky3/Plonky3?rev=3c84c158c0939345a3becba60a387643935593d2#3c84c158c0939345a3becba60a387643935593d2" dependencies = [ - "itertools 0.14.0", - "num-bigint", - "p3-dft", + "itertools 0.15.0", "p3-field", "p3-matrix", "p3-maybe-rayon", - "p3-mds", - "p3-poseidon1", - "p3-poseidon2", - "p3-symmetric", "p3-util", - "paste", "rand 0.10.1", "serde", - "spin 0.10.1", "tracing", ] [[package]] name = "p3-poseidon1" -version = "0.5.1" -source = "git+https://github.com/Plonky3/Plonky3?rev=e9d75614dd6816f9b5dbb4413c69be63536efd64#e9d75614dd6816f9b5dbb4413c69be63536efd64" +version = "0.6.0" +source = "git+https://github.com/Plonky3/Plonky3?rev=3c84c158c0939345a3becba60a387643935593d2#3c84c158c0939345a3becba60a387643935593d2" dependencies = [ "p3-field", + "p3-mds", "p3-symmetric", "rand 0.10.1", ] [[package]] name = "p3-poseidon2" -version = "0.5.1" -source = "git+https://github.com/Plonky3/Plonky3?rev=e9d75614dd6816f9b5dbb4413c69be63536efd64#e9d75614dd6816f9b5dbb4413c69be63536efd64" +version = "0.6.0" +source = "git+https://github.com/Plonky3/Plonky3?rev=3c84c158c0939345a3becba60a387643935593d2#3c84c158c0939345a3becba60a387643935593d2" dependencies = [ "p3-field", "p3-mds", @@ -2737,12 +2749,24 @@ dependencies = [ "rand 0.10.1", ] +[[package]] +name = "p3-security" +version = "0.6.0" +source = "git+https://github.com/Plonky3/Plonky3?rev=3c84c158c0939345a3becba60a387643935593d2#3c84c158c0939345a3becba60a387643935593d2" +dependencies = [ + "libm", + "p3-air", + "p3-field", + "p3-util", + "serde", +] + [[package]] name = "p3-symmetric" -version = "0.5.1" -source = "git+https://github.com/Plonky3/Plonky3?rev=e9d75614dd6816f9b5dbb4413c69be63536efd64#e9d75614dd6816f9b5dbb4413c69be63536efd64" +version = "0.6.0" +source = "git+https://github.com/Plonky3/Plonky3?rev=3c84c158c0939345a3becba60a387643935593d2#3c84c158c0939345a3becba60a387643935593d2" dependencies = [ - "itertools 0.14.0", + "itertools 0.15.0", "p3-field", "p3-util", "serde", @@ -2750,11 +2774,11 @@ dependencies = [ [[package]] name = "p3-util" -version = "0.5.1" -source = "git+https://github.com/Plonky3/Plonky3?rev=e9d75614dd6816f9b5dbb4413c69be63536efd64#e9d75614dd6816f9b5dbb4413c69be63536efd64" +version = "0.6.0" +source = "git+https://github.com/Plonky3/Plonky3?rev=3c84c158c0939345a3becba60a387643935593d2#3c84c158c0939345a3becba60a387643935593d2" dependencies = [ + "p3-maybe-rayon", "serde", - "transpose", ] [[package]] @@ -3156,6 +3180,7 @@ version = "0.10.1" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "d2e8e8bcc7961af1fdac401278c6a831614941f6164ee3bf4ce61b7edb162207" dependencies = [ + "chacha20", "getrandom 0.4.2", "rand_core 0.10.1", ] @@ -3612,6 +3637,12 @@ name = "spin" version = "0.10.1" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "023a211cb3138dbc438680b32560ad89f699977624c9f8dbb95a47d5b4c07dd3" + +[[package]] +name = "spin" +version = "0.12.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "0134f9043ed38b087ac4f7d4af44c79e2c9e5094421fe3164f435ce585953b10" dependencies = [ "lock_api", ] @@ -3645,12 +3676,6 @@ dependencies = [ "windows-sys 0.61.2", ] -[[package]] -name = "strength_reduce" -version = "0.2.4" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "fe895eb47f22e2ddd4dabc02bce419d2e643c8e3b585c78158b349195bc24d82" - [[package]] name = "strsim" version = "0.11.1" @@ -4062,16 +4087,6 @@ dependencies = [ "tracing-subscriber", ] -[[package]] -name = "transpose" -version = "0.2.3" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "1ad61aed86bc3faea4300c7aee358b4c6d0c8d6ccc36524c96e4c92ccf26e77e" -dependencies = [ - "num-integer", - "strength_reduce", -] - [[package]] name = "try-lock" version = "0.2.5" diff --git a/Cargo.toml b/Cargo.toml index f535dd771..8d5288835 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -42,8 +42,8 @@ ixon = { path = "crates/ixon" } ix-kernel = { path = "crates/kernel" } # lean-ffi tree (lean-ffi crate + factored-out bignat sub-crate) -bignat = { git = "https://github.com/argumentcomputer/lean-ffi.git", rev = "2a9c91eba44ea791978a086a6a19b3a922edfee5" } -lean-ffi = { git = "https://github.com/argumentcomputer/lean-ffi.git", rev = "2a9c91eba44ea791978a086a6a19b3a922edfee5" } +bignat = { git = "https://github.com/argumentcomputer/lean-ffi.git", rev = "93c7e52952ae94546be08313f4ff3922984c84d5" } +lean-ffi = { git = "https://github.com/argumentcomputer/lean-ffi.git", rev = "93c7e52952ae94546be08313f4ff3922984c84d5" } # External shared deps anyhow = "1" @@ -56,7 +56,7 @@ libc = "0.2" log = "0.4" memmap2 = "0.9" mimalloc = { version = "0.1", default-features = false } -multi-stark = { git = "https://github.com/argumentcomputer/multi-stark.git", rev = "c72d32130eb084327b73849e39c92734a8829011" } +multi-stark = { git = "https://github.com/argumentcomputer/multi-stark.git", rev = "249b74053c9dac775c5954af7d01fd3dae9d98ed" } nom = "7.1.3" num-bigint = "0.4.6" quickcheck = "1.0.3" @@ -98,7 +98,6 @@ filter_map_next = "warn" flat_map_option = "warn" fn_to_numeric_cast = "warn" fn_to_numeric_cast_with_truncation = "warn" -from_iter_instead_of_collect = "warn" implicit_clone = "warn" inefficient_to_string = "warn" invalid_upcast_comparisons = "warn" diff --git a/Ix/Aiur/Protocol.lean b/Ix/Aiur/Protocol.lean index 57f954a8c..0271e3bf1 100644 --- a/Ix/Aiur/Protocol.lean +++ b/Ix/Aiur/Protocol.lean @@ -189,6 +189,13 @@ def shardProveWithEnv (system : @& AiurSystem) opaque verify : @& AiurSystem → @& Array G → @& Proof → Except String Unit +/-- The proof re-encoded in the per-query advice transport the in-circuit +verifier consumes (pruned FRI multiproofs expanded to one authentication +path per query); errors if the proof does not verify natively. -/ +@[extern "rs_aiur_proof_to_advice_bytes"] +opaque proofToAdviceBytes : @& AiurSystem → + @& Array G → @& Proof → Except String ByteArray + end AiurSystem namespace Bytecode.Toplevel diff --git a/Ix/MultiStark/SystemDeserialize.lean b/Ix/MultiStark/SystemDeserialize.lean index 05ff6c915..7e30323ad 100644 --- a/Ix/MultiStark/SystemDeserialize.lean +++ b/Ix/MultiStark/SystemDeserialize.lean @@ -43,10 +43,11 @@ deserializer calls are constrained, so the public `system_digest` binds every value reconstructed below. Per-node degrees are neither serialized nor needed (the node sweep just evaluates the graph). -The Fiat-Shamir shape limbs (`observe_shape`): the circuit count then, -per circuit, the seven words constraint_count, max_constraint_degree, -preprocessed_height, preprocessed_width, main_width, stage_2_width, -lookup_group_size (as 8-byte LE limbs). +The Fiat-Shamir shape limbs (`observe_shape`): the width-binding policy +word, the circuit count, then per circuit the seven words +constraint_count, max_constraint_degree, preprocessed_height, +preprocessed_width, main_width, stage_2_width, lookup_group_size (as +8-byte LE limbs). -/ public section @@ -97,7 +98,8 @@ def systemDeserialize := ⟦ -- preprocessed_indices. The transcript limbs are the u64 words the -- challenger observes before any commitment — the 7 parameters (bound via -- the challenger seed) followed by the system shape (`observe_shape`: the - -- circuit count, then 6 metadata words per circuit) — kept as limbs because + -- width-binding policy word, the circuit count, then 7 metadata words per + -- circuit) — kept as limbs because -- the Fiat-Shamir replay needs their little-endian bytes. enum Sys { Mk(SysParams, List‹U64›, List‹SysCircuit›, OptCommit, List‹OptIdx›) } @@ -316,7 +318,12 @@ def systemDeserialize := ⟦ fn read_sys_lookup(i: ByteStream) -> (SysLookup, ByteStream) { let (m, i1) = read_vk_u16(i); - let (ac, i2) = read_vk_u16(i1); + -- The declared per-row multiplicity bound (u64 LE). It feeds the logUp + -- height bound, which the native verifier enforces; the in-circuit + -- verifier does not enforce it yet, so the value is parsed past and + -- bound only through the vk digest. + let (_mm, i1b) = read_vk_u64(i1); + let (ac, i2) = read_vk_u16(i1b); let (args, i3) = read_node_ids_n(i2, ac); (SysLookup.Mk(m, args), i3) } @@ -450,8 +457,13 @@ def systemDeserialize := ⟦ let (circuits, climbs, j2) = read_sys_circuits_n(j1, n); let (commit, j3) = read_opt_commit(j2); let (indices, j4) = read_opt_idx_n(j3, n); + -- The width-binding policy is the first `observe_shape` word. Aiur + -- declares `WidthBinding::ByConstruction` (discriminant 1); the plain + -- Horner fold in `logup_fingerprint` is the matching message shape. + let wblimb = @gl_to_bytes(1); (Sys.Mk(params, - list_concat(plimbs, store(ListNode.Cons(nlimb, climbs))), + list_concat(plimbs, + store(ListNode.Cons(wblimb, store(ListNode.Cons(nlimb, climbs))))), circuits, commit, indices), j4) } diff --git a/Ix/MultiStark/Verifier.lean b/Ix/MultiStark/Verifier.lean index b11b6a79e..6bbac80b8 100644 --- a/Ix/MultiStark/Verifier.lean +++ b/Ix/MultiStark/Verifier.lean @@ -308,8 +308,9 @@ def verifier := ⟦ -- Replay the verifier transcript and derive the four challenges -- `(lookup, fingerprint, alpha, zeta)`. Mirrors `verify_multiple_claims`'s -- challenger sequence exactly: - -- seed = tag + protocol parameters; observe_shape (circuit count + 6 - -- metadata words per circuit) → preprocessed_commit (if any) → stage_1 → + -- seed = tag + protocol parameters; observe_shape (width-binding policy + -- word, circuit count, 7 metadata words per circuit) → preprocessed_commit + -- (if any) → stage_1 → -- log_degrees → length-prefixed claims; -- sample lookup, observe it; sample fingerprint, observe it; -- observe stage_2; observe the intermediate accumulators; sample α; @@ -602,7 +603,9 @@ def verifier := ⟦ @eg_add(@eg_mul(a0, b1), @eg_mul(a1, b0))) } - -- fingerprint(γ, args) = Σᵢ argsᵢ·γ^i as a coordinate pair: + -- fingerprint(γ, args) = Σᵢ argsᵢ·γ^i as a coordinate pair — the plain + -- Horner fold of `WidthBinding::ByConstruction`, the policy aiur declares + -- (and the transcript replay observes): -- fp(Cons(a, rest)) = (eval a, 0) + γ ⊗ fp(rest); args embed in coord 0. fn logup_fingerprint(args: List‹G›, g0: Ext, g1: Ext, nodes: List‹SysNode›, main: List‹Ext›, main_next: List‹Ext›, prep: List‹Ext›, prep_next: List‹Ext›, diff --git a/Tests/MultiStark.lean b/Tests/MultiStark.lean index a1b09e149..94393d35f 100644 --- a/Tests/MultiStark.lean +++ b/Tests/MultiStark.lean @@ -155,7 +155,11 @@ def endToEndSuite : IO UInt32 := do let input := #[Aiur.G.ofNat 5] let (claim, proof, _) := facSystem.prove facIdx input default let expectedClaim := buildClaim facIdx input #[Aiur.G.ofNat 120] - let proofBytes := proof.toBytes + -- The in-circuit verifier consumes the per-query advice transport, not + -- the pruned-multiproof wire format `Proof.toBytes` carries. + let proofBytes ← match facSystem.proofToAdviceBytes claim proof with + | .ok bytes => pure bytes + | .error e => IO.eprintln s!"advice re-encoding failed: {e}"; return 1 -- ── serialize proof (advice) + vk + claims, with public Blake3 digests ── let proofGs : Array Aiur.G := proofBytes.data.map .ofUInt8 @@ -199,7 +203,9 @@ def endToEndSuite : IO UInt32 := do -- ── run the (expensive) checks, then assert ───────────────────────────────── IO.println "recursive-verifier (proving + recursive verification, ~1.5 min)…" - let innerVerify := facSystem.verify claim (.ofBytes proofBytes) + -- Native wire-format roundtrip; the in-circuit paths below consume the + -- per-query advice encoding instead. + let innerVerify := facSystem.verify claim (.ofBytes proof.toBytes) -- Native path: Rust-built advice buffer + codegen'd verifier -- (`crates/ixvm-codegen/src/aiur_multi_stark.rs`). let honest := diff --git a/crates/aiur/src/constraints.rs b/crates/aiur/src/constraints.rs index 26488ce50..f4a708cca 100644 --- a/crates/aiur/src/constraints.rs +++ b/crates/aiur/src/constraints.rs @@ -164,7 +164,10 @@ impl Toplevel { } fn empty_lookup() -> Lookup { - Lookup { multiplicity: konst(G::ZERO), args: vec![] } + // Slots accumulate mutually-exclusive branch selectors, so the per-row + // multiplicity is 0 or ±1; the function's return slot (a committed count + // column) overrides this with `COUNT_COLUMN_BUDGET`. + Lookup { multiplicity: konst(G::ZERO), args: vec![], max_multiplicity: 1 } } impl Function { @@ -182,6 +185,7 @@ impl Function { state.column += 1; // the return lookup occupies the first lookup slot state.lookups[0].multiplicity = -multiplicity.clone(); + state.lookups[0].max_multiplicity = crate::COUNT_COLUMN_BUDGET; state.lookup += 1; self.body.collect_constraints(self.body.get_block_selector(state), state); } diff --git a/crates/aiur/src/execute.rs b/crates/aiur/src/execute.rs index 3037a1d52..96f81c08b 100644 --- a/crates/aiur/src/execute.rs +++ b/crates/aiur/src/execute.rs @@ -209,7 +209,7 @@ fn dump_query_stats(record: &QueryRecord, tag: &str) { .map(|(i, m)| (i, m.len(), m.retained_elems())) .filter(|(_, n, _)| *n > 0) .collect(); - rows.sort_by(|a, b| b.2.cmp(&a.2)); + rows.sort_by_key(|r| std::cmp::Reverse(r.2)); let total_entries: usize = rows.iter().map(|r| r.1).sum(); let total_elems: usize = rows.iter().map(|r| r.2).sum(); eprintln!( @@ -1052,14 +1052,7 @@ fn biguint_to_klimbs_u64(n: &num_bigint::BigUint) -> Vec { while !bytes.len().is_multiple_of(8) { bytes.push(0); } - bytes - .chunks_exact(8) - .map(|c| { - let mut a = [0u8; 8]; - a.copy_from_slice(c); - u64::from_le_bytes(a) - }) - .collect() + bytes.as_chunks::<8>().0.iter().map(|c| u64::from_le_bytes(*c)).collect() } /// Build a `List` chain in `memory[10]` from `limbs` (head-first order) diff --git a/crates/aiur/src/gadgets/bytes1.rs b/crates/aiur/src/gadgets/bytes1.rs index 667cb8ad9..4765ca953 100644 --- a/crates/aiur/src/gadgets/bytes1.rs +++ b/crates/aiur/src/gadgets/bytes1.rs @@ -49,8 +49,12 @@ impl AiurGadget for Bytes1 { /// Builds the preprocessed trace over all 256 byte values. fn preprocessed(&self) -> Option> { let mut values = vec![G::ZERO; 256 * PREPROCESSED_TRACE_WIDTH]; - values.chunks_exact_mut(PREPROCESSED_TRACE_WIDTH).enumerate().for_each( - |(i, row)| { + values + .as_chunks_mut::() + .0 + .iter_mut() + .enumerate() + .for_each(|(i, row)| { let byte = G::from_usize(i); // Raw byte value @@ -68,8 +72,7 @@ impl AiurGadget for Bytes1 { // Byte shifted right row[10] = Self::shift_right(&byte); - }, - ); + }); Some(RowMajorMatrix::new(values, PREPROCESSED_TRACE_WIDTH)) } @@ -136,16 +139,19 @@ impl AiurGadget for Bytes1 { byte_bit6, byte_bit7, ], + max_multiplicity: crate::COUNT_COLUMN_BUDGET, }; let pull_shift_left = Lookup { multiplicity: -shift_left_multiplicity, args: vec![shift_left_channel, byte.clone(), byte_left_shifted], + max_multiplicity: crate::COUNT_COLUMN_BUDGET, }; let pull_shift_right = Lookup { multiplicity: -shift_right_multiplicity, args: vec![shift_right_channel, byte, byte_right_shifted], + max_multiplicity: crate::COUNT_COLUMN_BUDGET, }; vec![pull_bit_decomposition, pull_shift_left, pull_shift_right] @@ -168,7 +174,9 @@ impl AiurGadget for Bytes1 { // There are at most 256 rows so parallelism is not necessay. rows - .chunks_exact_mut(TRACE_WIDTH) + .as_chunks_mut::() + .0 + .iter_mut() .enumerate() .zip(&record.bytes1_queries.0) .zip(row_writers.iter_mut()) diff --git a/crates/aiur/src/gadgets/bytes2.rs b/crates/aiur/src/gadgets/bytes2.rs index 8a2e16ef4..e9e03d364 100644 --- a/crates/aiur/src/gadgets/bytes2.rs +++ b/crates/aiur/src/gadgets/bytes2.rs @@ -211,45 +211,54 @@ impl AiurGadget for Bytes2 { let xor_split4_hi = Expr::preprocessed(12); let xor_split4_lo = Expr::preprocessed(13); - // pull = negated multiplicity. + // pull = negated multiplicity; count columns declare the query budget. + let budget = crate::COUNT_COLUMN_BUDGET; let pull_xor = Lookup { multiplicity: -xor_multiplicity, args: vec![xor_channel, i.clone(), j.clone(), xor], + max_multiplicity: budget, }; let pull_add = Lookup { multiplicity: -add_multiplicity, args: vec![add_channel, i.clone(), j.clone(), add_r], + max_multiplicity: budget, }; let pull_sub = Lookup { multiplicity: -sub_multiplicity, args: vec![sub_channel, i.clone(), j.clone(), sub_r], + max_multiplicity: budget, }; let pull_and = Lookup { multiplicity: -and_multiplicity, args: vec![and_channel, i.clone(), j.clone(), and], + max_multiplicity: budget, }; let pull_or = Lookup { multiplicity: -or_multiplicity, args: vec![or_channel, i.clone(), j.clone(), or], + max_multiplicity: budget, }; let pull_less_than = Lookup { multiplicity: -less_than_multiplicity, args: vec![less_than_channel, i.clone(), j.clone(), less_than], + max_multiplicity: budget, }; let pull_mul = Lookup { multiplicity: -mul_multiplicity, args: vec![mul_channel, i.clone(), j.clone(), mul_lo, mul_hi], + max_multiplicity: budget, }; let pull_range_check = Lookup { multiplicity: -range_check_multiplicity, args: vec![range_check_channel, i.clone(), j.clone()], + max_multiplicity: budget, }; let pull_xor_split7 = Lookup { @@ -261,10 +270,12 @@ impl AiurGadget for Bytes2 { xor_split7_hi, xor_split7_lo, ], + max_multiplicity: budget, }; let pull_xor_split4 = Lookup { multiplicity: -xor_split4_multiplicity, args: vec![xor_split4_channel, i, j, xor_split4_hi, xor_split4_lo], + max_multiplicity: budget, }; vec![ @@ -304,7 +315,9 @@ impl AiurGadget for Bytes2 { let xor_split4_channel = u8_xor_split4_channel(); rows - .chunks_exact_mut(TRACE_WIDTH) + .as_chunks_mut::() + .0 + .iter_mut() .enumerate() .zip(&record.bytes2_queries.0) .zip(row_writers.iter_mut()) diff --git a/crates/aiur/src/lib.rs b/crates/aiur/src/lib.rs index 3acf6666a..f915d1e43 100644 --- a/crates/aiur/src/lib.rs +++ b/crates/aiur/src/lib.rs @@ -15,6 +15,39 @@ use rustc_hash::FxBuildHasher; pub type G = multi_stark::p3_goldilocks::Goldilocks; pub type FxIndexMap = IndexMap; +/// Per-row multiplicity budget declared for committed count columns — +/// function-call return counts, memory load counts, and gadget table +/// counts: each entry supports up to 2^32 queries. The columns are not +/// range-constrained; the weight-1 pushes at the query sites are what keep +/// actual counts within the budget. Feeds the logUp height bound +/// `Σ wᵢ·hᵢ + |claims| < p` (see `multi_stark::lookup::Lookup`'s +/// `max_multiplicity`). +pub const COUNT_COLUMN_BUDGET: u64 = 1 << 32; + +/// # Channel discipline (width binding by construction) +/// +/// Aiur declares `WidthBinding::ByConstruction` to multi-stark: message +/// fingerprints are the plain Horner fold, so a message equals its own +/// zero-padding. That is what licenses branch-shared lookup slots — with +/// mutually exclusive selectors, sibling branches superpose messages of +/// different natural widths into one slot at the maximum width, and the +/// padded send still matches its natural-width provider. +/// +/// The contract this declaration takes on is prefix-freeness: every +/// message's natural width must be a function of its constant-constrained +/// leading prefix, so zero-extension can only ever equate a padded message +/// with its own natural form. The channels below uphold it — +/// +/// - function channel: `[tag, fun_idx, inputs.., outputs..]`, width +/// `2 + in + out` fixed by `fun_idx`; +/// - memory channel: `[tag, size, ptr, values..]`, width `3 + size` fixed +/// by the size coordinate; +/// - gadget channels: one fixed width per tag (each byte-table op has its +/// own channel). +/// +/// Every op that emits a lookup gates these leading coordinates as +/// constants, so a new channel (or a new width for an existing one) must +/// keep the width derivable from the prefix. #[inline] pub const fn function_channel() -> G { G::ZERO diff --git a/crates/aiur/src/memory.rs b/crates/aiur/src/memory.rs index c3fd487d0..38550a1ee 100644 --- a/crates/aiur/src/memory.rs +++ b/crates/aiur/src/memory.rs @@ -46,7 +46,11 @@ impl Memory { } let width = Self::width(size); // pull = negated multiplicity. - let lookups = vec![Lookup { multiplicity: -multiplicity, args }]; + let lookups = vec![Lookup { + multiplicity: -multiplicity, + args, + max_multiplicity: crate::COUNT_COLUMN_BUDGET, + }]; // Transition constraints (formerly the `Air::eval` body): the selector is // boolean; a real next row implies a real current row; and the pointer diff --git a/crates/aiur/src/synthesis.rs b/crates/aiur/src/synthesis.rs index 552743c28..cd4762b5a 100644 --- a/crates/aiur/src/synthesis.rs +++ b/crates/aiur/src/synthesis.rs @@ -1,6 +1,6 @@ use multi_stark::{ expr::Expr, - lookup::Lookup, + lookup::{Lookup, WidthBinding}, p3_field::PrimeCharacteristicRing, p3_matrix::dense::RowMajorMatrix, prover::Proof, @@ -149,7 +149,11 @@ impl AiurSystem { 2, ); - let config = AiurConfig::new(commitment_parameters, fri_parameters); + // Aiur guarantees prefix-free messages by construction (see the channel + // constants in `lib.rs`), which is what licenses branch-shared lookup + // slots superposing messages of different natural widths. + let config = AiurConfig::new(commitment_parameters, fri_parameters) + .with_width_binding(WidthBinding::ByConstruction); let (system, key) = System::new(config, circuit_inputs); AiurSystem { system, @@ -443,6 +447,24 @@ impl AiurSystem { ) -> Result<(), VerificationError> { self.system.verify(claim, proof) } + + /// Re-encodes a verified proof into the per-query advice transport the + /// in-circuit verifier consumes (see `multi_stark::advice`): the pruned + /// FRI Merkle multiproofs expanded into one authentication path per + /// query. Fails if the proof does not verify natively. + pub fn proof_to_advice_bytes( + &self, + claim: &[G], + proof: &AiurProof, + ) -> Result, multi_stark::advice::AdviceError> { + multi_stark::advice::proof_to_advice_bytes( + &self.system, + self.commitment_parameters, + self.fri_parameters, + &[claim], + proof, + ) + } } #[cfg(test)] @@ -814,4 +836,82 @@ mod tests { assert_eq!(shapes[4].preprocessed_width, 14); assert_eq!(shapes[4].preprocessed_height, 65536); } + + /// Two match branches whose calls target functions of different arity, so + /// they share one lookup slot with mismatched message widths. + /// + /// - `f0(x)`: matches on `x`; branch `0` calls `f1(x)` (message width 4), + /// branch `1` calls `f2(x, x)` (message width 5). + /// - Both calls land in lookup slot 1, whose width is the max (5), so the + /// `f1` message is sent zero-padded to 5 while `f1`'s own return slot + /// provides it at width 4. + /// + /// Zero-padding transparency is what makes the padded send match the + /// natural-width provider — the `WidthBinding::ByConstruction` + /// declaration in `AiurSystem::build`. Under width-bound fingerprints + /// this shape fails to verify with `UnbalancedChannel`. + fn mismatched_call_widths_toplevel() -> Toplevel { + let branch_narrow = Block { + ops: vec![Op::Call(1, vec![0], 1, false)], + ctrl: Ctrl::Return(0, vec![1]), + }; + let branch_wide = Block { + ops: vec![Op::Call(2, vec![0, 0], 1, false)], + ctrl: Ctrl::Return(1, vec![1]), + }; + let cases: crate::FxIndexMap = + [(G::ZERO, branch_narrow), (G::ONE, branch_wide)].into_iter().collect(); + let f0 = Function { + body: Block { ops: vec![], ctrl: Ctrl::Match(0, cases, None) }, + layout: FunctionLayout { + input_size: 1, + selectors: 2, + auxiliaries: 2, + lookups: 2, + }, + entry: true, + constrained: true, + }; + // f1(a) = a + let f1 = Function { + body: Block { ops: vec![], ctrl: Ctrl::Return(0, vec![0]) }, + layout: FunctionLayout { + input_size: 1, + selectors: 1, + auxiliaries: 1, + lookups: 1, + }, + entry: false, + constrained: true, + }; + // f2(a, b) = a + let f2 = Function { + body: Block { ops: vec![], ctrl: Ctrl::Return(0, vec![0]) }, + layout: FunctionLayout { + input_size: 2, + selectors: 1, + auxiliaries: 1, + lookups: 1, + }, + entry: false, + constrained: true, + }; + Toplevel { functions: vec![f0, f1, f2], memory_sizes: vec![] } + } + + #[test] + fn prove_verify_mismatched_call_widths() { + let (cp, fp) = test_parameters(); + let system = AiurSystem::build(mismatched_call_widths_toplevel(), cp, fp); + + // Branch 0: the narrow call, whose slot is padded to the wide width. + let mut io_buffer = empty_io_buffer(); + let (claim, proof) = system.prove(0, &[G::ZERO], &mut io_buffer); + system.verify(&claim, &proof).expect("narrow-branch proof must verify"); + + // Branch 1: the wide call, whose width already matches its slot. + let mut io_buffer = empty_io_buffer(); + let (claim, proof) = system.prove(0, &[G::ONE], &mut io_buffer); + system.verify(&claim, &proof).expect("wide-branch proof must verify"); + } } diff --git a/crates/aiur/src/vk_codec.rs b/crates/aiur/src/vk_codec.rs index 9fa9e00ec..e19baf198 100644 --- a/crates/aiur/src/vk_codec.rs +++ b/crates/aiur/src/vk_codec.rs @@ -45,6 +45,7 @@ //! u32 zero_count, then zero_count x u16 LE constraint-root node ids //! u32 lookup_count, then per lookup: //! u16 LE multiplicity node id +//! u64 LE max_multiplicity (declared per-row multiplicity bound) //! u16 LE arg count, then arg_count x u16 LE arg node ids //! TRAILER //! u8 preprocessed commit flag (0 = None / 1 = Some) @@ -64,7 +65,7 @@ use multi_stark::{ expr::{ColRef, RowOffset, Source}, graph::{ConstraintGraph, Node, NodeId}, - lookup::Lookup, + lookup::{Lookup, WidthBinding}, p3_field::{PrimeCharacteristicRing, PrimeField64}, system::{Circuit, System}, types::{Commitment, CommitmentParameters, FriParameters, Val}, @@ -89,6 +90,10 @@ fn push_u32(buf: &mut Vec, v: usize) { buf.extend_from_slice(&v.to_le_bytes()); } +fn push_u64(buf: &mut Vec, v: u64) { + buf.extend_from_slice(&v.to_le_bytes()); +} + /// Node ids on the wire are u16: per-circuit graphs are far below 65k /// nodes (the whole kernel system is ~140k across 800+ circuits). fn push_node_id(buf: &mut Vec, id: NodeId) { @@ -185,6 +190,7 @@ fn encode_circuit(buf: &mut Vec, circuit: &Circuit) { push_u16(buf, compiled.lookups.len()); for lookup in &compiled.lookups { push_node_id(buf, lookup.multiplicity); + push_u64(buf, lookup.max_multiplicity); push_u16(buf, lookup.args.len()); for &arg in &lookup.args { push_node_id(buf, arg); @@ -361,12 +367,13 @@ fn decode_circuit(seg: &mut Seg<'_>) -> Result, String> { let mut lookups = Vec::with_capacity(lookup_count); for _ in 0..lookup_count { let multiplicity = seg.node_id()?; + let max_multiplicity = seg.u64()?; let arg_count = seg.u16()? as usize; let mut args = Vec::with_capacity(arg_count.min(1 << 16)); for _ in 0..arg_count { args.push(seg.node_id()?); } - lookups.push(Lookup { multiplicity, args }); + lookups.push(Lookup { multiplicity, args, max_multiplicity }); } let degrees = recompute_degrees(&nodes); @@ -483,7 +490,11 @@ pub(crate) fn from_bytes( } r.done("vk")?; let system = System { - config: AiurConfig::new(commitment_parameters, fri_parameters), + // Aiur systems are always built with `ByConstruction` width binding + // (see `AiurSystem::build`), so the decoder must rebuild the config + // identically for the verifier's transcript to match. + config: AiurConfig::new(commitment_parameters, fri_parameters) + .with_width_binding(WidthBinding::ByConstruction), circuits, preprocessed_commit, preprocessed_indices, @@ -532,7 +543,10 @@ mod tests { lookup_group_size: 2, }, ]; - let (system, _key) = System::new(AiurConfig::new(cp, fp), inputs); + let (system, _key) = System::new( + AiurConfig::new(cp, fp).with_width_binding(WidthBinding::ByConstruction), + inputs, + ); (system, cp, fp) } diff --git a/crates/common/src/address.rs b/crates/common/src/address.rs index 334aafd13..d4db7b777 100644 --- a/crates/common/src/address.rs +++ b/crates/common/src/address.rs @@ -49,7 +49,9 @@ impl Address { /// bytes shorter than 32 are silently dropped (via `chunks_exact`). pub fn unpack(bytes: &[u8]) -> impl Iterator + '_ { bytes - .chunks_exact(32) + .as_chunks::<32>() + .0 + .iter() .map(|c| Address::from_slice(c).expect("malformed address chunk")) } diff --git a/crates/compile/src/compile.rs b/crates/compile/src/compile.rs index 02309a6fb..df30175f3 100644 --- a/crates/compile/src/compile.rs +++ b/crates/compile/src/compile.rs @@ -1058,7 +1058,7 @@ pub fn compile_expr( }); } let n_specs = specs.len(); - canonical_args.extend(specs.into_iter()); + canonical_args.extend(specs); for (src_i, motive) in motives.iter().enumerate() { if plan.motive_keep[src_i] { canonical_args.push(motive.clone()); diff --git a/crates/compile/src/compile/aux_gen/brecon.rs b/crates/compile/src/compile/aux_gen/brecon.rs index 6f340cd13..f53719bc7 100644 --- a/crates/compile/src/compile/aux_gen/brecon.rs +++ b/crates/compile/src/compile/aux_gen/brecon.rs @@ -510,8 +510,7 @@ fn build_prop_below_minor_fvar( let mut lambda_fvars: Vec = Vec::new(); let mut ctor_args: Vec = Vec::new(); - for (fi, (decl, fvar)) in - field_decls.into_iter().zip(field_fvars.into_iter()).enumerate() + for (fi, (decl, fvar)) in field_decls.into_iter().zip(field_fvars).enumerate() { if let Some(j_prime) = find_motive_fvar(&decl.domain, motive_fvars) { // IH field. For a non-reflexive IH `motive args`, the new binder is @@ -1134,8 +1133,7 @@ fn build_type_minor_premise_fvar( let mut lambda_fvars: Vec = Vec::new(); let mut prod_entries: Vec<(LeanExpr, usize)> = Vec::new(); // (fvar, lambda_index) for IH fields - for (fi, (decl, fvar)) in - field_decls.into_iter().zip(field_fvars.into_iter()).enumerate() + for (fi, (decl, fvar)) in field_decls.into_iter().zip(field_fvars).enumerate() { if let Some(_j_prime) = find_motive_fvar(&decl.domain, motive_fvars) { // IH field: replace domain with PProd(motive, below) diff --git a/crates/compile/src/compile/aux_gen/cases_on.rs b/crates/compile/src/compile/aux_gen/cases_on.rs index bad60eee0..096891920 100644 --- a/crates/compile/src/compile/aux_gen/cases_on.rs +++ b/crates/compile/src/compile/aux_gen/cases_on.rs @@ -191,7 +191,7 @@ pub fn generate_cases_on( let mut non_ih_fvars: Vec = Vec::new(); let mut wrapper_decls: Vec = Vec::new(); // all fields for the rec lambda - for (decl, fvar) in field_decls.into_iter().zip(field_fvars.into_iter()) { + for (decl, fvar) in field_decls.into_iter().zip(field_fvars) { let motive_idx = find_motive_fvar(&decl.domain, &motive_fvars); if let Some(idx) = motive_idx { if idx == target_idx { diff --git a/crates/compile/src/compile/env.rs b/crates/compile/src/compile/env.rs index 2f4afa9f3..b30545b82 100644 --- a/crates/compile/src/compile/env.rs +++ b/crates/compile/src/compile/env.rs @@ -397,7 +397,7 @@ pub fn compile_env_with_options( // Use scoped threads to borrow from parent scope. `IX_COMPILE_WORKERS` // gives large-env callers a simple peak-memory/speed tradeoff knob. let available_threads = - thread::available_parallelism().map(|n| n.get()).unwrap_or(4); + thread::available_parallelism().map_or(4, |n| n.get()); let requested_threads = options.max_workers.or_else(|| { std::env::var("IX_COMPILE_WORKERS") .ok() diff --git a/crates/compile/src/compile/mutual.rs b/crates/compile/src/compile/mutual.rs index 17a67882a..e62050590 100644 --- a/crates/compile/src/compile/mutual.rs +++ b/crates/compile/src/compile/mutual.rs @@ -712,8 +712,8 @@ pub fn generate_and_compile_aux_recursors( // `populate_recursor_rules_from_block` comment in the kernel. let t1 = std::time::Instant::now(); let rec_consts: Vec = patches - .iter() - .filter_map(|(_, p)| match p { + .values() + .filter_map(|p| match p { PatchedConstant::Rec(r) => Some(MutConst::Recr(r.clone())), _ => None, }) @@ -822,8 +822,8 @@ pub fn generate_and_compile_aux_recursors( // (because .brecOn.eq references casesOn). let t2 = std::time::Instant::now(); let cases_on_defs: Vec = patches - .iter() - .filter_map(|(_, p)| match p { + .values() + .filter_map(|p| match p { PatchedConstant::CasesOn(d) => Some(MutConst::Defn(Def { name: d.name.clone(), level_params: d.level_params.clone(), @@ -846,8 +846,8 @@ pub fn generate_and_compile_aux_recursors( // recOn wraps .rec and must be compiled after .rec. let t3 = std::time::Instant::now(); let rec_on_defs: Vec = patches - .iter() - .filter_map(|(_, p)| match p { + .values() + .filter_map(|p| match p { PatchedConstant::RecOn(d) => Some(MutConst::Defn(Def { name: d.name.clone(), level_params: d.level_params.clone(), @@ -887,8 +887,8 @@ pub fn generate_and_compile_aux_recursors( // order with the canonical `all`. let t4 = std::time::Instant::now(); let mut below_raw: Vec<&BelowIndc> = patches - .iter() - .filter_map(|(_, p)| match p { + .values() + .filter_map(|p| match p { PatchedConstant::BelowIndc(bi) => Some(bi), _ => None, }) @@ -932,8 +932,8 @@ pub fn generate_and_compile_aux_recursors( // Phase 4: Compile .below definitions (Type-level). let below_defs: Vec = patches - .iter() - .filter_map(|(_, p)| match p { + .values() + .filter_map(|p| match p { PatchedConstant::BelowDef(d) => Some(MutConst::Defn(Def { name: d.name.clone(), level_params: d.level_params.clone(), @@ -970,8 +970,8 @@ pub fn generate_and_compile_aux_recursors( let t6 = std::time::Instant::now(); for batch in 0..3u8 { let defs: Vec = patches - .iter() - .filter_map(|(_, p)| match p { + .values() + .filter_map(|p| match p { PatchedConstant::BRecOn(d) if brecon_batch(&d.name) == batch => { Some(brecon_to_mut_const(d)) }, diff --git a/crates/ffi/src/aiur/protocol.rs b/crates/ffi/src/aiur/protocol.rs index acf20c60e..ecdf51e09 100644 --- a/crates/ffi/src/aiur/protocol.rs +++ b/crates/ffi/src/aiur/protocol.rs @@ -143,6 +143,24 @@ extern "C" fn rs_aiur_system_verify( } } +/// `AiurSystem.proofToAdviceBytes : @& AiurSystem → @& Array G → @& Proof → Except String ByteArray` +/// +/// The proof re-encoded in the per-query advice transport the in-circuit +/// verifier consumes (pruned FRI multiproofs expanded to one path per +/// query); errors if the proof does not verify natively. +#[unsafe(no_mangle)] +extern "C" fn rs_aiur_proof_to_advice_bytes( + aiur_system_obj: LeanExternal>, + claim: LeanArray>, + proof_obj: LeanExternal>, +) -> LeanExcept { + let claim = claim.map(|x| lean_unbox_g(&x)); + match aiur_system_obj.get().proof_to_advice_bytes(&claim, proof_obj.get()) { + Ok(bytes) => LeanExcept::ok(LeanByteArray::from_bytes(&bytes)), + Err(err) => LeanExcept::error_string(&format!("{err:?}")), + } +} + /// `Bytecode.Toplevel.execute`: runs execution only (no proof) and returns /// `Except String ExecuteResult` (see `Ix/Aiur/Semantics/BytecodeFfi.lean`). /// On execution failure (e.g. assertion mismatch from a typechecker @@ -400,7 +418,9 @@ fn decode_owned_blob( } Ok( bytes - .chunks_exact(32) + .as_chunks::<32>() + .0 + .iter() .map(|c| ix_common::address::Address::from_slice(c).unwrap()) .collect(), ) @@ -683,7 +703,9 @@ extern "C" fn rs_aiur_toplevel_shard_check_batch( } shards.push( bytes[off..off + n * 32] - .chunks_exact(32) + .as_chunks::<32>() + .0 + .iter() .map(|c| ix_common::address::Address::from_slice(c).unwrap()) .collect(), ); diff --git a/crates/ffi/src/kernel.rs b/crates/ffi/src/kernel.rs index a71a167d7..d2cfc88ff 100644 --- a/crates/ffi/src/kernel.rs +++ b/crates/ffi/src/kernel.rs @@ -1293,7 +1293,7 @@ where fn resolve_kernel_check_workers(total: usize, quiet: bool) -> usize { let env_workers = std::env::var("IX_KERNEL_CHECK_WORKERS").ok(); let no_par = std::env::var("IX_NO_PAR").ok().as_deref() == Some("1"); - let available = thread::available_parallelism().map(|n| n.get()).unwrap_or(1); + let available = thread::available_parallelism().map_or(1, |n| n.get()); resolve_kernel_check_workers_from( total, quiet, diff --git a/crates/ffi/src/lean_env.rs b/crates/ffi/src/lean_env.rs index 925fe6599..6decff38f 100644 --- a/crates/ffi/src/lean_env.rs +++ b/crates/ffi/src/lean_env.rs @@ -4265,7 +4265,7 @@ fn analyze_const_size(stt: &ix_compile::compile::CompileState, name_str: &str) { } // Sort by total size descending - dep_breakdowns.sort_by(|a, b| b.1.total().cmp(&a.1.total())); + dep_breakdowns.sort_by_key(|(_, b)| std::cmp::Reverse(b.total())); let total_deps_alpha: usize = dep_breakdowns.iter().map(|(_, b)| b.alpha_size).sum(); @@ -4469,7 +4469,7 @@ fn analyze_block_size_stats(stt: &ix_compile::compile::CompileState) { .collect(); // Sort by overhead descending (most bloated first) - overheads.sort_by(|a, b| b.1.cmp(&a.1)); + overheads.sort_by_key(|o| std::cmp::Reverse(o.1)); // Compute statistics let avg_ratio = if total_hash_consed > 0 { diff --git a/crates/ffi/src/lean_ixon/sharing.rs b/crates/ffi/src/lean_ixon/sharing.rs index 9811fb63d..9905fc331 100644 --- a/crates/ffi/src/lean_ixon/sharing.rs +++ b/crates/ffi/src/lean_ixon/sharing.rs @@ -36,7 +36,7 @@ pub extern "C" fn rs_debug_sharing_analysis( .collect(); // Sort by usage count descending - candidates.sort_by(|a, b| b.1.usage_count.cmp(&a.1.usage_count)); + candidates.sort_by_key(|c| std::cmp::Reverse(c.1.usage_count)); println!("[Rust] Subterms with usage >= 2:"); for (hash, info, eff_size) in candidates { diff --git a/crates/ixon/src/diff.rs b/crates/ixon/src/diff.rs index 788aa0585..cd8c9a491 100644 --- a/crates/ixon/src/diff.rs +++ b/crates/ixon/src/diff.rs @@ -2537,7 +2537,7 @@ mod tests { let index = Env::parse_lazy_index(&bytes).expect("lazy index"); let mut sizes: Vec<(usize, Address)> = index.consts.iter().map(|c| (c.len, c.addr.clone())).collect(); - sizes.sort_by(|a, b| b.0.cmp(&a.0)); + sizes.sort_by_key(|(l, _)| std::cmp::Reverse(*l)); let total: usize = sizes.iter().map(|(l, _)| *l).sum(); println!("consts: {} total bytes: {}", sizes.len(), total); for (len, addr) in sizes.iter().take(top) { diff --git a/crates/ixvm-codegen/src/aiur_ixvm_witness.rs b/crates/ixvm-codegen/src/aiur_ixvm_witness.rs index a194b0f94..67d3a95c5 100644 --- a/crates/ixvm-codegen/src/aiur_ixvm_witness.rs +++ b/crates/ixvm-codegen/src/aiur_ixvm_witness.rs @@ -75,7 +75,9 @@ fn addr_key(addr: &Address) -> Vec { fn packed_digest_key(addr: &Address) -> Vec { addr .as_bytes() - .chunks_exact(4) + .as_chunks::<4>() + .0 + .iter() .map(|w| { G::from_u32( u32::from(w[0]) diff --git a/crates/ixvm-codegen/src/aiur_multi_stark.rs b/crates/ixvm-codegen/src/aiur_multi_stark.rs index 051a10e1a..bbe5a9015 100644 --- a/crates/ixvm-codegen/src/aiur_multi_stark.rs +++ b/crates/ixvm-codegen/src/aiur_multi_stark.rs @@ -8073,13 +8073,23 @@ fn aiur_fn_85( let __r_arr: [G; OUT_76] = { let __args: [G; IN_76] = [__v_0]; let __cu = unconstrained; if let Some(result) = record.function_queries[76].get_mut(&__args[..]) { if !__cu && *result.multiplicity == G::ZERO { aiur_fn_76(__args, record, io_buffer, false)? } else { if !unconstrained { *result.multiplicity += G::ONE; } let __ret: [G; OUT_76] = unsafe { *(result.output.as_ptr() as *const [G; OUT_76]) }; __ret } } else { aiur_fn_76(__args, record, io_buffer, __cu)? } }; let __v_1: G = __r_arr[0]; let __v_2: G = __r_arr[1]; - let __r_arr: [G; OUT_76] = { let __args: [G; IN_76] = [__v_2]; let __cu = unconstrained; if let Some(result) = record.function_queries[76].get_mut(&__args[..]) { if !__cu && *result.multiplicity == G::ZERO { aiur_fn_76(__args, record, io_buffer, false)? } else { if !unconstrained { *result.multiplicity += G::ONE; } let __ret: [G; OUT_76] = unsafe { *(result.output.as_ptr() as *const [G; OUT_76]) }; __ret } } else { aiur_fn_76(__args, record, io_buffer, __cu)? } }; + let __r_arr: [G; OUT_79] = { let __args: [G; IN_79] = [__v_2]; let __cu = unconstrained; if let Some(result) = record.function_queries[79].get_mut(&__args[..]) { if !__cu && *result.multiplicity == G::ZERO { aiur_fn_79(__args, record, io_buffer, false)? } else { if !unconstrained { *result.multiplicity += G::ONE; } let __ret: [G; OUT_79] = unsafe { *(result.output.as_ptr() as *const [G; OUT_79]) }; __ret } } else { aiur_fn_79(__args, record, io_buffer, __cu)? } }; let __v_3: G = __r_arr[0]; let __v_4: G = __r_arr[1]; - let __r_arr: [G; OUT_84] = { let __args: [G; IN_84] = [__v_4, __v_3]; let __cu = unconstrained; if let Some(result) = record.function_queries[84].get_mut(&__args[..]) { if !__cu && *result.multiplicity == G::ZERO { aiur_fn_84(__args, record, io_buffer, false)? } else { if !unconstrained { *result.multiplicity += G::ONE; } let __ret: [G; OUT_84] = unsafe { *(result.output.as_ptr() as *const [G; OUT_84]) }; __ret } } else { aiur_fn_84(__args, record, io_buffer, __cu)? } }; - let __v_5: G = __r_arr[0]; - let __v_6: G = __r_arr[1]; - let __ret: [G; OUT_85] = [__v_1, __v_5, __v_6]; + let __v_5: G = __r_arr[2]; + let __v_6: G = __r_arr[3]; + let __v_7: G = __r_arr[4]; + let __v_8: G = __r_arr[5]; + let __v_9: G = __r_arr[6]; + let __v_10: G = __r_arr[7]; + let __v_11: G = __r_arr[8]; + let __r_arr: [G; OUT_76] = { let __args: [G; IN_76] = [__v_11]; let __cu = unconstrained; if let Some(result) = record.function_queries[76].get_mut(&__args[..]) { if !__cu && *result.multiplicity == G::ZERO { aiur_fn_76(__args, record, io_buffer, false)? } else { if !unconstrained { *result.multiplicity += G::ONE; } let __ret: [G; OUT_76] = unsafe { *(result.output.as_ptr() as *const [G; OUT_76]) }; __ret } } else { aiur_fn_76(__args, record, io_buffer, __cu)? } }; + let __v_12: G = __r_arr[0]; + let __v_13: G = __r_arr[1]; + let __r_arr: [G; OUT_84] = { let __args: [G; IN_84] = [__v_13, __v_12]; let __cu = unconstrained; if let Some(result) = record.function_queries[84].get_mut(&__args[..]) { if !__cu && *result.multiplicity == G::ZERO { aiur_fn_84(__args, record, io_buffer, false)? } else { if !unconstrained { *result.multiplicity += G::ONE; } let __ret: [G; OUT_84] = unsafe { *(result.output.as_ptr() as *const [G; OUT_84]) }; __ret } } else { aiur_fn_84(__args, record, io_buffer, __cu)? } }; + let __v_14: G = __r_arr[0]; + let __v_15: G = __r_arr[1]; + let __ret: [G; OUT_85] = [__v_1, __v_14, __v_15]; if let Some(result) = record.function_queries[85].get_mut(&inp[..]) { debug_assert_eq!(result.output, &__ret[..]); if !unconstrained { *result.multiplicity += G::ONE; } } else { record.function_queries[85].insert(&inp[..], &__ret[..], G::from_bool(!unconstrained)); }; return Ok(__ret); }) @@ -8110,20 +8120,30 @@ fn aiur_fn_86( let __r_arr: [G; OUT_76] = { let __args: [G; IN_76] = [__v_0]; let __cu = unconstrained; if let Some(result) = record.function_queries[76].get_mut(&__args[..]) { if !__cu && *result.multiplicity == G::ZERO { aiur_fn_76(__args, record, io_buffer, false)? } else { if !unconstrained { *result.multiplicity += G::ONE; } let __ret: [G; OUT_76] = unsafe { *(result.output.as_ptr() as *const [G; OUT_76]) }; __ret } } else { aiur_fn_76(__args, record, io_buffer, __cu)? } }; let __v_2: G = __r_arr[0]; let __v_3: G = __r_arr[1]; - let __r_arr: [G; OUT_76] = { let __args: [G; IN_76] = [__v_3]; let __cu = unconstrained; if let Some(result) = record.function_queries[76].get_mut(&__args[..]) { if !__cu && *result.multiplicity == G::ZERO { aiur_fn_76(__args, record, io_buffer, false)? } else { if !unconstrained { *result.multiplicity += G::ONE; } let __ret: [G; OUT_76] = unsafe { *(result.output.as_ptr() as *const [G; OUT_76]) }; __ret } } else { aiur_fn_76(__args, record, io_buffer, __cu)? } }; + let __r_arr: [G; OUT_79] = { let __args: [G; IN_79] = [__v_3]; let __cu = unconstrained; if let Some(result) = record.function_queries[79].get_mut(&__args[..]) { if !__cu && *result.multiplicity == G::ZERO { aiur_fn_79(__args, record, io_buffer, false)? } else { if !unconstrained { *result.multiplicity += G::ONE; } let __ret: [G; OUT_79] = unsafe { *(result.output.as_ptr() as *const [G; OUT_79]) }; __ret } } else { aiur_fn_79(__args, record, io_buffer, __cu)? } }; let __v_4: G = __r_arr[0]; let __v_5: G = __r_arr[1]; - let __r_arr: [G; OUT_84] = { let __args: [G; IN_84] = [__v_5, __v_4]; let __cu = unconstrained; if let Some(result) = record.function_queries[84].get_mut(&__args[..]) { if !__cu && *result.multiplicity == G::ZERO { aiur_fn_84(__args, record, io_buffer, false)? } else { if !unconstrained { *result.multiplicity += G::ONE; } let __ret: [G; OUT_84] = unsafe { *(result.output.as_ptr() as *const [G; OUT_84]) }; __ret } } else { aiur_fn_84(__args, record, io_buffer, __cu)? } }; - let __v_6: G = __r_arr[0]; - let __v_7: G = __r_arr[1]; - let __v_8: G = G::from_u64(1); - let __v_9: G = (__v_1 - __v_8); - let __r_arr: [G; OUT_86] = { let __args: [G; IN_86] = [__v_7, __v_9]; let __cu = unconstrained; if let Some(result) = record.function_queries[86].get_mut(&__args[..]) { if !__cu && *result.multiplicity == G::ZERO { aiur_fn_86(__args, record, io_buffer, false)? } else { if !unconstrained { *result.multiplicity += G::ONE; } let __ret: [G; OUT_86] = unsafe { *(result.output.as_ptr() as *const [G; OUT_86]) }; __ret } } else { aiur_fn_86(__args, record, io_buffer, __cu)? } }; - let __v_10: G = __r_arr[0]; - let __v_11: G = __r_arr[1]; - let __v_12: G = G::from_u64(0); - let __v_13: G = { let __values: [G; 4] = [__v_12, __v_2, __v_6, __v_10]; let __mq = record.memory_queries.get_mut(&4).ok_or(ExecError::InvalidMemorySize(4))?; if let Some(result) = __mq.get_mut(&__values[..]) { if !unconstrained { *result.multiplicity += G::ONE; } result.output[0] } else { let __ptr = G::from_usize(__mq.len()); __mq.insert(&__values[..], &[__ptr], G::from_bool(!unconstrained)); __ptr } }; - let __ret: [G; OUT_86] = [__v_13, __v_11]; + let __v_6: G = __r_arr[2]; + let __v_7: G = __r_arr[3]; + let __v_8: G = __r_arr[4]; + let __v_9: G = __r_arr[5]; + let __v_10: G = __r_arr[6]; + let __v_11: G = __r_arr[7]; + let __v_12: G = __r_arr[8]; + let __r_arr: [G; OUT_76] = { let __args: [G; IN_76] = [__v_12]; let __cu = unconstrained; if let Some(result) = record.function_queries[76].get_mut(&__args[..]) { if !__cu && *result.multiplicity == G::ZERO { aiur_fn_76(__args, record, io_buffer, false)? } else { if !unconstrained { *result.multiplicity += G::ONE; } let __ret: [G; OUT_76] = unsafe { *(result.output.as_ptr() as *const [G; OUT_76]) }; __ret } } else { aiur_fn_76(__args, record, io_buffer, __cu)? } }; + let __v_13: G = __r_arr[0]; + let __v_14: G = __r_arr[1]; + let __r_arr: [G; OUT_84] = { let __args: [G; IN_84] = [__v_14, __v_13]; let __cu = unconstrained; if let Some(result) = record.function_queries[84].get_mut(&__args[..]) { if !__cu && *result.multiplicity == G::ZERO { aiur_fn_84(__args, record, io_buffer, false)? } else { if !unconstrained { *result.multiplicity += G::ONE; } let __ret: [G; OUT_84] = unsafe { *(result.output.as_ptr() as *const [G; OUT_84]) }; __ret } } else { aiur_fn_84(__args, record, io_buffer, __cu)? } }; + let __v_15: G = __r_arr[0]; + let __v_16: G = __r_arr[1]; + let __v_17: G = G::from_u64(1); + let __v_18: G = (__v_1 - __v_17); + let __r_arr: [G; OUT_86] = { let __args: [G; IN_86] = [__v_16, __v_18]; let __cu = unconstrained; if let Some(result) = record.function_queries[86].get_mut(&__args[..]) { if !__cu && *result.multiplicity == G::ZERO { aiur_fn_86(__args, record, io_buffer, false)? } else { if !unconstrained { *result.multiplicity += G::ONE; } let __ret: [G; OUT_86] = unsafe { *(result.output.as_ptr() as *const [G; OUT_86]) }; __ret } } else { aiur_fn_86(__args, record, io_buffer, __cu)? } }; + let __v_19: G = __r_arr[0]; + let __v_20: G = __r_arr[1]; + let __v_21: G = G::from_u64(0); + let __v_22: G = { let __values: [G; 4] = [__v_21, __v_2, __v_15, __v_19]; let __mq = record.memory_queries.get_mut(&4).ok_or(ExecError::InvalidMemorySize(4))?; if let Some(result) = __mq.get_mut(&__values[..]) { if !unconstrained { *result.multiplicity += G::ONE; } result.output[0] } else { let __ptr = G::from_usize(__mq.len()); __mq.insert(&__values[..], &[__ptr], G::from_bool(!unconstrained)); __ptr } }; + let __ret: [G; OUT_86] = [__v_22, __v_20]; if let Some(result) = record.function_queries[86].get_mut(&inp[..]) { debug_assert_eq!(result.output, &__ret[..]); if !unconstrained { *result.multiplicity += G::ONE; } } else { record.function_queries[86].insert(&inp[..], &__ret[..], G::from_bool(!unconstrained)); }; return Ok(__ret); }, @@ -9154,11 +9174,70 @@ fn aiur_fn_94( let __r_arr: [G; OUT_92] = { let __args: [G; IN_92] = [__v_103, __v_88]; let __cu = unconstrained; if let Some(result) = record.function_queries[92].get_mut(&__args[..]) { if !__cu && *result.multiplicity == G::ZERO { aiur_fn_92(__args, record, io_buffer, false)? } else { if !unconstrained { *result.multiplicity += G::ONE; } let __ret: [G; OUT_92] = unsafe { *(result.output.as_ptr() as *const [G; OUT_92]) }; __ret } } else { aiur_fn_92(__args, record, io_buffer, __cu)? } }; let __v_104: G = __r_arr[0]; let __v_105: G = __r_arr[1]; - let __v_106: G = G::from_u64(0); - let __v_107: G = { let __values: [G; 10] = [__v_106, __v_89, __v_90, __v_91, __v_92, __v_93, __v_94, __v_95, __v_96, __v_99]; let __mq = record.memory_queries.get_mut(&10).ok_or(ExecError::InvalidMemorySize(10))?; if let Some(result) = __mq.get_mut(&__values[..]) { if !unconstrained { *result.multiplicity += G::ONE; } result.output[0] } else { let __ptr = G::from_usize(__mq.len()); __mq.insert(&__values[..], &[__ptr], G::from_bool(!unconstrained)); __ptr } }; - let __r_arr: [G; OUT_197] = { let __args: [G; IN_197] = [__v_87, __v_107]; let __cu = unconstrained; if let Some(result) = record.function_queries[197].get_mut(&__args[..]) { if !__cu && *result.multiplicity == G::ZERO { aiur_fn_197(__args, record, io_buffer, false)? } else { if !unconstrained { *result.multiplicity += G::ONE; } let __ret: [G; OUT_197] = unsafe { *(result.output.as_ptr() as *const [G; OUT_197]) }; __ret } } else { aiur_fn_197(__args, record, io_buffer, __cu)? } }; - let __v_108: G = __r_arr[0]; - let __ret: [G; OUT_94] = [__v_1, __v_11, __v_21, __v_31, __v_41, __v_51, __v_61, __v_108, __v_98, __v_101, __v_102, __v_104, __v_105]; + let __v_106: G = G::from_u64(1); + let __gb: [u8; 8] = __v_106.as_canonical_u64().to_le_bytes(); + let __v_107: G = G::from_u8(__gb[0]); + let __v_108: G = G::from_u8(__gb[1]); + let __v_109: G = G::from_u8(__gb[2]); + let __v_110: G = G::from_u8(__gb[3]); + let __v_111: G = G::from_u8(__gb[4]); + let __v_112: G = G::from_u8(__gb[5]); + let __v_113: G = G::from_u8(__gb[6]); + let __v_114: G = G::from_u8(__gb[7]); + if !unconstrained { let __vi = __v_107; let __vj = __v_108; let __bi = __vi.as_canonical_u64(); let __bj = __vj.as_canonical_u64(); if __bi >= 256 { return Err(ExecError::U8RangeCheckFailed(__bi)); } if __bj >= 256 { return Err(ExecError::U8RangeCheckFailed(__bj)); } record.bytes2_queries.bump_range_check(&__vi, &__vj); }; + if !unconstrained { let __vi = __v_109; let __vj = __v_110; let __bi = __vi.as_canonical_u64(); let __bj = __vj.as_canonical_u64(); if __bi >= 256 { return Err(ExecError::U8RangeCheckFailed(__bi)); } if __bj >= 256 { return Err(ExecError::U8RangeCheckFailed(__bj)); } record.bytes2_queries.bump_range_check(&__vi, &__vj); }; + if !unconstrained { let __vi = __v_111; let __vj = __v_112; let __bi = __vi.as_canonical_u64(); let __bj = __vj.as_canonical_u64(); if __bi >= 256 { return Err(ExecError::U8RangeCheckFailed(__bi)); } if __bj >= 256 { return Err(ExecError::U8RangeCheckFailed(__bj)); } record.bytes2_queries.bump_range_check(&__vi, &__vj); }; + if !unconstrained { let __vi = __v_113; let __vj = __v_114; let __bi = __vi.as_canonical_u64(); let __bj = __vj.as_canonical_u64(); if __bi >= 256 { return Err(ExecError::U8RangeCheckFailed(__bi)); } if __bj >= 256 { return Err(ExecError::U8RangeCheckFailed(__bj)); } record.bytes2_queries.bump_range_check(&__vi, &__vj); }; + let __v_115: G = G::from_u64(1020); + let __v_116: G = (__v_114 - __v_115); + let __v_117: G = (__v_113 + __v_116); + let __v_118: G = (__v_112 + __v_117); + let __v_119: G = (__v_111 + __v_118); + let __v_120: G = G::from_bool((__v_119 == G::ZERO)); + let __v_121: G = (__v_109 + __v_110); + let __v_122: G = (__v_108 + __v_121); + let __v_123: G = (__v_107 + __v_122); + let __v_124: G = G::from_bool((__v_123 == G::ZERO)); + let __v_125: G = G::from_u64(256); + let __v_126: G = (__v_125 * __v_108); + let __v_127: G = G::from_u64(65536); + let __v_128: G = (__v_127 * __v_109); + let __v_129: G = G::from_u64(16777216); + let __v_130: G = (__v_129 * __v_110); + let __v_131: G = G::from_u64(4294967296); + let __v_132: G = (__v_131 * __v_111); + let __v_133: G = G::from_u64(1099511627776); + let __v_134: G = (__v_133 * __v_112); + let __v_135: G = G::from_u64(281474976710656); + let __v_136: G = (__v_135 * __v_113); + let __v_137: G = G::from_u64(72057594037927936); + let __v_138: G = (__v_137 * __v_114); + let __v_139: G = (__v_136 + __v_138); + let __v_140: G = (__v_134 + __v_139); + let __v_141: G = (__v_132 + __v_140); + let __v_142: G = (__v_130 + __v_141); + let __v_143: G = (__v_128 + __v_142); + let __v_144: G = (__v_126 + __v_143); + let __v_145: G = (__v_107 + __v_144); + if (__v_145 != __v_106) { + return Err(ExecError::AssertEqMismatch { lhs: __v_145.as_canonical_u64(), rhs: __v_106.as_canonical_u64(), msg: None }); + } + let __v_146: G = G::from_u64(1); + let __v_147: G = G::from_u64(1); + let __v_148: G = (__v_147 - __v_124); + let __v_149: G = (__v_120 * __v_148); + let __v_150: G = (__v_146 - __v_149); + let __v_151: G = G::from_u64(1); + if (__v_150 != __v_151) { + return Err(ExecError::AssertEqMismatch { lhs: __v_150.as_canonical_u64(), rhs: __v_151.as_canonical_u64(), msg: None }); + } + let __v_152: G = G::from_u64(0); + let __v_153: G = G::from_u64(0); + let __v_154: G = { let __values: [G; 10] = [__v_153, __v_89, __v_90, __v_91, __v_92, __v_93, __v_94, __v_95, __v_96, __v_99]; let __mq = record.memory_queries.get_mut(&10).ok_or(ExecError::InvalidMemorySize(10))?; if let Some(result) = __mq.get_mut(&__values[..]) { if !unconstrained { *result.multiplicity += G::ONE; } result.output[0] } else { let __ptr = G::from_usize(__mq.len()); __mq.insert(&__values[..], &[__ptr], G::from_bool(!unconstrained)); __ptr } }; + let __v_155: G = { let __values: [G; 10] = [__v_152, __v_107, __v_108, __v_109, __v_110, __v_111, __v_112, __v_113, __v_114, __v_154]; let __mq = record.memory_queries.get_mut(&10).ok_or(ExecError::InvalidMemorySize(10))?; if let Some(result) = __mq.get_mut(&__values[..]) { if !unconstrained { *result.multiplicity += G::ONE; } result.output[0] } else { let __ptr = G::from_usize(__mq.len()); __mq.insert(&__values[..], &[__ptr], G::from_bool(!unconstrained)); __ptr } }; + let __r_arr: [G; OUT_197] = { let __args: [G; IN_197] = [__v_87, __v_155]; let __cu = unconstrained; if let Some(result) = record.function_queries[197].get_mut(&__args[..]) { if !__cu && *result.multiplicity == G::ZERO { aiur_fn_197(__args, record, io_buffer, false)? } else { if !unconstrained { *result.multiplicity += G::ONE; } let __ret: [G; OUT_197] = unsafe { *(result.output.as_ptr() as *const [G; OUT_197]) }; __ret } } else { aiur_fn_197(__args, record, io_buffer, __cu)? } }; + let __v_156: G = __r_arr[0]; + let __ret: [G; OUT_94] = [__v_1, __v_11, __v_21, __v_31, __v_41, __v_51, __v_61, __v_156, __v_98, __v_101, __v_102, __v_104, __v_105]; if let Some(result) = record.function_queries[94].get_mut(&inp[..]) { debug_assert_eq!(result.output, &__ret[..]); if !unconstrained { *result.multiplicity += G::ONE; } } else { record.function_queries[94].insert(&inp[..], &__ret[..], G::from_bool(!unconstrained)); }; return Ok(__ret); }) @@ -18492,145 +18571,204 @@ fn aiur_fn_191( let __r_arr: [G; OUT_92] = { let __args: [G; IN_92] = [__v_257, __v_242]; let __cu = unconstrained; if let Some(result) = record.function_queries[92].get_mut(&__args[..]) { if !__cu && *result.multiplicity == G::ZERO { aiur_fn_92(__args, record, io_buffer, false)? } else { if !unconstrained { *result.multiplicity += G::ONE; } let __ret: [G; OUT_92] = unsafe { *(result.output.as_ptr() as *const [G; OUT_92]) }; __ret } } else { aiur_fn_92(__args, record, io_buffer, __cu)? } }; let __v_258: G = __r_arr[0]; let __v_259: G = __r_arr[1]; - let __v_260: G = G::from_u64(0); - let __v_261: G = { let __values: [G; 10] = [__v_260, __v_243, __v_244, __v_245, __v_246, __v_247, __v_248, __v_249, __v_250, __v_253]; let __mq = record.memory_queries.get_mut(&10).ok_or(ExecError::InvalidMemorySize(10))?; if let Some(result) = __mq.get_mut(&__values[..]) { if !unconstrained { *result.multiplicity += G::ONE; } result.output[0] } else { let __ptr = G::from_usize(__mq.len()); __mq.insert(&__values[..], &[__ptr], G::from_bool(!unconstrained)); __ptr } }; - let __r_arr: [G; OUT_197] = { let __args: [G; IN_197] = [__v_241, __v_261]; let __cu = unconstrained; if let Some(result) = record.function_queries[197].get_mut(&__args[..]) { if !__cu && *result.multiplicity == G::ZERO { aiur_fn_197(__args, record, io_buffer, false)? } else { if !unconstrained { *result.multiplicity += G::ONE; } let __ret: [G; OUT_197] = unsafe { *(result.output.as_ptr() as *const [G; OUT_197]) }; __ret } } else { aiur_fn_197(__args, record, io_buffer, __cu)? } }; - let __v_262: G = __r_arr[0]; - let __v_263: G = G::from_u64(2); - let __v_264: G = G::from_u64(0); - let __io_pair: (G, G) = { let __key: [G; 1] = [__v_264]; let __info = io_buffer.get_info(__v_263, &__key[..])?; (G::from_usize(__info.idx), G::from_usize(__info.len)) }; - let __v_265: G = __io_pair.0; - let __v_266: G = __io_pair.1; - let __v_267: G = G::from_u64(2); - let __r_arr: [G; OUT_0] = { let __args: [G; IN_0] = [__v_267, __v_265, __v_266]; let __cu = true; if let Some(result) = record.function_queries[0].get_mut(&__args[..]) { if !__cu && *result.multiplicity == G::ZERO { aiur_fn_0(__args, record, io_buffer, false)? } else { let __ret: [G; OUT_0] = unsafe { *(result.output.as_ptr() as *const [G; OUT_0]) }; __ret } } else { aiur_fn_0(__args, record, io_buffer, __cu)? } }; - let __v_268: G = __r_arr[0]; - let __v_269: G = G::from_u64(103); - let __v_270: G = G::from_u64(230); - let __v_271: G = G::from_u64(9); - let __v_272: G = G::from_u64(106); - let __v_273: G = G::from_u64(133); - let __v_274: G = G::from_u64(174); - let __v_275: G = G::from_u64(103); - let __v_276: G = G::from_u64(187); - let __v_277: G = G::from_u64(114); - let __v_278: G = G::from_u64(243); - let __v_279: G = G::from_u64(110); - let __v_280: G = G::from_u64(60); - let __v_281: G = G::from_u64(58); - let __v_282: G = G::from_u64(245); - let __v_283: G = G::from_u64(79); - let __v_284: G = G::from_u64(165); - let __v_285: G = G::from_u64(127); - let __v_286: G = G::from_u64(82); - let __v_287: G = G::from_u64(14); - let __v_288: G = G::from_u64(81); - let __v_289: G = G::from_u64(140); - let __v_290: G = G::from_u64(104); - let __v_291: G = G::from_u64(5); - let __v_292: G = G::from_u64(155); - let __v_293: G = G::from_u64(171); - let __v_294: G = G::from_u64(217); - let __v_295: G = G::from_u64(131); - let __v_296: G = G::from_u64(31); - let __v_297: G = G::from_u64(25); - let __v_298: G = G::from_u64(205); - let __v_299: G = G::from_u64(224); - let __v_300: G = G::from_u64(91); + let __v_260: G = G::from_u64(1); + let __gb: [u8; 8] = __v_260.as_canonical_u64().to_le_bytes(); + let __v_261: G = G::from_u8(__gb[0]); + let __v_262: G = G::from_u8(__gb[1]); + let __v_263: G = G::from_u8(__gb[2]); + let __v_264: G = G::from_u8(__gb[3]); + let __v_265: G = G::from_u8(__gb[4]); + let __v_266: G = G::from_u8(__gb[5]); + let __v_267: G = G::from_u8(__gb[6]); + let __v_268: G = G::from_u8(__gb[7]); + if !unconstrained { let __vi = __v_261; let __vj = __v_262; let __bi = __vi.as_canonical_u64(); let __bj = __vj.as_canonical_u64(); if __bi >= 256 { return Err(ExecError::U8RangeCheckFailed(__bi)); } if __bj >= 256 { return Err(ExecError::U8RangeCheckFailed(__bj)); } record.bytes2_queries.bump_range_check(&__vi, &__vj); }; + if !unconstrained { let __vi = __v_263; let __vj = __v_264; let __bi = __vi.as_canonical_u64(); let __bj = __vj.as_canonical_u64(); if __bi >= 256 { return Err(ExecError::U8RangeCheckFailed(__bi)); } if __bj >= 256 { return Err(ExecError::U8RangeCheckFailed(__bj)); } record.bytes2_queries.bump_range_check(&__vi, &__vj); }; + if !unconstrained { let __vi = __v_265; let __vj = __v_266; let __bi = __vi.as_canonical_u64(); let __bj = __vj.as_canonical_u64(); if __bi >= 256 { return Err(ExecError::U8RangeCheckFailed(__bi)); } if __bj >= 256 { return Err(ExecError::U8RangeCheckFailed(__bj)); } record.bytes2_queries.bump_range_check(&__vi, &__vj); }; + if !unconstrained { let __vi = __v_267; let __vj = __v_268; let __bi = __vi.as_canonical_u64(); let __bj = __vj.as_canonical_u64(); if __bi >= 256 { return Err(ExecError::U8RangeCheckFailed(__bi)); } if __bj >= 256 { return Err(ExecError::U8RangeCheckFailed(__bj)); } record.bytes2_queries.bump_range_check(&__vi, &__vj); }; + let __v_269: G = G::from_u64(1020); + let __v_270: G = (__v_268 - __v_269); + let __v_271: G = (__v_267 + __v_270); + let __v_272: G = (__v_266 + __v_271); + let __v_273: G = (__v_265 + __v_272); + let __v_274: G = G::from_bool((__v_273 == G::ZERO)); + let __v_275: G = (__v_263 + __v_264); + let __v_276: G = (__v_262 + __v_275); + let __v_277: G = (__v_261 + __v_276); + let __v_278: G = G::from_bool((__v_277 == G::ZERO)); + let __v_279: G = G::from_u64(256); + let __v_280: G = (__v_279 * __v_262); + let __v_281: G = G::from_u64(65536); + let __v_282: G = (__v_281 * __v_263); + let __v_283: G = G::from_u64(16777216); + let __v_284: G = (__v_283 * __v_264); + let __v_285: G = G::from_u64(4294967296); + let __v_286: G = (__v_285 * __v_265); + let __v_287: G = G::from_u64(1099511627776); + let __v_288: G = (__v_287 * __v_266); + let __v_289: G = G::from_u64(281474976710656); + let __v_290: G = (__v_289 * __v_267); + let __v_291: G = G::from_u64(72057594037927936); + let __v_292: G = (__v_291 * __v_268); + let __v_293: G = (__v_290 + __v_292); + let __v_294: G = (__v_288 + __v_293); + let __v_295: G = (__v_286 + __v_294); + let __v_296: G = (__v_284 + __v_295); + let __v_297: G = (__v_282 + __v_296); + let __v_298: G = (__v_280 + __v_297); + let __v_299: G = (__v_261 + __v_298); + if (__v_299 != __v_260) { + return Err(ExecError::AssertEqMismatch { lhs: __v_299.as_canonical_u64(), rhs: __v_260.as_canonical_u64(), msg: None }); + } + let __v_300: G = G::from_u64(1); let __v_301: G = G::from_u64(1); - let __v_302: G = G::from_u64(1); - let __v_303: G = { let __values: [G; 3] = [__v_301, __v_302, __v_302]; let __mq = record.memory_queries.get_mut(&3).ok_or(ExecError::InvalidMemorySize(3))?; if let Some(result) = __mq.get_mut(&__values[..]) { if !unconstrained { *result.multiplicity += G::ONE; } result.output[0] } else { let __ptr = G::from_usize(__mq.len()); __mq.insert(&__values[..], &[__ptr], G::from_bool(!unconstrained)); __ptr } }; - let __v_304: G = G::from_u64(0); - let __v_305: G = G::from_u64(0); + let __v_302: G = (__v_301 - __v_278); + let __v_303: G = (__v_274 * __v_302); + let __v_304: G = (__v_300 - __v_303); + let __v_305: G = G::from_u64(1); + if (__v_304 != __v_305) { + return Err(ExecError::AssertEqMismatch { lhs: __v_304.as_canonical_u64(), rhs: __v_305.as_canonical_u64(), msg: None }); + } let __v_306: G = G::from_u64(0); let __v_307: G = G::from_u64(0); - let __v_308: G = G::from_u64(0); - let __v_309: G = G::from_u64(0); - let __v_310: G = G::from_u64(0); - let __v_311: G = G::from_u64(0); + let __v_308: G = { let __values: [G; 10] = [__v_307, __v_243, __v_244, __v_245, __v_246, __v_247, __v_248, __v_249, __v_250, __v_253]; let __mq = record.memory_queries.get_mut(&10).ok_or(ExecError::InvalidMemorySize(10))?; if let Some(result) = __mq.get_mut(&__values[..]) { if !unconstrained { *result.multiplicity += G::ONE; } result.output[0] } else { let __ptr = G::from_usize(__mq.len()); __mq.insert(&__values[..], &[__ptr], G::from_bool(!unconstrained)); __ptr } }; + let __v_309: G = { let __values: [G; 10] = [__v_306, __v_261, __v_262, __v_263, __v_264, __v_265, __v_266, __v_267, __v_268, __v_308]; let __mq = record.memory_queries.get_mut(&10).ok_or(ExecError::InvalidMemorySize(10))?; if let Some(result) = __mq.get_mut(&__values[..]) { if !unconstrained { *result.multiplicity += G::ONE; } result.output[0] } else { let __ptr = G::from_usize(__mq.len()); __mq.insert(&__values[..], &[__ptr], G::from_bool(!unconstrained)); __ptr } }; + let __r_arr: [G; OUT_197] = { let __args: [G; IN_197] = [__v_241, __v_309]; let __cu = unconstrained; if let Some(result) = record.function_queries[197].get_mut(&__args[..]) { if !__cu && *result.multiplicity == G::ZERO { aiur_fn_197(__args, record, io_buffer, false)? } else { if !unconstrained { *result.multiplicity += G::ONE; } let __ret: [G; OUT_197] = unsafe { *(result.output.as_ptr() as *const [G; OUT_197]) }; __ret } } else { aiur_fn_197(__args, record, io_buffer, __cu)? } }; + let __v_310: G = __r_arr[0]; + let __v_311: G = G::from_u64(2); let __v_312: G = G::from_u64(0); - let __v_313: G = G::from_u64(0); - let __v_314: G = { let __values: [G; 8] = [__v_306, __v_307, __v_308, __v_309, __v_310, __v_311, __v_312, __v_313]; let __mq = record.memory_queries.get_mut(&8).ok_or(ExecError::InvalidMemorySize(8))?; if let Some(result) = __mq.get_mut(&__values[..]) { if !unconstrained { *result.multiplicity += G::ONE; } result.output[0] } else { let __ptr = G::from_usize(__mq.len()); __mq.insert(&__values[..], &[__ptr], G::from_bool(!unconstrained)); __ptr } }; - let __v_315: G = { let __values: [G; 32] = [__v_269, __v_270, __v_271, __v_272, __v_273, __v_274, __v_275, __v_276, __v_277, __v_278, __v_279, __v_280, __v_281, __v_282, __v_283, __v_284, __v_285, __v_286, __v_287, __v_288, __v_289, __v_290, __v_291, __v_292, __v_293, __v_294, __v_295, __v_296, __v_297, __v_298, __v_299, __v_300]; let __mq = record.memory_queries.get_mut(&32).ok_or(ExecError::InvalidMemorySize(32))?; if let Some(result) = __mq.get_mut(&__values[..]) { if !unconstrained { *result.multiplicity += G::ONE; } result.output[0] } else { let __ptr = G::from_usize(__mq.len()); __mq.insert(&__values[..], &[__ptr], G::from_bool(!unconstrained)); __ptr } }; - let __v_316: G = G::from_u64(1); - let __v_317: G = G::from_u64(1); - let __v_318: G = { let __values: [G; 34] = [__v_316, __v_317, __v_317, __v_317, __v_317, __v_317, __v_317, __v_317, __v_317, __v_317, __v_317, __v_317, __v_317, __v_317, __v_317, __v_317, __v_317, __v_317, __v_317, __v_317, __v_317, __v_317, __v_317, __v_317, __v_317, __v_317, __v_317, __v_317, __v_317, __v_317, __v_317, __v_317, __v_317, __v_317]; let __mq = record.memory_queries.get_mut(&34).ok_or(ExecError::InvalidMemorySize(34))?; if let Some(result) = __mq.get_mut(&__values[..]) { if !unconstrained { *result.multiplicity += G::ONE; } result.output[0] } else { let __ptr = G::from_usize(__mq.len()); __mq.insert(&__values[..], &[__ptr], G::from_bool(!unconstrained)); __ptr } }; - let __r_arr: [G; OUT_65] = { let __args: [G; IN_65] = [__v_268, __v_303, __v_304, __v_305, __v_314, __v_315, __v_318]; let __cu = unconstrained; if let Some(result) = record.function_queries[65].get_mut(&__args[..]) { if !__cu && *result.multiplicity == G::ZERO { aiur_fn_65(__args, record, io_buffer, false)? } else { if !unconstrained { *result.multiplicity += G::ONE; } let __ret: [G; OUT_65] = unsafe { *(result.output.as_ptr() as *const [G; OUT_65]) }; __ret } } else { aiur_fn_65(__args, record, io_buffer, __cu)? } }; - let __v_319: G = __r_arr[0]; - let __r_arr: [G; OUT_64] = { let __args: [G; IN_64] = [__v_319]; let __cu = unconstrained; if let Some(result) = record.function_queries[64].get_mut(&__args[..]) { if !__cu && *result.multiplicity == G::ZERO { aiur_fn_64(__args, record, io_buffer, false)? } else { if !unconstrained { *result.multiplicity += G::ONE; } let __ret: [G; OUT_64] = unsafe { *(result.output.as_ptr() as *const [G; OUT_64]) }; __ret } } else { aiur_fn_64(__args, record, io_buffer, __cu)? } }; - let __v_320: G = __r_arr[0]; - let __v_321: G = __r_arr[1]; - let __v_322: G = __r_arr[2]; - let __v_323: G = __r_arr[3]; - let __v_324: G = __r_arr[4]; - let __v_325: G = __r_arr[5]; - let __v_326: G = __r_arr[6]; - let __v_327: G = __r_arr[7]; - let __v_328: G = __r_arr[8]; - let __v_329: G = __r_arr[9]; - let __v_330: G = __r_arr[10]; - let __v_331: G = __r_arr[11]; - let __v_332: G = __r_arr[12]; - let __v_333: G = __r_arr[13]; - let __v_334: G = __r_arr[14]; - let __v_335: G = __r_arr[15]; - let __v_336: G = __r_arr[16]; - let __v_337: G = __r_arr[17]; - let __v_338: G = __r_arr[18]; - let __v_339: G = __r_arr[19]; - let __v_340: G = __r_arr[20]; - let __v_341: G = __r_arr[21]; - let __v_342: G = __r_arr[22]; - let __v_343: G = __r_arr[23]; - let __v_344: G = __r_arr[24]; - let __v_345: G = __r_arr[25]; - let __v_346: G = __r_arr[26]; - let __v_347: G = __r_arr[27]; - let __v_348: G = __r_arr[28]; - let __v_349: G = __r_arr[29]; - let __v_350: G = __r_arr[30]; - let __v_351: G = __r_arr[31]; - let __r_arr: [G; OUT_24] = { let __args: [G; IN_24] = [__v_268]; let __cu = unconstrained; if let Some(result) = record.function_queries[24].get_mut(&__args[..]) { if !__cu && *result.multiplicity == G::ZERO { aiur_fn_24(__args, record, io_buffer, false)? } else { if !unconstrained { *result.multiplicity += G::ONE; } let __ret: [G; OUT_24] = unsafe { *(result.output.as_ptr() as *const [G; OUT_24]) }; __ret } } else { aiur_fn_24(__args, record, io_buffer, __cu)? } }; - let __v_352: G = __r_arr[0]; - let __v_353: G = __r_arr[1]; - let __r_arr: [G; OUT_188] = { let __args: [G; IN_188] = [__v_353, __v_352]; let __cu = unconstrained; if let Some(result) = record.function_queries[188].get_mut(&__args[..]) { if !__cu && *result.multiplicity == G::ZERO { aiur_fn_188(__args, record, io_buffer, false)? } else { if !unconstrained { *result.multiplicity += G::ONE; } let __ret: [G; OUT_188] = unsafe { *(result.output.as_ptr() as *const [G; OUT_188]) }; __ret } } else { aiur_fn_188(__args, record, io_buffer, __cu)? } }; - let __v_354: G = __r_arr[0]; - let __v_355: G = __r_arr[1]; + let __io_pair: (G, G) = { let __key: [G; 1] = [__v_312]; let __info = io_buffer.get_info(__v_311, &__key[..])?; (G::from_usize(__info.idx), G::from_usize(__info.len)) }; + let __v_313: G = __io_pair.0; + let __v_314: G = __io_pair.1; + let __v_315: G = G::from_u64(2); + let __r_arr: [G; OUT_0] = { let __args: [G; IN_0] = [__v_315, __v_313, __v_314]; let __cu = true; if let Some(result) = record.function_queries[0].get_mut(&__args[..]) { if !__cu && *result.multiplicity == G::ZERO { aiur_fn_0(__args, record, io_buffer, false)? } else { let __ret: [G; OUT_0] = unsafe { *(result.output.as_ptr() as *const [G; OUT_0]) }; __ret } } else { aiur_fn_0(__args, record, io_buffer, __cu)? } }; + let __v_316: G = __r_arr[0]; + let __v_317: G = G::from_u64(103); + let __v_318: G = G::from_u64(230); + let __v_319: G = G::from_u64(9); + let __v_320: G = G::from_u64(106); + let __v_321: G = G::from_u64(133); + let __v_322: G = G::from_u64(174); + let __v_323: G = G::from_u64(103); + let __v_324: G = G::from_u64(187); + let __v_325: G = G::from_u64(114); + let __v_326: G = G::from_u64(243); + let __v_327: G = G::from_u64(110); + let __v_328: G = G::from_u64(60); + let __v_329: G = G::from_u64(58); + let __v_330: G = G::from_u64(245); + let __v_331: G = G::from_u64(79); + let __v_332: G = G::from_u64(165); + let __v_333: G = G::from_u64(127); + let __v_334: G = G::from_u64(82); + let __v_335: G = G::from_u64(14); + let __v_336: G = G::from_u64(81); + let __v_337: G = G::from_u64(140); + let __v_338: G = G::from_u64(104); + let __v_339: G = G::from_u64(5); + let __v_340: G = G::from_u64(155); + let __v_341: G = G::from_u64(171); + let __v_342: G = G::from_u64(217); + let __v_343: G = G::from_u64(131); + let __v_344: G = G::from_u64(31); + let __v_345: G = G::from_u64(25); + let __v_346: G = G::from_u64(205); + let __v_347: G = G::from_u64(224); + let __v_348: G = G::from_u64(91); + let __v_349: G = G::from_u64(1); + let __v_350: G = G::from_u64(1); + let __v_351: G = { let __values: [G; 3] = [__v_349, __v_350, __v_350]; let __mq = record.memory_queries.get_mut(&3).ok_or(ExecError::InvalidMemorySize(3))?; if let Some(result) = __mq.get_mut(&__values[..]) { if !unconstrained { *result.multiplicity += G::ONE; } result.output[0] } else { let __ptr = G::from_usize(__mq.len()); __mq.insert(&__values[..], &[__ptr], G::from_bool(!unconstrained)); __ptr } }; + let __v_352: G = G::from_u64(0); + let __v_353: G = G::from_u64(0); + let __v_354: G = G::from_u64(0); + let __v_355: G = G::from_u64(0); + let __v_356: G = G::from_u64(0); + let __v_357: G = G::from_u64(0); + let __v_358: G = G::from_u64(0); + let __v_359: G = G::from_u64(0); + let __v_360: G = G::from_u64(0); + let __v_361: G = G::from_u64(0); + let __v_362: G = { let __values: [G; 8] = [__v_354, __v_355, __v_356, __v_357, __v_358, __v_359, __v_360, __v_361]; let __mq = record.memory_queries.get_mut(&8).ok_or(ExecError::InvalidMemorySize(8))?; if let Some(result) = __mq.get_mut(&__values[..]) { if !unconstrained { *result.multiplicity += G::ONE; } result.output[0] } else { let __ptr = G::from_usize(__mq.len()); __mq.insert(&__values[..], &[__ptr], G::from_bool(!unconstrained)); __ptr } }; + let __v_363: G = { let __values: [G; 32] = [__v_317, __v_318, __v_319, __v_320, __v_321, __v_322, __v_323, __v_324, __v_325, __v_326, __v_327, __v_328, __v_329, __v_330, __v_331, __v_332, __v_333, __v_334, __v_335, __v_336, __v_337, __v_338, __v_339, __v_340, __v_341, __v_342, __v_343, __v_344, __v_345, __v_346, __v_347, __v_348]; let __mq = record.memory_queries.get_mut(&32).ok_or(ExecError::InvalidMemorySize(32))?; if let Some(result) = __mq.get_mut(&__values[..]) { if !unconstrained { *result.multiplicity += G::ONE; } result.output[0] } else { let __ptr = G::from_usize(__mq.len()); __mq.insert(&__values[..], &[__ptr], G::from_bool(!unconstrained)); __ptr } }; + let __v_364: G = G::from_u64(1); + let __v_365: G = G::from_u64(1); + let __v_366: G = { let __values: [G; 34] = [__v_364, __v_365, __v_365, __v_365, __v_365, __v_365, __v_365, __v_365, __v_365, __v_365, __v_365, __v_365, __v_365, __v_365, __v_365, __v_365, __v_365, __v_365, __v_365, __v_365, __v_365, __v_365, __v_365, __v_365, __v_365, __v_365, __v_365, __v_365, __v_365, __v_365, __v_365, __v_365, __v_365, __v_365]; let __mq = record.memory_queries.get_mut(&34).ok_or(ExecError::InvalidMemorySize(34))?; if let Some(result) = __mq.get_mut(&__values[..]) { if !unconstrained { *result.multiplicity += G::ONE; } result.output[0] } else { let __ptr = G::from_usize(__mq.len()); __mq.insert(&__values[..], &[__ptr], G::from_bool(!unconstrained)); __ptr } }; + let __r_arr: [G; OUT_65] = { let __args: [G; IN_65] = [__v_316, __v_351, __v_352, __v_353, __v_362, __v_363, __v_366]; let __cu = unconstrained; if let Some(result) = record.function_queries[65].get_mut(&__args[..]) { if !__cu && *result.multiplicity == G::ZERO { aiur_fn_65(__args, record, io_buffer, false)? } else { if !unconstrained { *result.multiplicity += G::ONE; } let __ret: [G; OUT_65] = unsafe { *(result.output.as_ptr() as *const [G; OUT_65]) }; __ret } } else { aiur_fn_65(__args, record, io_buffer, __cu)? } }; + let __v_367: G = __r_arr[0]; + let __r_arr: [G; OUT_64] = { let __args: [G; IN_64] = [__v_367]; let __cu = unconstrained; if let Some(result) = record.function_queries[64].get_mut(&__args[..]) { if !__cu && *result.multiplicity == G::ZERO { aiur_fn_64(__args, record, io_buffer, false)? } else { if !unconstrained { *result.multiplicity += G::ONE; } let __ret: [G; OUT_64] = unsafe { *(result.output.as_ptr() as *const [G; OUT_64]) }; __ret } } else { aiur_fn_64(__args, record, io_buffer, __cu)? } }; + let __v_368: G = __r_arr[0]; + let __v_369: G = __r_arr[1]; + let __v_370: G = __r_arr[2]; + let __v_371: G = __r_arr[3]; + let __v_372: G = __r_arr[4]; + let __v_373: G = __r_arr[5]; + let __v_374: G = __r_arr[6]; + let __v_375: G = __r_arr[7]; + let __v_376: G = __r_arr[8]; + let __v_377: G = __r_arr[9]; + let __v_378: G = __r_arr[10]; + let __v_379: G = __r_arr[11]; + let __v_380: G = __r_arr[12]; + let __v_381: G = __r_arr[13]; + let __v_382: G = __r_arr[14]; + let __v_383: G = __r_arr[15]; + let __v_384: G = __r_arr[16]; + let __v_385: G = __r_arr[17]; + let __v_386: G = __r_arr[18]; + let __v_387: G = __r_arr[19]; + let __v_388: G = __r_arr[20]; + let __v_389: G = __r_arr[21]; + let __v_390: G = __r_arr[22]; + let __v_391: G = __r_arr[23]; + let __v_392: G = __r_arr[24]; + let __v_393: G = __r_arr[25]; + let __v_394: G = __r_arr[26]; + let __v_395: G = __r_arr[27]; + let __v_396: G = __r_arr[28]; + let __v_397: G = __r_arr[29]; + let __v_398: G = __r_arr[30]; + let __v_399: G = __r_arr[31]; + let __r_arr: [G; OUT_24] = { let __args: [G; IN_24] = [__v_316]; let __cu = unconstrained; if let Some(result) = record.function_queries[24].get_mut(&__args[..]) { if !__cu && *result.multiplicity == G::ZERO { aiur_fn_24(__args, record, io_buffer, false)? } else { if !unconstrained { *result.multiplicity += G::ONE; } let __ret: [G; OUT_24] = unsafe { *(result.output.as_ptr() as *const [G; OUT_24]) }; __ret } } else { aiur_fn_24(__args, record, io_buffer, __cu)? } }; + let __v_400: G = __r_arr[0]; + let __v_401: G = __r_arr[1]; + let __r_arr: [G; OUT_188] = { let __args: [G; IN_188] = [__v_401, __v_400]; let __cu = unconstrained; if let Some(result) = record.function_queries[188].get_mut(&__args[..]) { if !__cu && *result.multiplicity == G::ZERO { aiur_fn_188(__args, record, io_buffer, false)? } else { if !unconstrained { *result.multiplicity += G::ONE; } let __ret: [G; OUT_188] = unsafe { *(result.output.as_ptr() as *const [G; OUT_188]) }; __ret } } else { aiur_fn_188(__args, record, io_buffer, __cu)? } }; + let __v_402: G = __r_arr[0]; + let __v_403: G = __r_arr[1]; let __mc_out___mc_0: [G; 1] = '__mc_0: { match __v_22.as_canonical_u64() { _ => { let __r_arr: [G; OUT_196] = { let __args: [G; IN_196] = [__v_30]; let __cu = unconstrained; if let Some(result) = record.function_queries[196].get_mut(&__args[..]) { if !__cu && *result.multiplicity == G::ZERO { aiur_fn_196(__args, record, io_buffer, false)? } else { if !unconstrained { *result.multiplicity += G::ONE; } let __ret: [G; OUT_196] = unsafe { *(result.output.as_ptr() as *const [G; OUT_196]) }; __ret } } else { aiur_fn_196(__args, record, io_buffer, __cu)? } }; - let __v_356: G = __r_arr[0]; - let __v_357: G = G::from_bool((__v_356 == G::ZERO)); - let __v_358: G = G::from_u64(0); - if (__v_357 != __v_358) { - return Err(ExecError::AssertEqMismatch { lhs: __v_357.as_canonical_u64(), rhs: __v_358.as_canonical_u64(), msg: None }); + let __v_404: G = __r_arr[0]; + let __v_405: G = G::from_bool((__v_404 == G::ZERO)); + let __v_406: G = G::from_u64(0); + if (__v_405 != __v_406) { + return Err(ExecError::AssertEqMismatch { lhs: __v_405.as_canonical_u64(), rhs: __v_406.as_canonical_u64(), msg: None }); } let __r_arr: [G; OUT_204] = { let __args: [G; IN_204] = [__v_62]; let __cu = unconstrained; if let Some(result) = record.function_queries[204].get_mut(&__args[..]) { if !__cu && *result.multiplicity == G::ZERO { aiur_fn_204(__args, record, io_buffer, false)? } else { if !unconstrained { *result.multiplicity += G::ONE; } let __ret: [G; OUT_204] = unsafe { *(result.output.as_ptr() as *const [G; OUT_204]) }; __ret } } else { aiur_fn_204(__args, record, io_buffer, __cu)? } }; - let __v_359: G = __r_arr[0]; - if (__v_359 != __v_356) { - return Err(ExecError::AssertEqMismatch { lhs: __v_359.as_canonical_u64(), rhs: __v_356.as_canonical_u64(), msg: None }); + let __v_407: G = __r_arr[0]; + if (__v_407 != __v_404) { + return Err(ExecError::AssertEqMismatch { lhs: __v_407.as_canonical_u64(), rhs: __v_404.as_canonical_u64(), msg: None }); } let __r_arr: [G; OUT_204] = { let __args: [G; IN_204] = [__v_64]; let __cu = unconstrained; if let Some(result) = record.function_queries[204].get_mut(&__args[..]) { if !__cu && *result.multiplicity == G::ZERO { aiur_fn_204(__args, record, io_buffer, false)? } else { if !unconstrained { *result.multiplicity += G::ONE; } let __ret: [G; OUT_204] = unsafe { *(result.output.as_ptr() as *const [G; OUT_204]) }; __ret } } else { aiur_fn_204(__args, record, io_buffer, __cu)? } }; - let __v_360: G = __r_arr[0]; - if (__v_360 != __v_356) { - return Err(ExecError::AssertEqMismatch { lhs: __v_360.as_canonical_u64(), rhs: __v_356.as_canonical_u64(), msg: None }); + let __v_408: G = __r_arr[0]; + if (__v_408 != __v_404) { + return Err(ExecError::AssertEqMismatch { lhs: __v_408.as_canonical_u64(), rhs: __v_404.as_canonical_u64(), msg: None }); } let __r_arr: [G; OUT_204] = { let __args: [G; IN_204] = [__v_57]; let __cu = unconstrained; if let Some(result) = record.function_queries[204].get_mut(&__args[..]) { if !__cu && *result.multiplicity == G::ZERO { aiur_fn_204(__args, record, io_buffer, false)? } else { if !unconstrained { *result.multiplicity += G::ONE; } let __ret: [G; OUT_204] = unsafe { *(result.output.as_ptr() as *const [G; OUT_204]) }; __ret } } else { aiur_fn_204(__args, record, io_buffer, __cu)? } }; - let __v_361: G = __r_arr[0]; - if (__v_361 != __v_356) { - return Err(ExecError::AssertEqMismatch { lhs: __v_361.as_canonical_u64(), rhs: __v_356.as_canonical_u64(), msg: None }); + let __v_409: G = __r_arr[0]; + if (__v_409 != __v_404) { + return Err(ExecError::AssertEqMismatch { lhs: __v_409.as_canonical_u64(), rhs: __v_404.as_canonical_u64(), msg: None }); } let __r_arr: [G; OUT_145] = { let __args: [G; IN_145] = [__v_30]; let __cu = unconstrained; if let Some(result) = record.function_queries[145].get_mut(&__args[..]) { if !__cu && *result.multiplicity == G::ZERO { aiur_fn_145(__args, record, io_buffer, false)? } else { if !unconstrained { *result.multiplicity += G::ONE; } let __ret: [G; OUT_145] = unsafe { *(result.output.as_ptr() as *const [G; OUT_145]) }; __ret } } else { aiur_fn_145(__args, record, io_buffer, __cu)? } }; - let __v_362: G = __r_arr[0]; - let __v_363: G = G::from_u64(1); - if (__v_362 != __v_363) { - return Err(ExecError::AssertEqMismatch { lhs: __v_362.as_canonical_u64(), rhs: __v_363.as_canonical_u64(), msg: None }); + let __v_410: G = __r_arr[0]; + let __v_411: G = G::from_u64(1); + if (__v_410 != __v_411) { + return Err(ExecError::AssertEqMismatch { lhs: __v_410.as_canonical_u64(), rhs: __v_411.as_canonical_u64(), msg: None }); } - let __v_364: G = G::from_u64(1); - break '__mc_0 [__v_364]; + let __v_412: G = G::from_u64(1); + break '__mc_0 [__v_412]; }, } }; - let __v_356: G = __mc_out___mc_0[0]; + let __v_404: G = __mc_out___mc_0[0]; let __mc_out___mc_1: [G; 1] = '__mc_1: { match __v_155.as_canonical_u64() { _ => { match __v_155.as_canonical_u64() { @@ -18638,17 +18776,17 @@ fn aiur_fn_191( match __v_22.as_canonical_u64() { _ => { let __r_arr: [G; OUT_185] = { let __args: [G; IN_185] = [__v_252, __v_22]; let __cu = unconstrained; if let Some(result) = record.function_queries[185].get_mut(&__args[..]) { if !__cu && *result.multiplicity == G::ZERO { aiur_fn_185(__args, record, io_buffer, false)? } else { if !unconstrained { *result.multiplicity += G::ONE; } let __ret: [G; OUT_185] = unsafe { *(result.output.as_ptr() as *const [G; OUT_185]) }; __ret } } else { aiur_fn_185(__args, record, io_buffer, __cu)? } }; - let __v_357: G = __r_arr[0]; + let __v_405: G = __r_arr[0]; let __r_arr: [G; OUT_186] = { let __args: [G; IN_186] = [__v_258, __v_22]; let __cu = unconstrained; if let Some(result) = record.function_queries[186].get_mut(&__args[..]) { if !__cu && *result.multiplicity == G::ZERO { aiur_fn_186(__args, record, io_buffer, false)? } else { if !unconstrained { *result.multiplicity += G::ONE; } let __ret: [G; OUT_186] = unsafe { *(result.output.as_ptr() as *const [G; OUT_186]) }; __ret } } else { aiur_fn_186(__args, record, io_buffer, __cu)? } }; - let __v_358: G = __r_arr[0]; + let __v_406: G = __r_arr[0]; match __v_24.as_canonical_u64() { _ => { let __mc_out___mc_2: [G; 1] = '__mc_2: { match __v_255.as_canonical_u64() { 0u64 => { - let __v_359: G = G::from_u64(1); - let __v_360: G = G::from_u64(1); - let __v_361: G = { let __values: [G; 3] = [__v_359, __v_360, __v_360]; let __mq = record.memory_queries.get_mut(&3).ok_or(ExecError::InvalidMemorySize(3))?; if let Some(result) = __mq.get_mut(&__values[..]) { if !unconstrained { *result.multiplicity += G::ONE; } result.output[0] } else { let __ptr = G::from_usize(__mq.len()); __mq.insert(&__values[..], &[__ptr], G::from_bool(!unconstrained)); __ptr } }; - break '__mc_2 [__v_361]; + let __v_407: G = G::from_u64(1); + let __v_408: G = G::from_u64(1); + let __v_409: G = { let __values: [G; 3] = [__v_407, __v_408, __v_408]; let __mq = record.memory_queries.get_mut(&3).ok_or(ExecError::InvalidMemorySize(3))?; if let Some(result) = __mq.get_mut(&__values[..]) { if !unconstrained { *result.multiplicity += G::ONE; } result.output[0] } else { let __ptr = G::from_usize(__mq.len()); __mq.insert(&__values[..], &[__ptr], G::from_bool(!unconstrained)); __ptr } }; + break '__mc_2 [__v_409]; }, 1u64 => { break '__mc_2 [__v_256]; @@ -18658,521 +18796,521 @@ fn aiur_fn_191( }, } }; - let __v_359: G = __mc_out___mc_2[0]; - let __r_arr: [G; OUT_149] = { let __args: [G; IN_149] = [__v_34, __v_268]; let __cu = unconstrained; if let Some(result) = record.function_queries[149].get_mut(&__args[..]) { if !__cu && *result.multiplicity == G::ZERO { aiur_fn_149(__args, record, io_buffer, false)? } else { if !unconstrained { *result.multiplicity += G::ONE; } let __ret: [G; OUT_149] = unsafe { *(result.output.as_ptr() as *const [G; OUT_149]) }; __ret } } else { aiur_fn_149(__args, record, io_buffer, __cu)? } }; - let __v_360: G = __r_arr[0]; - let __r_arr: [G; OUT_148] = { let __args: [G; IN_148] = [__v_24, __v_360]; let __cu = unconstrained; if let Some(result) = record.function_queries[148].get_mut(&__args[..]) { if !__cu && *result.multiplicity == G::ZERO { aiur_fn_148(__args, record, io_buffer, false)? } else { if !unconstrained { *result.multiplicity += G::ONE; } let __ret: [G; OUT_148] = unsafe { *(result.output.as_ptr() as *const [G; OUT_148]) }; __ret } } else { aiur_fn_148(__args, record, io_buffer, __cu)? } }; - let __v_361: G = __r_arr[0]; - let __r_arr: [G; OUT_148] = { let __args: [G; IN_148] = [__v_359, __v_361]; let __cu = unconstrained; if let Some(result) = record.function_queries[148].get_mut(&__args[..]) { if !__cu && *result.multiplicity == G::ZERO { aiur_fn_148(__args, record, io_buffer, false)? } else { if !unconstrained { *result.multiplicity += G::ONE; } let __ret: [G; OUT_148] = unsafe { *(result.output.as_ptr() as *const [G; OUT_148]) }; __ret } } else { aiur_fn_148(__args, record, io_buffer, __cu)? } }; - let __v_362: G = __r_arr[0]; - let __r_arr: [G; OUT_149] = { let __args: [G; IN_149] = [__v_22, __v_362]; let __cu = unconstrained; if let Some(result) = record.function_queries[149].get_mut(&__args[..]) { if !__cu && *result.multiplicity == G::ZERO { aiur_fn_149(__args, record, io_buffer, false)? } else { if !unconstrained { *result.multiplicity += G::ONE; } let __ret: [G; OUT_149] = unsafe { *(result.output.as_ptr() as *const [G; OUT_149]) }; __ret } } else { aiur_fn_149(__args, record, io_buffer, __cu)? } }; - let __v_363: G = __r_arr[0]; - let __r_arr: [G; OUT_158] = { let __args: [G; IN_158] = [__v_262, __v_363]; let __cu = unconstrained; if let Some(result) = record.function_queries[158].get_mut(&__args[..]) { if !__cu && *result.multiplicity == G::ZERO { aiur_fn_158(__args, record, io_buffer, false)? } else { if !unconstrained { *result.multiplicity += G::ONE; } let __ret: [G; OUT_158] = unsafe { *(result.output.as_ptr() as *const [G; OUT_158]) }; __ret } } else { aiur_fn_158(__args, record, io_buffer, __cu)? } }; - let __v_364: G = __r_arr[0]; - let __v_365: G = G::from_u64(0); - let __v_366: G = G::from_u64(109); - let __v_367: G = G::from_u64(0); - let __v_368: G = G::from_u64(117); - let __v_369: G = G::from_u64(0); - let __v_370: G = G::from_u64(108); - let __v_371: G = G::from_u64(0); - let __v_372: G = G::from_u64(116); - let __v_373: G = G::from_u64(0); - let __v_374: G = G::from_u64(105); - let __v_375: G = G::from_u64(0); - let __v_376: G = G::from_u64(45); - let __v_377: G = G::from_u64(0); - let __v_378: G = G::from_u64(115); - let __v_379: G = G::from_u64(0); - let __v_380: G = G::from_u64(116); - let __v_381: G = G::from_u64(0); - let __v_382: G = G::from_u64(97); - let __v_383: G = G::from_u64(0); - let __v_384: G = G::from_u64(114); - let __v_385: G = G::from_u64(0); - let __v_386: G = G::from_u64(107); - let __v_387: G = G::from_u64(0); - let __v_388: G = G::from_u64(47); - let __v_389: G = G::from_u64(0); - let __v_390: G = G::from_u64(118); - let __v_391: G = G::from_u64(0); - let __v_392: G = G::from_u64(48); - let __v_393: G = { let __values: [G; 3] = [__v_391, __v_392, __v_364]; let __mq = record.memory_queries.get_mut(&3).ok_or(ExecError::InvalidMemorySize(3))?; if let Some(result) = __mq.get_mut(&__values[..]) { if !unconstrained { *result.multiplicity += G::ONE; } result.output[0] } else { let __ptr = G::from_usize(__mq.len()); __mq.insert(&__values[..], &[__ptr], G::from_bool(!unconstrained)); __ptr } }; - let __v_394: G = { let __values: [G; 3] = [__v_389, __v_390, __v_393]; let __mq = record.memory_queries.get_mut(&3).ok_or(ExecError::InvalidMemorySize(3))?; if let Some(result) = __mq.get_mut(&__values[..]) { if !unconstrained { *result.multiplicity += G::ONE; } result.output[0] } else { let __ptr = G::from_usize(__mq.len()); __mq.insert(&__values[..], &[__ptr], G::from_bool(!unconstrained)); __ptr } }; - let __v_395: G = { let __values: [G; 3] = [__v_387, __v_388, __v_394]; let __mq = record.memory_queries.get_mut(&3).ok_or(ExecError::InvalidMemorySize(3))?; if let Some(result) = __mq.get_mut(&__values[..]) { if !unconstrained { *result.multiplicity += G::ONE; } result.output[0] } else { let __ptr = G::from_usize(__mq.len()); __mq.insert(&__values[..], &[__ptr], G::from_bool(!unconstrained)); __ptr } }; - let __v_396: G = { let __values: [G; 3] = [__v_385, __v_386, __v_395]; let __mq = record.memory_queries.get_mut(&3).ok_or(ExecError::InvalidMemorySize(3))?; if let Some(result) = __mq.get_mut(&__values[..]) { if !unconstrained { *result.multiplicity += G::ONE; } result.output[0] } else { let __ptr = G::from_usize(__mq.len()); __mq.insert(&__values[..], &[__ptr], G::from_bool(!unconstrained)); __ptr } }; - let __v_397: G = { let __values: [G; 3] = [__v_383, __v_384, __v_396]; let __mq = record.memory_queries.get_mut(&3).ok_or(ExecError::InvalidMemorySize(3))?; if let Some(result) = __mq.get_mut(&__values[..]) { if !unconstrained { *result.multiplicity += G::ONE; } result.output[0] } else { let __ptr = G::from_usize(__mq.len()); __mq.insert(&__values[..], &[__ptr], G::from_bool(!unconstrained)); __ptr } }; - let __v_398: G = { let __values: [G; 3] = [__v_381, __v_382, __v_397]; let __mq = record.memory_queries.get_mut(&3).ok_or(ExecError::InvalidMemorySize(3))?; if let Some(result) = __mq.get_mut(&__values[..]) { if !unconstrained { *result.multiplicity += G::ONE; } result.output[0] } else { let __ptr = G::from_usize(__mq.len()); __mq.insert(&__values[..], &[__ptr], G::from_bool(!unconstrained)); __ptr } }; - let __v_399: G = { let __values: [G; 3] = [__v_379, __v_380, __v_398]; let __mq = record.memory_queries.get_mut(&3).ok_or(ExecError::InvalidMemorySize(3))?; if let Some(result) = __mq.get_mut(&__values[..]) { if !unconstrained { *result.multiplicity += G::ONE; } result.output[0] } else { let __ptr = G::from_usize(__mq.len()); __mq.insert(&__values[..], &[__ptr], G::from_bool(!unconstrained)); __ptr } }; - let __v_400: G = { let __values: [G; 3] = [__v_377, __v_378, __v_399]; let __mq = record.memory_queries.get_mut(&3).ok_or(ExecError::InvalidMemorySize(3))?; if let Some(result) = __mq.get_mut(&__values[..]) { if !unconstrained { *result.multiplicity += G::ONE; } result.output[0] } else { let __ptr = G::from_usize(__mq.len()); __mq.insert(&__values[..], &[__ptr], G::from_bool(!unconstrained)); __ptr } }; - let __v_401: G = { let __values: [G; 3] = [__v_375, __v_376, __v_400]; let __mq = record.memory_queries.get_mut(&3).ok_or(ExecError::InvalidMemorySize(3))?; if let Some(result) = __mq.get_mut(&__values[..]) { if !unconstrained { *result.multiplicity += G::ONE; } result.output[0] } else { let __ptr = G::from_usize(__mq.len()); __mq.insert(&__values[..], &[__ptr], G::from_bool(!unconstrained)); __ptr } }; - let __v_402: G = { let __values: [G; 3] = [__v_373, __v_374, __v_401]; let __mq = record.memory_queries.get_mut(&3).ok_or(ExecError::InvalidMemorySize(3))?; if let Some(result) = __mq.get_mut(&__values[..]) { if !unconstrained { *result.multiplicity += G::ONE; } result.output[0] } else { let __ptr = G::from_usize(__mq.len()); __mq.insert(&__values[..], &[__ptr], G::from_bool(!unconstrained)); __ptr } }; - let __v_403: G = { let __values: [G; 3] = [__v_371, __v_372, __v_402]; let __mq = record.memory_queries.get_mut(&3).ok_or(ExecError::InvalidMemorySize(3))?; if let Some(result) = __mq.get_mut(&__values[..]) { if !unconstrained { *result.multiplicity += G::ONE; } result.output[0] } else { let __ptr = G::from_usize(__mq.len()); __mq.insert(&__values[..], &[__ptr], G::from_bool(!unconstrained)); __ptr } }; - let __v_404: G = { let __values: [G; 3] = [__v_369, __v_370, __v_403]; let __mq = record.memory_queries.get_mut(&3).ok_or(ExecError::InvalidMemorySize(3))?; if let Some(result) = __mq.get_mut(&__values[..]) { if !unconstrained { *result.multiplicity += G::ONE; } result.output[0] } else { let __ptr = G::from_usize(__mq.len()); __mq.insert(&__values[..], &[__ptr], G::from_bool(!unconstrained)); __ptr } }; - let __v_405: G = { let __values: [G; 3] = [__v_367, __v_368, __v_404]; let __mq = record.memory_queries.get_mut(&3).ok_or(ExecError::InvalidMemorySize(3))?; if let Some(result) = __mq.get_mut(&__values[..]) { if !unconstrained { *result.multiplicity += G::ONE; } result.output[0] } else { let __ptr = G::from_usize(__mq.len()); __mq.insert(&__values[..], &[__ptr], G::from_bool(!unconstrained)); __ptr } }; - let __v_406: G = { let __values: [G; 3] = [__v_365, __v_366, __v_405]; let __mq = record.memory_queries.get_mut(&3).ok_or(ExecError::InvalidMemorySize(3))?; if let Some(result) = __mq.get_mut(&__values[..]) { if !unconstrained { *result.multiplicity += G::ONE; } result.output[0] } else { let __ptr = G::from_usize(__mq.len()); __mq.insert(&__values[..], &[__ptr], G::from_bool(!unconstrained)); __ptr } }; - let __v_407: G = G::from_u64(1); - let __v_408: G = G::from_u64(1); - let __v_409: G = { let __values: [G; 3] = [__v_407, __v_408, __v_408]; let __mq = record.memory_queries.get_mut(&3).ok_or(ExecError::InvalidMemorySize(3))?; if let Some(result) = __mq.get_mut(&__values[..]) { if !unconstrained { *result.multiplicity += G::ONE; } result.output[0] } else { let __ptr = G::from_usize(__mq.len()); __mq.insert(&__values[..], &[__ptr], G::from_bool(!unconstrained)); __ptr } }; - let __r_arr: [G; OUT_152] = { let __args: [G; IN_152] = [__v_406, __v_409]; let __cu = unconstrained; if let Some(result) = record.function_queries[152].get_mut(&__args[..]) { if !__cu && *result.multiplicity == G::ZERO { aiur_fn_152(__args, record, io_buffer, false)? } else { if !unconstrained { *result.multiplicity += G::ONE; } let __ret: [G; OUT_152] = unsafe { *(result.output.as_ptr() as *const [G; OUT_152]) }; __ret } } else { aiur_fn_152(__args, record, io_buffer, __cu)? } }; + let __v_407: G = __mc_out___mc_2[0]; + let __r_arr: [G; OUT_149] = { let __args: [G; IN_149] = [__v_34, __v_316]; let __cu = unconstrained; if let Some(result) = record.function_queries[149].get_mut(&__args[..]) { if !__cu && *result.multiplicity == G::ZERO { aiur_fn_149(__args, record, io_buffer, false)? } else { if !unconstrained { *result.multiplicity += G::ONE; } let __ret: [G; OUT_149] = unsafe { *(result.output.as_ptr() as *const [G; OUT_149]) }; __ret } } else { aiur_fn_149(__args, record, io_buffer, __cu)? } }; + let __v_408: G = __r_arr[0]; + let __r_arr: [G; OUT_148] = { let __args: [G; IN_148] = [__v_24, __v_408]; let __cu = unconstrained; if let Some(result) = record.function_queries[148].get_mut(&__args[..]) { if !__cu && *result.multiplicity == G::ZERO { aiur_fn_148(__args, record, io_buffer, false)? } else { if !unconstrained { *result.multiplicity += G::ONE; } let __ret: [G; OUT_148] = unsafe { *(result.output.as_ptr() as *const [G; OUT_148]) }; __ret } } else { aiur_fn_148(__args, record, io_buffer, __cu)? } }; + let __v_409: G = __r_arr[0]; + let __r_arr: [G; OUT_148] = { let __args: [G; IN_148] = [__v_407, __v_409]; let __cu = unconstrained; if let Some(result) = record.function_queries[148].get_mut(&__args[..]) { if !__cu && *result.multiplicity == G::ZERO { aiur_fn_148(__args, record, io_buffer, false)? } else { if !unconstrained { *result.multiplicity += G::ONE; } let __ret: [G; OUT_148] = unsafe { *(result.output.as_ptr() as *const [G; OUT_148]) }; __ret } } else { aiur_fn_148(__args, record, io_buffer, __cu)? } }; let __v_410: G = __r_arr[0]; - let __v_411: G = __r_arr[1]; - let __v_412: G = __r_arr[2]; - let __v_413: G = __r_arr[3]; - let __v_414: G = __r_arr[4]; - let __v_415: G = __r_arr[5]; - let __v_416: G = __r_arr[6]; - let __v_417: G = __r_arr[7]; - let __v_418: G = __r_arr[8]; - let __v_419: G = __r_arr[9]; - let __v_420: G = __r_arr[10]; - let __v_421: G = __r_arr[11]; - let __v_422: G = __r_arr[12]; - let __v_423: G = __r_arr[13]; - let __v_424: G = __r_arr[14]; - let __v_425: G = __r_arr[15]; - let __v_426: G = __r_arr[16]; - let __v_427: G = __r_arr[17]; - let __v_428: G = G::from_u64(1); - let __v_429: G = G::from_u64(1); - let __v_430: G = { let __values: [G; 3] = [__v_428, __v_429, __v_429]; let __mq = record.memory_queries.get_mut(&3).ok_or(ExecError::InvalidMemorySize(3))?; if let Some(result) = __mq.get_mut(&__values[..]) { if !unconstrained { *result.multiplicity += G::ONE; } result.output[0] } else { let __ptr = G::from_usize(__mq.len()); __mq.insert(&__values[..], &[__ptr], G::from_bool(!unconstrained)); __ptr } }; - let __r_arr: [G; OUT_146] = { let __args: [G; IN_146] = [__v_418, __v_419, __v_420, __v_421, __v_422, __v_423, __v_424, __v_425, __v_430]; let __cu = unconstrained; if let Some(result) = record.function_queries[146].get_mut(&__args[..]) { if !__cu && *result.multiplicity == G::ZERO { aiur_fn_146(__args, record, io_buffer, false)? } else { if !unconstrained { *result.multiplicity += G::ONE; } let __ret: [G; OUT_146] = unsafe { *(result.output.as_ptr() as *const [G; OUT_146]) }; __ret } } else { aiur_fn_146(__args, record, io_buffer, __cu)? } }; - let __v_431: G = __r_arr[0]; - let __r_arr: [G; OUT_146] = { let __args: [G; IN_146] = [__v_410, __v_411, __v_412, __v_413, __v_414, __v_415, __v_416, __v_417, __v_431]; let __cu = unconstrained; if let Some(result) = record.function_queries[146].get_mut(&__args[..]) { if !__cu && *result.multiplicity == G::ZERO { aiur_fn_146(__args, record, io_buffer, false)? } else { if !unconstrained { *result.multiplicity += G::ONE; } let __ret: [G; OUT_146] = unsafe { *(result.output.as_ptr() as *const [G; OUT_146]) }; __ret } } else { aiur_fn_146(__args, record, io_buffer, __cu)? } }; - let __v_432: G = __r_arr[0]; - let __r_arr: [G; OUT_198] = { let __args: [G; IN_198] = [__v_426, __v_432]; let __cu = unconstrained; if let Some(result) = record.function_queries[198].get_mut(&__args[..]) { if !__cu && *result.multiplicity == G::ZERO { aiur_fn_198(__args, record, io_buffer, false)? } else { if !unconstrained { *result.multiplicity += G::ONE; } let __ret: [G; OUT_198] = unsafe { *(result.output.as_ptr() as *const [G; OUT_198]) }; __ret } } else { aiur_fn_198(__args, record, io_buffer, __cu)? } }; - let __v_433: G = __r_arr[0]; - let __v_434: G = G::from_u64(1); - let __v_435: G = G::from_u64(1); - let __v_436: G = { let __values: [G; 3] = [__v_434, __v_435, __v_435]; let __mq = record.memory_queries.get_mut(&3).ok_or(ExecError::InvalidMemorySize(3))?; if let Some(result) = __mq.get_mut(&__values[..]) { if !unconstrained { *result.multiplicity += G::ONE; } result.output[0] } else { let __ptr = G::from_usize(__mq.len()); __mq.insert(&__values[..], &[__ptr], G::from_bool(!unconstrained)); __ptr } }; - let __r_arr: [G; OUT_152] = { let __args: [G; IN_152] = [__v_433, __v_436]; let __cu = unconstrained; if let Some(result) = record.function_queries[152].get_mut(&__args[..]) { if !__cu && *result.multiplicity == G::ZERO { aiur_fn_152(__args, record, io_buffer, false)? } else { if !unconstrained { *result.multiplicity += G::ONE; } let __ret: [G; OUT_152] = unsafe { *(result.output.as_ptr() as *const [G; OUT_152]) }; __ret } } else { aiur_fn_152(__args, record, io_buffer, __cu)? } }; - let __v_437: G = __r_arr[0]; - let __v_438: G = __r_arr[1]; - let __v_439: G = __r_arr[2]; - let __v_440: G = __r_arr[3]; - let __v_441: G = __r_arr[4]; - let __v_442: G = __r_arr[5]; - let __v_443: G = __r_arr[6]; - let __v_444: G = __r_arr[7]; - let __v_445: G = __r_arr[8]; - let __v_446: G = __r_arr[9]; - let __v_447: G = __r_arr[10]; - let __v_448: G = __r_arr[11]; - let __v_449: G = __r_arr[12]; - let __v_450: G = __r_arr[13]; - let __v_451: G = __r_arr[14]; - let __v_452: G = __r_arr[15]; - let __v_453: G = __r_arr[16]; - let __v_454: G = __r_arr[17]; + let __r_arr: [G; OUT_149] = { let __args: [G; IN_149] = [__v_22, __v_410]; let __cu = unconstrained; if let Some(result) = record.function_queries[149].get_mut(&__args[..]) { if !__cu && *result.multiplicity == G::ZERO { aiur_fn_149(__args, record, io_buffer, false)? } else { if !unconstrained { *result.multiplicity += G::ONE; } let __ret: [G; OUT_149] = unsafe { *(result.output.as_ptr() as *const [G; OUT_149]) }; __ret } } else { aiur_fn_149(__args, record, io_buffer, __cu)? } }; + let __v_411: G = __r_arr[0]; + let __r_arr: [G; OUT_158] = { let __args: [G; IN_158] = [__v_310, __v_411]; let __cu = unconstrained; if let Some(result) = record.function_queries[158].get_mut(&__args[..]) { if !__cu && *result.multiplicity == G::ZERO { aiur_fn_158(__args, record, io_buffer, false)? } else { if !unconstrained { *result.multiplicity += G::ONE; } let __ret: [G; OUT_158] = unsafe { *(result.output.as_ptr() as *const [G; OUT_158]) }; __ret } } else { aiur_fn_158(__args, record, io_buffer, __cu)? } }; + let __v_412: G = __r_arr[0]; + let __v_413: G = G::from_u64(0); + let __v_414: G = G::from_u64(109); + let __v_415: G = G::from_u64(0); + let __v_416: G = G::from_u64(117); + let __v_417: G = G::from_u64(0); + let __v_418: G = G::from_u64(108); + let __v_419: G = G::from_u64(0); + let __v_420: G = G::from_u64(116); + let __v_421: G = G::from_u64(0); + let __v_422: G = G::from_u64(105); + let __v_423: G = G::from_u64(0); + let __v_424: G = G::from_u64(45); + let __v_425: G = G::from_u64(0); + let __v_426: G = G::from_u64(115); + let __v_427: G = G::from_u64(0); + let __v_428: G = G::from_u64(116); + let __v_429: G = G::from_u64(0); + let __v_430: G = G::from_u64(97); + let __v_431: G = G::from_u64(0); + let __v_432: G = G::from_u64(114); + let __v_433: G = G::from_u64(0); + let __v_434: G = G::from_u64(107); + let __v_435: G = G::from_u64(0); + let __v_436: G = G::from_u64(47); + let __v_437: G = G::from_u64(0); + let __v_438: G = G::from_u64(118); + let __v_439: G = G::from_u64(0); + let __v_440: G = G::from_u64(48); + let __v_441: G = { let __values: [G; 3] = [__v_439, __v_440, __v_412]; let __mq = record.memory_queries.get_mut(&3).ok_or(ExecError::InvalidMemorySize(3))?; if let Some(result) = __mq.get_mut(&__values[..]) { if !unconstrained { *result.multiplicity += G::ONE; } result.output[0] } else { let __ptr = G::from_usize(__mq.len()); __mq.insert(&__values[..], &[__ptr], G::from_bool(!unconstrained)); __ptr } }; + let __v_442: G = { let __values: [G; 3] = [__v_437, __v_438, __v_441]; let __mq = record.memory_queries.get_mut(&3).ok_or(ExecError::InvalidMemorySize(3))?; if let Some(result) = __mq.get_mut(&__values[..]) { if !unconstrained { *result.multiplicity += G::ONE; } result.output[0] } else { let __ptr = G::from_usize(__mq.len()); __mq.insert(&__values[..], &[__ptr], G::from_bool(!unconstrained)); __ptr } }; + let __v_443: G = { let __values: [G; 3] = [__v_435, __v_436, __v_442]; let __mq = record.memory_queries.get_mut(&3).ok_or(ExecError::InvalidMemorySize(3))?; if let Some(result) = __mq.get_mut(&__values[..]) { if !unconstrained { *result.multiplicity += G::ONE; } result.output[0] } else { let __ptr = G::from_usize(__mq.len()); __mq.insert(&__values[..], &[__ptr], G::from_bool(!unconstrained)); __ptr } }; + let __v_444: G = { let __values: [G; 3] = [__v_433, __v_434, __v_443]; let __mq = record.memory_queries.get_mut(&3).ok_or(ExecError::InvalidMemorySize(3))?; if let Some(result) = __mq.get_mut(&__values[..]) { if !unconstrained { *result.multiplicity += G::ONE; } result.output[0] } else { let __ptr = G::from_usize(__mq.len()); __mq.insert(&__values[..], &[__ptr], G::from_bool(!unconstrained)); __ptr } }; + let __v_445: G = { let __values: [G; 3] = [__v_431, __v_432, __v_444]; let __mq = record.memory_queries.get_mut(&3).ok_or(ExecError::InvalidMemorySize(3))?; if let Some(result) = __mq.get_mut(&__values[..]) { if !unconstrained { *result.multiplicity += G::ONE; } result.output[0] } else { let __ptr = G::from_usize(__mq.len()); __mq.insert(&__values[..], &[__ptr], G::from_bool(!unconstrained)); __ptr } }; + let __v_446: G = { let __values: [G; 3] = [__v_429, __v_430, __v_445]; let __mq = record.memory_queries.get_mut(&3).ok_or(ExecError::InvalidMemorySize(3))?; if let Some(result) = __mq.get_mut(&__values[..]) { if !unconstrained { *result.multiplicity += G::ONE; } result.output[0] } else { let __ptr = G::from_usize(__mq.len()); __mq.insert(&__values[..], &[__ptr], G::from_bool(!unconstrained)); __ptr } }; + let __v_447: G = { let __values: [G; 3] = [__v_427, __v_428, __v_446]; let __mq = record.memory_queries.get_mut(&3).ok_or(ExecError::InvalidMemorySize(3))?; if let Some(result) = __mq.get_mut(&__values[..]) { if !unconstrained { *result.multiplicity += G::ONE; } result.output[0] } else { let __ptr = G::from_usize(__mq.len()); __mq.insert(&__values[..], &[__ptr], G::from_bool(!unconstrained)); __ptr } }; + let __v_448: G = { let __values: [G; 3] = [__v_425, __v_426, __v_447]; let __mq = record.memory_queries.get_mut(&3).ok_or(ExecError::InvalidMemorySize(3))?; if let Some(result) = __mq.get_mut(&__values[..]) { if !unconstrained { *result.multiplicity += G::ONE; } result.output[0] } else { let __ptr = G::from_usize(__mq.len()); __mq.insert(&__values[..], &[__ptr], G::from_bool(!unconstrained)); __ptr } }; + let __v_449: G = { let __values: [G; 3] = [__v_423, __v_424, __v_448]; let __mq = record.memory_queries.get_mut(&3).ok_or(ExecError::InvalidMemorySize(3))?; if let Some(result) = __mq.get_mut(&__values[..]) { if !unconstrained { *result.multiplicity += G::ONE; } result.output[0] } else { let __ptr = G::from_usize(__mq.len()); __mq.insert(&__values[..], &[__ptr], G::from_bool(!unconstrained)); __ptr } }; + let __v_450: G = { let __values: [G; 3] = [__v_421, __v_422, __v_449]; let __mq = record.memory_queries.get_mut(&3).ok_or(ExecError::InvalidMemorySize(3))?; if let Some(result) = __mq.get_mut(&__values[..]) { if !unconstrained { *result.multiplicity += G::ONE; } result.output[0] } else { let __ptr = G::from_usize(__mq.len()); __mq.insert(&__values[..], &[__ptr], G::from_bool(!unconstrained)); __ptr } }; + let __v_451: G = { let __values: [G; 3] = [__v_419, __v_420, __v_450]; let __mq = record.memory_queries.get_mut(&3).ok_or(ExecError::InvalidMemorySize(3))?; if let Some(result) = __mq.get_mut(&__values[..]) { if !unconstrained { *result.multiplicity += G::ONE; } result.output[0] } else { let __ptr = G::from_usize(__mq.len()); __mq.insert(&__values[..], &[__ptr], G::from_bool(!unconstrained)); __ptr } }; + let __v_452: G = { let __values: [G; 3] = [__v_417, __v_418, __v_451]; let __mq = record.memory_queries.get_mut(&3).ok_or(ExecError::InvalidMemorySize(3))?; if let Some(result) = __mq.get_mut(&__values[..]) { if !unconstrained { *result.multiplicity += G::ONE; } result.output[0] } else { let __ptr = G::from_usize(__mq.len()); __mq.insert(&__values[..], &[__ptr], G::from_bool(!unconstrained)); __ptr } }; + let __v_453: G = { let __values: [G; 3] = [__v_415, __v_416, __v_452]; let __mq = record.memory_queries.get_mut(&3).ok_or(ExecError::InvalidMemorySize(3))?; if let Some(result) = __mq.get_mut(&__values[..]) { if !unconstrained { *result.multiplicity += G::ONE; } result.output[0] } else { let __ptr = G::from_usize(__mq.len()); __mq.insert(&__values[..], &[__ptr], G::from_bool(!unconstrained)); __ptr } }; + let __v_454: G = { let __values: [G; 3] = [__v_413, __v_414, __v_453]; let __mq = record.memory_queries.get_mut(&3).ok_or(ExecError::InvalidMemorySize(3))?; if let Some(result) = __mq.get_mut(&__values[..]) { if !unconstrained { *result.multiplicity += G::ONE; } result.output[0] } else { let __ptr = G::from_usize(__mq.len()); __mq.insert(&__values[..], &[__ptr], G::from_bool(!unconstrained)); __ptr } }; let __v_455: G = G::from_u64(1); let __v_456: G = G::from_u64(1); let __v_457: G = { let __values: [G; 3] = [__v_455, __v_456, __v_456]; let __mq = record.memory_queries.get_mut(&3).ok_or(ExecError::InvalidMemorySize(3))?; if let Some(result) = __mq.get_mut(&__values[..]) { if !unconstrained { *result.multiplicity += G::ONE; } result.output[0] } else { let __ptr = G::from_usize(__mq.len()); __mq.insert(&__values[..], &[__ptr], G::from_bool(!unconstrained)); __ptr } }; - let __r_arr: [G; OUT_146] = { let __args: [G; IN_146] = [__v_445, __v_446, __v_447, __v_448, __v_449, __v_450, __v_451, __v_452, __v_457]; let __cu = unconstrained; if let Some(result) = record.function_queries[146].get_mut(&__args[..]) { if !__cu && *result.multiplicity == G::ZERO { aiur_fn_146(__args, record, io_buffer, false)? } else { if !unconstrained { *result.multiplicity += G::ONE; } let __ret: [G; OUT_146] = unsafe { *(result.output.as_ptr() as *const [G; OUT_146]) }; __ret } } else { aiur_fn_146(__args, record, io_buffer, __cu)? } }; + let __r_arr: [G; OUT_152] = { let __args: [G; IN_152] = [__v_454, __v_457]; let __cu = unconstrained; if let Some(result) = record.function_queries[152].get_mut(&__args[..]) { if !__cu && *result.multiplicity == G::ZERO { aiur_fn_152(__args, record, io_buffer, false)? } else { if !unconstrained { *result.multiplicity += G::ONE; } let __ret: [G; OUT_152] = unsafe { *(result.output.as_ptr() as *const [G; OUT_152]) }; __ret } } else { aiur_fn_152(__args, record, io_buffer, __cu)? } }; let __v_458: G = __r_arr[0]; - let __r_arr: [G; OUT_146] = { let __args: [G; IN_146] = [__v_437, __v_438, __v_439, __v_440, __v_441, __v_442, __v_443, __v_444, __v_458]; let __cu = unconstrained; if let Some(result) = record.function_queries[146].get_mut(&__args[..]) { if !__cu && *result.multiplicity == G::ZERO { aiur_fn_146(__args, record, io_buffer, false)? } else { if !unconstrained { *result.multiplicity += G::ONE; } let __ret: [G; OUT_146] = unsafe { *(result.output.as_ptr() as *const [G; OUT_146]) }; __ret } } else { aiur_fn_146(__args, record, io_buffer, __cu)? } }; - let __v_459: G = __r_arr[0]; - let __r_arr: [G; OUT_198] = { let __args: [G; IN_198] = [__v_453, __v_459]; let __cu = unconstrained; if let Some(result) = record.function_queries[198].get_mut(&__args[..]) { if !__cu && *result.multiplicity == G::ZERO { aiur_fn_198(__args, record, io_buffer, false)? } else { if !unconstrained { *result.multiplicity += G::ONE; } let __ret: [G; OUT_198] = unsafe { *(result.output.as_ptr() as *const [G; OUT_198]) }; __ret } } else { aiur_fn_198(__args, record, io_buffer, __cu)? } }; - let __v_460: G = __r_arr[0]; - let __r_arr: [G; OUT_156] = { let __args: [G; IN_156] = [__v_460, __v_26]; let __cu = unconstrained; if let Some(result) = record.function_queries[156].get_mut(&__args[..]) { if !__cu && *result.multiplicity == G::ZERO { aiur_fn_156(__args, record, io_buffer, false)? } else { if !unconstrained { *result.multiplicity += G::ONE; } let __ret: [G; OUT_156] = unsafe { *(result.output.as_ptr() as *const [G; OUT_156]) }; __ret } } else { aiur_fn_156(__args, record, io_buffer, __cu)? } }; - let __v_461: G = __r_arr[0]; - let __v_462: G = G::from_u64(1); - let __v_463: G = G::from_u64(1); - let __v_464: G = { let __values: [G; 3] = [__v_462, __v_463, __v_463]; let __mq = record.memory_queries.get_mut(&3).ok_or(ExecError::InvalidMemorySize(3))?; if let Some(result) = __mq.get_mut(&__values[..]) { if !unconstrained { *result.multiplicity += G::ONE; } result.output[0] } else { let __ptr = G::from_usize(__mq.len()); __mq.insert(&__values[..], &[__ptr], G::from_bool(!unconstrained)); __ptr } }; - let __r_arr: [G; OUT_116] = { let __args: [G; IN_116] = [__v_30, __v_464]; let __cu = unconstrained; if let Some(result) = record.function_queries[116].get_mut(&__args[..]) { if !__cu && *result.multiplicity == G::ZERO { aiur_fn_116(__args, record, io_buffer, false)? } else { if !unconstrained { *result.multiplicity += G::ONE; } let __ret: [G; OUT_116] = unsafe { *(result.output.as_ptr() as *const [G; OUT_116]) }; __ret } } else { aiur_fn_116(__args, record, io_buffer, __cu)? } }; - let __v_465: G = __r_arr[0]; - let __r_arr: [G; OUT_198] = { let __args: [G; IN_198] = [__v_461, __v_465]; let __cu = unconstrained; if let Some(result) = record.function_queries[198].get_mut(&__args[..]) { if !__cu && *result.multiplicity == G::ZERO { aiur_fn_198(__args, record, io_buffer, false)? } else { if !unconstrained { *result.multiplicity += G::ONE; } let __ret: [G; OUT_198] = unsafe { *(result.output.as_ptr() as *const [G; OUT_198]) }; __ret } } else { aiur_fn_198(__args, record, io_buffer, __cu)? } }; - let __v_466: G = __r_arr[0]; - let __v_467: G = G::from_u64(1); - let __v_468: G = G::from_u64(1); - let __v_469: G = { let __values: [G; 3] = [__v_467, __v_468, __v_468]; let __mq = record.memory_queries.get_mut(&3).ok_or(ExecError::InvalidMemorySize(3))?; if let Some(result) = __mq.get_mut(&__values[..]) { if !unconstrained { *result.multiplicity += G::ONE; } result.output[0] } else { let __ptr = G::from_usize(__mq.len()); __mq.insert(&__values[..], &[__ptr], G::from_bool(!unconstrained)); __ptr } }; - let __r_arr: [G; OUT_152] = { let __args: [G; IN_152] = [__v_466, __v_469]; let __cu = unconstrained; if let Some(result) = record.function_queries[152].get_mut(&__args[..]) { if !__cu && *result.multiplicity == G::ZERO { aiur_fn_152(__args, record, io_buffer, false)? } else { if !unconstrained { *result.multiplicity += G::ONE; } let __ret: [G; OUT_152] = unsafe { *(result.output.as_ptr() as *const [G; OUT_152]) }; __ret } } else { aiur_fn_152(__args, record, io_buffer, __cu)? } }; - let __v_470: G = __r_arr[0]; - let __v_471: G = __r_arr[1]; - let __v_472: G = __r_arr[2]; - let __v_473: G = __r_arr[3]; - let __v_474: G = __r_arr[4]; - let __v_475: G = __r_arr[5]; - let __v_476: G = __r_arr[6]; - let __v_477: G = __r_arr[7]; - let __v_478: G = __r_arr[8]; - let __v_479: G = __r_arr[9]; - let __v_480: G = __r_arr[10]; - let __v_481: G = __r_arr[11]; - let __v_482: G = __r_arr[12]; - let __v_483: G = __r_arr[13]; - let __v_484: G = __r_arr[14]; - let __v_485: G = __r_arr[15]; - let __v_486: G = __r_arr[16]; - let __v_487: G = __r_arr[17]; - let __r_arr: [G; OUT_156] = { let __args: [G; IN_156] = [__v_486, __v_28]; let __cu = unconstrained; if let Some(result) = record.function_queries[156].get_mut(&__args[..]) { if !__cu && *result.multiplicity == G::ZERO { aiur_fn_156(__args, record, io_buffer, false)? } else { if !unconstrained { *result.multiplicity += G::ONE; } let __ret: [G; OUT_156] = unsafe { *(result.output.as_ptr() as *const [G; OUT_156]) }; __ret } } else { aiur_fn_156(__args, record, io_buffer, __cu)? } }; - let __v_488: G = __r_arr[0]; - let __v_489: G = G::from_u64(1); - let __v_490: G = G::from_u64(1); - let __v_491: G = { let __values: [G; 3] = [__v_489, __v_490, __v_490]; let __mq = record.memory_queries.get_mut(&3).ok_or(ExecError::InvalidMemorySize(3))?; if let Some(result) = __mq.get_mut(&__values[..]) { if !unconstrained { *result.multiplicity += G::ONE; } result.output[0] } else { let __ptr = G::from_usize(__mq.len()); __mq.insert(&__values[..], &[__ptr], G::from_bool(!unconstrained)); __ptr } }; - let __r_arr: [G; OUT_152] = { let __args: [G; IN_152] = [__v_488, __v_491]; let __cu = unconstrained; if let Some(result) = record.function_queries[152].get_mut(&__args[..]) { if !__cu && *result.multiplicity == G::ZERO { aiur_fn_152(__args, record, io_buffer, false)? } else { if !unconstrained { *result.multiplicity += G::ONE; } let __ret: [G; OUT_152] = unsafe { *(result.output.as_ptr() as *const [G; OUT_152]) }; __ret } } else { aiur_fn_152(__args, record, io_buffer, __cu)? } }; - let __v_492: G = __r_arr[0]; - let __v_493: G = __r_arr[1]; - let __v_494: G = __r_arr[2]; - let __v_495: G = __r_arr[3]; - let __v_496: G = __r_arr[4]; - let __v_497: G = __r_arr[5]; - let __v_498: G = __r_arr[6]; - let __v_499: G = __r_arr[7]; - let __v_500: G = __r_arr[8]; - let __v_501: G = __r_arr[9]; - let __v_502: G = __r_arr[10]; - let __v_503: G = __r_arr[11]; - let __v_504: G = __r_arr[12]; - let __v_505: G = __r_arr[13]; - let __v_506: G = __r_arr[14]; - let __v_507: G = __r_arr[15]; - let __v_508: G = __r_arr[16]; - let __v_509: G = __r_arr[17]; - let __v_510: G = G::from_u64(256); - let __v_511: G = (__v_510 * __v_411); - let __v_512: G = G::from_u64(65536); - let __v_513: G = (__v_512 * __v_412); - let __v_514: G = G::from_u64(16777216); - let __v_515: G = (__v_514 * __v_413); - let __v_516: G = G::from_u64(4294967296); - let __v_517: G = (__v_516 * __v_414); - let __v_518: G = G::from_u64(1099511627776); - let __v_519: G = (__v_518 * __v_415); - let __v_520: G = G::from_u64(281474976710656); - let __v_521: G = (__v_520 * __v_416); - let __v_522: G = G::from_u64(72057594037927936); - let __v_523: G = (__v_522 * __v_417); - let __v_524: G = (__v_521 + __v_523); - let __v_525: G = (__v_519 + __v_524); - let __v_526: G = (__v_517 + __v_525); - let __v_527: G = (__v_515 + __v_526); - let __v_528: G = (__v_513 + __v_527); - let __v_529: G = (__v_511 + __v_528); - let __v_530: G = (__v_410 + __v_529); - let __v_531: G = G::from_u64(256); - let __v_532: G = (__v_531 * __v_419); - let __v_533: G = G::from_u64(65536); - let __v_534: G = (__v_533 * __v_420); - let __v_535: G = G::from_u64(16777216); - let __v_536: G = (__v_535 * __v_421); - let __v_537: G = G::from_u64(4294967296); - let __v_538: G = (__v_537 * __v_422); - let __v_539: G = G::from_u64(1099511627776); - let __v_540: G = (__v_539 * __v_423); - let __v_541: G = G::from_u64(281474976710656); - let __v_542: G = (__v_541 * __v_424); - let __v_543: G = G::from_u64(72057594037927936); - let __v_544: G = (__v_543 * __v_425); - let __v_545: G = (__v_542 + __v_544); - let __v_546: G = (__v_540 + __v_545); - let __v_547: G = (__v_538 + __v_546); - let __v_548: G = (__v_536 + __v_547); - let __v_549: G = (__v_534 + __v_548); - let __v_550: G = (__v_532 + __v_549); - let __v_551: G = (__v_418 + __v_550); - let __v_552: G = G::from_u64(256); - let __v_553: G = (__v_552 * __v_438); - let __v_554: G = G::from_u64(65536); - let __v_555: G = (__v_554 * __v_439); - let __v_556: G = G::from_u64(16777216); - let __v_557: G = (__v_556 * __v_440); - let __v_558: G = G::from_u64(4294967296); - let __v_559: G = (__v_558 * __v_441); - let __v_560: G = G::from_u64(1099511627776); - let __v_561: G = (__v_560 * __v_442); - let __v_562: G = G::from_u64(281474976710656); - let __v_563: G = (__v_562 * __v_443); - let __v_564: G = G::from_u64(72057594037927936); - let __v_565: G = (__v_564 * __v_444); - let __v_566: G = (__v_563 + __v_565); - let __v_567: G = (__v_561 + __v_566); - let __v_568: G = (__v_559 + __v_567); - let __v_569: G = (__v_557 + __v_568); - let __v_570: G = (__v_555 + __v_569); - let __v_571: G = (__v_553 + __v_570); - let __v_572: G = (__v_437 + __v_571); - let __v_573: G = G::from_u64(256); - let __v_574: G = (__v_573 * __v_446); - let __v_575: G = G::from_u64(65536); - let __v_576: G = (__v_575 * __v_447); - let __v_577: G = G::from_u64(16777216); - let __v_578: G = (__v_577 * __v_448); - let __v_579: G = G::from_u64(4294967296); - let __v_580: G = (__v_579 * __v_449); - let __v_581: G = G::from_u64(1099511627776); - let __v_582: G = (__v_581 * __v_450); - let __v_583: G = G::from_u64(281474976710656); - let __v_584: G = (__v_583 * __v_451); - let __v_585: G = G::from_u64(72057594037927936); - let __v_586: G = (__v_585 * __v_452); - let __v_587: G = (__v_584 + __v_586); - let __v_588: G = (__v_582 + __v_587); - let __v_589: G = (__v_580 + __v_588); - let __v_590: G = (__v_578 + __v_589); - let __v_591: G = (__v_576 + __v_590); - let __v_592: G = (__v_574 + __v_591); - let __v_593: G = (__v_445 + __v_592); - let __v_594: G = G::from_u64(256); - let __v_595: G = (__v_594 * __v_471); - let __v_596: G = G::from_u64(65536); - let __v_597: G = (__v_596 * __v_472); - let __v_598: G = G::from_u64(16777216); - let __v_599: G = (__v_598 * __v_473); - let __v_600: G = G::from_u64(4294967296); - let __v_601: G = (__v_600 * __v_474); - let __v_602: G = G::from_u64(1099511627776); - let __v_603: G = (__v_602 * __v_475); - let __v_604: G = G::from_u64(281474976710656); - let __v_605: G = (__v_604 * __v_476); - let __v_606: G = G::from_u64(72057594037927936); - let __v_607: G = (__v_606 * __v_477); - let __v_608: G = (__v_605 + __v_607); - let __v_609: G = (__v_603 + __v_608); - let __v_610: G = (__v_601 + __v_609); - let __v_611: G = (__v_599 + __v_610); - let __v_612: G = (__v_597 + __v_611); - let __v_613: G = (__v_595 + __v_612); - let __v_614: G = (__v_470 + __v_613); - let __v_615: G = G::from_u64(256); - let __v_616: G = (__v_615 * __v_479); - let __v_617: G = G::from_u64(65536); - let __v_618: G = (__v_617 * __v_480); - let __v_619: G = G::from_u64(16777216); - let __v_620: G = (__v_619 * __v_481); - let __v_621: G = G::from_u64(4294967296); - let __v_622: G = (__v_621 * __v_482); - let __v_623: G = G::from_u64(1099511627776); - let __v_624: G = (__v_623 * __v_483); - let __v_625: G = G::from_u64(281474976710656); - let __v_626: G = (__v_625 * __v_484); - let __v_627: G = G::from_u64(72057594037927936); - let __v_628: G = (__v_627 * __v_485); - let __v_629: G = (__v_626 + __v_628); - let __v_630: G = (__v_624 + __v_629); - let __v_631: G = (__v_622 + __v_630); - let __v_632: G = (__v_620 + __v_631); - let __v_633: G = (__v_618 + __v_632); - let __v_634: G = (__v_616 + __v_633); - let __v_635: G = (__v_478 + __v_634); - let __v_636: G = G::from_u64(256); - let __v_637: G = (__v_636 * __v_493); - let __v_638: G = G::from_u64(65536); - let __v_639: G = (__v_638 * __v_494); - let __v_640: G = G::from_u64(16777216); - let __v_641: G = (__v_640 * __v_495); - let __v_642: G = G::from_u64(4294967296); - let __v_643: G = (__v_642 * __v_496); - let __v_644: G = G::from_u64(1099511627776); - let __v_645: G = (__v_644 * __v_497); - let __v_646: G = G::from_u64(281474976710656); - let __v_647: G = (__v_646 * __v_498); - let __v_648: G = G::from_u64(72057594037927936); - let __v_649: G = (__v_648 * __v_499); - let __v_650: G = (__v_647 + __v_649); - let __v_651: G = (__v_645 + __v_650); - let __v_652: G = (__v_643 + __v_651); - let __v_653: G = (__v_641 + __v_652); - let __v_654: G = (__v_639 + __v_653); - let __v_655: G = (__v_637 + __v_654); - let __v_656: G = (__v_492 + __v_655); - let __v_657: G = G::from_u64(256); - let __v_658: G = (__v_657 * __v_501); - let __v_659: G = G::from_u64(65536); - let __v_660: G = (__v_659 * __v_502); - let __v_661: G = G::from_u64(16777216); - let __v_662: G = (__v_661 * __v_503); - let __v_663: G = G::from_u64(4294967296); - let __v_664: G = (__v_663 * __v_504); - let __v_665: G = G::from_u64(1099511627776); - let __v_666: G = (__v_665 * __v_505); - let __v_667: G = G::from_u64(281474976710656); - let __v_668: G = (__v_667 * __v_506); - let __v_669: G = G::from_u64(72057594037927936); - let __v_670: G = (__v_669 * __v_507); - let __v_671: G = (__v_668 + __v_670); - let __v_672: G = (__v_666 + __v_671); - let __v_673: G = (__v_664 + __v_672); - let __v_674: G = (__v_662 + __v_673); - let __v_675: G = (__v_660 + __v_674); - let __v_676: G = (__v_658 + __v_675); - let __v_677: G = (__v_500 + __v_676); - let __v_678: G = G::from_u64(0); - let __v_679: G = G::from_u64(0); - let __r_arr: [G; OUT_182] = { let __args: [G; IN_182] = [__v_678, __v_679, __v_354, __v_530, __v_551, __v_572, __v_593]; let __cu = unconstrained; if let Some(result) = record.function_queries[182].get_mut(&__args[..]) { if !__cu && *result.multiplicity == G::ZERO { aiur_fn_182(__args, record, io_buffer, false)? } else { if !unconstrained { *result.multiplicity += G::ONE; } let __ret: [G; OUT_182] = unsafe { *(result.output.as_ptr() as *const [G; OUT_182]) }; __ret } } else { aiur_fn_182(__args, record, io_buffer, __cu)? } }; - let __v_680: G = __r_arr[0]; - let __v_681: G = __r_arr[1]; - let __v_682: G = G::from_u64(0); - let __r_arr: [G; OUT_180] = { let __args: [G; IN_180] = [__v_357, __v_358, __v_34, __v_30, __v_62, __v_64, __v_59, __v_60, __v_57, __v_682, __v_680, __v_681, __v_530, __v_551, __v_572, __v_593, __v_614, __v_635, __v_656, __v_677]; let __cu = unconstrained; if let Some(result) = record.function_queries[180].get_mut(&__args[..]) { if !__cu && *result.multiplicity == G::ZERO { aiur_fn_180(__args, record, io_buffer, false)? } else { if !unconstrained { *result.multiplicity += G::ONE; } let __ret: [G; OUT_180] = unsafe { *(result.output.as_ptr() as *const [G; OUT_180]) }; __ret } } else { aiur_fn_180(__args, record, io_buffer, __cu)? } }; - let __v_683: G = __r_arr[0]; - let __r_arr: [G; OUT_203] = { let __args: [G; IN_203] = [__v_357]; let __cu = unconstrained; if let Some(result) = record.function_queries[203].get_mut(&__args[..]) { if !__cu && *result.multiplicity == G::ZERO { aiur_fn_203(__args, record, io_buffer, false)? } else { if !unconstrained { *result.multiplicity += G::ONE; } let __ret: [G; OUT_203] = unsafe { *(result.output.as_ptr() as *const [G; OUT_203]) }; __ret } } else { aiur_fn_203(__args, record, io_buffer, __cu)? } }; - let __v_684: G = __r_arr[0]; + let __v_459: G = __r_arr[1]; + let __v_460: G = __r_arr[2]; + let __v_461: G = __r_arr[3]; + let __v_462: G = __r_arr[4]; + let __v_463: G = __r_arr[5]; + let __v_464: G = __r_arr[6]; + let __v_465: G = __r_arr[7]; + let __v_466: G = __r_arr[8]; + let __v_467: G = __r_arr[9]; + let __v_468: G = __r_arr[10]; + let __v_469: G = __r_arr[11]; + let __v_470: G = __r_arr[12]; + let __v_471: G = __r_arr[13]; + let __v_472: G = __r_arr[14]; + let __v_473: G = __r_arr[15]; + let __v_474: G = __r_arr[16]; + let __v_475: G = __r_arr[17]; + let __v_476: G = G::from_u64(1); + let __v_477: G = G::from_u64(1); + let __v_478: G = { let __values: [G; 3] = [__v_476, __v_477, __v_477]; let __mq = record.memory_queries.get_mut(&3).ok_or(ExecError::InvalidMemorySize(3))?; if let Some(result) = __mq.get_mut(&__values[..]) { if !unconstrained { *result.multiplicity += G::ONE; } result.output[0] } else { let __ptr = G::from_usize(__mq.len()); __mq.insert(&__values[..], &[__ptr], G::from_bool(!unconstrained)); __ptr } }; + let __r_arr: [G; OUT_146] = { let __args: [G; IN_146] = [__v_466, __v_467, __v_468, __v_469, __v_470, __v_471, __v_472, __v_473, __v_478]; let __cu = unconstrained; if let Some(result) = record.function_queries[146].get_mut(&__args[..]) { if !__cu && *result.multiplicity == G::ZERO { aiur_fn_146(__args, record, io_buffer, false)? } else { if !unconstrained { *result.multiplicity += G::ONE; } let __ret: [G; OUT_146] = unsafe { *(result.output.as_ptr() as *const [G; OUT_146]) }; __ret } } else { aiur_fn_146(__args, record, io_buffer, __cu)? } }; + let __v_479: G = __r_arr[0]; + let __r_arr: [G; OUT_146] = { let __args: [G; IN_146] = [__v_458, __v_459, __v_460, __v_461, __v_462, __v_463, __v_464, __v_465, __v_479]; let __cu = unconstrained; if let Some(result) = record.function_queries[146].get_mut(&__args[..]) { if !__cu && *result.multiplicity == G::ZERO { aiur_fn_146(__args, record, io_buffer, false)? } else { if !unconstrained { *result.multiplicity += G::ONE; } let __ret: [G; OUT_146] = unsafe { *(result.output.as_ptr() as *const [G; OUT_146]) }; __ret } } else { aiur_fn_146(__args, record, io_buffer, __cu)? } }; + let __v_480: G = __r_arr[0]; + let __r_arr: [G; OUT_198] = { let __args: [G; IN_198] = [__v_474, __v_480]; let __cu = unconstrained; if let Some(result) = record.function_queries[198].get_mut(&__args[..]) { if !__cu && *result.multiplicity == G::ZERO { aiur_fn_198(__args, record, io_buffer, false)? } else { if !unconstrained { *result.multiplicity += G::ONE; } let __ret: [G; OUT_198] = unsafe { *(result.output.as_ptr() as *const [G; OUT_198]) }; __ret } } else { aiur_fn_198(__args, record, io_buffer, __cu)? } }; + let __v_481: G = __r_arr[0]; + let __v_482: G = G::from_u64(1); + let __v_483: G = G::from_u64(1); + let __v_484: G = { let __values: [G; 3] = [__v_482, __v_483, __v_483]; let __mq = record.memory_queries.get_mut(&3).ok_or(ExecError::InvalidMemorySize(3))?; if let Some(result) = __mq.get_mut(&__values[..]) { if !unconstrained { *result.multiplicity += G::ONE; } result.output[0] } else { let __ptr = G::from_usize(__mq.len()); __mq.insert(&__values[..], &[__ptr], G::from_bool(!unconstrained)); __ptr } }; + let __r_arr: [G; OUT_152] = { let __args: [G; IN_152] = [__v_481, __v_484]; let __cu = unconstrained; if let Some(result) = record.function_queries[152].get_mut(&__args[..]) { if !__cu && *result.multiplicity == G::ZERO { aiur_fn_152(__args, record, io_buffer, false)? } else { if !unconstrained { *result.multiplicity += G::ONE; } let __ret: [G; OUT_152] = unsafe { *(result.output.as_ptr() as *const [G; OUT_152]) }; __ret } } else { aiur_fn_152(__args, record, io_buffer, __cu)? } }; + let __v_485: G = __r_arr[0]; + let __v_486: G = __r_arr[1]; + let __v_487: G = __r_arr[2]; + let __v_488: G = __r_arr[3]; + let __v_489: G = __r_arr[4]; + let __v_490: G = __r_arr[5]; + let __v_491: G = __r_arr[6]; + let __v_492: G = __r_arr[7]; + let __v_493: G = __r_arr[8]; + let __v_494: G = __r_arr[9]; + let __v_495: G = __r_arr[10]; + let __v_496: G = __r_arr[11]; + let __v_497: G = __r_arr[12]; + let __v_498: G = __r_arr[13]; + let __v_499: G = __r_arr[14]; + let __v_500: G = __r_arr[15]; + let __v_501: G = __r_arr[16]; + let __v_502: G = __r_arr[17]; + let __v_503: G = G::from_u64(1); + let __v_504: G = G::from_u64(1); + let __v_505: G = { let __values: [G; 3] = [__v_503, __v_504, __v_504]; let __mq = record.memory_queries.get_mut(&3).ok_or(ExecError::InvalidMemorySize(3))?; if let Some(result) = __mq.get_mut(&__values[..]) { if !unconstrained { *result.multiplicity += G::ONE; } result.output[0] } else { let __ptr = G::from_usize(__mq.len()); __mq.insert(&__values[..], &[__ptr], G::from_bool(!unconstrained)); __ptr } }; + let __r_arr: [G; OUT_146] = { let __args: [G; IN_146] = [__v_493, __v_494, __v_495, __v_496, __v_497, __v_498, __v_499, __v_500, __v_505]; let __cu = unconstrained; if let Some(result) = record.function_queries[146].get_mut(&__args[..]) { if !__cu && *result.multiplicity == G::ZERO { aiur_fn_146(__args, record, io_buffer, false)? } else { if !unconstrained { *result.multiplicity += G::ONE; } let __ret: [G; OUT_146] = unsafe { *(result.output.as_ptr() as *const [G; OUT_146]) }; __ret } } else { aiur_fn_146(__args, record, io_buffer, __cu)? } }; + let __v_506: G = __r_arr[0]; + let __r_arr: [G; OUT_146] = { let __args: [G; IN_146] = [__v_485, __v_486, __v_487, __v_488, __v_489, __v_490, __v_491, __v_492, __v_506]; let __cu = unconstrained; if let Some(result) = record.function_queries[146].get_mut(&__args[..]) { if !__cu && *result.multiplicity == G::ZERO { aiur_fn_146(__args, record, io_buffer, false)? } else { if !unconstrained { *result.multiplicity += G::ONE; } let __ret: [G; OUT_146] = unsafe { *(result.output.as_ptr() as *const [G; OUT_146]) }; __ret } } else { aiur_fn_146(__args, record, io_buffer, __cu)? } }; + let __v_507: G = __r_arr[0]; + let __r_arr: [G; OUT_198] = { let __args: [G; IN_198] = [__v_501, __v_507]; let __cu = unconstrained; if let Some(result) = record.function_queries[198].get_mut(&__args[..]) { if !__cu && *result.multiplicity == G::ZERO { aiur_fn_198(__args, record, io_buffer, false)? } else { if !unconstrained { *result.multiplicity += G::ONE; } let __ret: [G; OUT_198] = unsafe { *(result.output.as_ptr() as *const [G; OUT_198]) }; __ret } } else { aiur_fn_198(__args, record, io_buffer, __cu)? } }; + let __v_508: G = __r_arr[0]; + let __r_arr: [G; OUT_156] = { let __args: [G; IN_156] = [__v_508, __v_26]; let __cu = unconstrained; if let Some(result) = record.function_queries[156].get_mut(&__args[..]) { if !__cu && *result.multiplicity == G::ZERO { aiur_fn_156(__args, record, io_buffer, false)? } else { if !unconstrained { *result.multiplicity += G::ONE; } let __ret: [G; OUT_156] = unsafe { *(result.output.as_ptr() as *const [G; OUT_156]) }; __ret } } else { aiur_fn_156(__args, record, io_buffer, __cu)? } }; + let __v_509: G = __r_arr[0]; + let __v_510: G = G::from_u64(1); + let __v_511: G = G::from_u64(1); + let __v_512: G = { let __values: [G; 3] = [__v_510, __v_511, __v_511]; let __mq = record.memory_queries.get_mut(&3).ok_or(ExecError::InvalidMemorySize(3))?; if let Some(result) = __mq.get_mut(&__values[..]) { if !unconstrained { *result.multiplicity += G::ONE; } result.output[0] } else { let __ptr = G::from_usize(__mq.len()); __mq.insert(&__values[..], &[__ptr], G::from_bool(!unconstrained)); __ptr } }; + let __r_arr: [G; OUT_116] = { let __args: [G; IN_116] = [__v_30, __v_512]; let __cu = unconstrained; if let Some(result) = record.function_queries[116].get_mut(&__args[..]) { if !__cu && *result.multiplicity == G::ZERO { aiur_fn_116(__args, record, io_buffer, false)? } else { if !unconstrained { *result.multiplicity += G::ONE; } let __ret: [G; OUT_116] = unsafe { *(result.output.as_ptr() as *const [G; OUT_116]) }; __ret } } else { aiur_fn_116(__args, record, io_buffer, __cu)? } }; + let __v_513: G = __r_arr[0]; + let __r_arr: [G; OUT_198] = { let __args: [G; IN_198] = [__v_509, __v_513]; let __cu = unconstrained; if let Some(result) = record.function_queries[198].get_mut(&__args[..]) { if !__cu && *result.multiplicity == G::ZERO { aiur_fn_198(__args, record, io_buffer, false)? } else { if !unconstrained { *result.multiplicity += G::ONE; } let __ret: [G; OUT_198] = unsafe { *(result.output.as_ptr() as *const [G; OUT_198]) }; __ret } } else { aiur_fn_198(__args, record, io_buffer, __cu)? } }; + let __v_514: G = __r_arr[0]; + let __v_515: G = G::from_u64(1); + let __v_516: G = G::from_u64(1); + let __v_517: G = { let __values: [G; 3] = [__v_515, __v_516, __v_516]; let __mq = record.memory_queries.get_mut(&3).ok_or(ExecError::InvalidMemorySize(3))?; if let Some(result) = __mq.get_mut(&__values[..]) { if !unconstrained { *result.multiplicity += G::ONE; } result.output[0] } else { let __ptr = G::from_usize(__mq.len()); __mq.insert(&__values[..], &[__ptr], G::from_bool(!unconstrained)); __ptr } }; + let __r_arr: [G; OUT_152] = { let __args: [G; IN_152] = [__v_514, __v_517]; let __cu = unconstrained; if let Some(result) = record.function_queries[152].get_mut(&__args[..]) { if !__cu && *result.multiplicity == G::ZERO { aiur_fn_152(__args, record, io_buffer, false)? } else { if !unconstrained { *result.multiplicity += G::ONE; } let __ret: [G; OUT_152] = unsafe { *(result.output.as_ptr() as *const [G; OUT_152]) }; __ret } } else { aiur_fn_152(__args, record, io_buffer, __cu)? } }; + let __v_518: G = __r_arr[0]; + let __v_519: G = __r_arr[1]; + let __v_520: G = __r_arr[2]; + let __v_521: G = __r_arr[3]; + let __v_522: G = __r_arr[4]; + let __v_523: G = __r_arr[5]; + let __v_524: G = __r_arr[6]; + let __v_525: G = __r_arr[7]; + let __v_526: G = __r_arr[8]; + let __v_527: G = __r_arr[9]; + let __v_528: G = __r_arr[10]; + let __v_529: G = __r_arr[11]; + let __v_530: G = __r_arr[12]; + let __v_531: G = __r_arr[13]; + let __v_532: G = __r_arr[14]; + let __v_533: G = __r_arr[15]; + let __v_534: G = __r_arr[16]; + let __v_535: G = __r_arr[17]; + let __r_arr: [G; OUT_156] = { let __args: [G; IN_156] = [__v_534, __v_28]; let __cu = unconstrained; if let Some(result) = record.function_queries[156].get_mut(&__args[..]) { if !__cu && *result.multiplicity == G::ZERO { aiur_fn_156(__args, record, io_buffer, false)? } else { if !unconstrained { *result.multiplicity += G::ONE; } let __ret: [G; OUT_156] = unsafe { *(result.output.as_ptr() as *const [G; OUT_156]) }; __ret } } else { aiur_fn_156(__args, record, io_buffer, __cu)? } }; + let __v_536: G = __r_arr[0]; + let __v_537: G = G::from_u64(1); + let __v_538: G = G::from_u64(1); + let __v_539: G = { let __values: [G; 3] = [__v_537, __v_538, __v_538]; let __mq = record.memory_queries.get_mut(&3).ok_or(ExecError::InvalidMemorySize(3))?; if let Some(result) = __mq.get_mut(&__values[..]) { if !unconstrained { *result.multiplicity += G::ONE; } result.output[0] } else { let __ptr = G::from_usize(__mq.len()); __mq.insert(&__values[..], &[__ptr], G::from_bool(!unconstrained)); __ptr } }; + let __r_arr: [G; OUT_152] = { let __args: [G; IN_152] = [__v_536, __v_539]; let __cu = unconstrained; if let Some(result) = record.function_queries[152].get_mut(&__args[..]) { if !__cu && *result.multiplicity == G::ZERO { aiur_fn_152(__args, record, io_buffer, false)? } else { if !unconstrained { *result.multiplicity += G::ONE; } let __ret: [G; OUT_152] = unsafe { *(result.output.as_ptr() as *const [G; OUT_152]) }; __ret } } else { aiur_fn_152(__args, record, io_buffer, __cu)? } }; + let __v_540: G = __r_arr[0]; + let __v_541: G = __r_arr[1]; + let __v_542: G = __r_arr[2]; + let __v_543: G = __r_arr[3]; + let __v_544: G = __r_arr[4]; + let __v_545: G = __r_arr[5]; + let __v_546: G = __r_arr[6]; + let __v_547: G = __r_arr[7]; + let __v_548: G = __r_arr[8]; + let __v_549: G = __r_arr[9]; + let __v_550: G = __r_arr[10]; + let __v_551: G = __r_arr[11]; + let __v_552: G = __r_arr[12]; + let __v_553: G = __r_arr[13]; + let __v_554: G = __r_arr[14]; + let __v_555: G = __r_arr[15]; + let __v_556: G = __r_arr[16]; + let __v_557: G = __r_arr[17]; + let __v_558: G = G::from_u64(256); + let __v_559: G = (__v_558 * __v_459); + let __v_560: G = G::from_u64(65536); + let __v_561: G = (__v_560 * __v_460); + let __v_562: G = G::from_u64(16777216); + let __v_563: G = (__v_562 * __v_461); + let __v_564: G = G::from_u64(4294967296); + let __v_565: G = (__v_564 * __v_462); + let __v_566: G = G::from_u64(1099511627776); + let __v_567: G = (__v_566 * __v_463); + let __v_568: G = G::from_u64(281474976710656); + let __v_569: G = (__v_568 * __v_464); + let __v_570: G = G::from_u64(72057594037927936); + let __v_571: G = (__v_570 * __v_465); + let __v_572: G = (__v_569 + __v_571); + let __v_573: G = (__v_567 + __v_572); + let __v_574: G = (__v_565 + __v_573); + let __v_575: G = (__v_563 + __v_574); + let __v_576: G = (__v_561 + __v_575); + let __v_577: G = (__v_559 + __v_576); + let __v_578: G = (__v_458 + __v_577); + let __v_579: G = G::from_u64(256); + let __v_580: G = (__v_579 * __v_467); + let __v_581: G = G::from_u64(65536); + let __v_582: G = (__v_581 * __v_468); + let __v_583: G = G::from_u64(16777216); + let __v_584: G = (__v_583 * __v_469); + let __v_585: G = G::from_u64(4294967296); + let __v_586: G = (__v_585 * __v_470); + let __v_587: G = G::from_u64(1099511627776); + let __v_588: G = (__v_587 * __v_471); + let __v_589: G = G::from_u64(281474976710656); + let __v_590: G = (__v_589 * __v_472); + let __v_591: G = G::from_u64(72057594037927936); + let __v_592: G = (__v_591 * __v_473); + let __v_593: G = (__v_590 + __v_592); + let __v_594: G = (__v_588 + __v_593); + let __v_595: G = (__v_586 + __v_594); + let __v_596: G = (__v_584 + __v_595); + let __v_597: G = (__v_582 + __v_596); + let __v_598: G = (__v_580 + __v_597); + let __v_599: G = (__v_466 + __v_598); + let __v_600: G = G::from_u64(256); + let __v_601: G = (__v_600 * __v_486); + let __v_602: G = G::from_u64(65536); + let __v_603: G = (__v_602 * __v_487); + let __v_604: G = G::from_u64(16777216); + let __v_605: G = (__v_604 * __v_488); + let __v_606: G = G::from_u64(4294967296); + let __v_607: G = (__v_606 * __v_489); + let __v_608: G = G::from_u64(1099511627776); + let __v_609: G = (__v_608 * __v_490); + let __v_610: G = G::from_u64(281474976710656); + let __v_611: G = (__v_610 * __v_491); + let __v_612: G = G::from_u64(72057594037927936); + let __v_613: G = (__v_612 * __v_492); + let __v_614: G = (__v_611 + __v_613); + let __v_615: G = (__v_609 + __v_614); + let __v_616: G = (__v_607 + __v_615); + let __v_617: G = (__v_605 + __v_616); + let __v_618: G = (__v_603 + __v_617); + let __v_619: G = (__v_601 + __v_618); + let __v_620: G = (__v_485 + __v_619); + let __v_621: G = G::from_u64(256); + let __v_622: G = (__v_621 * __v_494); + let __v_623: G = G::from_u64(65536); + let __v_624: G = (__v_623 * __v_495); + let __v_625: G = G::from_u64(16777216); + let __v_626: G = (__v_625 * __v_496); + let __v_627: G = G::from_u64(4294967296); + let __v_628: G = (__v_627 * __v_497); + let __v_629: G = G::from_u64(1099511627776); + let __v_630: G = (__v_629 * __v_498); + let __v_631: G = G::from_u64(281474976710656); + let __v_632: G = (__v_631 * __v_499); + let __v_633: G = G::from_u64(72057594037927936); + let __v_634: G = (__v_633 * __v_500); + let __v_635: G = (__v_632 + __v_634); + let __v_636: G = (__v_630 + __v_635); + let __v_637: G = (__v_628 + __v_636); + let __v_638: G = (__v_626 + __v_637); + let __v_639: G = (__v_624 + __v_638); + let __v_640: G = (__v_622 + __v_639); + let __v_641: G = (__v_493 + __v_640); + let __v_642: G = G::from_u64(256); + let __v_643: G = (__v_642 * __v_519); + let __v_644: G = G::from_u64(65536); + let __v_645: G = (__v_644 * __v_520); + let __v_646: G = G::from_u64(16777216); + let __v_647: G = (__v_646 * __v_521); + let __v_648: G = G::from_u64(4294967296); + let __v_649: G = (__v_648 * __v_522); + let __v_650: G = G::from_u64(1099511627776); + let __v_651: G = (__v_650 * __v_523); + let __v_652: G = G::from_u64(281474976710656); + let __v_653: G = (__v_652 * __v_524); + let __v_654: G = G::from_u64(72057594037927936); + let __v_655: G = (__v_654 * __v_525); + let __v_656: G = (__v_653 + __v_655); + let __v_657: G = (__v_651 + __v_656); + let __v_658: G = (__v_649 + __v_657); + let __v_659: G = (__v_647 + __v_658); + let __v_660: G = (__v_645 + __v_659); + let __v_661: G = (__v_643 + __v_660); + let __v_662: G = (__v_518 + __v_661); + let __v_663: G = G::from_u64(256); + let __v_664: G = (__v_663 * __v_527); + let __v_665: G = G::from_u64(65536); + let __v_666: G = (__v_665 * __v_528); + let __v_667: G = G::from_u64(16777216); + let __v_668: G = (__v_667 * __v_529); + let __v_669: G = G::from_u64(4294967296); + let __v_670: G = (__v_669 * __v_530); + let __v_671: G = G::from_u64(1099511627776); + let __v_672: G = (__v_671 * __v_531); + let __v_673: G = G::from_u64(281474976710656); + let __v_674: G = (__v_673 * __v_532); + let __v_675: G = G::from_u64(72057594037927936); + let __v_676: G = (__v_675 * __v_533); + let __v_677: G = (__v_674 + __v_676); + let __v_678: G = (__v_672 + __v_677); + let __v_679: G = (__v_670 + __v_678); + let __v_680: G = (__v_668 + __v_679); + let __v_681: G = (__v_666 + __v_680); + let __v_682: G = (__v_664 + __v_681); + let __v_683: G = (__v_526 + __v_682); + let __v_684: G = G::from_u64(256); + let __v_685: G = (__v_684 * __v_541); + let __v_686: G = G::from_u64(65536); + let __v_687: G = (__v_686 * __v_542); + let __v_688: G = G::from_u64(16777216); + let __v_689: G = (__v_688 * __v_543); + let __v_690: G = G::from_u64(4294967296); + let __v_691: G = (__v_690 * __v_544); + let __v_692: G = G::from_u64(1099511627776); + let __v_693: G = (__v_692 * __v_545); + let __v_694: G = G::from_u64(281474976710656); + let __v_695: G = (__v_694 * __v_546); + let __v_696: G = G::from_u64(72057594037927936); + let __v_697: G = (__v_696 * __v_547); + let __v_698: G = (__v_695 + __v_697); + let __v_699: G = (__v_693 + __v_698); + let __v_700: G = (__v_691 + __v_699); + let __v_701: G = (__v_689 + __v_700); + let __v_702: G = (__v_687 + __v_701); + let __v_703: G = (__v_685 + __v_702); + let __v_704: G = (__v_540 + __v_703); + let __v_705: G = G::from_u64(256); + let __v_706: G = (__v_705 * __v_549); + let __v_707: G = G::from_u64(65536); + let __v_708: G = (__v_707 * __v_550); + let __v_709: G = G::from_u64(16777216); + let __v_710: G = (__v_709 * __v_551); + let __v_711: G = G::from_u64(4294967296); + let __v_712: G = (__v_711 * __v_552); + let __v_713: G = G::from_u64(1099511627776); + let __v_714: G = (__v_713 * __v_553); + let __v_715: G = G::from_u64(281474976710656); + let __v_716: G = (__v_715 * __v_554); + let __v_717: G = G::from_u64(72057594037927936); + let __v_718: G = (__v_717 * __v_555); + let __v_719: G = (__v_716 + __v_718); + let __v_720: G = (__v_714 + __v_719); + let __v_721: G = (__v_712 + __v_720); + let __v_722: G = (__v_710 + __v_721); + let __v_723: G = (__v_708 + __v_722); + let __v_724: G = (__v_706 + __v_723); + let __v_725: G = (__v_548 + __v_724); + let __v_726: G = G::from_u64(0); + let __v_727: G = G::from_u64(0); + let __r_arr: [G; OUT_182] = { let __args: [G; IN_182] = [__v_726, __v_727, __v_402, __v_578, __v_599, __v_620, __v_641]; let __cu = unconstrained; if let Some(result) = record.function_queries[182].get_mut(&__args[..]) { if !__cu && *result.multiplicity == G::ZERO { aiur_fn_182(__args, record, io_buffer, false)? } else { if !unconstrained { *result.multiplicity += G::ONE; } let __ret: [G; OUT_182] = unsafe { *(result.output.as_ptr() as *const [G; OUT_182]) }; __ret } } else { aiur_fn_182(__args, record, io_buffer, __cu)? } }; + let __v_728: G = __r_arr[0]; + let __v_729: G = __r_arr[1]; + let __v_730: G = G::from_u64(0); + let __r_arr: [G; OUT_180] = { let __args: [G; IN_180] = [__v_405, __v_406, __v_34, __v_30, __v_62, __v_64, __v_59, __v_60, __v_57, __v_730, __v_728, __v_729, __v_578, __v_599, __v_620, __v_641, __v_662, __v_683, __v_704, __v_725]; let __cu = unconstrained; if let Some(result) = record.function_queries[180].get_mut(&__args[..]) { if !__cu && *result.multiplicity == G::ZERO { aiur_fn_180(__args, record, io_buffer, false)? } else { if !unconstrained { *result.multiplicity += G::ONE; } let __ret: [G; OUT_180] = unsafe { *(result.output.as_ptr() as *const [G; OUT_180]) }; __ret } } else { aiur_fn_180(__args, record, io_buffer, __cu)? } }; + let __v_731: G = __r_arr[0]; + let __r_arr: [G; OUT_203] = { let __args: [G; IN_203] = [__v_405]; let __cu = unconstrained; if let Some(result) = record.function_queries[203].get_mut(&__args[..]) { if !__cu && *result.multiplicity == G::ZERO { aiur_fn_203(__args, record, io_buffer, false)? } else { if !unconstrained { *result.multiplicity += G::ONE; } let __ret: [G; OUT_203] = unsafe { *(result.output.as_ptr() as *const [G; OUT_203]) }; __ret } } else { aiur_fn_203(__args, record, io_buffer, __cu)? } }; + let __v_732: G = __r_arr[0]; match __v_38.as_canonical_u64() { _ => { let __r_arr: [G; OUT_204] = { let __args: [G; IN_204] = [__v_38]; let __cu = unconstrained; if let Some(result) = record.function_queries[204].get_mut(&__args[..]) { if !__cu && *result.multiplicity == G::ZERO { aiur_fn_204(__args, record, io_buffer, false)? } else { if !unconstrained { *result.multiplicity += G::ONE; } let __ret: [G; OUT_204] = unsafe { *(result.output.as_ptr() as *const [G; OUT_204]) }; __ret } } else { aiur_fn_204(__args, record, io_buffer, __cu)? } }; - let __v_685: G = __r_arr[0]; - let __v_686: G = G::from_u64(1); - let __v_687: G = G::from_u64(1); - let __v_688: G = { let __values: [G; 3] = [__v_686, __v_687, __v_687]; let __mq = record.memory_queries.get_mut(&3).ok_or(ExecError::InvalidMemorySize(3))?; if let Some(result) = __mq.get_mut(&__values[..]) { if !unconstrained { *result.multiplicity += G::ONE; } result.output[0] } else { let __ptr = G::from_usize(__mq.len()); __mq.insert(&__values[..], &[__ptr], G::from_bool(!unconstrained)); __ptr } }; + let __v_733: G = __r_arr[0]; + let __v_734: G = G::from_u64(1); + let __v_735: G = G::from_u64(1); + let __v_736: G = { let __values: [G; 3] = [__v_734, __v_735, __v_735]; let __mq = record.memory_queries.get_mut(&3).ok_or(ExecError::InvalidMemorySize(3))?; if let Some(result) = __mq.get_mut(&__values[..]) { if !unconstrained { *result.multiplicity += G::ONE; } result.output[0] } else { let __ptr = G::from_usize(__mq.len()); __mq.insert(&__values[..], &[__ptr], G::from_bool(!unconstrained)); __ptr } }; let __mc_out___mc_3: [G; 1] = '__mc_3: { match __v_59.as_canonical_u64() { 0u64 => { - break '__mc_3 [__v_688]; + break '__mc_3 [__v_736]; }, 1u64 => { - let __r_arr: [G; OUT_118] = { let __args: [G; IN_118] = [__v_60, __v_688]; let __cu = unconstrained; if let Some(result) = record.function_queries[118].get_mut(&__args[..]) { if !__cu && *result.multiplicity == G::ZERO { aiur_fn_118(__args, record, io_buffer, false)? } else { if !unconstrained { *result.multiplicity += G::ONE; } let __ret: [G; OUT_118] = unsafe { *(result.output.as_ptr() as *const [G; OUT_118]) }; __ret } } else { aiur_fn_118(__args, record, io_buffer, __cu)? } }; - let __v_689: G = __r_arr[0]; - break '__mc_3 [__v_689]; + let __r_arr: [G; OUT_118] = { let __args: [G; IN_118] = [__v_60, __v_736]; let __cu = unconstrained; if let Some(result) = record.function_queries[118].get_mut(&__args[..]) { if !__cu && *result.multiplicity == G::ZERO { aiur_fn_118(__args, record, io_buffer, false)? } else { if !unconstrained { *result.multiplicity += G::ONE; } let __ret: [G; OUT_118] = unsafe { *(result.output.as_ptr() as *const [G; OUT_118]) }; __ret } } else { aiur_fn_118(__args, record, io_buffer, __cu)? } }; + let __v_737: G = __r_arr[0]; + break '__mc_3 [__v_737]; }, _ => { return Err(ExecError::MatchNoCase(__v_59.as_canonical_u64())); }, } }; - let __v_689: G = __mc_out___mc_3[0]; - let __r_arr: [G; OUT_118] = { let __args: [G; IN_118] = [__v_57, __v_689]; let __cu = unconstrained; if let Some(result) = record.function_queries[118].get_mut(&__args[..]) { if !__cu && *result.multiplicity == G::ZERO { aiur_fn_118(__args, record, io_buffer, false)? } else { if !unconstrained { *result.multiplicity += G::ONE; } let __ret: [G; OUT_118] = unsafe { *(result.output.as_ptr() as *const [G; OUT_118]) }; __ret } } else { aiur_fn_118(__args, record, io_buffer, __cu)? } }; - let __v_690: G = __r_arr[0]; - let __r_arr: [G; OUT_118] = { let __args: [G; IN_118] = [__v_64, __v_690]; let __cu = unconstrained; if let Some(result) = record.function_queries[118].get_mut(&__args[..]) { if !__cu && *result.multiplicity == G::ZERO { aiur_fn_118(__args, record, io_buffer, false)? } else { if !unconstrained { *result.multiplicity += G::ONE; } let __ret: [G; OUT_118] = unsafe { *(result.output.as_ptr() as *const [G; OUT_118]) }; __ret } } else { aiur_fn_118(__args, record, io_buffer, __cu)? } }; - let __v_691: G = __r_arr[0]; - let __r_arr: [G; OUT_118] = { let __args: [G; IN_118] = [__v_62, __v_691]; let __cu = unconstrained; if let Some(result) = record.function_queries[118].get_mut(&__args[..]) { if !__cu && *result.multiplicity == G::ZERO { aiur_fn_118(__args, record, io_buffer, false)? } else { if !unconstrained { *result.multiplicity += G::ONE; } let __ret: [G; OUT_118] = unsafe { *(result.output.as_ptr() as *const [G; OUT_118]) }; __ret } } else { aiur_fn_118(__args, record, io_buffer, __cu)? } }; - let __v_692: G = __r_arr[0]; - let __r_arr: [G; OUT_198] = { let __args: [G; IN_198] = [__v_508, __v_692]; let __cu = unconstrained; if let Some(result) = record.function_queries[198].get_mut(&__args[..]) { if !__cu && *result.multiplicity == G::ZERO { aiur_fn_198(__args, record, io_buffer, false)? } else { if !unconstrained { *result.multiplicity += G::ONE; } let __ret: [G; OUT_198] = unsafe { *(result.output.as_ptr() as *const [G; OUT_198]) }; __ret } } else { aiur_fn_198(__args, record, io_buffer, __cu)? } }; - let __v_693: G = __r_arr[0]; - let __v_694: G = G::from_u64(1); - let __v_695: G = G::from_u64(1); - let __v_696: G = { let __values: [G; 3] = [__v_694, __v_695, __v_695]; let __mq = record.memory_queries.get_mut(&3).ok_or(ExecError::InvalidMemorySize(3))?; if let Some(result) = __mq.get_mut(&__values[..]) { if !unconstrained { *result.multiplicity += G::ONE; } result.output[0] } else { let __ptr = G::from_usize(__mq.len()); __mq.insert(&__values[..], &[__ptr], G::from_bool(!unconstrained)); __ptr } }; - let __r_arr: [G; OUT_152] = { let __args: [G; IN_152] = [__v_693, __v_696]; let __cu = unconstrained; if let Some(result) = record.function_queries[152].get_mut(&__args[..]) { if !__cu && *result.multiplicity == G::ZERO { aiur_fn_152(__args, record, io_buffer, false)? } else { if !unconstrained { *result.multiplicity += G::ONE; } let __ret: [G; OUT_152] = unsafe { *(result.output.as_ptr() as *const [G; OUT_152]) }; __ret } } else { aiur_fn_152(__args, record, io_buffer, __cu)? } }; - let __v_697: G = __r_arr[0]; - let __v_698: G = __r_arr[1]; - let __v_699: G = __r_arr[2]; - let __v_700: G = __r_arr[3]; - let __v_701: G = __r_arr[4]; - let __v_702: G = __r_arr[5]; - let __v_703: G = __r_arr[6]; - let __v_704: G = __r_arr[7]; - let __v_705: G = __r_arr[8]; - let __v_706: G = __r_arr[9]; - let __v_707: G = __r_arr[10]; - let __v_708: G = __r_arr[11]; - let __v_709: G = __r_arr[12]; - let __v_710: G = __r_arr[13]; - let __v_711: G = __r_arr[14]; - let __v_712: G = __r_arr[15]; - let __v_713: G = __r_arr[16]; - let __v_714: G = __r_arr[17]; - let __v_715: G = G::from_u64(256); - let __v_716: G = (__v_715 * __v_698); - let __v_717: G = G::from_u64(65536); - let __v_718: G = (__v_717 * __v_699); - let __v_719: G = G::from_u64(16777216); - let __v_720: G = (__v_719 * __v_700); - let __v_721: G = G::from_u64(4294967296); - let __v_722: G = (__v_721 * __v_701); - let __v_723: G = G::from_u64(1099511627776); - let __v_724: G = (__v_723 * __v_702); - let __v_725: G = G::from_u64(281474976710656); - let __v_726: G = (__v_725 * __v_703); - let __v_727: G = G::from_u64(72057594037927936); - let __v_728: G = (__v_727 * __v_704); - let __v_729: G = (__v_726 + __v_728); - let __v_730: G = (__v_724 + __v_729); - let __v_731: G = (__v_722 + __v_730); - let __v_732: G = (__v_720 + __v_731); - let __v_733: G = (__v_718 + __v_732); - let __v_734: G = (__v_716 + __v_733); - let __v_735: G = (__v_697 + __v_734); - let __v_736: G = G::from_u64(256); - let __v_737: G = (__v_736 * __v_706); - let __v_738: G = G::from_u64(65536); - let __v_739: G = (__v_738 * __v_707); - let __v_740: G = G::from_u64(16777216); - let __v_741: G = (__v_740 * __v_708); - let __v_742: G = G::from_u64(4294967296); - let __v_743: G = (__v_742 * __v_709); - let __v_744: G = G::from_u64(1099511627776); - let __v_745: G = (__v_744 * __v_710); - let __v_746: G = G::from_u64(281474976710656); - let __v_747: G = (__v_746 * __v_711); - let __v_748: G = G::from_u64(72057594037927936); - let __v_749: G = (__v_748 * __v_712); - let __v_750: G = (__v_747 + __v_749); - let __v_751: G = (__v_745 + __v_750); - let __v_752: G = (__v_743 + __v_751); - let __v_753: G = (__v_741 + __v_752); - let __v_754: G = (__v_739 + __v_753); - let __v_755: G = (__v_737 + __v_754); - let __v_756: G = (__v_705 + __v_755); - let __r_arr: [G; OUT_122] = { let __args: [G; IN_122] = [__v_713, __v_38, __v_40, __v_205]; let __cu = unconstrained; if let Some(result) = record.function_queries[122].get_mut(&__args[..]) { if !__cu && *result.multiplicity == G::ZERO { aiur_fn_122(__args, record, io_buffer, false)? } else { if !unconstrained { *result.multiplicity += G::ONE; } let __ret: [G; OUT_122] = unsafe { *(result.output.as_ptr() as *const [G; OUT_122]) }; __ret } } else { aiur_fn_122(__args, record, io_buffer, __cu)? } }; - let __v_757: G = __r_arr[0]; - let __v_758: G = __r_arr[1]; - let __v_759: G = G::from_u64(1); - let __v_760: G = G::from_u64(1); - let __v_761: G = { let __values: [G; 3] = [__v_759, __v_760, __v_760]; let __mq = record.memory_queries.get_mut(&3).ok_or(ExecError::InvalidMemorySize(3))?; if let Some(result) = __mq.get_mut(&__values[..]) { if !unconstrained { *result.multiplicity += G::ONE; } result.output[0] } else { let __ptr = G::from_usize(__mq.len()); __mq.insert(&__values[..], &[__ptr], G::from_bool(!unconstrained)); __ptr } }; - let __r_arr: [G; OUT_116] = { let __args: [G; IN_116] = [__v_46, __v_761]; let __cu = unconstrained; if let Some(result) = record.function_queries[116].get_mut(&__args[..]) { if !__cu && *result.multiplicity == G::ZERO { aiur_fn_116(__args, record, io_buffer, false)? } else { if !unconstrained { *result.multiplicity += G::ONE; } let __ret: [G; OUT_116] = unsafe { *(result.output.as_ptr() as *const [G; OUT_116]) }; __ret } } else { aiur_fn_116(__args, record, io_buffer, __cu)? } }; - let __v_762: G = __r_arr[0]; - let __r_arr: [G; OUT_198] = { let __args: [G; IN_198] = [__v_758, __v_762]; let __cu = unconstrained; if let Some(result) = record.function_queries[198].get_mut(&__args[..]) { if !__cu && *result.multiplicity == G::ZERO { aiur_fn_198(__args, record, io_buffer, false)? } else { if !unconstrained { *result.multiplicity += G::ONE; } let __ret: [G; OUT_198] = unsafe { *(result.output.as_ptr() as *const [G; OUT_198]) }; __ret } } else { aiur_fn_198(__args, record, io_buffer, __cu)? } }; - let __v_763: G = __r_arr[0]; - let __r_arr: [G; OUT_120] = { let __args: [G; IN_120] = [__v_763, __v_38]; let __cu = unconstrained; if let Some(result) = record.function_queries[120].get_mut(&__args[..]) { if !__cu && *result.multiplicity == G::ZERO { aiur_fn_120(__args, record, io_buffer, false)? } else { if !unconstrained { *result.multiplicity += G::ONE; } let __ret: [G; OUT_120] = unsafe { *(result.output.as_ptr() as *const [G; OUT_120]) }; __ret } } else { aiur_fn_120(__args, record, io_buffer, __cu)? } }; - let __v_764: G = __r_arr[0]; - let __r_arr: [G; OUT_121] = { let __args: [G; IN_121] = [__v_764, __v_48, __v_49, __v_50, __v_51, __v_52, __v_53, __v_54, __v_55, __v_215]; let __cu = unconstrained; if let Some(result) = record.function_queries[121].get_mut(&__args[..]) { if !__cu && *result.multiplicity == G::ZERO { aiur_fn_121(__args, record, io_buffer, false)? } else { if !unconstrained { *result.multiplicity += G::ONE; } let __ret: [G; OUT_121] = unsafe { *(result.output.as_ptr() as *const [G; OUT_121]) }; __ret } } else { aiur_fn_121(__args, record, io_buffer, __cu)? } }; - let __v_765: G = __r_arr[0]; - let __v_766: G = __r_arr[1]; - let __v_767: G = (__v_685 + __v_155); + let __v_737: G = __mc_out___mc_3[0]; + let __r_arr: [G; OUT_118] = { let __args: [G; IN_118] = [__v_57, __v_737]; let __cu = unconstrained; if let Some(result) = record.function_queries[118].get_mut(&__args[..]) { if !__cu && *result.multiplicity == G::ZERO { aiur_fn_118(__args, record, io_buffer, false)? } else { if !unconstrained { *result.multiplicity += G::ONE; } let __ret: [G; OUT_118] = unsafe { *(result.output.as_ptr() as *const [G; OUT_118]) }; __ret } } else { aiur_fn_118(__args, record, io_buffer, __cu)? } }; + let __v_738: G = __r_arr[0]; + let __r_arr: [G; OUT_118] = { let __args: [G; IN_118] = [__v_64, __v_738]; let __cu = unconstrained; if let Some(result) = record.function_queries[118].get_mut(&__args[..]) { if !__cu && *result.multiplicity == G::ZERO { aiur_fn_118(__args, record, io_buffer, false)? } else { if !unconstrained { *result.multiplicity += G::ONE; } let __ret: [G; OUT_118] = unsafe { *(result.output.as_ptr() as *const [G; OUT_118]) }; __ret } } else { aiur_fn_118(__args, record, io_buffer, __cu)? } }; + let __v_739: G = __r_arr[0]; + let __r_arr: [G; OUT_118] = { let __args: [G; IN_118] = [__v_62, __v_739]; let __cu = unconstrained; if let Some(result) = record.function_queries[118].get_mut(&__args[..]) { if !__cu && *result.multiplicity == G::ZERO { aiur_fn_118(__args, record, io_buffer, false)? } else { if !unconstrained { *result.multiplicity += G::ONE; } let __ret: [G; OUT_118] = unsafe { *(result.output.as_ptr() as *const [G; OUT_118]) }; __ret } } else { aiur_fn_118(__args, record, io_buffer, __cu)? } }; + let __v_740: G = __r_arr[0]; + let __r_arr: [G; OUT_198] = { let __args: [G; IN_198] = [__v_556, __v_740]; let __cu = unconstrained; if let Some(result) = record.function_queries[198].get_mut(&__args[..]) { if !__cu && *result.multiplicity == G::ZERO { aiur_fn_198(__args, record, io_buffer, false)? } else { if !unconstrained { *result.multiplicity += G::ONE; } let __ret: [G; OUT_198] = unsafe { *(result.output.as_ptr() as *const [G; OUT_198]) }; __ret } } else { aiur_fn_198(__args, record, io_buffer, __cu)? } }; + let __v_741: G = __r_arr[0]; + let __v_742: G = G::from_u64(1); + let __v_743: G = G::from_u64(1); + let __v_744: G = { let __values: [G; 3] = [__v_742, __v_743, __v_743]; let __mq = record.memory_queries.get_mut(&3).ok_or(ExecError::InvalidMemorySize(3))?; if let Some(result) = __mq.get_mut(&__values[..]) { if !unconstrained { *result.multiplicity += G::ONE; } result.output[0] } else { let __ptr = G::from_usize(__mq.len()); __mq.insert(&__values[..], &[__ptr], G::from_bool(!unconstrained)); __ptr } }; + let __r_arr: [G; OUT_152] = { let __args: [G; IN_152] = [__v_741, __v_744]; let __cu = unconstrained; if let Some(result) = record.function_queries[152].get_mut(&__args[..]) { if !__cu && *result.multiplicity == G::ZERO { aiur_fn_152(__args, record, io_buffer, false)? } else { if !unconstrained { *result.multiplicity += G::ONE; } let __ret: [G; OUT_152] = unsafe { *(result.output.as_ptr() as *const [G; OUT_152]) }; __ret } } else { aiur_fn_152(__args, record, io_buffer, __cu)? } }; + let __v_745: G = __r_arr[0]; + let __v_746: G = __r_arr[1]; + let __v_747: G = __r_arr[2]; + let __v_748: G = __r_arr[3]; + let __v_749: G = __r_arr[4]; + let __v_750: G = __r_arr[5]; + let __v_751: G = __r_arr[6]; + let __v_752: G = __r_arr[7]; + let __v_753: G = __r_arr[8]; + let __v_754: G = __r_arr[9]; + let __v_755: G = __r_arr[10]; + let __v_756: G = __r_arr[11]; + let __v_757: G = __r_arr[12]; + let __v_758: G = __r_arr[13]; + let __v_759: G = __r_arr[14]; + let __v_760: G = __r_arr[15]; + let __v_761: G = __r_arr[16]; + let __v_762: G = __r_arr[17]; + let __v_763: G = G::from_u64(256); + let __v_764: G = (__v_763 * __v_746); + let __v_765: G = G::from_u64(65536); + let __v_766: G = (__v_765 * __v_747); + let __v_767: G = G::from_u64(16777216); + let __v_768: G = (__v_767 * __v_748); + let __v_769: G = G::from_u64(4294967296); + let __v_770: G = (__v_769 * __v_749); + let __v_771: G = G::from_u64(1099511627776); + let __v_772: G = (__v_771 * __v_750); + let __v_773: G = G::from_u64(281474976710656); + let __v_774: G = (__v_773 * __v_751); + let __v_775: G = G::from_u64(72057594037927936); + let __v_776: G = (__v_775 * __v_752); + let __v_777: G = (__v_774 + __v_776); + let __v_778: G = (__v_772 + __v_777); + let __v_779: G = (__v_770 + __v_778); + let __v_780: G = (__v_768 + __v_779); + let __v_781: G = (__v_766 + __v_780); + let __v_782: G = (__v_764 + __v_781); + let __v_783: G = (__v_745 + __v_782); + let __v_784: G = G::from_u64(256); + let __v_785: G = (__v_784 * __v_754); + let __v_786: G = G::from_u64(65536); + let __v_787: G = (__v_786 * __v_755); + let __v_788: G = G::from_u64(16777216); + let __v_789: G = (__v_788 * __v_756); + let __v_790: G = G::from_u64(4294967296); + let __v_791: G = (__v_790 * __v_757); + let __v_792: G = G::from_u64(1099511627776); + let __v_793: G = (__v_792 * __v_758); + let __v_794: G = G::from_u64(281474976710656); + let __v_795: G = (__v_794 * __v_759); + let __v_796: G = G::from_u64(72057594037927936); + let __v_797: G = (__v_796 * __v_760); + let __v_798: G = (__v_795 + __v_797); + let __v_799: G = (__v_793 + __v_798); + let __v_800: G = (__v_791 + __v_799); + let __v_801: G = (__v_789 + __v_800); + let __v_802: G = (__v_787 + __v_801); + let __v_803: G = (__v_785 + __v_802); + let __v_804: G = (__v_753 + __v_803); + let __r_arr: [G; OUT_122] = { let __args: [G; IN_122] = [__v_761, __v_38, __v_40, __v_205]; let __cu = unconstrained; if let Some(result) = record.function_queries[122].get_mut(&__args[..]) { if !__cu && *result.multiplicity == G::ZERO { aiur_fn_122(__args, record, io_buffer, false)? } else { if !unconstrained { *result.multiplicity += G::ONE; } let __ret: [G; OUT_122] = unsafe { *(result.output.as_ptr() as *const [G; OUT_122]) }; __ret } } else { aiur_fn_122(__args, record, io_buffer, __cu)? } }; + let __v_805: G = __r_arr[0]; + let __v_806: G = __r_arr[1]; + let __v_807: G = G::from_u64(1); + let __v_808: G = G::from_u64(1); + let __v_809: G = { let __values: [G; 3] = [__v_807, __v_808, __v_808]; let __mq = record.memory_queries.get_mut(&3).ok_or(ExecError::InvalidMemorySize(3))?; if let Some(result) = __mq.get_mut(&__values[..]) { if !unconstrained { *result.multiplicity += G::ONE; } result.output[0] } else { let __ptr = G::from_usize(__mq.len()); __mq.insert(&__values[..], &[__ptr], G::from_bool(!unconstrained)); __ptr } }; + let __r_arr: [G; OUT_116] = { let __args: [G; IN_116] = [__v_46, __v_809]; let __cu = unconstrained; if let Some(result) = record.function_queries[116].get_mut(&__args[..]) { if !__cu && *result.multiplicity == G::ZERO { aiur_fn_116(__args, record, io_buffer, false)? } else { if !unconstrained { *result.multiplicity += G::ONE; } let __ret: [G; OUT_116] = unsafe { *(result.output.as_ptr() as *const [G; OUT_116]) }; __ret } } else { aiur_fn_116(__args, record, io_buffer, __cu)? } }; + let __v_810: G = __r_arr[0]; + let __r_arr: [G; OUT_198] = { let __args: [G; IN_198] = [__v_806, __v_810]; let __cu = unconstrained; if let Some(result) = record.function_queries[198].get_mut(&__args[..]) { if !__cu && *result.multiplicity == G::ZERO { aiur_fn_198(__args, record, io_buffer, false)? } else { if !unconstrained { *result.multiplicity += G::ONE; } let __ret: [G; OUT_198] = unsafe { *(result.output.as_ptr() as *const [G; OUT_198]) }; __ret } } else { aiur_fn_198(__args, record, io_buffer, __cu)? } }; + let __v_811: G = __r_arr[0]; + let __r_arr: [G; OUT_120] = { let __args: [G; IN_120] = [__v_811, __v_38]; let __cu = unconstrained; if let Some(result) = record.function_queries[120].get_mut(&__args[..]) { if !__cu && *result.multiplicity == G::ZERO { aiur_fn_120(__args, record, io_buffer, false)? } else { if !unconstrained { *result.multiplicity += G::ONE; } let __ret: [G; OUT_120] = unsafe { *(result.output.as_ptr() as *const [G; OUT_120]) }; __ret } } else { aiur_fn_120(__args, record, io_buffer, __cu)? } }; + let __v_812: G = __r_arr[0]; + let __r_arr: [G; OUT_121] = { let __args: [G; IN_121] = [__v_812, __v_48, __v_49, __v_50, __v_51, __v_52, __v_53, __v_54, __v_55, __v_215]; let __cu = unconstrained; if let Some(result) = record.function_queries[121].get_mut(&__args[..]) { if !__cu && *result.multiplicity == G::ZERO { aiur_fn_121(__args, record, io_buffer, false)? } else { if !unconstrained { *result.multiplicity += G::ONE; } let __ret: [G; OUT_121] = unsafe { *(result.output.as_ptr() as *const [G; OUT_121]) }; __ret } } else { aiur_fn_121(__args, record, io_buffer, __cu)? } }; + let __v_813: G = __r_arr[0]; + let __v_814: G = __r_arr[1]; + let __v_815: G = (__v_733 + __v_155); let __r_arr: [G; OUT_184] = { let __args: [G; IN_184] = [__v_22]; let __cu = unconstrained; if let Some(result) = record.function_queries[184].get_mut(&__args[..]) { if !__cu && *result.multiplicity == G::ZERO { aiur_fn_184(__args, record, io_buffer, false)? } else { if !unconstrained { *result.multiplicity += G::ONE; } let __ret: [G; OUT_184] = unsafe { *(result.output.as_ptr() as *const [G; OUT_184]) }; __ret } } else { aiur_fn_184(__args, record, io_buffer, __cu)? } }; - let __v_768: G = __r_arr[0]; - let __v_769: G = G::from_u64(1); - if (__v_768 != __v_769) { - return Err(ExecError::AssertEqMismatch { lhs: __v_768.as_canonical_u64(), rhs: __v_769.as_canonical_u64(), msg: None }); + let __v_816: G = __r_arr[0]; + let __v_817: G = G::from_u64(1); + if (__v_816 != __v_817) { + return Err(ExecError::AssertEqMismatch { lhs: __v_816.as_canonical_u64(), rhs: __v_817.as_canonical_u64(), msg: None }); } let __r_arr: [G; OUT_204] = { let __args: [G; IN_204] = [__v_22]; let __cu = unconstrained; if let Some(result) = record.function_queries[204].get_mut(&__args[..]) { if !__cu && *result.multiplicity == G::ZERO { aiur_fn_204(__args, record, io_buffer, false)? } else { if !unconstrained { *result.multiplicity += G::ONE; } let __ret: [G; OUT_204] = unsafe { *(result.output.as_ptr() as *const [G; OUT_204]) }; __ret } } else { aiur_fn_204(__args, record, io_buffer, __cu)? } }; - let __v_770: G = __r_arr[0]; + let __v_818: G = __r_arr[0]; let __r_arr: [G; OUT_203] = { let __args: [G; IN_203] = [__v_252]; let __cu = unconstrained; if let Some(result) = record.function_queries[203].get_mut(&__args[..]) { if !__cu && *result.multiplicity == G::ZERO { aiur_fn_203(__args, record, io_buffer, false)? } else { if !unconstrained { *result.multiplicity += G::ONE; } let __ret: [G; OUT_203] = unsafe { *(result.output.as_ptr() as *const [G; OUT_203]) }; __ret } } else { aiur_fn_203(__args, record, io_buffer, __cu)? } }; - let __v_771: G = __r_arr[0]; - let __v_772: G = (__v_770 - __v_771); - let __v_773: G = G::from_bool((__v_772 == G::ZERO)); - let __v_774: G = G::from_u64(1); - if (__v_773 != __v_774) { - return Err(ExecError::AssertEqMismatch { lhs: __v_773.as_canonical_u64(), rhs: __v_774.as_canonical_u64(), msg: None }); + let __v_819: G = __r_arr[0]; + let __v_820: G = (__v_818 - __v_819); + let __v_821: G = G::from_bool((__v_820 == G::ZERO)); + let __v_822: G = G::from_u64(1); + if (__v_821 != __v_822) { + return Err(ExecError::AssertEqMismatch { lhs: __v_821.as_canonical_u64(), rhs: __v_822.as_canonical_u64(), msg: None }); } - let __r_arr: [G; OUT_203] = { let __args: [G; IN_203] = [__v_357]; let __cu = unconstrained; if let Some(result) = record.function_queries[203].get_mut(&__args[..]) { if !__cu && *result.multiplicity == G::ZERO { aiur_fn_203(__args, record, io_buffer, false)? } else { if !unconstrained { *result.multiplicity += G::ONE; } let __ret: [G; OUT_203] = unsafe { *(result.output.as_ptr() as *const [G; OUT_203]) }; __ret } } else { aiur_fn_203(__args, record, io_buffer, __cu)? } }; - let __v_775: G = __r_arr[0]; + let __r_arr: [G; OUT_203] = { let __args: [G; IN_203] = [__v_405]; let __cu = unconstrained; if let Some(result) = record.function_queries[203].get_mut(&__args[..]) { if !__cu && *result.multiplicity == G::ZERO { aiur_fn_203(__args, record, io_buffer, false)? } else { if !unconstrained { *result.multiplicity += G::ONE; } let __ret: [G; OUT_203] = unsafe { *(result.output.as_ptr() as *const [G; OUT_203]) }; __ret } } else { aiur_fn_203(__args, record, io_buffer, __cu)? } }; + let __v_823: G = __r_arr[0]; let __r_arr: [G; OUT_196] = { let __args: [G; IN_196] = [__v_30]; let __cu = unconstrained; if let Some(result) = record.function_queries[196].get_mut(&__args[..]) { if !__cu && *result.multiplicity == G::ZERO { aiur_fn_196(__args, record, io_buffer, false)? } else { if !unconstrained { *result.multiplicity += G::ONE; } let __ret: [G; OUT_196] = unsafe { *(result.output.as_ptr() as *const [G; OUT_196]) }; __ret } } else { aiur_fn_196(__args, record, io_buffer, __cu)? } }; - let __v_776: G = __r_arr[0]; - let __v_777: G = (__v_775 - __v_776); - let __v_778: G = G::from_bool((__v_777 == G::ZERO)); - let __v_779: G = G::from_u64(1); - if (__v_778 != __v_779) { - return Err(ExecError::AssertEqMismatch { lhs: __v_778.as_canonical_u64(), rhs: __v_779.as_canonical_u64(), msg: None }); + let __v_824: G = __r_arr[0]; + let __v_825: G = (__v_823 - __v_824); + let __v_826: G = G::from_bool((__v_825 == G::ZERO)); + let __v_827: G = G::from_u64(1); + if (__v_826 != __v_827) { + return Err(ExecError::AssertEqMismatch { lhs: __v_826.as_canonical_u64(), rhs: __v_827.as_canonical_u64(), msg: None }); } let __r_arr: [G; OUT_201] = { let __args: [G; IN_201] = [__v_40]; let __cu = unconstrained; if let Some(result) = record.function_queries[201].get_mut(&__args[..]) { if !__cu && *result.multiplicity == G::ZERO { aiur_fn_201(__args, record, io_buffer, false)? } else { if !unconstrained { *result.multiplicity += G::ONE; } let __ret: [G; OUT_201] = unsafe { *(result.output.as_ptr() as *const [G; OUT_201]) }; __ret } } else { aiur_fn_201(__args, record, io_buffer, __cu)? } }; - let __v_780: G = __r_arr[0]; - let __v_781: G = (__v_780 - __v_685); - let __v_782: G = G::from_bool((__v_781 == G::ZERO)); - let __v_783: G = G::from_u64(1); - if (__v_782 != __v_783) { - return Err(ExecError::AssertEqMismatch { lhs: __v_782.as_canonical_u64(), rhs: __v_783.as_canonical_u64(), msg: None }); + let __v_828: G = __r_arr[0]; + let __v_829: G = (__v_828 - __v_733); + let __v_830: G = G::from_bool((__v_829 == G::ZERO)); + let __v_831: G = G::from_u64(1); + if (__v_830 != __v_831) { + return Err(ExecError::AssertEqMismatch { lhs: __v_830.as_canonical_u64(), rhs: __v_831.as_canonical_u64(), msg: None }); } let __r_arr: [G; OUT_196] = { let __args: [G; IN_196] = [__v_44]; let __cu = unconstrained; if let Some(result) = record.function_queries[196].get_mut(&__args[..]) { if !__cu && *result.multiplicity == G::ZERO { aiur_fn_196(__args, record, io_buffer, false)? } else { if !unconstrained { *result.multiplicity += G::ONE; } let __ret: [G; OUT_196] = unsafe { *(result.output.as_ptr() as *const [G; OUT_196]) }; __ret } } else { aiur_fn_196(__args, record, io_buffer, __cu)? } }; - let __v_784: G = __r_arr[0]; - let __v_785: G = (__v_784 - __v_195); - let __v_786: G = G::from_bool((__v_785 == G::ZERO)); - let __v_787: G = G::from_u64(1); - if (__v_786 != __v_787) { - return Err(ExecError::AssertEqMismatch { lhs: __v_786.as_canonical_u64(), rhs: __v_787.as_canonical_u64(), msg: None }); + let __v_832: G = __r_arr[0]; + let __v_833: G = (__v_832 - __v_195); + let __v_834: G = G::from_bool((__v_833 == G::ZERO)); + let __v_835: G = G::from_u64(1); + if (__v_834 != __v_835) { + return Err(ExecError::AssertEqMismatch { lhs: __v_834.as_canonical_u64(), rhs: __v_835.as_canonical_u64(), msg: None }); } let __r_arr: [G; OUT_196] = { let __args: [G; IN_196] = [__v_46]; let __cu = unconstrained; if let Some(result) = record.function_queries[196].get_mut(&__args[..]) { if !__cu && *result.multiplicity == G::ZERO { aiur_fn_196(__args, record, io_buffer, false)? } else { if !unconstrained { *result.multiplicity += G::ONE; } let __ret: [G; OUT_196] = unsafe { *(result.output.as_ptr() as *const [G; OUT_196]) }; __ret } } else { aiur_fn_196(__args, record, io_buffer, __cu)? } }; - let __v_788: G = __r_arr[0]; - let __v_789: G = G::from_u64(1); - if (__v_788 != __v_789) { - return Err(ExecError::AssertEqMismatch { lhs: __v_788.as_canonical_u64(), rhs: __v_789.as_canonical_u64(), msg: None }); + let __v_836: G = __r_arr[0]; + let __v_837: G = G::from_u64(1); + if (__v_836 != __v_837) { + return Err(ExecError::AssertEqMismatch { lhs: __v_836.as_canonical_u64(), rhs: __v_837.as_canonical_u64(), msg: None }); } - let __v_790: G = G::from_u64(33); - let __v_791: G = { let __a_val = __v_767.as_canonical_u64(); let __b_val = __v_790.as_canonical_u64(); let __a_u32 = u32::try_from(__a_val).ok().ok_or(ExecError::U32OutOfRange(__a_val))?; let __b_u32 = u32::try_from(__b_val).ok().ok_or(ExecError::U32OutOfRange(__b_val))?; let __result = G::from_bool(__a_u32 < __b_u32); if !unconstrained { let __x_bytes = __a_u32.to_le_bytes(); let __z_bytes = __b_u32.to_le_bytes(); let __c_u32 = __b_u32.wrapping_sub(__a_u32).wrapping_sub(1); let __y_bytes = __c_u32.to_le_bytes(); record.bytes2_queries.bump_range_check(&G::from_u8(__x_bytes[0]), &G::from_u8(__x_bytes[1])); record.bytes2_queries.bump_range_check(&G::from_u8(__x_bytes[2]), &G::from_u8(__x_bytes[3])); record.bytes2_queries.bump_range_check(&G::from_u8(__y_bytes[0]), &G::from_u8(__y_bytes[1])); record.bytes2_queries.bump_range_check(&G::from_u8(__y_bytes[2]), &G::from_u8(__y_bytes[3])); record.bytes2_queries.bump_range_check(&G::from_u8(__z_bytes[0]), &G::from_u8(__z_bytes[1])); record.bytes2_queries.bump_range_check(&G::from_u8(__z_bytes[2]), &G::from_u8(__z_bytes[3])); } __result }; - let __v_792: G = G::from_u64(1); - if (__v_791 != __v_792) { - return Err(ExecError::AssertEqMismatch { lhs: __v_791.as_canonical_u64(), rhs: __v_792.as_canonical_u64(), msg: None }); + let __v_838: G = G::from_u64(33); + let __v_839: G = { let __a_val = __v_815.as_canonical_u64(); let __b_val = __v_838.as_canonical_u64(); let __a_u32 = u32::try_from(__a_val).ok().ok_or(ExecError::U32OutOfRange(__a_val))?; let __b_u32 = u32::try_from(__b_val).ok().ok_or(ExecError::U32OutOfRange(__b_val))?; let __result = G::from_bool(__a_u32 < __b_u32); if !unconstrained { let __x_bytes = __a_u32.to_le_bytes(); let __z_bytes = __b_u32.to_le_bytes(); let __c_u32 = __b_u32.wrapping_sub(__a_u32).wrapping_sub(1); let __y_bytes = __c_u32.to_le_bytes(); record.bytes2_queries.bump_range_check(&G::from_u8(__x_bytes[0]), &G::from_u8(__x_bytes[1])); record.bytes2_queries.bump_range_check(&G::from_u8(__x_bytes[2]), &G::from_u8(__x_bytes[3])); record.bytes2_queries.bump_range_check(&G::from_u8(__y_bytes[0]), &G::from_u8(__y_bytes[1])); record.bytes2_queries.bump_range_check(&G::from_u8(__y_bytes[2]), &G::from_u8(__y_bytes[3])); record.bytes2_queries.bump_range_check(&G::from_u8(__z_bytes[0]), &G::from_u8(__z_bytes[1])); record.bytes2_queries.bump_range_check(&G::from_u8(__z_bytes[2]), &G::from_u8(__z_bytes[3])); } __result }; + let __v_840: G = G::from_u64(1); + if (__v_839 != __v_840) { + return Err(ExecError::AssertEqMismatch { lhs: __v_839.as_canonical_u64(), rhs: __v_840.as_canonical_u64(), msg: None }); } - let __r_arr: [G; OUT_142] = { let __args: [G; IN_142] = [__v_765, __v_766, __v_44, __v_735, __v_756, __v_62, __v_64, __v_57, __v_59, __v_60, __v_24, __v_26, __v_28, __v_359, __v_358, __v_34, __v_656, __v_677, __v_684, __v_155, __v_767, __v_757, __v_38, __v_46, __v_685]; let __cu = unconstrained; if let Some(result) = record.function_queries[142].get_mut(&__args[..]) { if !__cu && *result.multiplicity == G::ZERO { aiur_fn_142(__args, record, io_buffer, false)? } else { if !unconstrained { *result.multiplicity += G::ONE; } let __ret: [G; OUT_142] = unsafe { *(result.output.as_ptr() as *const [G; OUT_142]) }; __ret } } else { aiur_fn_142(__args, record, io_buffer, __cu)? } }; - let __v_793: G = __r_arr[0]; - break '__mc_1 [__v_793]; + let __r_arr: [G; OUT_142] = { let __args: [G; IN_142] = [__v_813, __v_814, __v_44, __v_783, __v_804, __v_62, __v_64, __v_57, __v_59, __v_60, __v_24, __v_26, __v_28, __v_407, __v_406, __v_34, __v_704, __v_725, __v_732, __v_155, __v_815, __v_805, __v_38, __v_46, __v_733]; let __cu = unconstrained; if let Some(result) = record.function_queries[142].get_mut(&__args[..]) { if !__cu && *result.multiplicity == G::ZERO { aiur_fn_142(__args, record, io_buffer, false)? } else { if !unconstrained { *result.multiplicity += G::ONE; } let __ret: [G; OUT_142] = unsafe { *(result.output.as_ptr() as *const [G; OUT_142]) }; __ret } } else { aiur_fn_142(__args, record, io_buffer, __cu)? } }; + let __v_841: G = __r_arr[0]; + break '__mc_1 [__v_841]; }, } }, @@ -19184,240 +19322,240 @@ fn aiur_fn_191( }, } }; - let __v_357: G = __mc_out___mc_1[0]; - let __v_358: G = (__v_18 + __v_19); - if (__v_65 != __v_358) { - return Err(ExecError::AssertEqMismatch { lhs: __v_65.as_canonical_u64(), rhs: __v_358.as_canonical_u64(), msg: None }); + let __v_405: G = __mc_out___mc_1[0]; + let __v_406: G = (__v_18 + __v_19); + if (__v_65 != __v_406) { + return Err(ExecError::AssertEqMismatch { lhs: __v_65.as_canonical_u64(), rhs: __v_406.as_canonical_u64(), msg: None }); } - let __v_359: G = G::from_u64(256); - let __v_360: G = (__v_359 * __v_124); - let __v_361: G = G::from_u64(65536); - let __v_362: G = (__v_361 * __v_125); - let __v_363: G = G::from_u64(16777216); - let __v_364: G = (__v_363 * __v_126); - let __v_365: G = (__v_362 + __v_364); - let __v_366: G = (__v_360 + __v_365); - let __v_367: G = (__v_123 + __v_366); - let __v_368: G = G::from_u64(256); - let __v_369: G = (__v_368 * __v_128); - let __v_370: G = G::from_u64(65536); - let __v_371: G = (__v_370 * __v_129); - let __v_372: G = G::from_u64(16777216); - let __v_373: G = (__v_372 * __v_130); - let __v_374: G = (__v_371 + __v_373); - let __v_375: G = (__v_369 + __v_374); - let __v_376: G = (__v_127 + __v_375); - let __v_377: G = G::from_u64(256); - let __v_378: G = (__v_377 * __v_132); - let __v_379: G = G::from_u64(65536); - let __v_380: G = (__v_379 * __v_133); - let __v_381: G = G::from_u64(16777216); - let __v_382: G = (__v_381 * __v_134); - let __v_383: G = (__v_380 + __v_382); - let __v_384: G = (__v_378 + __v_383); - let __v_385: G = (__v_131 + __v_384); - let __v_386: G = G::from_u64(256); - let __v_387: G = (__v_386 * __v_136); - let __v_388: G = G::from_u64(65536); - let __v_389: G = (__v_388 * __v_137); - let __v_390: G = G::from_u64(16777216); - let __v_391: G = (__v_390 * __v_138); - let __v_392: G = (__v_389 + __v_391); - let __v_393: G = (__v_387 + __v_392); - let __v_394: G = (__v_135 + __v_393); - let __v_395: G = G::from_u64(256); - let __v_396: G = (__v_395 * __v_140); - let __v_397: G = G::from_u64(65536); - let __v_398: G = (__v_397 * __v_141); - let __v_399: G = G::from_u64(16777216); - let __v_400: G = (__v_399 * __v_142); - let __v_401: G = (__v_398 + __v_400); - let __v_402: G = (__v_396 + __v_401); - let __v_403: G = (__v_139 + __v_402); - let __v_404: G = G::from_u64(256); - let __v_405: G = (__v_404 * __v_144); - let __v_406: G = G::from_u64(65536); - let __v_407: G = (__v_406 * __v_145); - let __v_408: G = G::from_u64(16777216); - let __v_409: G = (__v_408 * __v_146); - let __v_410: G = (__v_407 + __v_409); - let __v_411: G = (__v_405 + __v_410); - let __v_412: G = (__v_143 + __v_411); - let __v_413: G = G::from_u64(256); - let __v_414: G = (__v_413 * __v_148); - let __v_415: G = G::from_u64(65536); - let __v_416: G = (__v_415 * __v_149); - let __v_417: G = G::from_u64(16777216); - let __v_418: G = (__v_417 * __v_150); - let __v_419: G = (__v_416 + __v_418); - let __v_420: G = (__v_414 + __v_419); - let __v_421: G = (__v_147 + __v_420); - let __v_422: G = G::from_u64(256); - let __v_423: G = (__v_422 * __v_152); - let __v_424: G = G::from_u64(65536); - let __v_425: G = (__v_424 * __v_153); - let __v_426: G = G::from_u64(16777216); - let __v_427: G = (__v_426 * __v_154); - let __v_428: G = (__v_425 + __v_427); - let __v_429: G = (__v_423 + __v_428); - let __v_430: G = (__v_151 + __v_429); - if (__v_367 != __v_0) { - return Err(ExecError::AssertEqMismatch { lhs: __v_367.as_canonical_u64(), rhs: __v_0.as_canonical_u64(), msg: None }); + let __v_407: G = G::from_u64(256); + let __v_408: G = (__v_407 * __v_124); + let __v_409: G = G::from_u64(65536); + let __v_410: G = (__v_409 * __v_125); + let __v_411: G = G::from_u64(16777216); + let __v_412: G = (__v_411 * __v_126); + let __v_413: G = (__v_410 + __v_412); + let __v_414: G = (__v_408 + __v_413); + let __v_415: G = (__v_123 + __v_414); + let __v_416: G = G::from_u64(256); + let __v_417: G = (__v_416 * __v_128); + let __v_418: G = G::from_u64(65536); + let __v_419: G = (__v_418 * __v_129); + let __v_420: G = G::from_u64(16777216); + let __v_421: G = (__v_420 * __v_130); + let __v_422: G = (__v_419 + __v_421); + let __v_423: G = (__v_417 + __v_422); + let __v_424: G = (__v_127 + __v_423); + let __v_425: G = G::from_u64(256); + let __v_426: G = (__v_425 * __v_132); + let __v_427: G = G::from_u64(65536); + let __v_428: G = (__v_427 * __v_133); + let __v_429: G = G::from_u64(16777216); + let __v_430: G = (__v_429 * __v_134); + let __v_431: G = (__v_428 + __v_430); + let __v_432: G = (__v_426 + __v_431); + let __v_433: G = (__v_131 + __v_432); + let __v_434: G = G::from_u64(256); + let __v_435: G = (__v_434 * __v_136); + let __v_436: G = G::from_u64(65536); + let __v_437: G = (__v_436 * __v_137); + let __v_438: G = G::from_u64(16777216); + let __v_439: G = (__v_438 * __v_138); + let __v_440: G = (__v_437 + __v_439); + let __v_441: G = (__v_435 + __v_440); + let __v_442: G = (__v_135 + __v_441); + let __v_443: G = G::from_u64(256); + let __v_444: G = (__v_443 * __v_140); + let __v_445: G = G::from_u64(65536); + let __v_446: G = (__v_445 * __v_141); + let __v_447: G = G::from_u64(16777216); + let __v_448: G = (__v_447 * __v_142); + let __v_449: G = (__v_446 + __v_448); + let __v_450: G = (__v_444 + __v_449); + let __v_451: G = (__v_139 + __v_450); + let __v_452: G = G::from_u64(256); + let __v_453: G = (__v_452 * __v_144); + let __v_454: G = G::from_u64(65536); + let __v_455: G = (__v_454 * __v_145); + let __v_456: G = G::from_u64(16777216); + let __v_457: G = (__v_456 * __v_146); + let __v_458: G = (__v_455 + __v_457); + let __v_459: G = (__v_453 + __v_458); + let __v_460: G = (__v_143 + __v_459); + let __v_461: G = G::from_u64(256); + let __v_462: G = (__v_461 * __v_148); + let __v_463: G = G::from_u64(65536); + let __v_464: G = (__v_463 * __v_149); + let __v_465: G = G::from_u64(16777216); + let __v_466: G = (__v_465 * __v_150); + let __v_467: G = (__v_464 + __v_466); + let __v_468: G = (__v_462 + __v_467); + let __v_469: G = (__v_147 + __v_468); + let __v_470: G = G::from_u64(256); + let __v_471: G = (__v_470 * __v_152); + let __v_472: G = G::from_u64(65536); + let __v_473: G = (__v_472 * __v_153); + let __v_474: G = G::from_u64(16777216); + let __v_475: G = (__v_474 * __v_154); + let __v_476: G = (__v_473 + __v_475); + let __v_477: G = (__v_471 + __v_476); + let __v_478: G = (__v_151 + __v_477); + if (__v_415 != __v_0) { + return Err(ExecError::AssertEqMismatch { lhs: __v_415.as_canonical_u64(), rhs: __v_0.as_canonical_u64(), msg: None }); } - if (__v_376 != __v_1) { - return Err(ExecError::AssertEqMismatch { lhs: __v_376.as_canonical_u64(), rhs: __v_1.as_canonical_u64(), msg: None }); + if (__v_424 != __v_1) { + return Err(ExecError::AssertEqMismatch { lhs: __v_424.as_canonical_u64(), rhs: __v_1.as_canonical_u64(), msg: None }); } - if (__v_385 != __v_2) { - return Err(ExecError::AssertEqMismatch { lhs: __v_385.as_canonical_u64(), rhs: __v_2.as_canonical_u64(), msg: None }); + if (__v_433 != __v_2) { + return Err(ExecError::AssertEqMismatch { lhs: __v_433.as_canonical_u64(), rhs: __v_2.as_canonical_u64(), msg: None }); } - if (__v_394 != __v_3) { - return Err(ExecError::AssertEqMismatch { lhs: __v_394.as_canonical_u64(), rhs: __v_3.as_canonical_u64(), msg: None }); + if (__v_442 != __v_3) { + return Err(ExecError::AssertEqMismatch { lhs: __v_442.as_canonical_u64(), rhs: __v_3.as_canonical_u64(), msg: None }); } - if (__v_403 != __v_4) { - return Err(ExecError::AssertEqMismatch { lhs: __v_403.as_canonical_u64(), rhs: __v_4.as_canonical_u64(), msg: None }); + if (__v_451 != __v_4) { + return Err(ExecError::AssertEqMismatch { lhs: __v_451.as_canonical_u64(), rhs: __v_4.as_canonical_u64(), msg: None }); } - if (__v_412 != __v_5) { - return Err(ExecError::AssertEqMismatch { lhs: __v_412.as_canonical_u64(), rhs: __v_5.as_canonical_u64(), msg: None }); + if (__v_460 != __v_5) { + return Err(ExecError::AssertEqMismatch { lhs: __v_460.as_canonical_u64(), rhs: __v_5.as_canonical_u64(), msg: None }); } - if (__v_421 != __v_6) { - return Err(ExecError::AssertEqMismatch { lhs: __v_421.as_canonical_u64(), rhs: __v_6.as_canonical_u64(), msg: None }); + if (__v_469 != __v_6) { + return Err(ExecError::AssertEqMismatch { lhs: __v_469.as_canonical_u64(), rhs: __v_6.as_canonical_u64(), msg: None }); } - if (__v_430 != __v_7) { - return Err(ExecError::AssertEqMismatch { lhs: __v_430.as_canonical_u64(), rhs: __v_7.as_canonical_u64(), msg: None }); + if (__v_478 != __v_7) { + return Err(ExecError::AssertEqMismatch { lhs: __v_478.as_canonical_u64(), rhs: __v_7.as_canonical_u64(), msg: None }); } let __loaded: [G; 3] = { let __mq = record.memory_queries.get_mut(&3).ok_or(ExecError::InvalidMemorySize(3))?; let __ptr_u64 = __v_259.as_canonical_u64(); let __ptr_usize = usize::try_from(__ptr_u64).ok().ok_or(ExecError::PointerTooLarge(__ptr_u64))?; let (__args, __mult) = __mq.get_index_mut(__ptr_usize).ok_or(ExecError::UnboundPointer { ptr: __ptr_u64, size: 3 })?; if !unconstrained { *__mult += G::ONE; } let __arr: [G; 3] = __args[..3].try_into().unwrap(); __arr }; - let __v_431: G = __loaded[0]; - let __v_432: G = __loaded[1]; - let __v_433: G = __loaded[2]; - let __v_434: G = G::from_u64(1); - let __v_435: G = G::from_u64(1); - if (__v_431 != __v_434) { - return Err(ExecError::AssertEqMismatch { lhs: __v_431.as_canonical_u64(), rhs: __v_434.as_canonical_u64(), msg: None }); + let __v_479: G = __loaded[0]; + let __v_480: G = __loaded[1]; + let __v_481: G = __loaded[2]; + let __v_482: G = G::from_u64(1); + let __v_483: G = G::from_u64(1); + if (__v_479 != __v_482) { + return Err(ExecError::AssertEqMismatch { lhs: __v_479.as_canonical_u64(), rhs: __v_482.as_canonical_u64(), msg: None }); } - if (__v_432 != __v_435) { - return Err(ExecError::AssertEqMismatch { lhs: __v_432.as_canonical_u64(), rhs: __v_435.as_canonical_u64(), msg: None }); + if (__v_480 != __v_483) { + return Err(ExecError::AssertEqMismatch { lhs: __v_480.as_canonical_u64(), rhs: __v_483.as_canonical_u64(), msg: None }); } - if (__v_433 != __v_435) { - return Err(ExecError::AssertEqMismatch { lhs: __v_433.as_canonical_u64(), rhs: __v_435.as_canonical_u64(), msg: None }); + if (__v_481 != __v_483) { + return Err(ExecError::AssertEqMismatch { lhs: __v_481.as_canonical_u64(), rhs: __v_483.as_canonical_u64(), msg: None }); } - let __v_436: G = G::from_u64(256); - let __v_437: G = (__v_436 * __v_321); - let __v_438: G = G::from_u64(65536); - let __v_439: G = (__v_438 * __v_322); - let __v_440: G = G::from_u64(16777216); - let __v_441: G = (__v_440 * __v_323); - let __v_442: G = (__v_439 + __v_441); - let __v_443: G = (__v_437 + __v_442); - let __v_444: G = (__v_320 + __v_443); - let __v_445: G = G::from_u64(256); - let __v_446: G = (__v_445 * __v_325); - let __v_447: G = G::from_u64(65536); - let __v_448: G = (__v_447 * __v_326); - let __v_449: G = G::from_u64(16777216); - let __v_450: G = (__v_449 * __v_327); - let __v_451: G = (__v_448 + __v_450); - let __v_452: G = (__v_446 + __v_451); - let __v_453: G = (__v_324 + __v_452); - let __v_454: G = G::from_u64(256); - let __v_455: G = (__v_454 * __v_329); - let __v_456: G = G::from_u64(65536); - let __v_457: G = (__v_456 * __v_330); - let __v_458: G = G::from_u64(16777216); - let __v_459: G = (__v_458 * __v_331); - let __v_460: G = (__v_457 + __v_459); - let __v_461: G = (__v_455 + __v_460); - let __v_462: G = (__v_328 + __v_461); - let __v_463: G = G::from_u64(256); - let __v_464: G = (__v_463 * __v_333); - let __v_465: G = G::from_u64(65536); - let __v_466: G = (__v_465 * __v_334); - let __v_467: G = G::from_u64(16777216); - let __v_468: G = (__v_467 * __v_335); - let __v_469: G = (__v_466 + __v_468); - let __v_470: G = (__v_464 + __v_469); - let __v_471: G = (__v_332 + __v_470); - let __v_472: G = G::from_u64(256); - let __v_473: G = (__v_472 * __v_337); - let __v_474: G = G::from_u64(65536); - let __v_475: G = (__v_474 * __v_338); - let __v_476: G = G::from_u64(16777216); - let __v_477: G = (__v_476 * __v_339); - let __v_478: G = (__v_475 + __v_477); - let __v_479: G = (__v_473 + __v_478); - let __v_480: G = (__v_336 + __v_479); - let __v_481: G = G::from_u64(256); - let __v_482: G = (__v_481 * __v_341); - let __v_483: G = G::from_u64(65536); - let __v_484: G = (__v_483 * __v_342); - let __v_485: G = G::from_u64(16777216); - let __v_486: G = (__v_485 * __v_343); - let __v_487: G = (__v_484 + __v_486); - let __v_488: G = (__v_482 + __v_487); - let __v_489: G = (__v_340 + __v_488); - let __v_490: G = G::from_u64(256); - let __v_491: G = (__v_490 * __v_345); - let __v_492: G = G::from_u64(65536); - let __v_493: G = (__v_492 * __v_346); - let __v_494: G = G::from_u64(16777216); - let __v_495: G = (__v_494 * __v_347); - let __v_496: G = (__v_493 + __v_495); - let __v_497: G = (__v_491 + __v_496); - let __v_498: G = (__v_344 + __v_497); - let __v_499: G = G::from_u64(256); - let __v_500: G = (__v_499 * __v_349); - let __v_501: G = G::from_u64(65536); - let __v_502: G = (__v_501 * __v_350); - let __v_503: G = G::from_u64(16777216); - let __v_504: G = (__v_503 * __v_351); - let __v_505: G = (__v_502 + __v_504); - let __v_506: G = (__v_500 + __v_505); - let __v_507: G = (__v_348 + __v_506); - if (__v_444 != __v_8) { - return Err(ExecError::AssertEqMismatch { lhs: __v_444.as_canonical_u64(), rhs: __v_8.as_canonical_u64(), msg: None }); + let __v_484: G = G::from_u64(256); + let __v_485: G = (__v_484 * __v_369); + let __v_486: G = G::from_u64(65536); + let __v_487: G = (__v_486 * __v_370); + let __v_488: G = G::from_u64(16777216); + let __v_489: G = (__v_488 * __v_371); + let __v_490: G = (__v_487 + __v_489); + let __v_491: G = (__v_485 + __v_490); + let __v_492: G = (__v_368 + __v_491); + let __v_493: G = G::from_u64(256); + let __v_494: G = (__v_493 * __v_373); + let __v_495: G = G::from_u64(65536); + let __v_496: G = (__v_495 * __v_374); + let __v_497: G = G::from_u64(16777216); + let __v_498: G = (__v_497 * __v_375); + let __v_499: G = (__v_496 + __v_498); + let __v_500: G = (__v_494 + __v_499); + let __v_501: G = (__v_372 + __v_500); + let __v_502: G = G::from_u64(256); + let __v_503: G = (__v_502 * __v_377); + let __v_504: G = G::from_u64(65536); + let __v_505: G = (__v_504 * __v_378); + let __v_506: G = G::from_u64(16777216); + let __v_507: G = (__v_506 * __v_379); + let __v_508: G = (__v_505 + __v_507); + let __v_509: G = (__v_503 + __v_508); + let __v_510: G = (__v_376 + __v_509); + let __v_511: G = G::from_u64(256); + let __v_512: G = (__v_511 * __v_381); + let __v_513: G = G::from_u64(65536); + let __v_514: G = (__v_513 * __v_382); + let __v_515: G = G::from_u64(16777216); + let __v_516: G = (__v_515 * __v_383); + let __v_517: G = (__v_514 + __v_516); + let __v_518: G = (__v_512 + __v_517); + let __v_519: G = (__v_380 + __v_518); + let __v_520: G = G::from_u64(256); + let __v_521: G = (__v_520 * __v_385); + let __v_522: G = G::from_u64(65536); + let __v_523: G = (__v_522 * __v_386); + let __v_524: G = G::from_u64(16777216); + let __v_525: G = (__v_524 * __v_387); + let __v_526: G = (__v_523 + __v_525); + let __v_527: G = (__v_521 + __v_526); + let __v_528: G = (__v_384 + __v_527); + let __v_529: G = G::from_u64(256); + let __v_530: G = (__v_529 * __v_389); + let __v_531: G = G::from_u64(65536); + let __v_532: G = (__v_531 * __v_390); + let __v_533: G = G::from_u64(16777216); + let __v_534: G = (__v_533 * __v_391); + let __v_535: G = (__v_532 + __v_534); + let __v_536: G = (__v_530 + __v_535); + let __v_537: G = (__v_388 + __v_536); + let __v_538: G = G::from_u64(256); + let __v_539: G = (__v_538 * __v_393); + let __v_540: G = G::from_u64(65536); + let __v_541: G = (__v_540 * __v_394); + let __v_542: G = G::from_u64(16777216); + let __v_543: G = (__v_542 * __v_395); + let __v_544: G = (__v_541 + __v_543); + let __v_545: G = (__v_539 + __v_544); + let __v_546: G = (__v_392 + __v_545); + let __v_547: G = G::from_u64(256); + let __v_548: G = (__v_547 * __v_397); + let __v_549: G = G::from_u64(65536); + let __v_550: G = (__v_549 * __v_398); + let __v_551: G = G::from_u64(16777216); + let __v_552: G = (__v_551 * __v_399); + let __v_553: G = (__v_550 + __v_552); + let __v_554: G = (__v_548 + __v_553); + let __v_555: G = (__v_396 + __v_554); + if (__v_492 != __v_8) { + return Err(ExecError::AssertEqMismatch { lhs: __v_492.as_canonical_u64(), rhs: __v_8.as_canonical_u64(), msg: None }); } - if (__v_453 != __v_9) { - return Err(ExecError::AssertEqMismatch { lhs: __v_453.as_canonical_u64(), rhs: __v_9.as_canonical_u64(), msg: None }); + if (__v_501 != __v_9) { + return Err(ExecError::AssertEqMismatch { lhs: __v_501.as_canonical_u64(), rhs: __v_9.as_canonical_u64(), msg: None }); } - if (__v_462 != __v_10) { - return Err(ExecError::AssertEqMismatch { lhs: __v_462.as_canonical_u64(), rhs: __v_10.as_canonical_u64(), msg: None }); + if (__v_510 != __v_10) { + return Err(ExecError::AssertEqMismatch { lhs: __v_510.as_canonical_u64(), rhs: __v_10.as_canonical_u64(), msg: None }); } - if (__v_471 != __v_11) { - return Err(ExecError::AssertEqMismatch { lhs: __v_471.as_canonical_u64(), rhs: __v_11.as_canonical_u64(), msg: None }); + if (__v_519 != __v_11) { + return Err(ExecError::AssertEqMismatch { lhs: __v_519.as_canonical_u64(), rhs: __v_11.as_canonical_u64(), msg: None }); } - if (__v_480 != __v_12) { - return Err(ExecError::AssertEqMismatch { lhs: __v_480.as_canonical_u64(), rhs: __v_12.as_canonical_u64(), msg: None }); + if (__v_528 != __v_12) { + return Err(ExecError::AssertEqMismatch { lhs: __v_528.as_canonical_u64(), rhs: __v_12.as_canonical_u64(), msg: None }); } - if (__v_489 != __v_13) { - return Err(ExecError::AssertEqMismatch { lhs: __v_489.as_canonical_u64(), rhs: __v_13.as_canonical_u64(), msg: None }); + if (__v_537 != __v_13) { + return Err(ExecError::AssertEqMismatch { lhs: __v_537.as_canonical_u64(), rhs: __v_13.as_canonical_u64(), msg: None }); } - if (__v_498 != __v_14) { - return Err(ExecError::AssertEqMismatch { lhs: __v_498.as_canonical_u64(), rhs: __v_14.as_canonical_u64(), msg: None }); + if (__v_546 != __v_14) { + return Err(ExecError::AssertEqMismatch { lhs: __v_546.as_canonical_u64(), rhs: __v_14.as_canonical_u64(), msg: None }); } - if (__v_507 != __v_15) { - return Err(ExecError::AssertEqMismatch { lhs: __v_507.as_canonical_u64(), rhs: __v_15.as_canonical_u64(), msg: None }); + if (__v_555 != __v_15) { + return Err(ExecError::AssertEqMismatch { lhs: __v_555.as_canonical_u64(), rhs: __v_15.as_canonical_u64(), msg: None }); } - let __loaded: [G; 3] = { let __mq = record.memory_queries.get_mut(&3).ok_or(ExecError::InvalidMemorySize(3))?; let __ptr_u64 = __v_355.as_canonical_u64(); let __ptr_usize = usize::try_from(__ptr_u64).ok().ok_or(ExecError::PointerTooLarge(__ptr_u64))?; let (__args, __mult) = __mq.get_index_mut(__ptr_usize).ok_or(ExecError::UnboundPointer { ptr: __ptr_u64, size: 3 })?; if !unconstrained { *__mult += G::ONE; } let __arr: [G; 3] = __args[..3].try_into().unwrap(); __arr }; - let __v_508: G = __loaded[0]; - let __v_509: G = __loaded[1]; - let __v_510: G = __loaded[2]; - let __v_511: G = G::from_u64(1); - let __v_512: G = G::from_u64(1); - if (__v_508 != __v_511) { - return Err(ExecError::AssertEqMismatch { lhs: __v_508.as_canonical_u64(), rhs: __v_511.as_canonical_u64(), msg: None }); + let __loaded: [G; 3] = { let __mq = record.memory_queries.get_mut(&3).ok_or(ExecError::InvalidMemorySize(3))?; let __ptr_u64 = __v_403.as_canonical_u64(); let __ptr_usize = usize::try_from(__ptr_u64).ok().ok_or(ExecError::PointerTooLarge(__ptr_u64))?; let (__args, __mult) = __mq.get_index_mut(__ptr_usize).ok_or(ExecError::UnboundPointer { ptr: __ptr_u64, size: 3 })?; if !unconstrained { *__mult += G::ONE; } let __arr: [G; 3] = __args[..3].try_into().unwrap(); __arr }; + let __v_556: G = __loaded[0]; + let __v_557: G = __loaded[1]; + let __v_558: G = __loaded[2]; + let __v_559: G = G::from_u64(1); + let __v_560: G = G::from_u64(1); + if (__v_556 != __v_559) { + return Err(ExecError::AssertEqMismatch { lhs: __v_556.as_canonical_u64(), rhs: __v_559.as_canonical_u64(), msg: None }); } - if (__v_509 != __v_512) { - return Err(ExecError::AssertEqMismatch { lhs: __v_509.as_canonical_u64(), rhs: __v_512.as_canonical_u64(), msg: None }); + if (__v_557 != __v_560) { + return Err(ExecError::AssertEqMismatch { lhs: __v_557.as_canonical_u64(), rhs: __v_560.as_canonical_u64(), msg: None }); } - if (__v_510 != __v_512) { - return Err(ExecError::AssertEqMismatch { lhs: __v_510.as_canonical_u64(), rhs: __v_512.as_canonical_u64(), msg: None }); + if (__v_558 != __v_560) { + return Err(ExecError::AssertEqMismatch { lhs: __v_558.as_canonical_u64(), rhs: __v_560.as_canonical_u64(), msg: None }); } - let __v_513: G = G::from_u64(1); - if (__v_356 != __v_513) { - return Err(ExecError::AssertEqMismatch { lhs: __v_356.as_canonical_u64(), rhs: __v_513.as_canonical_u64(), msg: None }); + let __v_561: G = G::from_u64(1); + if (__v_404 != __v_561) { + return Err(ExecError::AssertEqMismatch { lhs: __v_404.as_canonical_u64(), rhs: __v_561.as_canonical_u64(), msg: None }); } - let __v_514: G = G::from_u64(1); - if (__v_357 != __v_514) { - return Err(ExecError::AssertEqMismatch { lhs: __v_357.as_canonical_u64(), rhs: __v_514.as_canonical_u64(), msg: None }); + let __v_562: G = G::from_u64(1); + if (__v_405 != __v_562) { + return Err(ExecError::AssertEqMismatch { lhs: __v_405.as_canonical_u64(), rhs: __v_562.as_canonical_u64(), msg: None }); } let __ret: [G; OUT_191] = []; if let Some(result) = record.function_queries[191].get_mut(&inp[..]) { debug_assert_eq!(result.output, &__ret[..]); if !unconstrained { *result.multiplicity += G::ONE; } } else { record.function_queries[191].insert(&inp[..], &__ret[..], G::from_bool(!unconstrained)); }; diff --git a/crates/kernel/src/def_eq.rs b/crates/kernel/src/def_eq.rs index bfbd0d1f4..534579174 100644 --- a/crates/kernel/src/def_eq.rs +++ b/crates/kernel/src/def_eq.rs @@ -81,8 +81,8 @@ impl TypeChecker<'_, M> { eprintln!( "[deq] {} {} ~ {}", self.fuel_used(), - &a.hash_key(), - &b.hash_key(), + a.hash_key(), + b.hash_key(), ); } if a.ptr_eq(b) { diff --git a/crates/kernel/src/inductive.rs b/crates/kernel/src/inductive.rs index 561c0fdca..4cad5c7bd 100644 --- a/crates/kernel/src/inductive.rs +++ b/crates/kernel/src/inductive.rs @@ -3969,13 +3969,7 @@ peers={} flat={} rec_ids={} failed_gi={failed_gi}", }; let univ_offset = match rec_ids.first() { Some(rid) => match self.try_get_const(rid)? { - Some(KConst::Recr { lvls, .. }) => { - if lvls > ind_lvls { - 1u64 - } else { - 0u64 - } - }, + Some(KConst::Recr { lvls, .. }) if lvls > ind_lvls => 1u64, _ => 0, }, None => 0, @@ -4160,8 +4154,7 @@ re-run with `IX_RECURSOR_DUMP={}` for the full breakdown.", generated_with_rules.len() ))); } - for (dst, src) in cached.iter_mut().zip(generated_with_rules.into_iter()) - { + for (dst, src) in cached.iter_mut().zip(generated_with_rules) { dst.rules = src.rules; } } diff --git a/crates/kernel/src/ingress.rs b/crates/kernel/src/ingress.rs index 262eb5165..8696081c4 100644 --- a/crates/kernel/src/ingress.rs +++ b/crates/kernel/src/ingress.rs @@ -3863,17 +3863,7 @@ fn drop_ixon_env(ixon_env: IxonEnv, quiet: bool) { // set. Dropping them inline alongside the bookkeeping below is // negligible compared to the DashMap dropdance. // `..` covers the env's private fields. - let IxonEnv { - consts, - named, - blobs, - names, - comms, - anon_hints: _, - main: _, - assumptions: _, - .. - } = ixon_env; + let IxonEnv { consts, named, blobs, names, comms, .. } = ixon_env; let consts_len = consts.len(); let named_len = named.len(); let names_len = names.len(); diff --git a/crates/kernel/src/perf.rs b/crates/kernel/src/perf.rs index 8f1bcf888..033a77615 100644 --- a/crates/kernel/src/perf.rs +++ b/crates/kernel/src/perf.rs @@ -291,7 +291,7 @@ impl PerfCounters { let peak = self.peak_rec_fuel_used.load(Ordering::Relaxed); let total = self.total_rec_fuel_used.load(Ordering::Relaxed); let n = self.constants_checked.load(Ordering::Relaxed); - let avg = if n > 0 { total / n } else { 0 }; + let avg = total.checked_div(n).unwrap_or(0); writeln!(out, "[ix-perf] rec_fuel:")?; writeln!( out, diff --git a/crates/kernel/src/tc.rs b/crates/kernel/src/tc.rs index 252798cc4..0451dc2d9 100644 --- a/crates/kernel/src/tc.rs +++ b/crates/kernel/src/tc.rs @@ -913,13 +913,12 @@ impl<'a, M: KernelMode> TypeChecker<'a, M> { // Sharding profiler: flush the just-finished constant's heartbeats and // delta-unfold edges. `delta_targets` is always drained (even when // `cur_const` is unset) so producers never leak into the next constant. - if self.env.profile_sink.is_some() { + if let Some(sink) = self.env.profile_sink.as_mut() { let producers = std::mem::take(&mut self.delta_targets); // Always drain the op counters (even when `cur_const` is unset) so they // never leak into the next constant, mirroring `delta_targets`. let ops = crate::profile::take_op_counts(); if let Some(addr) = self.cur_const.take() { - let sink = self.env.profile_sink.as_mut().unwrap(); sink.record(addr, used, producers, ops); } } diff --git a/crates/kernel/src/whnf.rs b/crates/kernel/src/whnf.rs index 288f61c42..e66c3fb90 100644 --- a/crates/kernel/src/whnf.rs +++ b/crates/kernel/src/whnf.rs @@ -342,7 +342,7 @@ impl TypeChecker<'_, M> { // Step journal (see `IX_STEP_TRACE` in def_eq.rs); placed after the // quick exit to mirror the Lean kernel's `[whnf+]` site. if *IX_STEP_TRACE { - eprintln!("[whnf+] {} {}", self.fuel_used(), &e.hash_key()); + eprintln!("[whnf+] {} {}", self.fuel_used(), e.hash_key()); } // Context-aware cache: closed exprs use ptr only; open exprs include @@ -1983,11 +1983,11 @@ impl TypeChecker<'_, M> { Err(_) => return Ok(None), }; if *IX_KSYNTH_LOG { - eprintln!("[ksynth-attempt] {}", &ctor_app.hash_key()); + eprintln!("[ksynth-attempt] {}", ctor_app.hash_key()); } if !self.is_def_eq(&major_ty_w, &ctor_ty)? { if *IX_KSYNTH_LOG { - eprintln!("[ksynth-reject] {}", &ctor_app.hash_key()); + eprintln!("[ksynth-reject] {}", ctor_app.hash_key()); } return Ok(None); } diff --git a/flake.lock b/flake.lock index a5b07edb9..a18b189f8 100644 --- a/flake.lock +++ b/flake.lock @@ -33,17 +33,17 @@ ] }, "locked": { - "lastModified": 1787415051, - "narHash": "sha256-14ziKcXwmJ/ZihFpp3Cg6FLVPM8kCUVzR6t0iyae1hE=", + "lastModified": 1787430037, + "narHash": "sha256-0dLeEO55z4nHvSv8xb9BMoCZTbIc9IqVuId7z8oa4kA=", "owner": "argumentcomputer", "repo": "Blake3.lean", - "rev": "1b0fbd2bd78b2b873e14264037af8c8b1536b9e9", + "rev": "e6e908bfd3af607ab44fb462fa2276a2c81addba", "type": "github" }, "original": { "owner": "argumentcomputer", "repo": "Blake3.lean", - "rev": "1b0fbd2bd78b2b873e14264037af8c8b1536b9e9", + "rev": "e6e908bfd3af607ab44fb462fa2276a2c81addba", "type": "github" } }, diff --git a/flake.nix b/flake.nix index ce74d895f..a12cebf4f 100644 --- a/flake.nix +++ b/flake.nix @@ -31,7 +31,7 @@ # Blake3 Rust bindings for Lean blake3-lean = { - url = "github:argumentcomputer/Blake3.lean/1b0fbd2bd78b2b873e14264037af8c8b1536b9e9"; + url = "github:argumentcomputer/Blake3.lean/e6e908bfd3af607ab44fb462fa2276a2c81addba"; # System packages, follows lean4-nix so we stay in sync inputs.lean4-nix.follows = "lean4-nix"; }; @@ -79,7 +79,7 @@ # Pins the Rust toolchain rustToolchain = fenix.packages.${system}.fromToolchainFile { file = ./rust-toolchain.toml; - sha256 = "sha256-sqSWJDUxc+zaz1nBWMAJKTAGBuGWP25GCftIOlCEAtA="; + sha256 = "sha256-P30Tm3O7vQAE725YtDCDHGjNrSsfZO4us11UwJGZSJo="; }; # Rust package diff --git a/lake-manifest.json b/lake-manifest.json index bb37bc7a4..780fb24d5 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -35,10 +35,10 @@ "type": "git", "subDir": null, "scope": "", - "rev": "1b0fbd2bd78b2b873e14264037af8c8b1536b9e9", + "rev": "e6e908bfd3af607ab44fb462fa2276a2c81addba", "name": "Blake3", "manifestFile": "lake-manifest.json", - "inputRev": "1b0fbd2bd78b2b873e14264037af8c8b1536b9e9", + "inputRev": "e6e908bfd3af607ab44fb462fa2276a2c81addba", "inherited": false, "configFile": "lakefile.lean"}, {"url": "https://github.com/argumentcomputer/LSpec", diff --git a/lakefile.lean b/lakefile.lean index e741fbab8..5be3b13ca 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -13,7 +13,7 @@ BLAKE3 backend to Lean's native evaluator, and that dynlib gates every `IxTcVerify` module, so this pin must stay at or after the revision that introduced the target. -/ require Blake3 from git - "https://github.com/argumentcomputer/Blake3.lean" @ "1b0fbd2bd78b2b873e14264037af8c8b1536b9e9" + "https://github.com/argumentcomputer/Blake3.lean" @ "e6e908bfd3af607ab44fb462fa2276a2c81addba" require Cli from git "https://github.com/leanprover/lean4-cli" @ "v4.33.0" diff --git a/rust-toolchain.toml b/rust-toolchain.toml index a5b578d83..23de05434 100644 --- a/rust-toolchain.toml +++ b/rust-toolchain.toml @@ -1,4 +1,4 @@ [toolchain] # The default profile includes rustc, rust-std, cargo, rust-docs, rustfmt and clippy. profile = "default" -channel = "1.92" +channel = "1.98" diff --git a/sp1/Cargo.lock b/sp1/Cargo.lock index 0a1a98ec6..66fb34e20 100644 --- a/sp1/Cargo.lock +++ b/sp1/Cargo.lock @@ -290,7 +290,7 @@ checksum = "2af50177e190e07a26ab74f8b1efbfe2ef87da2116221318cb1c2e82baf7de06" [[package]] name = "bignat" version = "0.1.0" -source = "git+https://github.com/argumentcomputer/lean-ffi.git?rev=2a9c91eba44ea791978a086a6a19b3a922edfee5#2a9c91eba44ea791978a086a6a19b3a922edfee5" +source = "git+https://github.com/argumentcomputer/lean-ffi.git?rev=93c7e52952ae94546be08313f4ff3922984c84d5#93c7e52952ae94546be08313f4ff3922984c84d5" dependencies = [ "num-bigint 0.4.6", ] diff --git a/sp1/guest/Cargo.lock b/sp1/guest/Cargo.lock index 7ea41e7e9..a21ce1a81 100644 --- a/sp1/guest/Cargo.lock +++ b/sp1/guest/Cargo.lock @@ -40,7 +40,7 @@ checksum = "9e1b586273c5702936fe7b7d6896644d8be71e6314cfe09d3167c95f712589e8" [[package]] name = "bignat" version = "0.1.0" -source = "git+https://github.com/argumentcomputer/lean-ffi.git?rev=2a9c91eba44ea791978a086a6a19b3a922edfee5#2a9c91eba44ea791978a086a6a19b3a922edfee5" +source = "git+https://github.com/argumentcomputer/lean-ffi.git?rev=93c7e52952ae94546be08313f4ff3922984c84d5#93c7e52952ae94546be08313f4ff3922984c84d5" dependencies = [ "num-bigint 0.4.6", ] diff --git a/zisk/Cargo.lock b/zisk/Cargo.lock index a685b02a3..f6a8b8728 100644 --- a/zisk/Cargo.lock +++ b/zisk/Cargo.lock @@ -786,7 +786,7 @@ checksum = "2af50177e190e07a26ab74f8b1efbfe2ef87da2116221318cb1c2e82baf7de06" [[package]] name = "bignat" version = "0.1.0" -source = "git+https://github.com/argumentcomputer/lean-ffi.git?rev=2a9c91eba44ea791978a086a6a19b3a922edfee5#2a9c91eba44ea791978a086a6a19b3a922edfee5" +source = "git+https://github.com/argumentcomputer/lean-ffi.git?rev=93c7e52952ae94546be08313f4ff3922984c84d5#93c7e52952ae94546be08313f4ff3922984c84d5" dependencies = [ "num-bigint", ] diff --git a/zisk/agg-guest/Cargo.lock b/zisk/agg-guest/Cargo.lock index b69c70429..55b8da879 100644 --- a/zisk/agg-guest/Cargo.lock +++ b/zisk/agg-guest/Cargo.lock @@ -212,7 +212,7 @@ checksum = "f2032f911046de80f0a198e0901378627c33f59ea0ac00e363d481118bd70a53" [[package]] name = "bignat" version = "0.1.0" -source = "git+https://github.com/argumentcomputer/lean-ffi.git?rev=2a9c91eba44ea791978a086a6a19b3a922edfee5#2a9c91eba44ea791978a086a6a19b3a922edfee5" +source = "git+https://github.com/argumentcomputer/lean-ffi.git?rev=93c7e52952ae94546be08313f4ff3922984c84d5#93c7e52952ae94546be08313f4ff3922984c84d5" dependencies = [ "num-bigint", ] diff --git a/zisk/guest/Cargo.lock b/zisk/guest/Cargo.lock index 528b4de77..fab480ef6 100644 --- a/zisk/guest/Cargo.lock +++ b/zisk/guest/Cargo.lock @@ -212,7 +212,7 @@ checksum = "f2032f911046de80f0a198e0901378627c33f59ea0ac00e363d481118bd70a53" [[package]] name = "bignat" version = "0.1.0" -source = "git+https://github.com/argumentcomputer/lean-ffi.git?rev=2a9c91eba44ea791978a086a6a19b3a922edfee5#2a9c91eba44ea791978a086a6a19b3a922edfee5" +source = "git+https://github.com/argumentcomputer/lean-ffi.git?rev=93c7e52952ae94546be08313f4ff3922984c84d5#93c7e52952ae94546be08313f4ff3922984c84d5" dependencies = [ "num-bigint", ]