"""Single-file version.  Known-plaintext key recovery for class-XGAK ('letters in a class share one shuffle') via SAT.

Cipher (read-then-shuffle form, equivalent to xgak_sim's shuffle-then-read with k_a = r_c(o_a)):
    CT_t = D_{t-1}[k_{a_t}];   D_t = D_{t-1} o s_{c(a_t)}    (D_t[p] = D_{t-1}[s_c[p]])
    letters have distinct read positions k_a (unique decryption); no doubles <=> s_c^-1(k_a) not in K.
Key observation: whether CT_t == CT_{t+d} depends only on the plaintext between t and t+d.
P(t,d) := position in D_{t-1} of the card read at step t+d.  P(t,0) = k_{a_t},
P(t,d) = s_{c_t}[P(t+1,d-1)],  and CT_t == CT_{t+d}  <=>  P(t,d) == k_{a_t}.
Positions can be relabelled freely (conjugation), so WLOG k_a = a (letter index).
All messages start from the same D0, so P(1,d) values of different messages are equal iff their
CT symbols are equal (cross-message anchoring).
Encoding: s_c[p] binary (B bits) channelled to one-hot (permutation); P(t,d) binary via a MUX.
The class of each letter can be given, or left to the solver (K=2).
Run `python xgak_sat.py -h` for usage (subcommands: synth = experiments on fake messages, eyes = test a crib)."""
import sys, os, random, time, itertools, threading
from pysat.solvers import Solver
from pysat.card import CardEnc, EncType

HERE = os.path.dirname(os.path.abspath(__file__))

# ---- embedded data (single-file version) -------------------------------------------------------
# The nine eye messages, trigram values 0..82, orthodox reading order (community transcription,
# verified against the game executable). Same as data/eyes_ascii32.txt with value = ord(c) - 32.
NAMES = ['E1', 'W1', 'E2', 'W2', 'E3', 'W3', 'E4', 'W4', 'E5']
MSGS = [
    [50, 66, 5, 48, 62, 13, 75, 29, 24, 61, 42, 70, 66, 62, 32, 14, 81, 8, 15, 78, 2, 29, 13, 49, 1, 80, 82, 40, 63, 81, 21, 19, 0, 40, 51, 65, 26, 14, 21, 70, 47, 44, 48, 42, 19, 48, 13, 47, 19, 49, 72, 31, 5, 24, 3, 43, 59, 67, 33, 49, 41, 60, 21, 26, 30, 5, 25, 20, 71, 11, 74, 56, 4, 74, 19, 71, 4, 51, 41, 43, 80, 72, 54, 63, 79, 81, 15, 16, 44, 31, 30, 12, 33, 57, 28, 13, 64, 43, 48],
    [80, 66, 5, 48, 62, 13, 75, 29, 24, 61, 42, 70, 66, 62, 32, 14, 81, 8, 15, 78, 2, 29, 13, 49, 1, 29, 11, 30, 52, 81, 21, 19, 0, 25, 26, 54, 20, 14, 21, 70, 47, 44, 48, 42, 19, 48, 13, 47, 19, 49, 44, 26, 59, 77, 64, 43, 79, 28, 72, 64, 1, 30, 73, 23, 67, 6, 33, 25, 64, 81, 68, 46, 17, 36, 13, 17, 21, 68, 13, 9, 46, 67, 57, 34, 62, 82, 15, 10, 73, 62, 2, 11, 65, 72, 37, 44, 10, 43, 68, 62, 9, 34, 18],
    [36, 66, 5, 48, 62, 13, 75, 29, 24, 61, 42, 70, 66, 62, 32, 14, 81, 8, 15, 78, 2, 29, 13, 49, 1, 69, 76, 52, 9, 48, 66, 80, 22, 64, 57, 40, 49, 78, 3, 16, 56, 19, 47, 40, 80, 6, 13, 64, 29, 49, 64, 63, 6, 49, 31, 13, 16, 10, 45, 24, 26, 77, 10, 60, 81, 61, 34, 54, 70, 21, 15, 4, 66, 77, 42, 37, 30, 22, 0, 11, 41, 72, 57, 20, 23, 57, 65, 41, 23, 18, 72, 42, 5, 3, 26, 78, 8, 5, 54, 45, 77, 25, 64, 61, 16, 44, 54, 51, 20, 63, 25, 11, 26, 45, 53, 60, 38, 34],
    [76, 66, 5, 49, 75, 54, 69, 46, 32, 1, 42, 60, 26, 48, 50, 80, 32, 24, 55, 61, 47, 12, 21, 12, 49, 54, 34, 25, 36, 15, 56, 55, 20, 9, 8, 62, 13, 82, 9, 44, 29, 60, 53, 82, 42, 80, 5, 43, 71, 3, 80, 77, 47, 78, 34, 25, 62, 18, 10, 49, 62, 64, 52, 81, 11, 66, 62, 13, 47, 17, 52, 70, 26, 23, 32, 31, 64, 23, 35, 32, 50, 6, 1, 25, 8, 37, 47, 43, 26, 76, 65, 68, 80, 17, 7, 45, 63, 14, 53, 63, 60, 16],
    [63, 66, 5, 49, 75, 54, 2, 60, 29, 40, 78, 47, 60, 75, 67, 71, 60, 2, 65, 7, 47, 14, 45, 74, 59, 41, 80, 13, 60, 13, 81, 22, 35, 50, 40, 39, 2, 59, 48, 31, 76, 2, 80, 75, 1, 56, 67, 11, 21, 8, 40, 65, 45, 75, 55, 39, 60, 42, 13, 3, 22, 57, 2, 6, 58, 9, 70, 1, 58, 56, 63, 68, 25, 79, 7, 20, 19, 64, 2, 66, 73, 30, 71, 16, 12, 30, 65, 37, 20, 13, 22, 63, 18, 46, 64, 59, 41, 81, 82, 22, 78, 36, 47, 17, 4, 6, 17, 5, 36, 79, 63, 1, 64, 69, 15, 43, 4, 58, 56, 31, 14, 64, 58, 18, 44, 78, 69, 1, 0, 46, 20, 71, 73, 25, 35, 8, 24],
    [34, 66, 5, 49, 75, 54, 23, 74, 11, 13, 28, 26, 19, 48, 67, 57, 37, 60, 34, 28, 74, 10, 17, 32, 11, 18, 19, 43, 19, 81, 42, 4, 62, 9, 46, 49, 32, 51, 76, 58, 4, 43, 47, 17, 67, 79, 21, 32, 44, 16, 30, 37, 26, 28, 41, 68, 57, 34, 51, 10, 69, 70, 8, 6, 46, 43, 18, 39, 47, 43, 15, 13, 33, 30, 35, 62, 37, 0, 37, 5, 38, 55, 37, 13, 40, 25, 9, 21, 11, 64, 5, 79, 42, 68, 11, 71, 11, 48, 3, 67, 61, 40, 22, 14, 35, 50, 61, 39, 11, 2, 66, 49, 51, 53, 17, 73, 36, 75, 74, 54, 24, 30, 54, 70],
    [27, 66, 5, 49, 75, 54, 2, 60, 29, 40, 2, 55, 9, 15, 59, 18, 68, 3, 36, 5, 47, 77, 44, 38, 1, 18, 28, 76, 4, 34, 60, 63, 58, 80, 17, 54, 79, 75, 48, 54, 55, 19, 62, 64, 14, 47, 51, 70, 75, 5, 11, 47, 45, 58, 68, 69, 79, 25, 38, 45, 73, 47, 68, 50, 34, 45, 78, 26, 79, 57, 4, 56, 22, 60, 18, 75, 43, 60, 59, 67, 63, 42, 49, 33, 40, 65, 79, 77, 7, 3, 26, 62, 31, 78, 26, 57, 69, 40, 4, 23, 26, 13, 67, 42, 38, 72, 11, 39, 65, 60, 25, 6, 80, 66, 68, 77, 59, 78, 19],
    [77, 66, 5, 49, 75, 54, 2, 60, 29, 40, 2, 55, 9, 15, 59, 18, 68, 3, 36, 5, 47, 60, 21, 80, 1, 72, 55, 16, 82, 35, 57, 19, 1, 66, 18, 27, 39, 17, 74, 81, 39, 14, 78, 0, 25, 65, 43, 66, 64, 38, 81, 23, 24, 50, 57, 30, 71, 75, 26, 68, 54, 57, 56, 50, 71, 73, 14, 21, 8, 32, 26, 63, 5, 37, 19, 43, 66, 47, 53, 34, 66, 23, 73, 31, 54, 38, 77, 67, 11, 63, 79, 6, 22, 21, 51, 69, 74, 21, 5, 17, 67, 37, 29, 21, 60, 14, 82, 44, 30, 4, 20, 42, 35, 1, 31, 54, 46, 20, 40, 30],
    [33, 66, 5, 49, 75, 54, 2, 60, 29, 40, 2, 55, 9, 15, 59, 18, 68, 3, 36, 5, 47, 33, 21, 59, 44, 18, 28, 76, 59, 34, 60, 63, 79, 27, 12, 54, 5, 49, 48, 54, 55, 52, 62, 72, 69, 10, 57, 22, 58, 48, 67, 53, 7, 34, 32, 30, 31, 19, 26, 8, 34, 46, 7, 30, 71, 55, 34, 75, 54, 9, 6, 60, 5, 23, 25, 45, 42, 80, 25, 12, 22, 76, 20, 51, 62, 21, 40, 9, 41, 10, 44, 73, 8, 33, 70, 73, 6, 31, 21, 72, 5, 40, 61, 51, 42, 66, 64, 74, 61, 25, 63, 42, 24, 41],
]
# ~25 KB of Finnish prose (written for these experiments) used to make fake plaintexts.
CORPUS_FI = """OLIPA KERRAN PIENI KYLÄ SUUREN METSÄN LAIDALLA KYLÄSSÄ ASUI VANHA MIES JOTA KAIKKI KUTSUIVAT TIETÄJÄKSI VAIKKA HÄN ITSE SANOI OLEVANSA VAIN KALASTAJA JOKA AAMU HÄN NOUSI ENNEN AURINKOA KEITTI KAHVIT JA KÄVELI RANTAAN KATSOMAAN MILLAINEN SÄÄ OLI TULOSSA JOS JÄRVI OLI TYYNI JA PEILIKIRKAS HÄN TIESI ETTÄ PÄIVÄSTÄ TULISI KAUNIS JOS TAAS TUULI NOSTI VAAHTOPÄITÄ JA LOKIT HUUSIVAT KOVAA HÄN PALASI SISÄLLE JA JÄI LUKEMAAN VANHOJA KIRJOJAAN KIRJAT OLIVAT HÄNEN SUURIN AARTEENSA NE OLI KIRJOITETTU KIELELLÄ JOTA KUKAAN MUU KYLÄSSÄ EI YMMÄRTÄNYT SIVUILLA OLI MERKKEJÄ JOTKA MUISTUTTIVAT SILMIÄ PIENIÄ SOIKEITA KUVIOITA JOIDEN KESKELLÄ OLI PISTE JOTKUT SILMÄT KATSOIVAT YLÖS JOTKUT ALAS JOTKUT VASEMMALLE JA JOTKUT OIKEALLE VANHA MIES SANOI ETTÄ NIISSÄ OLI VIESTI JONKA JUMALAT OLIVAT JÄTTÄNEET IHMISILLE KAUAN SITTEN KUKAAN EI USKONUT HÄNTÄ MUTTA KAIKKI KUUNTELIVAT MIELELLÄÄN KUN HÄN KERTOI TARINOITAAN ILTAISIN SAUNAN JÄLKEEN ERÄÄNÄ SYKSYNÄ KYLÄÄN SAAPUI NUORI NAINEN HÄNELLÄ OLI HARMAA VIITTA PITKÄ SAUVA JA REPPU JOKA NÄYTTI RASKAALTA HÄN KERTOI TULLEENSA KAUKAA IDÄSTÄ VUORTEN TAKAA JA ETSIVÄNSÄ MIESTÄ JOKA OSAISI LUKEA SILMIEN KIELTÄ KYLÄLÄISET OSOITTIVAT HÄNELLE TIEN VANHAN KALASTAJAN MÖKILLE NAINEN KOPUTTI OVEEN KOLME KERTAA JA KUN OVI AUKESI HÄN SANOI VAIN YHDEN SANAN VIISAUS VANHA MIES KATSOI HÄNTÄ PITKÄÄN SITTEN HÄN PÄÄSTI NAISEN SISÄÄN KAATOI KUPPIIN KUUMAA KAHVIA JA ISTUI PÖYDÄN ÄÄREEN NAINEN AVASI REPPUNSA JA NOSTI PÖYDÄLLE KIVEN JOKA HEHKUI HIMMEÄSTI KUIN HIILLOS KIVEN PINTAAN OLI KAIVERRETTU SAMOJA SILMIÄ KUIN KIRJOISSA MIES HENKÄISI SYVÄÄN HÄN EI OLLUT KOSKAAN NÄHNYT MITÄÄN SELLAISTA VAIKKA OLI TUTKINUT MERKKEJÄ KOKO IKÄNSÄ SEURAAVAT VIIKOT HE TYÖSKENTELIVÄT YHDESSÄ AAMUISIN HE VERTASIVAT KIVEN MERKKEJÄ KIRJOJEN MERKKEIHIN JA KIRJOITTIVAT MUISTIIN JOKAISEN YHTÄLÄISYYDEN ILTAPÄIVISIN HE KÄVELIVÄT METSÄSSÄ JA KESKUSTELIVAT SIITÄ MITÄ VIESTI VOISI TARKOITTAA NAINEN USKOI ETTÄ SE KERTOI KULTAISESTA PALLOSTA JOKA OLI PIILOTETTU SYVÄLLE MAAN ALLE MIES TAAS ARVELI ETTÄ VIESTI VAROITTI IHMISIÄ ETSIMÄSTÄ LIIKAA KOSKA TOTUUS VOISI OLLA VAARALLISEMPI KUIN TIETÄMÄTTÖMYYS TALVI TULI AIKAISIN SINÄ VUONNA LUNTA SATOI PÄIVÄKAUSIA JA JÄRVI JÄÄTYI NIIN PAKSULTI ETTÄ SEN YLI PYSTYI AJAMAAN HEVOSELLA KYLÄN LAPSET LASKIVAT MÄKEÄ JA RAKENSIVAT LUMILINNOJA JA AIKUISET HAKIVAT METSÄSTÄ POLTTOPUITA VANHAN MIEHEN MÖKISSÄ PALOI TULI YÖTÄ PÄIVÄÄ JA IKKUNASTA NÄKYI KAKSI HAHMOA KUMARTUNEENA PÖYDÄN YLLE HE OLIVAT LÖYTÄNEET JOTAIN TÄRKEÄÄ MUTTA EIVÄT VIELÄ TIENNEET MITÄ ERÄÄNÄ YÖNÄ KUN KUU PAISTOI TÄYTENÄ JA REVONTULET LEISKUIVAT TAIVAALLA NAINEN HERÄSI OUTOON ÄÄNEEN KIVI PÖYDÄLLÄ LAULOI SE EI OLLUT TAVALLISTA LAULUA VAAN MATALA VÄRISEVÄ SÄVEL JOKA TUNTUI TULEVAN JOSTAIN HYVIN KAUKAA NAINEN HERÄTTI MIEHEN JA YHDESSÄ HE KATSOIVAT KUINKA KIVEN SILMÄT ALKOIVAT LIIKKUA NE KÄÄNTYIVÄT YKSI KERRALLAAN YLÖS ALAS VASEMMALLE OIKEALLE JA MUODOSTIVAT UUSIA KUVIOITA MIES OTTI KYNÄN JA ALKOI KIRJOITTAA HÄN KIRJOITTI KOKO YÖN JA KUN AAMU VALKENI PAPERILLA OLI PITKÄ RIVI MERKKEJÄ NE EIVÄT OLLEET SANOJA MUTTA NIISSÄ OLI JÄRJESTYS JOKAINEN KOLMEN SILMÄN RYHMÄ VASTASI JOTAIN LUKUA JA LUVUT TOISTUIVAT OUDOLLA TAVALLA JOSKUS SAMA KUVIO PALASI NELJÄN ASKELEEN PÄÄSTÄ JOSKUS KYMMENEN MUTTA EI KOSKAAN HETI PERÄÄN MIES SANOI ETTÄ TÄMÄ OLI AVAIN MUTTA LUKKO OLI VIELÄ LÖYTÄMÄTTÄ KEVÄÄLLÄ NAINEN LÄHTI JATKAMAAN MATKAANSA HÄN LUPASI PALATA KUN OLISI LÖYTÄNYT LISÄÄ KIVIÄ VANHA MIES JÄI YKSIN MÖKKIINSÄ MUTTA HÄN EI OLLUT ENÄÄ SAMANLAINEN KUIN ENNEN HÄN PUHUI VÄHEMMÄN JA AJATTELI ENEMMÄN ILTAISIN HÄN ISTUI RANNALLA JA KATSELI KUINKA AURINKO LASKI JÄRVEN TAAKSE JA MIETTI OLIVATKO JUMALAT TODELLA JÄTTÄNEET VIESTIN VAI OLIKO KAIKKI VAIN SATTUMAA KYLÄSSÄ KERROTTIIN MYÖHEMMIN ETTÄ VANHA MIES OLI LOPULTA RATKAISSUT ARVOITUKSEN KUKAAN EI TIENNYT MITÄ VIESTI SANOI KOSKA MIES EI KERTONUT SITÄ KENELLEKÄÄN HÄN SANOI VAIN ETTÄ JOTKUT ASIAT ON PAREMPI JÄTTÄÄ SANOMATTA KUN HÄN KUOLI HÄNEN KIRJANSA HAUDATTIIN HÄNEN KANSSAAN JA KIVI KATOSI JÄLJETTÖMIIN MUTTA VIELÄ TÄNÄKIN PÄIVÄNÄ KUN KUU ON TÄYSI JA REVONTULET LEISKUVAT JOTKUT KYLÄLÄISET SANOVAT KUULEVANSA JÄRVEN YLLÄ MATALAN VÄRISEVÄN LAULUN ALKEMISTIN TYÖPAJA SIJAITSI VANHAN LINNAN KELLARISSA SINNE JOHTI KAPEA KIVIPORTAIKKO JONKA SEINILLÄ PALOIVAT SOIHDUT ILMASSA LEIJUI RIKIN JA SUOLAN HAJU JA PÖYDILLÄ KUPLI LASIASTIOITA JOISSA OLI KAIKENVÄRISIÄ NESTEITÄ ALKEMISTI ITSE OLI PITKÄ JA LAIHA MIES JOLLA OLI VALKOINEN PARTA JA SILMÄT JOTKA NÄYTTIVÄT NÄKEVÄN IHMISEN LÄPI HÄN OLI ETSINYT VIISASTEN KIVEÄ YLI NELJÄKYMMENTÄ VUOTTA HÄNEN OPPIPOIKANSA OLI NUORI JA INNOKAS MUTTA USEIN HUOLIMATON HÄN SEKOITTI VÄÄRÄT AINEET UNOHTI SAMMUTTAA TULEN TAI PUDOTTI KALLIITA PULLOJA LATTIALLE ALKEMISTI EI KOSKAAN SUUTTUNUT HÄNELLE HÄN SANOI AINA ETTÄ VIRHEET OVAT PARHAITA OPETTAJIA JA ETTÄ JOKAINEN RÄJÄHDYS VIE ASKELEEN LÄHEMMÄKSI TOTUUTTA OPPIPOIKA EI OLLUT TÄSTÄ AIVAN VARMA VARSINKAAN SEN JÄLKEEN KUN HÄNEN KULMAKARVANSA OLIVAT PALANEET KOLMANNEN KERRAN VIISASTEN KIVEN VALMISTAMISEEN TARVITTIIN SEITSEMÄN VAIHETTA ENSIN AINE PITI MUSTATA SITTEN VALKAISTA SITTEN KELTAISTAA JA LOPUKSI PUNAISTAA JOKAISESSA VAIHEESSA OLI OMAT VAARANSA MUSTAUSVAIHEESSA AINE SAATTOI SYTTYÄ TULEEN VALKAISUSSA SE SAATTOI MUUTTUA MYRKYLLISEKSI KAASUKSI JA PUNAISTAMISESSA SE SAATTOI KADOTA KOKONAAN JOS LÄMPÖTILA NOUSI LIIAN KORKEAKSI ALKEMISTI OLI PÄÄSSYT KUUDENTEEN VAIHEESEEN MONTA KERTAA MUTTA SEITSEMÄS OLI AINA EPÄONNISTUNUT ERÄÄNÄ PÄIVÄNÄ OPPIPOIKA LÖYSI KELLARIN NURKASTA VANHAN ARKUN SEN KANNESSA OLI SAMOJA SILMÄKUVIOITA JOITA ALKEMISTI OLI NÄHNYT MUINAISISSA KÄSIKIRJOITUKSISSA ARKUSSA OLI KIRJE JOKA OLI KIRJOITETTU KULTAISELLA MUSTEELLA KIRJEEN MUKAAN VIISASTEN KIVEÄ EI VOINUT VALMISTAA PELKILLÄ AINEILLA VAAN SIIHEN TARVITTIIN MYÖS SANA JOKA PITI LAUSUA OIKEALLA HETKELLÄ SANA OLI KÄTKETTY SILMIEN VIESTIIN JA VAIN SE JOKA OSASI LUKEA VIESTIN PYSTYI SAATTAMAAN TYÖN LOPPUUN ALKEMISTI LUKI KIRJEEN MONEEN KERTAAN HÄNEN KÄTENSÄ VAPISIVAT JA HÄNEN ÄÄNENSÄ OLI KÄHEÄ KUN HÄN LOPULTA PUHUI HÄN KERTOI OPPIPOJALLE ETTÄ OLI KUULLUT TÄSTÄ SANASTA JO NUORUUDESSAAN MUTTA EI OLLUT KOSKAAN USKONUT SEN OLEVAN TOTTA NYT HÄN TIESI ETTÄ HÄNEN KOKO ELÄMÄNSÄ TYÖ OLI OLLUT VAIN PUOLET TEHTÄVÄSTÄ TOINEN PUOLI OLI KIELESSÄ EI KEMIASSA HE ALOITTIVAT TYÖN HETI ALKEMISTI KOPIOI SILMÄT SUURELLE PAPERILLE JA JAKOI NE KOLMEN RYHMIIN OPPIPOIKA LASKI KUINKA MONTA KERTAA KUKIN RYHMÄ ESIINTYI JA KIRJOITTI LUVUT TAULUKKOON HE HUOMASIVAT PIAN ETTÄ RYHMIÄ OLI TÄSMÄLLEEN KAHDEKSANKYMMENTÄKOLME ERILAISTA JA ETTÄ MIKÄÄN NIISTÄ EI KOSKAAN TOISTUNUT HETI PERÄKKÄIN ALKEMISTI SANOI ETTÄ TÄMÄ EI VOINUT OLLA SATTUMAA JOKU OLI SUUNNITELLUT VIESTIN HYVIN HUOLELLISESTI VIIKOT KULUIVAT JA KELLARIN SEINÄT TÄYTTYIVÄT PAPEREISTA OPPIPOIKA OLI OPPINUT LUKEMAAN VANHOJA KIELIÄ LASKEMAAN MONIMUTKAISIA LASKUJA JA PIIRTÄMÄÄN TARKKOJA KAAVIOITA HÄN EI ENÄÄ PUDOTTANUT PULLOJA EIKÄ UNOHTANUT TULTA ALKEMISTI OLI YLPEÄ HÄNESTÄ VAIKKA EI SANONUT SITÄ ÄÄNEEN HE OLIVAT YHDESSÄ PÄÄSSEET PIDEMMÄLLE KUIN KUKAAN ENNEN HEITÄ MUTTA VIESTI PYSYI SILTI SALAISUUTENA LOPULTA ALKEMISTI SAIRASTUI HÄN MAKASI VUOTEESSA VIIKKOJA EIKÄ MIKÄÄN LÄÄKE AUTTANUT ENNEN KUOLEMAANSA HÄN KUTSUI OPPIPOJAN LUOKSEEN JA ANTOI TÄLLE AVAIMEN JOKA AVASI ARKUN POHJAN SALAISEN LOKERON LOKEROSSA OLI PIENI KULTAINEN PALLO JOKA HEHKUI LÄMPIMÄSTI KÄMMENELLÄ ALKEMISTI KUISKASI ETTÄ PALLO OLI HÄNEN OPETTAJANSA LAHJA JA ETTÄ SE NÄYTTÄISI TIEN KUN AIKA OLISI OIKEA SITTEN HÄN SULKI SILMÄNSÄ VIIMEISEN KERRAN OPPIPOIKA JATKOI TYÖTÄ YKSIN VUODET KULUIVAT JA HÄNESTÄ TULI ITSE VANHA MIES JOLLA OLI VALKOINEN PARTA HÄNELLÄ OLI OMA OPPIPOIKA NUORI JA INNOKAS MUTTA USEIN HUOLIMATON KUN OPPIPOIKA PUDOTTI PULLON LATTIALLE VANHA ALKEMISTI HYMYILI JA SANOI ETTÄ VIRHEET OVAT PARHAITA OPETTAJIA JA JOSKUS KUN YÖ OLI HILJAINEN HÄN OTTI ESIIN KULTAISEN PALLON JA KATSOI SITÄ PITKÄÄN ODOTTAEN MERKKIÄ JOKA EI KOSKAAN TULLUT POHJOISESSA MISSÄ AURINKO EI LASKE KESÄLLÄ EIKÄ NOUSE TALVELLA ASUI KANSA JOKA PUHUI TÄHTIEN KANSSA HE USKOIVAT ETTÄ JOKAINEN TÄHTI OLI ESI ISÄN SILMÄ JOKA KATSOI ALAS MAAHAN JA VARTIOI ELÄVIEN KULKUA KUN TÄHTI PUTOSI JOKU ESI ISÄ OLI SULKENUT SILMÄNSÄ JA KANSAN PITI LAULAA HÄNELLE UUSI LAULU JOTTA HÄN VOISI AVATA NE TAAS LAULUT OLIVAT PITKIÄ JA MONIMUTKAISIA JA NIIDEN OPETTELU KESTI VUOSIA LAULAJIA KUTSUTTIIN TIETÄJIKSI HE OLIVAT KANSAN ARVOSTETUIMPIA JÄSENIÄ JA HEIDÄN SANANSA PAINOI ENEMMÄN KUIN PÄÄLLIKÖIDEN TIETÄJÄ OSASI PARANTAA SAIRAITA ENNUSTAA SÄÄTÄ JA LÖYTÄÄ KADONNEITA POROJA HÄN OSASI MYÖS PUHUA ELÄINTEN KANSSA AINAKIN NIIN KERROTTIIN KUN KARHU TULI LIIAN LÄHELLE KYLÄÄ TIETÄJÄ MENI METSÄÄN JA KESKUSTELI SEN KANSSA JA KARHU LÄHTI POIS EIKÄ PALANNUT NUORIN TIETÄJÄ OLI TYTTÖ NIMELTÄ AINO HÄN OLI VASTA VIISITOISTA VUOTTA VANHA MUTTA OSASI JO ENEMMÄN LAULUJA KUIN MONI VANHEMPI HÄNEN ÄITINSÄ OLI OLLUT TIETÄJÄ JA HÄNEN ISOÄITINSÄ JA TÄMÄN ÄITI ENNEN HÄNTÄ AINON SUVUSSA TAITO OLI KULKENUT NAISELTA NAISELLE NIIN KAUAN KUIN KUKAAN MUISTI AINO EI KUITENKAAN HALUNNUT OLLA TIETÄJÄ HÄN HALUSI MATKUSTAA ETELÄÄN JA NÄHDÄ MAAILMAN JOSTA KAUPPIAAT KERTOIVAT ERÄÄNÄ TALVENA KYLÄÄN TULI SAIRAUS JOTA KUKAAN EI TUNTENUT IHMISET HEIKKENIVÄT PÄIVÄ PÄIVÄLTÄ JA HEIDÄN SILMÄNSÄ MUUTTUIVAT SAMEIKSI KUIN JÄÄTYNYT JÄRVI VANHAT TIETÄJÄT LAULOIVAT KAIKKI LAULUNSA MUTTA MIKÄÄN EI AUTTANUT LOPULTA HE KÄÄNTYIVÄT AINON PUOLEEN HÄNEN ISOÄITINSÄ OLI KERTONUT HÄNELLE LAULUSTA JOTA EI SAANUT LAULAA KUIN SUURIMMASSA HÄDÄSSÄ KOSKA SE VAATI LAULAJALTA JOTAIN HYVIN KALLISTA AINO AJATTELI ASIAA KOLME PÄIVÄÄ JA KOLME YÖTÄ SITTEN HÄN MENI KYLÄN KESKELLE NOUSI SUURELLE KIVELLE JA ALKOI LAULAA LAULU OLI NIIN VANHA ETTÄ SEN SANAT OLIVAT MUUTTUNEET MELKEIN KÄSITTÄMÄTTÖMIKSI SE KERTOI AJASTA ENNEN MAAILMAA JOLLOIN OLI VAIN PIMEYS JA VESI JA LINNUSTA JOKA MUNI KULTAISEN MUNAN PIMEÄN VEDEN PINNALLE MUNASTA SYNTYI TAIVAS JA MAA AURINKO JA KUU JA TÄHDET JOTKA OLIVAT ESI ISIEN SILMIÄ KUN AINO LAULOI REVONTULET SYTTYIVÄT TAIVAALLE KIRKKAAMPINA KUIN KOSKAAN NE LASKEUTUIVAT ALAS KYLÄN YLLE KUIN VERHO JA NIIDEN VALOSSA SAIRAIDEN SILMÄT KIRKASTUIVAT IHMISET NOUSIVAT VUOTEISTAAN JA TULIVAT ULOS KATSOMAAN KUN LAULU LOPPUI KAIKKI OLIVAT TERVEITÄ MUTTA AINO EI ENÄÄ NÄHNYT HÄNEN SILMÄNSÄ OLIVAT MUUTTUNEET VALKOISIKSI JA HÄN SANOI NÄKEVÄNSÄ NYT VAIN TÄHDET MUTTA NE HÄN NÄKI SELVEMMIN KUIN KUKAAN MUU AINOSTA TULI KANSAN SUURIN TIETÄJÄ HÄN ELI PITKÄN ELÄMÄN JA OPETTI SATOJA LAULUJA NUORILLE HÄN EI KOSKAAN MATKUSTANUT ETELÄÄN MUTTA HÄN SANOI ETTEI SITÄ TARVINNUT KOSKA TÄHDET KERTOIVAT HÄNELLE KAIKEN MITÄ MAAILMASSA TAPAHTUI KUN HÄN KUOLI TAIVAALLE SYTTYI UUSI TÄHTI KIRKKAAMPI KUIN MUUT JA KANSA SANOI ETTÄ SE OLI AINON SILMÄ JOKA VARTIOI HEITÄ IKUISESTI KAUPUNGIN TORILLA OLI JOKA LAUANTAI SUURI MARKKINAPÄIVÄ MAALAISET TOIVAT MYYTÄVÄKSI PERUNOITA PORKKANOITA SIPULEITA JA KAALIA JA KALASTAJAT KANTOIVAT KOREITTAIN SILAKKAA JA AHVENTA LEIPURIN KOJUSSA TUOKSUI TUORE RUISLEIPÄ JA PULLA JA LAPSET JONOTTIVAT JÄÄTELÖÄ VAIKKA ILMA OLI VIELÄ VIILEÄ VANHA ROUVA MYI VILLASUKKIA JOTKA HÄN OLI NEULONUT KOKO TALVEN JA HÄNEN VIERESSÄÄN NUORI MIES KAUPPASI ITSE TEHTYJÄ PUULUSIKOITA MINÄ KÄVIN TORILLA AINA ÄITINI KANSSA HÄN OSTI VIIKON RUOAT JA JUTTELI TUTTUJEN KANSSA JA MINÄ SAIN YLEENSÄ YHDEN MUNKIN JOS OLIN OLLUT KILTISTI MUISTAN ERITYISESTI ERÄÄN KEVÄTAAMUN KUN TORI OLI TÄYNNÄ IHMISIÄ JA AURINKO PAISTOI ENSIMMÄISTÄ KERTAA MONEEN VIIKKOON LÄMPIMÄSTI KAIKKI OLIVAT HYVÄLLÄ TUULELLA JA JOPA KALAKAUPPIAS JOKA YLEENSÄ OLI TUIMA JA VÄHÄPUHEINEN HYMYILI JA VITSAILI ASIAKKAIDEN KANSSA SINÄ AAMUNA TORILLA OLI MYÖS MIES JOTA EN OLLUT NÄHNYT KOSKAAN AIEMMIN HÄNELLÄ OLI PITKÄ MUSTA TAKKI JA LEVEÄLIERINEN HATTU JA HÄN MYI OUTOJA ESINEITÄ PIENESTÄ PUULAATIKOSTA SIELLÄ OLI KIVIÄ JOISSA OLI KUVIOITA VANHOJA KOLIKOITA JOIDEN KIRJOITUSTA KUKAAN EI OSANNUT LUKEA JA LASIPULLOJA JOISSA OLI VÄRIKÄSTÄ HIEKKAA ÄITINI SANOI ETTÄ MIES OLI VARMAAN HUIJARI MUTTA MINÄ EN VOINUT OLLA KATSOMATTA HÄNEN TAVAROITAAN MIES HUOMASI KIINNOSTUKSENI JA VIITTASI MINUA TULEMAAN LÄHEMMÄKSI HÄN OTTI LAATIKOSTA PIENEN PYÖREÄN KIVEN JA OJENSI SEN MINULLE KIVEN PINNASSA OLI KOLME SILMÄÄ JOTKA KATSOIVAT ERI SUUNTIIN MIES SANOI ETTÄ KIVI OLI TUOTU KAUKAA VUORTEN TAKAA JA ETTÄ SE TOISI ONNEA SILLE JOKA OSAISI KUUNNELLA SITÄ HÄN EI PYYTÄNYT SIITÄ RAHAA HÄN SANOI VAIN ETTÄ MINUN PITI PITÄÄ SIITÄ HYVÄÄ HUOLTA PIDIN KIVEÄ TASKUSSANI MONTA VUOTTA EN KOSKAAN KUULLUT SEN SANOVAN MITÄÄN MUTTA JOSKUS KUN OLIN SURULLINEN TAI PELOISSANI PURISTIN SITÄ KÄDESSÄNI JA TUNSIN OLONI RAUHALLISEMMAKSI KUN MUUTIN POIS KOTOA KIVI TULI MUKAANI KUN MENIN NAIMISIIN SE OLI TASKUSSANI JA KUN ENSIMMÄINEN LAPSENI SYNTYI ANNOIN KIVEN HÄNELLE JA KERROIN TARINAN TORIN OUDOSTA MIEHESTÄ NYT LAPSENI ON ITSE AIKUINEN JA KIVI ON HÄNEN LAPSELLAAN JOSKUS MIETIN KUKA MIES OLI JA MISTÄ HÄN OLI TULLUT EN NÄHNYT HÄNTÄ ENÄÄ KOSKAAN SEN JÄLKEEN KUN KYSYIN MUILTA TORIKAUPPIAILTA KUKAAN EI MUISTANUT HÄNTÄ ÄITINI SANOI ETTÄ OLIN VARMAAN NÄHNYT UNTA MUTTA MINULLA OLI KIVI JA SE OLI TODELLINEN EHKÄ KAIKKI TARINAT EIVÄT TARVITSE SELITYSTÄ SUOMEN KESÄ ON LYHYT MUTTA VALOISA KESÄKUUN LOPUSSA AURINKO PAISTAA LÄHES KOKO VUOROKAUDEN JA IHMISET VIETTÄVÄT JUHANNUSTA MÖKEILLÄ JÄRVIEN RANNOILLA HE SAUNOVAT UIVAT GRILLAAVAT MAKKARAA JA POLTTAVAT KOKKOJA VANHAN USKOMUKSEN MUKAAN JUHANNUSYÖNÄ TYTÖT VOIVAT NÄHDÄ TULEVAN PUOLISONSA JOS HE KERÄÄVÄT SEITSEMÄN ERILAISTA KUKKAA JA LAITTAVAT NE TYYNYN ALLE MONET TEKEVÄT NÄIN VIELÄ NYKYÄÄNKIN VAIKKA EIVÄT USKO SIIHEN SYKSY TUO MUKANAAN SATEET JA PIMEYDEN LEHDET MUUTTUVAT KELTAISIKSI JA PUNAISIKSI JA PUTOAVAT PUISTA JA METSÄSSÄ ON PALJON SIENIÄ JA MARJOJA IHMISET KERÄÄVÄT MUSTIKOITA PUOLUKOITA JA KARPALOITA JA TEKEVÄT NIISTÄ HILLOA JA MEHUA TALVEN VARALLE KANTARELLIT JA SUPPILOVAHVEROT OVAT SUOSITTUJA SIENIÄ JA MONELLA PERHEELLÄ ON OMAT SALAISET SIENIPAIKKANSA JOISTA EI KERROTA KENELLEKÄÄN TALVI ON PITKÄ JA KYLMÄ LUNTA ON MAASSA USEIN MARRASKUUSTA HUHTIKUUHUN JA PAKKASTA VOI OLLA KOLMEKYMMENTÄ ASTETTA TAI ENEMMÄNKIN POHJOISESSA AURINKO EI NOUSE LAINKAAN JOULUKUUSSA JA KAAMOS KESTÄÄ VIIKKOJA SILLOIN TAIVAALLA NÄKYY USEIN REVONTULIA JOTKA LOISTAVAT VIHREINÄ JA VIOLETTEINA IHMISET HIIHTÄVÄT LUISTELEVAT JA PILKKIVÄT KALAA JÄÄTYNEILTÄ JÄRVILTÄ JOULU ON TALVEN TÄRKEIN JUHLA JA SILLOIN PERHEET KOKOONTUVAT YHTEEN SYÖMÄÄN KINKKUA ROSOLLIA JA LAATIKOITA KEVÄT TULEE HITAASTI ENSIN PÄIVÄT PITENEVÄT SITTEN LUMI ALKAA SULAA JA LOPULTA MUUTTOLINNUT PALAAVAT ETELÄSTÄ KUN ENSIMMÄINEN LESKENLEHTI KUKKII TIENVARRESSA KAIKKI TIETÄVÄT ETTÄ TALVI ON OHI VAPPUNA OPISKELIJAT LAITTAVAT VALKOISET LAKIT PÄÄHÄNSÄ JA KAUPUNGEISSA JUHLITAAN KADUILLA JA PUISTOISSA IHMISET JUOVAT SIMAA JA SYÖVÄT TIPPALEIPIÄ JA ILMAPALLOT VÄRITTÄVÄT TORIT NOIDAN MÖKKI OLI SYVÄLLÄ SUOLLA MINNE EI JOHTANUT YHTÄÄN POLKUA SINNE PÄÄSI VAIN JOS TIESI MILLE MÄTTÄILLE ASTUA JA JOS SATTUI VÄÄRÄÄN PAIKKAAN SUO NIELI KULKIJAN KOKONAAN KYLÄN LAPSIA VAROITETTIIN MENEMÄSTÄ SUOLLE MUTTA TIETENKIN HE MENIVÄT SILTI ROHKEIMMAT HEISTÄ SANOIVAT NÄHNEENSÄ NOIDAN PITKÄN JA KUMARAN HAHMON JOKA KERÄSI YRTTEJÄ KUUN VALOSSA JA PUHUI ITSEKSEEN OUDOLLA KIELELLÄ ERÄÄNÄ KESÄNÄ KAKSI VELJESTÄ PÄÄTTI ETSIÄ NOIDAN MÖKIN HE OLIVAT KUULLEET ETTÄ NOIDALLA OLI KIRJA JOSSA OLI KAIKKIEN TAIKOJEN SALAISUUDET JA HE HALUSIVAT NÄHDÄ SEN VANHEMPI VELI OLI VAROVAINEN JA HARKITSEVA NUOREMPI ROHKEA JA KÄRSIMÄTÖN HE LÄHTIVÄT AAMULLA VARHAIN JA OTTIVAT MUKAANSA LEIPÄÄ JUUSTOA JA KÖYDEN ISOÄITI OLI KERTONUT HEILLE ETTÄ SUOLLA PITI AINA KULKEA MYÖTÄPÄIVÄÄN EIKÄ KOSKAAN SAANUT KATSOA TAAKSEEN PUOLENPÄIVÄN AIKAAN HE LÖYSIVÄT MÖKIN SE OLI PIENI JA HARMAA JA SEN KATOLLA KASVOI SAMMALTA JA KOIVUN TAIMIA OVI OLI RAOLLAAN JA SISÄLTÄ KUULUI HILJAISTA HYRÄILYÄ VELJEKSET KATSOIVAT TOISIAAN NUOREMPI HALUSI MENNÄ SISÄÄN HETI MUTTA VANHEMPI PIDÄTTELI HÄNTÄ HE ODOTTIVAT JA KUUNTELIVAT HETKEN PÄÄSTÄ HYRÄILY LOPPUI JA OVEN RAOSTA KURKISTI VANHA NAINEN JOLLA OLI YSTÄVÄLLISET KASVOT JA KIRKKAAN SINISET SILMÄT NOITA EI OLLUT LAINKAAN SELLAINEN KUIN HE OLIVAT KUVITELLEET HÄN KUTSUI HEIDÄT SISÄÄN KEITTI HEILLE TEETÄ JA TARJOSI HUNAJAKAKKUA HÄN KERTOI ASUNEENSA SUOLLA VIISIKYMMENTÄ VUOTTA KOSKA SIELLÄ KASVOIVAT PARHAAT PARANTAVAT YRTIT HÄN EI OLLUT PAHA EIKÄ VAARALLINEN VAAN HÄN OLI AUTTANUT KYLÄN IHMISIÄ MONTA KERTAA VAIKKA KUKAAN EI TIENNYT SITÄ KUN LAPSET SAIRASTUIVAT KUUMEESEEN HÄN JÄTTI YÖLLÄ LÄÄKKEITÄ HEIDÄN KOTIENSA PORTAILLE VELJEKSET KYSYIVÄT KIRJASTA NOITA NAUROI JA OTTI HYLLYLTÄ PAKSUN NAHKAKANTISEN KIRJAN HÄN AVASI SEN JA NÄYTTI HEILLE SIVUJA JOTKA OLIVAT TÄYNNÄ KASVIEN KUVIA JA RESEPTEJÄ SIINÄ EI OLLUT YHTÄÄN TAIKAA VAIN TIETOA SIITÄ MIKÄ KASVI AUTTOI MIHINKIN VAIVAAN NOITA SANOI ETTÄ TIETO OLI KAIKKEIN VOIMAKKAIN TAIKA JA ETTÄ JOKAINEN JOKA JAKSOI OPETELLA VOISI TEHDÄ SAMOJA ASIOITA KUIN HÄN NUOREMPI VELI OLI PETTYNYT MUTTA VANHEMPI OLI INNOISSAAN HÄN PYYSI NOITAA OPETTAMAAN HÄNTÄ JA NOITA SUOSTUI SIITÄ LÄHTIEN VANHEMPI VELI KÄVI SUOLLA JOKA VIIKKO JA OPPI TUNTEMAAN KAIKKI KASVIT JA NIIDEN VOIMAT KUN NOITA LOPULTA KUOLI HÄN JÄTTI KIRJANSA VANHEMMALLE VELJELLE JOSTA TULI KYLÄN PARANTAJA JA NUOREMPI VELI JOKA OLI HALUNNUT NÄHDÄ TAIKOJA LÄHTI MERILLE JA NÄKI MAAILMAN JOSSA OLI ENEMMÄN IHMEITÄ KUIN MISSÄÄN KIRJASSA KULTAINEN PALLO MAKASI KIRKON ALLA SYVÄLLÄ KALLIOSSA MISSÄ OLI AINA PIMEÄÄ JA KYLMÄÄ SE OLI OLLUT SIELLÄ TUHANSIA VUOSIA KAUAN ENNEN KUIN KIRKKOA OLI RAKENNETTU TAI KYLÄÄ PERUSTETTU KUKAAN EI TIENNYT KUKA OLI TUONUT SEN SINNE TAI MIKSI VANHAT TARINAT KERTOIVAT ETTÄ PALLO OLI PUDONNUT TAIVAALTA TÄHTENÄ JA ETTÄ SE SISÄLSI KOKO MAAILMAN MUISTIN JOKA SATA VUOTTA SE HERÄSI HETKEKSI JA LAULOI JA SILLOIN MAA VAPISI KOKO PITÄJÄSSÄ KIRKON VANHA SUNTIO OLI AINOA JOKA USKOI TARINOIHIN HÄN OLI KUULLUT LAULUN KERRAN LAPSENA JA HÄN MUISTI SEN YHÄ SE OLI OLLUT KAUNEIN ÄÄNI JONKA HÄN OLI KOSKAAN KUULLUT JA SAMALLA PELOTTAVIN HÄN SANOI ETTÄ LAULUSSA OLI SANOJA MUTTA NE EIVÄT OLLEET MINKÄÄN IHMISKIELEN SANOJA NE OLIVAT VANHEMPIA KUIN IHMISET VANHEMPIA KUIN MAA ITSE JA HÄN SANOI ETTÄ JOKA YMMÄRTÄISI LAULUN YMMÄRTÄISI MYÖS MIKSI MAAILMA OLI OLEMASSA KUN SATA VUOTTA OLI TAAS KULUMASSA UMPEEN SUNTIO ALKOI VALMISTAUTUA HÄN KIRJOITTI MUISTIIN KAIKEN MITÄ MUISTI LAULUSTA JA KÄVI JOKA ILTA KIRKON KELLARISSA KUUNTELEMASSA KYLÄLÄISET NAUROIVAT HÄNELLE JA SANOIVAT ETTÄ VANHUS OLI TULLUT HULLUKSI MUTTA PAPPI JOKA OLI NUORI JA UTELIAS ALKOI KIINNOSTUA HÄN LUKI KIRKON VANHOJA ASIAKIRJOJA JA LÖYSI MERKINTÖJÄ JOTKA VAHVISTIVAT SUNTION TARINAN JOKA SATA VUOTTA AINA SAMANA PÄIVÄNÄ MAA OLI VAPISSUT JA KIRKONKELLOT OLIVAT SOINEET ITSESTÄÄN SINÄ YÖNÄ PAPPI JA SUNTIO MENIVÄT YHDESSÄ KELLARIIN HE ISTUIVAT KYLMÄLLÄ KIVILATTIALLA JA ODOTTIVAT KESKIYÖLLÄ KUULUI ENSIN HILJAINEN HUMINA SITTEN MATALA SÄVEL JOKA NOUSI JA LASKI KUIN AALLOT MAA ALKOI VÄRISTÄ JA KIRKONKELLOT YLHÄÄLLÄ ALKOIVAT SOIDA SUNTIO ITKI ONNESTA JA PAPPI KIRJOITTI NIIN NOPEASTI KUIN PYSTYI LAULU KESTI TUNNIN JA SITTEN SE LOPPUI YHTÄ ÄKKIÄ KUIN OLI ALKANUTKIN PAPPI TUTKI MUISTIINPANOJAAN SEURAAVAT KYMMENEN VUOTTA HÄN HUOMASI ETTÄ LAULUN SÄVELET MUODOSTIVAT KUVIOITA JOTKA TOISTUIVAT TIETYIN VÄLEIN JOKAINEN KUVIO KOOSTUI KOLMESTA OSASTA JA OSIA OLI VIISI ERILAISTA KUN HÄN LASKI KAIKKI MAHDOLLISET YHDISTELMÄT HÄN SAI LUVUN SATAKAKSIKYMMENTÄVIISI MUTTA LAULUSSA ESIINTYI VAIN KAHDEKSANKYMMENTÄKOLME HÄN EI KOSKAAN SAANUT SELVILLE MIKSI JUURI NIIN MONTA HÄN KIRJOITTI LÖYDÖISTÄÄN KIRJAN MUTTA KUKAAN EI JULKAISSUT SITÄ KIRJA ON YHÄ KIRKON ARKISTOSSA SITÄ ON LUKENUT MONI MUTTA KUKAAN EI OLE RATKAISSUT LAULUN ARVOITUSTA JOTKUT USKOVAT ETTÄ RATKAISU ON NUMEROISSA TOISET TAAS ETTÄ SE ON SANOISSA JA JOTKUT SANOVAT ETTÄ LAULUA EI OLE TARKOITETTU RATKAISTAVAKSI VAAN KUUNNELTAVAKSI SEURAAVAN KERRAN PALLO HERÄÄ VASTA MONEN VUODEN PÄÄSTÄ JA SILLOIN JOKU TOINEN ISTUU KELLARISSA JA KUUNTELEE ENSIMMÄINEN SÄÄNTÖ ÄLÄ KOSKAAN KULJE YKSIN SYVÄLLE LUOLAAN TOINEN SÄÄNTÖ OTA AINA MUKAAN TARPEEKSI VETTÄ JA RUOKAA KOLMAS SÄÄNTÖ JOS KUULET LAULUA ÄLÄ SEURAA SITÄ NELJÄS SÄÄNTÖ JOS NÄET KULTAA ÄLÄ KOSKE SIIHEN ENNEN KUIN OLET VARMISTANUT ETTEI SE OLE ANSA VIIDES SÄÄNTÖ MUISTA AINA MISTÄ TULIT JA MERKITSE REITTISI KUUDES SÄÄNTÖ JOS KOHTAAT NOIDAN OLE KOHTELIAS SEITSEMÄS SÄÄNTÖ ÄLÄ KOSKAAN JUO TUNTEMATONTA NESTETTÄ KAHDEKSAS SÄÄNTÖ TULI JA VESI EIVÄT SOVI YHTEEN MUTTA ÖLJY JA TULI SOPIVAT LIIANKIN HYVIN YHDEKSÄS SÄÄNTÖ JOS LATTIA TUNTUU LIIAN LÄMPIMÄLTÄ SE ON LUULTAVASTI LAAVAA KYMMENES SÄÄNTÖ KAIKKI MIKÄ KIILTÄÄ EI OLE KULTAA MUTTA KAIKKI KULTA KIILTÄÄ YHDESTOISTA SÄÄNTÖ LUOTA SILMIISI MUTTA ÄLÄ LUOTA KAIKKEEN MITÄ SILMÄT NÄYTTÄVÄT KAHDESTOISTA SÄÄNTÖ KUN ET ENÄÄ TIEDÄ MITÄ TEHDÄ PALAA ALKUUN JA ALOITA UUDELLEEN ITÄ JA LÄNSI OVAT KUIN KAKSI VELJESTÄ JOTKA EIVÄT KOSKAAN KOHTAA KUN AURINKO NOUSEE IDÄSTÄ LÄNSI ON VIELÄ PIMEÄ JA KUN SE LASKEE LÄNTEEN ITÄ ON JO YÖN VALLASSA VANHA SANANLASKU SANOO ETTÄ VIISAS KATSOO MOLEMPIIN SUUNTIIN MUTTA KULKEE VAIN YHTEEN TOINEN SANANLASKU SANOO ETTÄ JOKA ETSII IDÄSTÄ LÖYTÄÄ LÄNNESTÄ JA JOKA ETSII LÄNNESTÄ LÖYTÄÄ IDÄSTÄ KUMPIKIN ON TOTTA JA KUMPIKIN ON VÄÄRIN TIEDEMIEHET OVAT TUTKINEET TÄHTIÄ TUHANSIA VUOSIA HE OVAT LASKENEET NIIDEN ETÄISYYKSIÄ MITANNEET NIIDEN KIRKKAUTTA JA ENNUSTANEET NIIDEN LIIKKEITÄ MUTTA KUKAAN EI OLE VIELÄ PYSTYNYT VASTAAMAAN KYSYMYKSEEN MIKSI TÄHDET OVAT OLEMASSA JOTKUT SANOVAT ETTÄ KYSYMYS ON VÄÄRÄ JA ETTÄ TIETEEN TEHTÄVÄ ON KERTOA MITEN EI MIKSI TOISET TAAS USKOVAT ETTÄ JOKAINEN MITEN JOHTAA LOPULTA MIKSI JOS SITÄ SEURAA TARPEEKSI PITKÄLLE ISÄNI OLI PUUSEPPÄ HÄN TEKI PÖYTIÄ TUOLEJA KAAPPEJA JA SÄNKYJÄ JA HÄNEN TYÖNSÄ OLIVAT TUNNETTUJA KOKO MAAKUNNASSA HÄN SANOI AINA ETTÄ PUU PUHUU JOS SITÄ OSAA KUUNNELLA JOKAISELLA LAUDALLA OLI OMA TARINANSA JOKA NÄKYI SYISSÄ JA OKSANKOHDISSA JA HYVÄ PUUSEPPÄ EI PAKOTTANUT PUUTA MUOTOON VAAN ANTOI SEN LÖYTÄÄ OMAN MUOTONSA MINÄ EN KOSKAAN OPPINUT KUUNTELEMAAN PUUTA MUTTA OPIN KUUNTELEMAAN ISÄÄNI HÄNEN VERSTAANSA OLI TALON TAKANA VANHASSA NAVETASSA JONKA HÄN OLI KORJANNUT ITSE SIELLÄ TUOKSUI KOIVU MÄNTY JA TERVAÖLJY JA LATTIALLA OLI AINA PAKSU KERROS SAHANPURUA TALVELLA HÄN LÄMMITTI VERSTASTA VANHALLA VALURAUTAKAMIINALLA JA MINÄ ISTUIN SEN VIERESSÄ JA KATSELIN KUINKA HÄN HÖYLÄSI SAHASI JA HIOI HÄN EI PUHUNUT PALJON TYÖN AIKANA MUTTA JOSKUS HÄN VIHELSI VANHOJA KANSANLAULUJA JOIDEN SANAT HÄN OLI UNOHTANUT KUN OLIN KYMMENEN VUOTTA VANHA ISÄNI ANTOI MINULLE OMAN PUUKON SE OLI PIENI JA TERÄVÄ JA SEN KAHVA OLI TEHTY VISAKOIVUSTA HÄN NÄYTTI MINULLE KUINKA PUUKKOA PIDETÄÄN KUINKA SILLÄ VUOLLAAN JA KUINKA SE TEROITETAAN ENSIMMÄINEN ASIA JONKA TEIN OLI PIENI LINTU JOKA NÄYTTI ENEMMÄN PERUNALTA KUIN LINNULTA ISÄNI PITI SITÄ SILTI IKKUNALAUDALLA MONTA VUOTTA JA KUN KYSYIN MIKSI HÄN SANOI ETTÄ JOKAINEN MESTARI ON JOSKUS TEHNYT ENSIMMÄISEN PERUNANSA KAUPPIAS SAAPUI KYLÄÄN JOKA KUUKAUDEN ENSIMMÄISENÄ MAANANTAINA HÄNELLÄ OLI KAKSI HEVOSTA JA SUURI KATETTU KÄRRY JOKA OLI TÄYNNÄ TAVARAA SUOLAA SOKERIA KAHVIA TUPAKKAA KANGASTA NEULOJA LANKAA NAULOJA LAMPPUÖLJYÄ JA KIRJOJA KYLÄLÄISET KOKOONTUIVAT HÄNEN YMPÄRILLEEN KUIN KÄRPÄSET HUNAJAN YMPÄRILLE JA KAUPANKÄYNTI KESTI KOKO PÄIVÄN KAUPPIAS TIESI MYÖS KAIKKI UUTISET JA HÄN KERTOI NIITÄ MIELELLÄÄN JOS OSTOKSIA OLI TEHTY TARPEEKSI SINÄ VUONNA KAUPPIAS TOI MUKANAAN JOTAIN UUTTA KIRJAN JOKA OLI TÄYNNÄ OUTOJA MERKKEJÄ HÄN SANOI OSTANEENSA SEN ETELÄN SUURESTA KAUPUNGISTA MIEHELTÄ JOKA VÄITTI SEN OLEVAN MUINAISEN KANSAN ARVOITUS KUKAAN KYLÄSSÄ EI HALUNNUT OSTAA SITÄ KOSKA SE OLI KALLIS EIKÄ KUKAAN OSANNUT LUKEA SITÄ LOPULTA OPETTAJA OSTI SEN KOSKA HÄN SANOI ETTÄ ARVOITUKSET OVAT PARASTA RAVINTOA MIELELLE HÄN NÄYTTI KIRJAA OPPILAILLEEN JA PIAN KOKO KOULU YRITTI RATKAISTA SEN MERKKEJÄ LAPSET KEKSIVÄT KAIKENLAISIA TEORIOITA YKSI SANOI ETTÄ MERKIT OLIVAT NUMEROITA TOINEN ETTÄ NE OLIVAT KIRJAIMIA KOLMAS ETTÄ NE OLIVAT NUOTTEJA JOKU HUOMASI ETTÄ SAMAT MERKIT TOISTUIVAT TIETYIN VÄLEIN JA JOKU TOINEN LASKI KUINKA MONTA ERILAISTA MERKKIÄ KIRJASSA OLI OPETTAJA KIRJOITTI KAIKKI TEORIAT TAULULLE JA JOKA PÄIVÄ NIITÄ TULI LISÄÄ ARVOITUS EI RATKENNUT MUTTA LAPSET OPPIVAT SINÄ VUONNA ENEMMÄN MATEMATIIKKAA KUIN KOSKAAN ENNEN MONTA VUOTTA MYÖHEMMIN YKSI NOISTA LAPSISTA JOKA OLI KASVANUT AIKUISEKSI JA RYHTYNYT TUTKIJAKSI PALASI KYLÄÄN HÄN MENI VANHALLE KOULULLE JOKA OLI NYT MUSEO JA PYYSI NÄHDÄ KIRJAN HÄN ISTUI SEN ÄÄRESSÄ KOKO PÄIVÄN JA KIRJOITTI MUISTIINPANOJA ILLALLA HÄN SULKI KIRJAN KIITTI MUSEON HOITAJAA JA LÄHTI POIS KUKAAN EI TIEDÄ MITÄ HÄN LÖYSI MUTTA HÄNEN SANOTAAN HYMYILLEEN KOKO MATKAN ASEMALLE JOS HALUAT OPPIA JOTAIN SINUN TÄYTYY ENSIN MYÖNTÄÄ ETTET TIEDÄ SITÄ TÄMÄ KUULOSTAA HELPOLTA MUTTA SE ON YKSI VAIKEIMMISTA ASIOISTA JOITA IHMINEN VOI TEHDÄ ME KAIKKI HALUAMME OLLA OIKEASSA JA ME KAIKKI PELKÄÄMME NÄYTTÄÄ TYHMILTÄ MUTTA JOKAINEN KYSYMYS JONKA USKALLAMME KYSYÄ AVAA OVEN JA JOKAINEN VIRHE JONKA MYÖNNÄMME OPETTAA MEILLE JOTAIN UUTTA VIISAUS EI OLE SITÄ ETTÄ TIETÄÄ KAIKEN VAAN SITÄ ETTÄ TIETÄÄ MITÄ EI TIEDÄ NUMERO YKSI ON ALOITUS JA KAKSI ON JATKO KOLME ON TÄYDELLISYYS NELJÄ ON VAKAUS JA VIISI ON MUUTOS KUUSI ON TASAPAINO SEITSEMÄN ON SALAISUUS KAHDEKSAN ON ÄÄRETÖN JA YHDEKSÄN ON LOPPU NOLLA ON TYHJYYS JOSTA KAIKKI ALKAA JA JOHON KAIKKI PALAA VANHAT MESTARIT USKOIVAT ETTÄ NUMEROISSA OLI KOKO MAAILMAN RAKENNE JA ETTÄ JOKA YMMÄRSI NUMEROT YMMÄRSI MYÖS JUMALTEN AJATUKSET"""
# -------------------------------------------------------------------------------------------------


class Pool:
    def __init__(self): self.n = 0
    def new(self, k=1):
        r = list(range(self.n + 1, self.n + 1 + k)); self.n += k; return r


def gen_key(rnd, N, A, K):
    """Distinct read positions K (letters 0..A-1 -> k[a]); class map; class shuffles with no doubles."""
    k = rnd.sample(range(N), A); Kset = set(k)
    cls = [rnd.randrange(K) for _ in range(A)]
    for c in range(K): cls[c] = c                      # every class non-empty
    outside = [p for p in range(N) if p not in Kset]
    sig = []
    for c in range(K):
        inv = [None] * N                               # inv[q] = s_c^-1(q)
        mine = [k[a] for a in range(A) if cls[a] == c]
        img = rnd.sample(outside, len(mine))
        for q, v in zip(mine, img): inv[q] = v
        rest_q = [q for q in range(N) if inv[q] is None]
        rest_v = [v for v in range(N) if v not in set(img)]
        rnd.shuffle(rest_v)
        for q, v in zip(rest_q, rest_v): inv[q] = v
        s = [None] * N
        for q, v in enumerate(inv): s[v] = q
        sig.append(s)
    return k, cls, sig


def encrypt(key, pt, N, D0=None):
    k, cls, sig = key
    D = list(range(N)) if D0 is None else list(D0)
    out = []
    for a in pt:
        out.append(D[k[a]])
        s = sig[cls[a]]
        D = [D[s[p]] for p in range(N)]
    return out


def make_texts(rnd, lang, A, lens):
    """Plaintexts as letter indices 0..A-1: corpus excerpts, characters folded onto A letters by frequency rank."""
    if lang == 'fi':
        c = CORPUS_FI
    else:
        c = open(os.path.join(HERE, 'corpus_%s.txt' % lang), encoding='utf-8').read()
    from collections import Counter
    rank = {ch: i for i, (ch, _) in enumerate(Counter(c).most_common())}
    texts = []
    for L in lens:
        s = rnd.randrange(len(c) - L)
        texts.append([rank[ch] % A for ch in c[s:s + L]])
    return texts


def encode(cts, pts, cls, N, A, K, Dmax, anchor=True, solver='cadical153', prefix=None, symbreak=False, longeq=False, onehot=False,
           anchor_all=False, old_anchor=False):
    """cts/pts: per-message ciphertext symbols and plaintext letter indices (0..A-1, equal index = same letter).
    cls: class of each letter, or None to let the solver choose (K must be 2).  A crib may cover a different
    prefix of each message (ciphertext is cut to the plaintext length); empty messages are skipped."""
    if prefix:   # crib attack: only the first `prefix` letters of every message are known
        cts = [ct[:prefix] for ct in cts]; pts = [pt[:prefix] for pt in pts]
    keep = [i for i, pt in enumerate(pts) if len(pt) > 0]
    cts = [cts[i][:len(pts[i])] for i in keep]; pts = [pts[i] for i in keep]
    unknown = cls is None
    if unknown and K != 2: raise ValueError('unknown classes are supported for K=2 only')
    if unknown and onehot: raise ValueError('onehot encoding needs known classes')
    B = max(1, (N - 1).bit_length())
    vp = Pool()
    S = Solver(name=solver)
    ncl = [0]
    def add(cl): S.add_clause(cl); ncl[0] += 1
    # class shuffles: binary bits + one-hot channel
    sb = [[vp.new(B) for p in range(N)] for c in range(K)]
    sx = [[vp.new(N) for p in range(N)] for c in range(K)]
    for c in range(K):
        for p in range(N):
            add(sx[c][p])                                     # at least one value
            for q in range(N):
                x = sx[c][p][q]
                for j in range(B):
                    add([-x, sb[c][p][j] if (q >> j) & 1 else -sb[c][p][j]])
        for q in range(N):                                    # each value used at most once (column AMO)
            enc = CardEnc.atmost([sx[c][p][q] for p in range(N)], 1, top_id=vp.n, encoding=EncType.seqcounter)
            for cl in enc.clauses: add(cl)
            vp.n = max(vp.n, enc.nv)
    if symbreak:
        # Non-read positions (>= A) can be relabelled freely.  Canonical labelling (fresh labels handed
        # out in order while scanning s_0(0), s_0(1), ...) implies s_0(i) <= A + i.
        for i in range(N):
            for q in range(A + i + 1, N):
                add([-sx[0][i][q]])
    cb = None
    if unknown:
        cb = vp.new(A); add([-cb[0]])                      # class bit per letter; class symmetry: letter 0 in class 0
    def classes_of(a):
        """[(class, selector)]: the selector literals are false exactly when letter a has that class"""
        if not unknown: return [(cls[a], [])]
        return [(0, [cb[a]]), (1, [-cb[a]])]
    def mux(prev, a, z):
        for c, sel in classes_of(a):
            for p in range(N):
                cond = [prev[j] if not (p >> j) & 1 else -prev[j] for j in range(B)]   # false exactly when prev == p
                for j in range(B):
                    add(sel + cond + [-z[j], sb[c][p][j]]); add(sel + cond + [z[j], -sb[c][p][j]])
    def eq_const(bits, v):  # bits == v (unit clauses)
        for j in range(B):
            add([bits[j] if (v >> j) & 1 else -bits[j]])
    def neq_const(bits, v):
        add([-bits[j] if (v >> j) & 1 else bits[j] for j in range(B)])
    Pv = []          # per message: dict (t,d) -> bit vars (t 0-based)
    for m, (ct, pt) in enumerate(zip(cts, pts)):
        L = len(ct); P = {}; Y = {}
        for d in range(1, Dmax + 1):
            for t in range(L - d):
                c = None if unknown else cls[pt[t]]
                if d == 1 and not unknown:
                    P[(t, 1)] = sb[c][pt[t + 1]]              # alias: s_c[k_{a_{t+1}}]
                    if onehot: Y[(t, 1)] = sx[c][pt[t + 1]]
                elif d == 1:
                    z = vp.new(B)
                    for c2, sel in classes_of(pt[t]):
                        for j in range(B):
                            add(sel + [-z[j], sb[c2][pt[t + 1]][j]]); add(sel + [z[j], -sb[c2][pt[t + 1]][j]])
                    P[(t, 1)] = z
                elif onehot:
                    z = vp.new(B); y = vp.new(N); yp = Y[(t + 1, d - 1)]
                    for p in range(N):
                        for j in range(B):
                            add([-yp[p], -z[j], sb[c][p][j]]); add([-yp[p], z[j], -sb[c][p][j]])
                    for q in range(N):                        # channel y <-> z
                        for j in range(B): add([-y[q], z[j] if (q >> j) & 1 else -z[j]])
                        add([y[q]] + [-z[j] if (q >> j) & 1 else z[j] for j in range(B)])
                    P[(t, d)] = z; Y[(t, d)] = y
                else:
                    z = vp.new(B); mux(P[(t + 1, d - 1)], pt[t], z)
                    P[(t, d)] = z
                if ct[t] == ct[t + d]: eq_const(P[(t, d)], pt[t])
                else: neq_const(P[(t, d)], pt[t])
        if longeq:   # long-range repeats (d > Dmax): build only the diagonal chains they need
            def getP(t, d):
                if (t, d) in P: return P[(t, d)]
                prev = getP(t + 1, d - 1); z = vp.new(B)
                mux(prev, pt[t], z)
                P[(t, d)] = z
                if ct[t] == ct[t + d]: eq_const(z, pt[t])
                else: neq_const(z, pt[t])
                return z
            for d in range(Dmax + 1, L):
                for t in range(L - d):
                    if ct[t] == ct[t + d]:
                        getP(t, d)
        Pv.append(P)
    def chain(m, t, d):
        """P(t,d) of message m, building the diagonal chain down to the window if needed."""
        P = Pv[m]
        if (t, d) in P: return P[(t, d)]
        ct, pt = cts[m], pts[m]
        z = vp.new(B); mux(chain(m, t + 1, d - 1), pt[t], z)
        P[(t, d)] = z
        if ct[t] == ct[t + d]: eq_const(z, pt[t])
        else: neq_const(z, pt[t])
        return z
    if anchor and old_anchor:   # (old) pairwise equal/different constraints between anchored values
        vals = []
        for m, (ct, pt) in enumerate(zip(cts, pts)):
            vals.append((ct[0], ('c', pt[0])))
            for d in range(1, min(Dmax, len(ct) - 1) + 1):
                vals.append((ct[d], ('v', Pv[m][(0, d)])))
        for (x1, v1), (x2, v2) in itertools.combinations(vals, 2):
            if v1[0] == 'c' and v2[0] == 'c':
                continue
            if v1[0] == 'c': v1, v2 = v2, v1
            b1 = v1[1]
            if v2[0] == 'c':
                if x1 == x2: eq_const(b1, v2[1])
                else: neq_const(b1, v2[1])
            else:
                b2 = v2[1]
                if x1 == x2:
                    for j in range(B):
                        add([-b1[j], b2[j]]); add([b1[j], -b2[j]])
                else:
                    u = vp.new(B)
                    for j in range(B):   # u_j -> b1_j xor b2_j
                        add([-u[j], b1[j], b2[j]]); add([-u[j], -b1[j], -b2[j]])
                    add(u)
    elif anchor:
        # All messages start from the same deck D0, so every card x has ONE starting position pos(x), and
        # different cards have different starting positions (all-different via one-hot + at-most-one per slot).
        # P(0,d) of each message = pos(card read at step d).
        vals = []
        for m, (ct, pt) in enumerate(zip(cts, pts)):
            vals.append((ct[0], ('c', pt[0])))
            dm = len(ct) - 1 if anchor_all else min(Dmax, len(ct) - 1)
            for d in range(1, dm + 1):
                vals.append((ct[d], ('v', chain(m, 0, d))))
        cards = sorted(set(x for x, _ in vals))
        ph, pb = {}, {}
        for x in cards:
            ph[x] = vp.new(N); pb[x] = vp.new(B)
            add(ph[x])
            for q in range(N):
                for j in range(B): add([-ph[x][q], pb[x][j] if (q >> j) & 1 else -pb[x][j]])
                add([ph[x][q]] + [-pb[x][j] if (q >> j) & 1 else pb[x][j] for j in range(B)])
        for q in range(N):
            if len(cards) > 1:
                enc = CardEnc.atmost([ph[x][q] for x in cards], 1, top_id=vp.n, encoding=EncType.seqcounter)
                for cl in enc.clauses: add(cl)
                vp.n = max(vp.n, enc.nv)
        for x, v in vals:
            if v[0] == 'c':
                add([ph[x][v[1]]])
            else:
                for j in range(B):
                    add([-v[1][j], pb[x][j]]); add([v[1][j], -pb[x][j]])
    encode.class_vars = cb
    return S, sb, ncl[0], vp.n, B


def decode_sigma(model, sb, N, K, B):
    ms = set(l for l in model if l > 0)
    return [[sum(1 << j for j in range(B) if sb[c][p][j] in ms) for p in range(N)] for c in range(K)]


def check_full(sig, cts, pts, cls, N):
    """Using recovered shuffles (with k_a = a), count CT-equality mismatches at ALL distances within messages."""
    bad = tot = 0
    for ct, pt in zip(cts, pts):
        L = len(ct)
        D = list(range(N)); orig = []          # deck labelled by original (D0) position
        for a in pt:
            orig.append(D[a])
            s = sig[cls[a]]
            D = [D[s[p]] for p in range(N)]
        for i in range(L):
            for j in range(i + 1, L):
                tot += 1
                bad += (orig[i] == orig[j]) != (ct[i] == ct[j])
    return bad, tot


def solve(S, timeout=None):
    """Run the solver; True / False.  pysat's CaDiCaL ignores interrupts and keeps Python's interpreter lock while it
    runs, so a timer thread never gets to act.  A timeout is therefore a separate watchdog process that prints
    TIMEOUT and ends this one (exit code 3 on Windows, killed by SIGKILL elsewhere)."""
    import subprocess
    dog = None
    if timeout:
        sig = 3 if os.name == 'nt' else 9
        code = (f'import os, time; time.sleep({float(timeout)!r}); '
                f'print("TIMEOUT after {timeout:.0f}s (no answer)", flush=True); os.kill({os.getpid()}, {sig})')
        dog = subprocess.Popen([sys.executable, '-c', code])
    try:
        res = S.solve()
    finally:
        if dog is not None and dog.poll() is None: dog.kill()
    return res


def run_synth(a):
    lens = [len(m) for m in MSGS]
    rnd = random.Random(a.seed)
    key = gen_key(rnd, a.N, a.A, a.K)
    pts = make_texts(rnd, a.lang, a.A, lens)
    D0 = list(range(a.N)); rnd.shuffle(D0)
    cts = [encrypt(key, pt, a.N, D0) for pt in pts]
    dbl = sum(1 for ct in cts for i in range(len(ct) - 1) if ct[i] == ct[i + 1])
    if a.mode == 'wrong':          # wrong plaintext guess: fresh excerpts, same lengths -> expect UNSAT
        pts = make_texts(random.Random(a.seed + 1000), a.lang, a.A, lens)
    elif a.mode.startswith('mut'):  # change a fraction of letters, e.g. mut0.05
        f = float(a.mode[3:]); r2 = random.Random(a.seed + 2000)
        pts = [[(x if r2.random() > f else r2.randrange(a.A)) for x in pt] for pt in pts]
    t0 = time.time()
    S, sb, ncl, nv, B = encode(cts, pts, None if a.unknown_classes else key[1], a.N, a.A, a.K, a.dmax,
                               prefix=a.prefix, symbreak=not a.no_symbreak, longeq=a.long, onehot=a.onehot, solver=a.solver,
                               anchor_all=a.anchor_all, old_anchor=a.old_anchor)
    t1 = time.time()
    res = solve(S, a.timeout); t2 = time.time()
    msg = (f'synth N={a.N} A={a.A} K={a.K} dmax={a.dmax} seed={a.seed} lang={a.lang} mode={a.mode} prefix={a.prefix} '
           f'unknown_classes={a.unknown_classes} long={a.long} doubles={dbl} vars={nv} clauses={ncl} '
           f'encode={t1-t0:.1f}s solve={t2-t1:.1f}s result={"SAT" if res else "UNSAT"}')
    if res:
        model = S.get_model()
        sig = decode_sigma(model, sb, a.N, a.K, B)
        cls = key[1]
        if a.unknown_classes:
            ms = set(l for l in model if l > 0)
            cls = [1 if v in ms else 0 for v in encode.class_vars]
        bad, tot = check_full(sig, cts, pts, cls, a.N)
        msg += f' full-message check: {bad} wrong of {tot} symbol pairs'
    print(msg, flush=True)


def read_crib(path, names):
    crib = {}
    for ln in open(path, encoding='utf-8').read().split('\n'):
        ln = ln.rstrip('\r')
        if not ln.strip() or ln.lstrip().startswith('#'): continue
        name, sep, text = ln.partition(':')
        name = name.strip().upper()
        if not sep or name not in names:
            raise SystemExit(f'bad crib line {ln!r}: expected "NAME: text" with NAME one of {names}')
        if text.startswith(' '): text = text[1:]          # "E1: TEXT" -> "TEXT" (other spaces are letters)
        crib[name] = text
    return crib


def run_eyes(a):
    """Test a crib (plaintext guess) against the real eye messages under class-XGAK."""
    msgs = MSGS
    if a.ct:   # alternative ciphertext (same format as data/eyes_ascii32.txt: 9 lines, value = ord(c) - 32)
        msgs = [[ord(ch) - 32 for ch in l.rstrip('\r\n')] for l in open(a.ct, encoding='utf-8') if l.strip('\r\n')]
        assert len(msgs) == 9, 'ciphertext file must have 9 lines'
    crib = read_crib(a.crib, NAMES)
    off = 1 if a.skip_label else 0
    alphabet = sorted(set(''.join(crib.values())))
    idx = {ch: i for i, ch in enumerate(alphabet)}
    A = len(alphabet)
    if A > 83: raise SystemExit('more than 83 distinct letters')
    cts, pts = [], []
    for name, m in zip(NAMES, msgs):
        ct = m[off:]; text = crib.get(name, '')
        if len(text) > len(ct): raise SystemExit(f'crib for {name} is longer than the message ({len(ct)} symbols)')
        cts.append(ct[:len(text)]); pts.append([idx[ch] for ch in text])
    cls = None
    if a.classes:
        groups = a.classes.split('|')
        if len(groups) != a.K: raise SystemExit('--classes needs exactly K groups separated by |')
        cls = []
        for ch in alphabet:
            g = [i for i, grp in enumerate(groups) if ch in grp]
            cls.append(g[0] if g else len(groups) - 1)       # letters not listed go to the last group
    elif a.K != 2:
        raise SystemExit('without --classes the solver chooses the groups, which needs K=2')
    used = sum(len(p) for p in pts)
    print(f'crib covers {used} symbols in {sum(1 for p in pts if p)} messages; {A} distinct letters; '
          f'groups {"given" if cls else "chosen by the solver"}; K={a.K}; deck of {a.N} cards', flush=True)
    t0 = time.time()
    S, sb, ncl, nv, B = encode(cts, pts, cls, a.N, A, a.K, a.dmax, symbreak=not a.no_symbreak, longeq=a.long, solver=a.solver,
                               anchor_all=a.anchor_all, old_anchor=a.old_anchor)
    t1 = time.time()
    res = solve(S, a.timeout); t2 = time.time()
    print(f'encode {t1-t0:.1f}s, solve {t2-t1:.1f}s, {nv} variables, {ncl} clauses', flush=True)
    if res:
        print('CONSISTENT: some class-XGAK key produces exactly these eye symbols from this crib.')
        if cls is None:
            ms = set(l for l in S.get_model() if l > 0)
            g = [''.join(ch for ch, v in zip(alphabet, encode.class_vars) if (v in ms) == bool(k)) for k in (0, 1)]
            print(f'  one grouping that works: {g[0]!r} | {g[1]!r}')
        print('  Note: short cribs are easy to satisfy. A result only means something once random guesses of the'
              ' same shape fail; run a control (e.g. the same crib with its letters shuffled).')
    else:
        print('IMPOSSIBLE: no class-XGAK key fits this crib (assuming all messages start from the same deck'
              + (' and all first letters share a group' if a.skip_label else '') + ').')


if __name__ == '__main__':
    import argparse
    ap = argparse.ArgumentParser(description=__doc__, formatter_class=argparse.RawDescriptionHelpFormatter)
    sub = ap.add_subparsers(dest='cmd', required=True)
    common = argparse.ArgumentParser(add_help=False)
    common.add_argument('--dmax', type=int, default=16, help='encode all repeats up to this distance (default 16)')
    common.add_argument('--long', action='store_true', help='also encode every longer-distance repeat (faster on big decks)')
    common.add_argument('--no-symbreak', action='store_true', help='disable symmetry breaking')
    common.add_argument('--timeout', type=float, default=None, help='give up after this many seconds')
    common.add_argument('--anchor-all', action='store_true', help='tie every crib position to the shared starting deck (stronger, bigger)')
    common.add_argument('--old-anchor', action='store_true', help='previous pairwise anchoring encoding (for comparison)')
    common.add_argument('--solver', default='cadical153', help='pysat solver name (cadical153, cadical195, glucose4, maplechrono, lingeling, minisat22)')
    sy = sub.add_parser('synth', parents=[common], help='known-plaintext recovery on fake messages (eye lengths)')
    sy.add_argument('N', type=int, help='deck size (83 for the eyes)')
    sy.add_argument('A', type=int, help='number of plaintext letters')
    sy.add_argument('--K', type=int, default=2, help='number of letter groups (default 2)')
    sy.add_argument('--seed', type=int, default=1)
    sy.add_argument('--lang', default='fi', help='corpus for the fake text: fi (built in) or X for a file corpus_X.txt next to this script')
    sy.add_argument('--mode', default='true', help='true | wrong (wrong plaintext: expect UNSAT) | mutF (change fraction F of letters)')
    sy.add_argument('--prefix', type=int, default=None, help='only the first PREFIX letters of each message are known (crib)')
    sy.add_argument('--unknown-classes', action='store_true', help="don't tell the solver which letters share a shuffle (K=2)")
    sy.add_argument('--onehot', action='store_true', help='alternative encoding (needs known classes)')
    ey = sub.add_parser('eyes', parents=[common], help='test a plaintext guess (crib) against the real eye messages')
    ey.add_argument('crib', help='text file with lines "E1: SOMETEXT" (names E1 W1 E2 W2 E3 W3 E4 W4 E5); same character = same letter')
    ey.add_argument('--K', type=int, default=2)
    ey.add_argument('--N', type=int, default=83, help='deck size (83 for the eyes; smaller only for --ct experiments)')
    ey.add_argument('--classes', default=None, help='letter groups, e.g. "0123456789|ABCDEFG..." (default: solver chooses, K=2)')
    ey.add_argument('--skip-label', action='store_true', help='crib starts at the 2nd symbol (assumes all first letters share a group)')
    ey.add_argument('--ct', default=None, help='use this ciphertext file (eyes_ascii32 format) instead of the real eyes, e.g. for controls')
    a = ap.parse_args()
    a.onehot = getattr(a, 'onehot', False)
    if a.cmd == 'synth': run_synth(a)
    else: run_eyes(a)
