Define checked Google search URLs for IB → ICU acquisition

bin/ci_browser_foundation.grease

@@ -100,6 +100,13 @@ 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-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 \
     2>&1 | tee /tmp/idric-occurrence-compile.txt

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.

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 ()

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.

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'

examples/autogenerated/chordsearch/observations/.gitattributes

@@ -0,0 +1 @@
+*.html linguist-generated=true linguist-vendored=true

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

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

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"

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 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