From 26ed114a0ad5f7e78378d4c7812add590a0b258e Mon Sep 17 00:00:00 2001 From: i Date: Sat, 24 Oct 2026 15:33:53 -0400 Subject: [PATCH 1/9] Define checked IB Google search request URL for ICU acquisition --- src/IB/WebSearch.idric | 67 ++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 67 insertions(+) create mode 100644 src/IB/WebSearch.idric diff --git a/src/IB/WebSearch.idric b/src/IB/WebSearch.idric new file mode 100644 index 0000000..600830a --- /dev/null +++ b/src/IB/WebSearch.idric @@ -0,0 +1,67 @@ +module IB.WebSearch + +import Data.Text + +%default total + +-- This is a browser-owned *request address*, not a browser intent or an +-- acquired page. The consumer sends only this complete HTTPS URL to ICU; +-- ICU and the Arena owner retain their own acquisition/admission checks. +-- Spaces are form-encoded as '+', as with IFS=+ over search words. +private +hex_digit : Int → Char +hex_digit nibble = + if nibble < 10 + then chr (ord '0' + nibble) + else chr (ord 'A' + nibble - 10) + +private +encoded_byte : Int → Text +encoded_byte value = + pack ['%', hex_digit (value `div` 16), hex_digit (value `mod` 16)] + +private +utf8_octets : Int → List Int +utf8_octets scalar = + if scalar < 128 then [scalar] + else if scalar < 2048 then + [192 + scalar `div` 64, 128 + scalar `mod` 64] + else if scalar < 65536 then + [224 + scalar `div` 4096, + 128 + (scalar `div` 64) `mod` 64, + 128 + scalar `mod` 64] + else + [240 + scalar `div` 262144, + 128 + (scalar `div` 4096) `mod` 64, + 128 + (scalar `div` 64) `mod` 64, + 128 + scalar `mod` 64] + +private +unreserved_ascii : Int → Bool +unreserved_ascii value = + (value >= 65 && value <= 90) || + (value >= 97 && value <= 122) || + (value >= 48 && value <= 57) || + elem value [45, 46, 95, 126] + +private +encoded_character : Char → Text +encoded_character character = + let scalar = ord character in + if character == ' ' then "+" + else if unreserved_ascii scalar then pack [character] + else concat (map encoded_byte (utf8_octets scalar)) + +private +unsafe_control : Char → Bool +unsafe_control character = + let scalar = ord character in scalar < 32 || scalar == 127 + +public export +google_icu_url : Text → Maybe Text +google_icu_url supplied = + let terms = trim supplied in + if terms == "" || any unsafe_control (unpack terms) then Nothing + else let url = "https://google.com/search?q=" ++ + concat (map encoded_character (unpack terms)) + in if length (unpack url) > 2048 then Nothing else Just url From f9c696272da5f051b8ac91d20fa1e5f30c727624 Mon Sep 17 00:00:00 2001 From: i Date: Sat, 24 Oct 2026 15:34:10 -0400 Subject: [PATCH 2/9] =?UTF-8?q?Check=20Google/ICU=20URL=20encoding=20and?= =?UTF-8?q?=20refusal=20cases=20against=20Idri=C3=A7=20smoke?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/Smoke.idric | 14 ++++++++++++++ 1 file changed, 14 insertions(+) diff --git a/src/Smoke.idric b/src/Smoke.idric index 4e9610b..e1ad030 100644 --- a/src/Smoke.idric +++ b/src/Smoke.idric @@ -7,6 +7,7 @@ import IB.Inspect import IB.DisplayRepair import IB.ScientificMedia import IB.Prefetch +import IB.WebSearch import IB.LongViewTask import System @@ -168,6 +169,19 @@ main = do putStrLn ("temporary-needs-language-model=" ++ show (needs_language_model_image_name temporary_image_name)) putStrLn ("prefetch-bounded=" ++ show (length prefetch)) putStrLn ("prefetch-reading=" ++ show (reading_target_count prefetch)) + putStrLn ("google-query-spaces=" ++ show + (google_icu_url "piano voicings" == Just "https://google.com/search?q=piano+voicings")) + putStrLn ("google-query-unicode=" ++ show + (google_icu_url "Björk & C# chords" == + Just "https://google.com/search?q=Bj%C3%B6rk+%26+C%23+chords")) + putStrLn ("google-query-reserved=" ++ show + (google_icu_url "a+b/𝄞" == + Just "https://google.com/search?q=a%2Bb%2F%F0%9D%84%9E")) + putStrLn ("google-query-empty-refused=" ++ show (google_icu_url " " == Nothing)) + putStrLn ("google-query-control-refused=" ++ show + (google_icu_url "piano\nchords" == Nothing)) + putStrLn ("google-query-length-refused=" ++ show + (google_icu_url (pack (replicate 2100 'a')) == Nothing)) putStrLn long_view_report case long_view_evidence of Just evidence ⇒ if evidence_passes evidence then pure () else exitFailure From a283e7c94f3fa3d910ca0c4c99918950ed72f5b5 Mon Sep 17 00:00:00 2001 From: i Date: Sat, 24 Oct 2026 15:34:12 -0400 Subject: [PATCH 3/9] =?UTF-8?q?Check=20Google/ICU=20URL=20encoding=20and?= =?UTF-8?q?=20refusal=20cases=20against=20Idri=C3=A7=20smoke?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- bin/ci_browser_foundation.grease | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/bin/ci_browser_foundation.grease b/bin/ci_browser_foundation.grease index ea976ac..d5608bc 100755 --- a/bin/ci_browser_foundation.grease +++ b/bin/ci_browser_foundation.grease @@ -100,6 +100,12 @@ exercise_core() { grep -Fx 'temporary-needs-language-model=True' /tmp/ib-smoke.txt grep -Fx 'prefetch-bounded=2' /tmp/ib-smoke.txt grep -Fx 'prefetch-reading=1' /tmp/ib-smoke.txt + grep -Fx 'google-query-spaces=True' /tmp/ib-smoke.txt + grep -Fx 'google-query-unicode=True' /tmp/ib-smoke.txt + grep -Fx 'google-query-reserved=True' /tmp/ib-smoke.txt + grep -Fx 'google-query-empty-refused=True' /tmp/ib-smoke.txt + grep -Fx 'google-query-control-refused=True' /tmp/ib-smoke.txt + grep -Fx 'google-query-length-refused=True' /tmp/ib-smoke.txt "$idric_prefix/bin/idris2" OccurrenceSmoke.idric -o ib-occurrence-smoke \ 2>&1 | tee /tmp/idric-occurrence-compile.txt From 7a3e835d8a99b95daee2cc84cc003a0cb049f488 Mon Sep 17 00:00:00 2001 From: i Date: Sat, 24 Oct 2026 15:35:07 -0400 Subject: [PATCH 4/9] Document ChordReader to IB to ICU Google search contract and missing Android path --- docs/icu-google-search-route.md | 68 +++++++++++++++++++++++++++++++++ 1 file changed, 68 insertions(+) create mode 100644 docs/icu-google-search-route.md diff --git a/docs/icu-google-search-route.md b/docs/icu-google-search-route.md new file mode 100644 index 0000000..7357fa1 --- /dev/null +++ b/docs/icu-google-search-route.md @@ -0,0 +1,68 @@ +# External search through IB and ICU + +Requested on 2026-10-24 after the physical MIRO C67 ChordReader development +APK installed and launched. Selecting **Search web** currently leaves the +application through a generic Android browser intent; the user sees DDG. +That is not an IB search or an ICU acquisition. + +## Browser-owned route + +```text +ChordReader search input (unescaped UTF-8 terms) + → explicit Android ACTION_SEARCH directed to the installed IB package + (SearchManager query extra: "query"; never ACTION_VIEW or implicit browser) + → IB validates the incoming search and records the search occurrence + → IB.WebSearch.google_icu_url builds one request target + → existing IB Binder-shaped ICU capability + → ICU GET over HTTPS + → checked response metadata and exact source bytes in the canonical Arena + → IB reader's authorized extraction, history and view +``` + +`IB.WebSearch.google_icu_url` is the **pure typed request-address decision**. +It uses `https://google.com/search?q=` followed by UTF-8 +application/x-www-form-urlencoded query terms. Ordinary spaces are `+` +(the requested `IFS=+` joining convention). `+`, `&`, `#`, `/`, +apostrophes, percent signs and non-ASCII characters are percent-escaped as +UTF-8 bytes. Empty/all-whitespace input, control characters and URLs above +2,048 characters are refused. Raw user text never becomes shell syntax. + +The source application must pass the **original, unescaped** query once. +Only IB constructs the provider URL, so callers do not each implement +Google encoding or own the default provider. ChordReader may append its +user-visible `chords` search context before handoff, but IB owns the URL. + +## Status and acceptance boundaries + +- The typed URL constructor and refusal/encoding cases are now on this + proposed IB branch, exercised by `Smoke.idric` / the core CI lane. +- The current NativeReader branch `native/no-java-frontend` is a text reader; + its `org.isomorphisms.ib.prepaint` package receives plain-text shares, + **not** SEARCH, ICU responses, or rendered search results. This package is + a development identity, not a permanent production app identity. +- The real ICU→Shizuku→Arena work is in the existing IB #152/#153/#155 + stack, with source extraction at IB #154 and the checked NativeReader at + #147. It is **not** currently a working C67 search-results APK. +- A production handoff requires an exported SEARCH receiver with appropriate + query validation and a completed native/checked Idriç-to-ICU navigation + route. An Android Activity that merely displays the query is **not** + equivalent to completing search. Do not add Java or a WebView transport. +- No implicit `ACTION_VIEW`, DDG/Startpage, app-side Java URLConnection, or + hidden alternative browser is an acceptable fallback for this route. If IB + cannot accept the request, show an explicit unavailable state in ChordReader. +- Live Google may return consent, bot-check, HTML without explicit UTF-8 + charset, or other responses the existing Arena admission policy refuses. + Record the actual HTTP/metadata outcome. Do not weaken ICU/Arena checks + merely to claim a search succeeded. +- Installation of ChordReader on C67 and its launch are **user-reported PASS** + for the prior candidate. These do not qualify this not-yet-built integration. + +## Acceptance + +A qualified C67 build must show one unescaped source term request; the exact +Google URL with encoded spaces/Unicode and reserved characters; an +authenticated routing handoff to IB; ICU rather than a generic Android +browser making the HTTPS request; an admitted committed response or +accurately reported refusal; history/source identity; click/open navigation; +and complete physical-device tests. A fake URL builder or hosted mock does +not accept the phone path. From d01e6890505cb6d78139ad25bb5e368db42ab4f1 Mon Sep 17 00:00:00 2001 From: i Date: Sat, 24 Oct 2026 15:42:21 -0400 Subject: [PATCH 5/9] Refuse even leading and trailing controls before trimming Google queries --- src/IB/WebSearch.idric | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/IB/WebSearch.idric b/src/IB/WebSearch.idric index 600830a..c286bac 100644 --- a/src/IB/WebSearch.idric +++ b/src/IB/WebSearch.idric @@ -61,7 +61,7 @@ public export google_icu_url : Text → Maybe Text google_icu_url supplied = let terms = trim supplied in - if terms == "" || any unsafe_control (unpack terms) then Nothing + if any unsafe_control (unpack supplied) || terms == "" then Nothing else let url = "https://google.com/search?q=" ++ concat (map encoded_character (unpack terms)) in if length (unpack url) > 2048 then Nothing else Just url From abc59a038e352cd6c1d6483462eff0fb5f33ffe1 Mon Sep 17 00:00:00 2001 From: i Date: Sat, 24 Oct 2026 15:42:24 -0400 Subject: [PATCH 6/9] Add trailing-control adversarial search fixture --- src/Smoke.idric | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/Smoke.idric b/src/Smoke.idric index e1ad030..ced9f5b 100644 --- a/src/Smoke.idric +++ b/src/Smoke.idric @@ -180,6 +180,8 @@ main = do putStrLn ("google-query-empty-refused=" ++ show (google_icu_url " " == Nothing)) putStrLn ("google-query-control-refused=" ++ show (google_icu_url "piano\nchords" == Nothing)) + putStrLn ("google-query-trailing-control-refused=" ++ show + (google_icu_url "piano\n" == Nothing)) putStrLn ("google-query-length-refused=" ++ show (google_icu_url (pack (replicate 2100 'a')) == Nothing)) putStrLn long_view_report From 8e1cb46362887791dd616f0127baf9c620666ae5 Mon Sep 17 00:00:00 2001 From: i Date: Sat, 24 Oct 2026 15:42:26 -0400 Subject: [PATCH 7/9] Enforce missing/unsafe web search query refusal in CI --- bin/ci_browser_foundation.grease | 1 + 1 file changed, 1 insertion(+) diff --git a/bin/ci_browser_foundation.grease b/bin/ci_browser_foundation.grease index d5608bc..db9c739 100755 --- a/bin/ci_browser_foundation.grease +++ b/bin/ci_browser_foundation.grease @@ -105,6 +105,7 @@ exercise_core() { grep -Fx 'google-query-reserved=True' /tmp/ib-smoke.txt grep -Fx 'google-query-empty-refused=True' /tmp/ib-smoke.txt grep -Fx 'google-query-control-refused=True' /tmp/ib-smoke.txt + grep -Fx 'google-query-trailing-control-refused=True' /tmp/ib-smoke.txt grep -Fx 'google-query-length-refused=True' /tmp/ib-smoke.txt "$idric_prefix/bin/idris2" OccurrenceSmoke.idric -o ib-occurrence-smoke \ From d143cfd4262195f397848075b491894213686e31 Mon Sep 17 00:00:00 2001 From: i Date: Sat, 24 Oct 2026 19:31:56 -0400 Subject: [PATCH 8/9] =?UTF-8?q?Fix=20Idri=C3=A7=20search-smoke=20long=20fi?= =?UTF-8?q?xture=20without=20undefined=20replicate?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/Smoke.idric | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/src/Smoke.idric b/src/Smoke.idric index ced9f5b..1290ead 100644 --- a/src/Smoke.idric +++ b/src/Smoke.idric @@ -138,6 +138,11 @@ long_view_report = "sensitive-url-refused=" ++ show evidence.sensitive_url_refused ++ "\n" ++ "long-view-record-contract=" ++ show evidence.record_contract_matches +-- Construct the long fixture without relying on an unavailable replicate name. +repeat_search_a : Number → List Char +repeat_search_a Z = [] +repeat_search_a (S remaining) = 'a' :: repeat_search_a remaining + main : IO () main = do let raw = ingest_raw_lines ["# ignored", " https://example.test/a ", "https://example.test/a", "https://other.test/b"] @@ -183,7 +188,7 @@ main = do putStrLn ("google-query-trailing-control-refused=" ++ show (google_icu_url "piano\n" == Nothing)) putStrLn ("google-query-length-refused=" ++ show - (google_icu_url (pack (replicate 2100 'a')) == Nothing)) + (google_icu_url (pack (repeat_search_a 2100)) == Nothing)) putStrLn long_view_report case long_view_evidence of Just evidence ⇒ if evidence_passes evidence then pure () else exitFailure From dcbd86c0f7a69c4e0b381c0ab53f7c41f9966900 Mon Sep 17 00:00:00 2001 From: i Date: Sun, 25 Oct 2026 00:21:46 -0400 Subject: [PATCH 9/9] Retain real Google ICU response and reproduce checked receiver blocker --- .../chordsearch/SearchIntentRequest.idric | 28 +++++++ examples/autogenerated/chordsearch/attempt.md | 41 ++++++++++ .../chordsearch/capture-google.grease | 76 +++++++++++++++++++ .../chordsearch/observations/.gitattributes | 1 + .../observations/google-http11.html | 18 +++++ .../observations/google-http11.tsv | 10 +++ .../chordsearch/observations/receipt.tsv | 36 +++++++++ .../chordsearch/verify-receiver.grease | 47 ++++++++++++ 8 files changed, 257 insertions(+) create mode 100644 examples/autogenerated/chordsearch/SearchIntentRequest.idric create mode 100644 examples/autogenerated/chordsearch/attempt.md create mode 100644 examples/autogenerated/chordsearch/capture-google.grease create mode 100644 examples/autogenerated/chordsearch/observations/.gitattributes create mode 100644 examples/autogenerated/chordsearch/observations/google-http11.html create mode 100644 examples/autogenerated/chordsearch/observations/google-http11.tsv create mode 100644 examples/autogenerated/chordsearch/observations/receipt.tsv create mode 100644 examples/autogenerated/chordsearch/verify-receiver.grease diff --git a/examples/autogenerated/chordsearch/SearchIntentRequest.idric b/examples/autogenerated/chordsearch/SearchIntentRequest.idric new file mode 100644 index 0000000..fa1a461 --- /dev/null +++ b/examples/autogenerated/chordsearch/SearchIntentRequest.idric @@ -0,0 +1,28 @@ +module SearchIntentRequest + +import Data.Text +import IB.WebSearch + +data IntentReference : Type where [external] + +%foreign "dex:virtual:Landroid/content/Intent;:getStringExtra:(Ljava/lang/String;)Ljava/lang/String;" +original_query_from_intent : IntentReference → Text → PrimIO Text + +%foreign "dex:static:Landroid/text/TextUtils;:isEmpty:(Ljava/lang/CharSequence;)Z" +query_is_empty : Text → PrimIO Int32 + +-- This is only the checked receiver-to-acquisition request boundary. An empty +-- result refuses navigation. Acquisition and history are not implemented here. +%export "dex:search_request_from_intent" +search_request_from_intent : IntentReference → IO Text +search_request_from_intent intent = do + supplied ← primIO (original_query_from_intent intent "query") + empty ← primIO (query_is_empty supplied) + if empty ≟ 0 + then case google_icu_url supplied of + Just address ⇒ pure address + Nothing ⇒ pure "" + else pure "" + +main : IO () +main = pure () diff --git a/examples/autogenerated/chordsearch/attempt.md b/examples/autogenerated/chordsearch/attempt.md new file mode 100644 index 0000000..022497f --- /dev/null +++ b/examples/autogenerated/chordsearch/attempt.md @@ -0,0 +1,41 @@ +# Complete ChordReader search through IB and ICU + +The current user has authorized this one-off without Flexible Pipes. Existing +independent ai-ci and source/admission checks remain required. + +Types and ownership: original UTF-8 query text enters the Android adapter; +IB.WebSearch validates and constructs the provider request. Browser-owned +navigation identity and history precede acquisition. ICU owns HTTPS and observed +metadata; canonical appendfat Arena owns immutable admitted source. Existing +Idriç recovery and extraction feed native reader views. None of these stages +may silently stand in for another. + +Initial independently executable action: build the unchanged ICU command with +the maintained Idriç frontend and its unchanged native transport with ICK, then +request the exact Google address using private response capture. The requested +URL and observed stdout, stderr, process exit, body and metadata are separate +evidence. This host command does not prove Shizuku, Android Binder or C67. + +Required platform work includes checked onNewIntent(Intent) delivery, app-owned +private Binder capability lifecycle, source-generation-bound worker delivery, +native selectable results and durable recovery. Installed package/certificate +identity remains a required observation before manifest or signer changes. + +Actual results are retained in observations/receipt.tsv and the exact Google +HTML/metadata files. HTTP/1.0 received 426; ICU's existing HTTP/1.1 mode received +200 and 93,166 bytes. The current native private ingress repair validates ICU's +ten-field metadata, retains the exact body in canonical Arena, and leaves it +reader-ineligible for its observed ISO-8859-1 charset and incomplete redirect +provenance. The independent ai-ci source oracle accepts the prior admitted +source and refuses the actual Google receipt at its UTF-8 charset check. + +SearchIntentRequest.idric uses the existing unchanged google_icu_url operation +on the raw Intent query. It actually typechecks, then direct DEX exits 1 with +`No checked helper body for DEX call Prelude.Types.fastUnpack`; no DEX exists. +The compiler's separately managed command mode is not a framework Activity +bridge and is not relabeled as one. verify-receiver.grease preserves the real +compiler result rather than treating an expected failure as application PASS. + +No application manifest, signer, version or ChordReader data was changed. No +replacement APK is offered before the receiver, acquisition and admitted-view +boundaries work together. C67 and A1 physical execution remain unverified. diff --git a/examples/autogenerated/chordsearch/capture-google.grease b/examples/autogenerated/chordsearch/capture-google.grease new file mode 100644 index 0000000..f88b215 --- /dev/null +++ b/examples/autogenerated/chordsearch/capture-google.grease @@ -0,0 +1,76 @@ +#!/usr/bin/env grease +# Execute the existing ICU command and transport; never another HTTP client. +if (len(ARGV) !== 8 and len(ARGV) !== 9) { + echo 'usage: grease capture-google.grease ICU NET FRONTEND ICK ICK_TOOLS HOST_SUPPORT NEW_OUTPUT URL [--http1.0|--http1.1]' >&2 + exit 2 +} +var icu = ARGV[0] +var network = ARGV[1] +var frontend = ARGV[2] +var compiler = ARGV[3] +var compiler_tools = ARGV[4] +var host_support = ARGV[5] +var output = ARGV[6] +var url = ARGV[7] +var version = '--http1.0' +if (len(ARGV) === 9) { setvar version = ARGV[8] } +if (version !== '--http1.0' and version !== '--http1.1') { echo 'FAIL HTTP version' >&2; exit 2 } +for path in "$icu" "$network" "$frontend" "$compiler" "$compiler_tools" "$host_support" "$output" { + if (path[0] !== '/') { echo 'FAIL absolute path required' >&2; exit 2 } +} +if test -e "$output" { echo 'FAIL output already exists' >&2; exit 2 } +mkdir -m 700 -p "$output/capture" "$output/source" +git -C "$icu" diff --quiet HEAD -- native/transport.c src +git -C "$network" diff --quiet HEAD -- Network +git -C "$icu" rev-parse HEAD > "$output/icu-ref.txt" +git -C "$network" rev-parse HEAD > "$output/network-ref.txt" +git -C "$frontend" rev-parse HEAD > "$output/frontend-ref.txt" +printf '%s\n' "$url" > "$output/requested-url.txt" +printf '%s\n' "$version" > "$output/http-version.txt" +sha256sum "$icu/native/transport.c" "$compiler" "$compiler_tools/cc1" > "$output/native-inputs.sha256" +printf 'stage\ticu-native-transport\ntoolchain\tick\nhost\tLinux-x86_64\n' > "$output/native-build.tsv" +sha256sum "$host_support/include/stddef.h" "$host_support/crtbeginS.o" "$host_support/crtendS.o" >> "$output/native-inputs.sha256" +"$compiler" -B "$compiler_tools/" -B "$host_support/" -isystem "$host_support/include" \ + -fno-link-libatomic -O2 -std=c11 -Wall -Wextra \ + -fPIC -shared "$icu/native/transport.c" -o "$output/libicu_transport.so" -lssl -lcrypto \ + > "$output/native-build.txt" 2>&1 +cp -a "$network/Network" "$output/source/Network" +cp -a "$icu/src/." "$output/source/" +var prefix = "$frontend/_/bootstrap-build" +var scheme = "$frontend/_/.tools/bin/scheme" +env IDRIS2_PREFIX="$prefix" IDRIS2_PACKAGE_PATH="$prefix/idris2-0.8.0" \ + CHEZ="$scheme" IDRIS2_CG=chez IDRIS2_DATA="$frontend/_/support" \ + IDRIS2_LIBS="$frontend/_/build/exec/idris2_app" \ + "$frontend/_/build/exec/idris2" --source-dir "$output/source" \ + --build-dir "$output/build" --output-dir "$output" "$output/source/Main.idric" -o icu \ + > "$output/idric-build.txt" 2>&1 +if rg -n '^[[:space:]]*(Error:|INTERNAL ERROR)' "$output/idric-build.txt" { + echo 'FAIL ICU source compiler diagnostic' >&2; exit 1 +} +test -x "$output/icu" +cp "$frontend/_/build/exec/idris2_app/libidris2_support.so" "$output/icu_app/" +sha256sum "$output/icu" "$output/icu_app/icu.so" "$output/libicu_transport.so" > "$output/command.sha256" +cd "$output" +try { + env LD_LIBRARY_PATH="$output" ICU_CAPTURE_BODY_PATH="$output/capture/body" \ + ICU_CAPTURE_METADATA_PATH="$output/capture/metadata" \ + timeout 60 "$output/icu" "$version" get "$url" > "$output/stdout.bin" 2> "$output/stderr.txt" +} +var status = _error.code +printf '%s\n' "$status" > "$output/process.exit" +cat "$output/stderr.txt" +if test -f "$output/capture/metadata" { + cat "$output/capture/metadata" + sha256sum "$output/capture/metadata" > "$output/capture.sha256" +} +if test -f "$output/capture/body" { sha256sum "$output/capture/body" >> "$output/capture.sha256" } +if (status !== 0) { + printf 'ICU_command\tFAIL\nprocess_exit\t%s\nArena_admission\tNOT_RUN\nphysical_C67\tNOT_RUN\n' "$status" > "$output/result.tsv" + printf '\033[31mFAIL\033[0m actual ICU Google request; exit %s\n' "$status" >&2 + exit 1 +} +test -s "$output/capture/metadata" +cat "$output/capture/metadata" +sha256sum "$output/capture/body" "$output/capture/metadata" > "$output/capture.sha256" +printf 'ICU_command\tPASS\nArena_admission\tNOT_RUN\nresults_view\tNOT_RUN\nphysical_C67\tNOT_RUN\n' > "$output/result.tsv" +printf '\033[32mPASS\033[0m actual ICU transport completed; admission and results remain separate\n' diff --git a/examples/autogenerated/chordsearch/observations/.gitattributes b/examples/autogenerated/chordsearch/observations/.gitattributes new file mode 100644 index 0000000..780735a --- /dev/null +++ b/examples/autogenerated/chordsearch/observations/.gitattributes @@ -0,0 +1 @@ +*.html linguist-generated=true linguist-vendored=true diff --git a/examples/autogenerated/chordsearch/observations/google-http11.html b/examples/autogenerated/chordsearch/observations/google-http11.html new file mode 100644 index 0000000..94247d1 --- /dev/null +++ b/examples/autogenerated/chordsearch/observations/google-http11.html @@ -0,0 +1,18 @@ +Google Search \ No newline at end of file diff --git a/examples/autogenerated/chordsearch/observations/google-http11.tsv b/examples/autogenerated/chordsearch/observations/google-http11.tsv new file mode 100644 index 0000000..12f8c3e --- /dev/null +++ b/examples/autogenerated/chordsearch/observations/google-http11.tsv @@ -0,0 +1,10 @@ +http_status 200 +content_type text/html; charset=ISO-8859-1 +content_encoding identity +content_range absent +declared_length -1 +received_length 93166 +transfer_decoding chunked +utf8 valid +resolved_url https://www.google.com/search?q=Bj%C3%B6rk+%26+C%23+chords +redirect_count 1 diff --git a/examples/autogenerated/chordsearch/observations/receipt.tsv b/examples/autogenerated/chordsearch/observations/receipt.tsv new file mode 100644 index 0000000..1b464fa --- /dev/null +++ b/examples/autogenerated/chordsearch/observations/receipt.tsv @@ -0,0 +1,36 @@ +field value +scope HOST_ICU_CAPTURE_AND_CANONICAL_ARENA_REPLAY +query Björk & C# chords +requested_url https://google.com/search?q=Bj%C3%B6rk+%26+C%23+chords +resolved_url https://www.google.com/search?q=Bj%C3%B6rk+%26+C%23+chords +icu_source b1c19dc281e5e7d3d326c9275093fb379bafd4bd +network_source b21801b72acb8ab835c297bbe298af8599550134 +frontend_source 740bbf2b1d9e811fd00c719c3473eede17ceea3b +http_1_0_status 426 +http_1_0_body Upgrade Required +http_1_0_process_exit 10 +http_1_1_status 200 +http_1_1_process_exit 0 +declared_charset ISO-8859-1 +body_bytes 93166 +body_sha256 f71e991ab87271e77255fe2d2454cb4cb401fe47cdf953ea550c6e0fcd8afeb4 +metadata_sha256 5ec84abb836e460f2ac4ec3c99acb13fbbdbb12a47dbd4a47b16bb2f56977666 +transfer_decoding chunked +redirect_count 1 +observed_metadata_fields 10 +canonical_source 05a0cb7246c5a9f46abfbe92925812e7b607f454 +canonical_object_sha256 da6f5ac730526505dc838937d7c057858d76b0e8243c256e0195a79bb7611c0f +canonical_tool_sha256 a573f5093f512630159b54af0ea029a8dbf7c9baccfac81ac4ca6c0b2a9f71f4 +canonical_source_retention PASS_EXACT_BODY_REOPENED +reader_admission NO +independent_ai_ci_original_admitted_source PASS +independent_ai_ci_live_google REFUSED_charset_not_observed_UTF-8 +search_receiver_typecheck PASS +search_receiver_dex BLOCKED_No_checked_helper_body_for_DEX_call_Prelude.Types.fastUnpack +search_results_usability NOT_RUN +app_owned_Binder_lifecycle INCOMPLETE +installed_C67_package_and_certificate UNKNOWN +emulator NOT_RUN +physical_C67 NOT_RUN +physical_A1 NOT_VERIFIED +overall_search INCOMPLETE diff --git a/examples/autogenerated/chordsearch/verify-receiver.grease b/examples/autogenerated/chordsearch/verify-receiver.grease new file mode 100644 index 0000000..6f7cd72 --- /dev/null +++ b/examples/autogenerated/chordsearch/verify-receiver.grease @@ -0,0 +1,47 @@ +#!/usr/bin/env grease +if (len(ARGV) !== 4) { + echo 'usage: grease verify-receiver.grease IB BACKEND FRONTEND NEW_EVIDENCE' >&2 + exit 2 +} +var repository = ARGV[0] +var backend = ARGV[1] +var frontend = ARGV[2] +var evidence = ARGV[3] +for path in "$repository" "$backend" "$frontend" "$evidence" { + if (path[0] !== '/') { echo 'FAIL absolute path required' >&2; exit 2 } +} +if test -e "$evidence" { echo 'FAIL evidence already exists' >&2; exit 2 } +mkdir -p "$evidence/source/IB" +cp "$repository/src/IB/WebSearch.idric" "$evidence/source/IB/" +cp "$repository/examples/autogenerated/chordsearch/SearchIntentRequest.idric" "$evidence/source/" +var prefix = "$frontend/_/bootstrap-build" +setglobal ENV.IDRIS2_PREFIX = prefix +setglobal ENV.IDRIS2_PACKAGE_PATH = "$prefix/idris2-0.8.0" +setglobal ENV.IDRIS2_DATA = "$frontend/_/support" +setglobal ENV.IDRIS2_LIBS = "$frontend/_/build/exec/idris2_app" +setglobal ENV.CHEZ = "$frontend/_/.tools/bin/scheme" +setglobal ENV.IDRIS2_CG = 'chez' +var driver = "$backend/dex/idric/build/exec/idric-dex" +sha256sum "$driver" "${driver}_app/idric-dex.so" "$evidence/source/SearchIntentRequest.idric" \ + "$evidence/source/IB/WebSearch.idric" > "$evidence/input.sha256" +"$driver" --source-dir "$evidence/source" --build-dir "$evidence/check" \ + --check "$evidence/source/SearchIntentRequest.idric" > "$evidence/typecheck.txt" 2>&1 +if rg -n '^[[:space:]]*(Error:|INTERNAL ERROR)' "$evidence/typecheck.txt" { + echo 'FAIL receiver source typecheck' >&2; exit 1 +} +try { + "$driver" --cg dex --source-dir "$evidence/source" --build-dir "$evidence/build" \ + --output-dir "$evidence" "$evidence/source/SearchIntentRequest.idric" -o receiver \ + > "$evidence/compiler.txt" 2>&1 +} +var status = _error.code +printf '%s\n' "$status" > "$evidence/compiler.exit" +cat "$evidence/compiler.txt" +if (status !== 0) { + test ! -e "$evidence/receiver.dex" + printf 'source_typecheck\tPASS\nsource_to_dex\tBLOCKED\ncompiler_exit\t%s\nART\tNOT_RUN\nphysical_C67\tNOT_RUN\n' "$status" > "$evidence/result.tsv" + exit 1 +} +test -s "$evidence/receiver.dex" +sha256sum "$evidence/receiver.dex" > "$evidence/output.sha256" +printf 'source_typecheck\tPASS\nsource_to_dex\tPASS\nART\tNOT_RUN\nphysical_C67\tNOT_RUN\n' > "$evidence/result.tsv"