রেল ফেন্স সাইফার

নির্দেশনা

রেল ফেন্স সাইফারের জন্য এনকোডিং ও ডিকোডিং বাস্তবায়ন করুন।

রেল ফেন্স সাইফার হলো এক ধরনের ট্রান্সপোজিশন সাইফার, যার নাম এসেছে এটি যেভাবে এনকোড করা হয় তা থেকেই। প্রাচীন গ্রিকরা এটি ব্যবহার করত।

রেল ফেন্স সাইফারে বার্তাটি একটি কাল্পনিক বেড়ার পরপর কয়েকটি "রেল"-এ নিচের দিকে লেখা হয়, আর নিচে পৌঁছে গেলে আবার উপরে ওঠা হয় (জিগজ্যাগের মতো)। সবশেষে বার্তাটি সারি সারি করে পড়ে নেওয়া হয়।

যেমন, তিনটি "রেল" ও "WE ARE DISCOVERED FLEE AT ONCE" বার্তা ব্যবহার করলে সাইফারটি এভাবে লেখা হয়:

W . . . E . . . C . . . R . . . L . . . T . . . E
. E . R . D . S . O . E . E . F . E . A . O . C .
. . A . . . I . . . V . . . D . . . E . . . N . .

এরপর তা এভাবে পড়ে নেওয়া হয়:

WECRLTEERDSOEEFEAOCAIVDEN

একটি বার্তা ডিক্রিপ্ট করতে আপনি জিগজ্যাগ আকৃতিটি নেন এবং সারিগুলো বরাবর সাইফারটেক্সট বসিয়ে দেন।

? . . . ? . . . ? . . . ? . . . ? . . . ? . . . ?
. ? . ? . ? . ? . ? . ? . ? . ? . ? . ? . ? . ? .
. . ? . . . ? . . . ? . . . ? . . . ? . . . ? . .

প্রথম সারিতে সাতটি জায়গা আছে, যেগুলো "WECRLTE" দিয়ে ভরা যায়।

W . . . E . . . C . . . R . . . L . . . T . . . E
. ? . ? . ? . ? . ? . ? . ? . ? . ? . ? . ? . ? .
. . ? . . . ? . . . ? . . . ? . . . ? . . . ? . .

এখন দ্বিতীয় সারিতে বসে "ERDSOEEFEAOC"।

W . . . E . . . C . . . R . . . L . . . T . . . E
. E . R . D . S . O . E . E . F . E . A . O . C .
. . ? . . . ? . . . ? . . . ? . . . ? . . . ? . .

শেষ সারির জন্য বাকি থাকে "AIVDEN"।

W . . . E . . . C . . . R . . . L . . . T . . . E
. E . R . D . S . O . E . E . F . E . A . O . C .
. . A . . . I . . . V . . . D . . . E . . . N . .

এখন আপনি যদি জিগজ্যাগ আকৃতি ধরে পড়েন, তবে মূল বার্তাটি পড়তে পারবেন।

সাবটাইপ

এই অনুশীলনীতে ০-এর চেয়ে বড় সমস্ত স্বাভাবিক সংখ্যার জন্য Positive নামের একটি সাবটাইপ ডিফাইন করা হয়েছে। একটি সাবটাইপকে একটি জোড়া ⟨x, h⟩ হিসেবে ভাবা যায়, যেখানে x হলো মান আর h হলো তার বৈধতার প্রমাণ।

সাবটাইপের ভেতরের মানটি (এক্ষেত্রে x) .val দিয়ে বের করা যায়, যেমন x.val। আর তার প্রমাণ বের করা যায় .property দিয়ে, যেমন x.property। চিরাচরিত নিয়মেই প্যাটার্ন ম্যাচিং দিয়েও দুটোই বের করা যায়।

একটি সাবটাইপের জন্য মান তৈরি করতে হলে তার বৈধতা প্রমাণ করা জরুরি, এক্ষেত্রে সংখ্যাটি যে ০-এর চেয়ে বড়, তা প্রমাণ করা।

Lean-এ এমন অনেক লেমা ও থিওরেম আছে, যেগুলো এই প্রমাণের সূচনা বিন্দু হিসেবে কাজ করতে পারে। যেমন, Nat.zero_lt_succ হলো এমন একটি লেমা, যা বলে যে যেকোনো স্বাভাবিক সংখ্যা n-এর জন্য 0 < n + 1।

---

সূত্র

Wikipedia